ι : Type ?u.1334907
ι' : Type ?u.1334910
𝕜 : Type ?u.1334913
inst✝⁹ : IsROrC 𝕜
E : Type ?u.1334919
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.1334939
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_2
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
v : OrthonormalBasis (Fin 2) ℝ F
f : F ≃ₗᵢ[ℝ] F'
⊢ LinearIsometryEquiv.trans orthonormalBasisOneI.repr (LinearIsometryEquiv.trans (LinearIsometryEquiv.symm v.repr) f) =
    LinearIsometryEquiv.trans (LinearIsometryEquiv.trans orthonormalBasisOneI.repr (LinearIsometryEquiv.symm v.repr)) f
ι : Type ?u.1334907
ι' : Type ?u.1334910
𝕜 : Type ?u.1334913
inst✝⁹ : IsROrC 𝕜
E : Type ?u.1334919
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.1334939
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_2
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
v : OrthonormalBasis (Fin 2) ℝ F
f : F ≃ₗᵢ[ℝ] F'
⊢ isometryOfOrthonormal (OrthonormalBasis.map v f) = LinearIsometryEquiv.trans (isometryOfOrthonormal v) f
simp [Complex.isometryOfOrthonormal, LinearIsometryEquiv.trans_assoc, OrthonormalBasis.map]
no goals
ι : Type ?u.1334907
ι' : Type ?u.1334910
𝕜 : Type ?u.1334913
inst✝⁹ : IsROrC 𝕜
E : Type ?u.1334919
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : InnerProductSpace 𝕜 E
E' : Type ?u.1334939
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : InnerProductSpace 𝕜 E'
F : Type u_1
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
F' : Type u_2
inst✝² : NormedAddCommGroup F'
inst✝¹ : InnerProductSpace ℝ F'
inst✝ : Fintype ι
v : OrthonormalBasis (Fin 2) ℝ F
f : F ≃ₗᵢ[ℝ] F'
⊢ LinearIsometryEquiv.trans orthonormalBasisOneI.repr (LinearIsometryEquiv.trans (LinearIsometryEquiv.symm v.repr) f) =
    LinearIsometryEquiv.trans (LinearIsometryEquiv.trans orthonormalBasisOneI.repr (LinearIsometryEquiv.symm v.repr)) f
rw [LinearIsometryEquiv.trans_assoc]