English
The symmetric version of piCongrLeft' respects updates: (e.piCongrLeft' P).symm (update f b x) = update ((e.piCongrLeft' P).symm f) (e^{-1} b) x.
Русский
Симметричная версия piCongrLeft' сохраняет обновления: (e.piCongrLeft' P).symm (update f b x) = update ((e.piCongrLeft' P).symm f) (e^{-1} b) x.
LaTeX
$$$(e.piCongrLeft' P).symm (\\text{update } f b x) = \\text{update }((e.piCongrLeft' P).symm f) (e^{-1} b) x.$$$
Lean4
theorem piCongrLeft'_symm_update [DecidableEq α] [DecidableEq β] (P : α → Sort*) (e : α ≃ β) (f : ∀ b, P (e.symm b))
(b : β) (x : P (e.symm b)) :
(e.piCongrLeft' P).symm (update f b x) = update ((e.piCongrLeft' P).symm f) (e.symm b) x := by
simp [(e.piCongrLeft' P).symm_apply_eq, piCongrLeft'_update]
