[GOAL]
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E → F
x : E
⊢ ConformalAt f x ↔ ∃ c, 0 < c ∧ ∀ (u v : E), inner (↑(fderiv ℝ f x) u) (↑(fderiv ℝ f x) v) = c * inner u v
[PROOFSTEP]
rw [conformalAt_iff_isConformalMap_fderiv, isConformalMap_iff]
[GOAL]
E : Type u_1
F : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ E
inst✝ : InnerProductSpace ℝ F
f : E → F
x : E
f' : E →L[ℝ] F
h : HasFDerivAt f f' x
⊢ ConformalAt f x ↔ ∃ c, 0 < c ∧ ∀ (u v : E), inner (↑f' u) (↑f' v) = c * inner u v
[PROOFSTEP]
simp only [conformalAt_iff', h.fderiv]
