case intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
u v : E
c : ℝ
hc : c ≠ 0
li : E →ₗᵢ[ℝ] F
⊢ angle (↑(c • LinearIsometry.toContinuousLinearMap li) u) (↑(c • LinearIsometry.toContinuousLinearMap li) v) =
    angle u v
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f' : E →L[ℝ] F
h : IsConformalMap f'
u v : E
⊢ angle (↑f' u) (↑f' v) = angle u v
obtain ⟨c, hc, li, rfl⟩ := h
no goals
case intro.intro.intro
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
u v : E
c : ℝ
hc : c ≠ 0
li : E →ₗᵢ[ℝ] F
⊢ angle (↑(c • LinearIsometry.toContinuousLinearMap li) u) (↑(c • LinearIsometry.toContinuousLinearMap li) v) =
    angle u v
exact (angle_smul_smul hc _ _).trans (li.angle_map _ _)