English
Similarly, for the right branch, transporting the pair (f,g) and evaluating at e(inr j) yields g j.
Русский
Аналогично для правой ветви: транспонируя пару (f,g) и вычисляя в точке e(inr j), получаем g j.
LaTeX
$$$\\forall j:\\iota',\\quad \\pi_{\\text{CongrLeft}}\\,\\pi\\,e\\,({\\text{sumPiEquivProdPi}(f,g)})\\big(e(\\mathrm{inr}\\ j)\\big)=g\\ j.$$$
Lean4
theorem piCongrLeft_sumInr {ι ι' ι''} (π : ι'' → Type*) (e : ι ⊕ ι' ≃ ι'') (f : ∀ i, π (e (inl i)))
(g : ∀ i, π (e (inr i))) (j : ι') :
piCongrLeft π e (sumPiEquivProdPi (fun x => π (e x)) |>.symm (f, g)) (e (inr j)) = g j := by
simp_rw [piCongrLeft_apply_eq_cast, sumPiEquivProdPi_symm_apply, sum_rec_congr _ _ _ (e.symm_apply_apply (inr j)),
cast_cast, cast_eq]
