English
The symmetric of piCongrLeft acts by sending g to the value g at the image under e, i.e., (piCongrLeft P e).symm g a = g (e a).
Русский
Обратное к piCongrLeft действует так: (piCongrLeft P e).symm g a = g (e a).
LaTeX
$$$(\\mathrm{piCongrLeft} \\ P\\ e).\\mathrm{symm}\\ g\\ a = g (e a).$$$
Lean4
/-- Note: the "obvious" statement `(piCongrLeft P e) f b = f (e.symm b)` doesn't typecheck: the
LHS would have type `P b` while the RHS would have type `P (e (e.symm b))`. This lemma is a way
around it in the case where `b` is of the form `e a`, so we can use `f a` instead of
`f (e.symm (e a))`. -/
@[simp]
theorem piCongrLeft_apply_apply (f : ∀ a, P (e a)) (a : α) : (piCongrLeft P e) f (e a) = f a :=
piCongrLeft'_symm_apply_apply P e.symm f a
