case h
a b : { x // x ∈ circle }
x✝ : ℂ
⊢ ↑(LinearIsometryEquiv.trans (↑rotation a) (↑rotation b)) x✝ = ↑(↑rotation (b * a)) x✝
a b : { x // x ∈ circle }
⊢ LinearIsometryEquiv.trans (↑rotation a) (↑rotation b) = ↑rotation (b * a)
ext1
no goals
case h
a b : { x // x ∈ circle }
x✝ : ℂ
⊢ ↑(LinearIsometryEquiv.trans (↑rotation a) (↑rotation b)) x✝ = ↑(↑rotation (b * a)) x✝
simp