English
The composition of arrowCongrLeft for e1 and e2 equals the arrowCongrLeft of the composition: e1.arrowCongrLeft.trans e2.arrowCongrLeft = (e1.trans e2).arrowCongrLeft.
Русский
Композиция arrowCongrLeft двух вложений равна вложению от композиции: e1.arrowCongrLeft.trans e2.arrowCongrLeft = (e1.trans e2).arrowCongrLeft.
LaTeX
$$$ e_{12}.\\mathrm{arrowCongrLeft} \\;\\text{trans } e_{23}.\\mathrm{arrowCongrLeft} = (e_{12} \\text{ trans } e_{23}).\\mathrm{arrowCongrLeft}$$$
Lean4
@[simp]
theorem trans_arrowCongrLeft {α₁ : Sort u} {α₂ : Sort v} {α₃ : Sort x} {γ : Sort w} [Inhabited γ] (e₁₂ : α₁ ↪ α₂)
(e₂₃ : α₂ ↪ α₃) : e₁₂.arrowCongrLeft.trans e₂₃.arrowCongrLeft = (e₁₂.trans e₂₃).arrowCongrLeft (γ := γ) :=
by
ext f a
simp only [trans_apply, arrowCongrLeft_apply, Pi.default_def, coe_trans]
rw [e₁₂.injective.extend_comp e₂₃.injective, Function.comp_def]
