English
Given a family of types indexed by a sum ι ⊕ ι' and an equivalence e: ι ⊕ ι' ≃ ι'', transporting a pair (f,g) along the equivalence and evaluating on e(inl i) yields f i. In other words, the left branch is preserved under the transported function.
Русский
Пусть дано эйлевентность e: ι ⊕ ι' ≃ ι'' и функции f,g по соответствующим индексам. Применение транспарентной функции к синтетической записи и вычисление в виде e(inl i) даёт f i.
LaTeX
$$$\\forall i:\\iota,\\quad \\pi_{\\text{CongrLeft}}\\,\\pi\\,e\\,({\\text{sumPiEquivProdPi}(f,g)})\\big(e(\\mathrm{inl}\\ i)\\big)=f\\ i.$$$
Lean4
theorem piCongrLeft_sumInl {ι ι' ι''} (π : ι'' → Type*) (e : ι ⊕ ι' ≃ ι'') (f : ∀ i, π (e (inl i)))
(g : ∀ i, π (e (inr i))) (i : ι) :
piCongrLeft π e (sumPiEquivProdPi (fun x => π (e x)) |>.symm (f, g)) (e (inl i)) = f i := by
simp_rw [piCongrLeft_apply_eq_cast, sumPiEquivProdPi_symm_apply, sum_rec_congr _ _ _ (e.symm_apply_apply (inl i)),
cast_cast, cast_eq]
