English
Let α, β, γ be types with relations r, s, t respectively, and let h1: α = β, h1': β = γ be two type equalities, and h2: r ≍ s, h2': s ≍ t be two relation isomorphisms. Then composing the two casts corresponds to casting by the composition of the equalities and the composition of the isomorphisms: (RelIso.cast h1 h2).trans (RelIso.cast h1' h2') = RelIso.cast (h1.trans h1') (h2.trans h2').
Русский
Пусть α, β, γ — множества, на них заданы отношения r, s, t. Пусть даны равенства h1: α = β, h1': β = γ и изоморфизмы r ≃ s, s ≃ t. Тогда композиция преобразований RelIso, получаемая как (RelIso.cast h1 h2).trans (RelIso.cast h1' h2'), равна RelIso.cast (h1.trans h1') (h2.trans h2').
LaTeX
$$$$(RelIso.cast\ h_1\ h_2)\ \mathrm{trans}\ (RelIso.cast\ h_1'\ h_2') = RelIso.cast\ (h_1\ \mathrm{trans}\ h_1')\ (h_2\ \mathrm{trans}\ h_2').$$$$
Lean4
@[simp]
protected theorem cast_trans {α β γ : Type u} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop} (h₁ : α = β)
(h₁' : β = γ) (h₂ : r ≍ s) (h₂' : s ≍ t) :
(RelIso.cast h₁ h₂).trans (RelIso.cast h₁' h₂') = RelIso.cast (h₁.trans h₁') (h₂.trans h₂') :=
ext fun x => by subst h₁; rfl
