English
Composition of three pseudoequivalences is associative: (f trans g) trans h = f trans (g trans h).
Русский
Объединение трёх псевдоэквивалентностей ассоциативно: (f.trans g).trans h = f.trans (g.trans h).
LaTeX
$$$$ (f\\,\\trans\\, g)\\,\\trans\\, h = f\\,\\trans\\, (g\\,\\trans\\, h). $$$$
Lean4
theorem trans_assoc (f : α ≃. β) (g : β ≃. γ) (h : γ ≃. δ) : (f.trans g).trans h = f.trans (g.trans h) :=
ext fun _ => Option.bind_assoc _ _ _