English
Composition of subtypeEquiv along two equivalences gives the subtypeEquiv of the composed equivalence with a combined predicate relation.
Русский
Сложение subtypeEquiv вдоль двух эквивалентностей даёт subtypeEquiv от составной эквивалентности с объединённым отношением предикатов.
LaTeX
$$$$ (e.subtypeEquiv h).trans (f.subtypeEquiv h') = (e.trans f).subtypeEquiv (\\text{by auxiliary lemma}). $$$$
Lean4
@[simp]
theorem subtypeEquiv_trans {p : α → Prop} {q : β → Prop} {r : γ → Prop} (e : α ≃ β) (f : β ≃ γ)
(h : ∀ a : α, p a ↔ q (e a)) (h' : ∀ b : β, q b ↔ r (f b)) :
(e.subtypeEquiv h).trans (f.subtypeEquiv h') =
(e.trans f).subtypeEquiv (by as_aux_lemma => exact fun a => (h a).trans (h' <| e a)) :=
rfl
