English
If you cast two consecutive paths γ from a2 to b2 and γ′ from b2 to c2, their concatenation cast back equals the cast of their concatenation: (γ.cast ha hb).trans (γ'.cast hb hc) = (γ.trans γ').cast ha hc.
Русский
Если привести две последовательные части пути, то их конкатенация после приведения равна привведённой конкатенации: (γ.cast ha hb).trans (γ'.cast hb hc) = (γ.trans γ').cast ha hc.
LaTeX
$$$(\gamma.cast ha hb).trans (\gamma'.cast hb hc) = (\gamma.trans \gamma').cast ha hc$$$
Lean4
@[simp]
theorem trans_cast {a₁ a₂ b₁ b₂ c₁ c₂ : X} (γ : Path a₂ b₂) (γ' : Path b₂ c₂) (ha : a₁ = a₂) (hb : b₁ = b₂)
(hc : c₁ = c₂) : (γ.cast ha hb).trans (γ'.cast hb hc) = (γ.trans γ').cast ha hc :=
rfl
