English
For P, e, g, and b, we have (piCongrLeft' P e).symm g (e^{-1}(b)) = g(b).
Русский
Для P, e и g и b выполняется (piCongrLeft' P e).symm g (e^{-1}(b)) = g(b).
LaTeX
$$$(\piCongrLeft' P e)^{\!-1} g (e^{-1}(b)) = g(b).$$$
Lean4
/-- Note: the "obvious" statement `(piCongrLeft' P e).symm g a = g (e a)` doesn't typecheck: the
LHS would have type `P a` while the RHS would have type `P (e.symm (e a))`. This lemma is a way
around it in the case where `a` is of the form `e.symm b`, so we can use `g b` instead of
`g (e (e.symm b))`. -/
@[simp]
theorem piCongrLeft'_symm_apply_apply (P : α → Sort*) (e : α ≃ β) (g : ∀ b, P (e.symm b)) (b : β) :
(piCongrLeft' P e).symm g (e.symm b) = g b :=
by
rw [piCongrLeft'_symm_apply, ← heq_iff_eq, eqRec_heq_iff_heq]
exact congr_arg_heq _ (e.apply_symm_apply _)
