[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
⊢ ConformalAt f x ↔ IsConformalMap (fderiv ℝ f x)
[PROOFSTEP]
constructor
[GOAL]
case mp
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
⊢ ConformalAt f x → IsConformalMap (fderiv ℝ f x)
[PROOFSTEP]
rintro ⟨f', hf, hf'⟩
[GOAL]
case mp.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
f' : X →L[ℝ] Y
hf : HasFDerivAt f f' x
hf' : IsConformalMap f'
⊢ IsConformalMap (fderiv ℝ f x)
[PROOFSTEP]
rwa [hf.fderiv]
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
⊢ IsConformalMap (fderiv ℝ f x) → ConformalAt f x
[PROOFSTEP]
intro H
[GOAL]
case mpr
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
⊢ ConformalAt f x
[PROOFSTEP]
by_cases h : DifferentiableAt ℝ f x
[GOAL]
case pos
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
h : DifferentiableAt ℝ f x
⊢ ConformalAt f x
[PROOFSTEP]
exact ⟨fderiv ℝ f x, h.hasFDerivAt, H⟩
[GOAL]
case neg
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
h : ¬DifferentiableAt ℝ f x
⊢ ConformalAt f x
[PROOFSTEP]
nontriviality X
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
x : X
H : IsConformalMap (fderiv ℝ f x)
h : ¬DifferentiableAt ℝ f x
✝ : Nontrivial X
⊢ ConformalAt f x
[PROOFSTEP]
exact absurd (fderiv_zero_of_not_differentiableAt h) H.ne_zero
[GOAL]
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
hg : ConformalAt g (f x)
hf : ConformalAt f x
⊢ ConformalAt (g ∘ f) x
[PROOFSTEP]
rcases hf with ⟨f', hf₁, cf⟩
[GOAL]
case intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
hg : ConformalAt g (f x)
f' : X →L[ℝ] Y
hf₁ : HasFDerivAt f f' x
cf : IsConformalMap f'
⊢ ConformalAt (g ∘ f) x
[PROOFSTEP]
rcases hg with ⟨g', hg₁, cg⟩
[GOAL]
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝⁵ : NormedAddCommGroup X
inst✝⁴ : NormedAddCommGroup Y
inst✝³ : NormedAddCommGroup Z
inst✝² : NormedSpace ℝ X
inst✝¹ : NormedSpace ℝ Y
inst✝ : NormedSpace ℝ Z
f : X → Y
g : Y → Z
x : X
f' : X →L[ℝ] Y
hf₁ : HasFDerivAt f f' x
cf : IsConformalMap f'
g' : Y →L[ℝ] Z
hg₁ : HasFDerivAt g g' (f x)
cg : IsConformalMap g'
⊢ ConformalAt (g ∘ f) x
[PROOFSTEP]
exact ⟨g'.comp f', hg₁.comp x hf₁, cg.comp cf⟩
