English
Transporting a family of predicates along an equivalence commutes with updating at a point: e.piCongrLeft' P (update f (e^{-1} b) x) = update (e.piCongrLeft' P f) b x.
Русский
Перенос семейства предикатов вдоль эквививалентности commuting с обновлением в точке: e.piCongrLeft' P (update f (e^{-1} b) x) = update (e.piCongrLeft' P f) b x.
LaTeX
$$$e\\piCongrLeft' P\\big(\\text{update } f (e^{-1} b) x\\big) = \\text{update }\\big(e\\piCongrLeft' P f\\big)\\; b\\; x.$$$
Lean4
theorem piCongrLeft'_update [DecidableEq α] [DecidableEq β] (P : α → Sort*) (e : α ≃ β) (f : ∀ a, P a) (b : β)
(x : P (e.symm b)) : e.piCongrLeft' P (update f (e.symm b) x) = update (e.piCongrLeft' P f) b x :=
by
ext b'
rcases eq_or_ne b' b with (rfl | h) <;> simp_all
