@[simp]

theorem Equiv.symm_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α ≃ β) (g : β ≃ γ) : (f.trans g).symm = g.symm.trans f.symm