case mp
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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)

case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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)
constructor
case mp.intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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)
case mp
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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)
rintro ⟨f', hf, hf'⟩
no goals
case mp.intro.intro
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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)
rwa [hf.fderiv]
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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
intro H
case pos
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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

case neg
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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
case mpr
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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
by_cases h : DifferentiableAt ℝ f x
no goals
case pos
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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
exact ⟨fderiv ℝ f x, h.hasFDerivAt, H⟩
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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
case neg
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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
nontriviality X
no goals
X : Type u_1
Y : Type u_2
Z : Type ?u.68199
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
exact absurd (fderiv_zero_of_not_differentiableAt h) H.ne_zero