E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ IsConformalMap (fderiv ℝ f z) ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ ConformalAt f z ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
rw [conformalAt_iff_isConformalMap_fderiv]
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ∧
      fderiv ℝ f z ≠ 0 ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ IsConformalMap (fderiv ℝ f z) ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
rw [isConformalMap_iff_is_complex_or_conj_linear]
case h
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ fderiv ℝ f z ≠ 0 →
    (((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
      DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z))
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ∧
      fderiv ℝ f z ≠ 0 ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
apply and_congr_left
case h
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
case h
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ fderiv ℝ f z ≠ 0 →
    (((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
      DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z))
intro h
case h
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
case h
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
have h_diff := h.imp_symm fderiv_zero_of_not_differentiableAt
case h.h₁
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ map, restrictScalars ℝ map = fderiv ℝ f z) ↔ DifferentiableAt ℂ f z

case h.h₂
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
case h
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
apply or_congr
case h.h₂
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
⊢ (∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
case h.h₂
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
rw [← conj_conj z] at h_diff
case h.h₂
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
⊢ (∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    ∃ g', restrictScalars ℝ g' = fderiv ℝ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
case h.h₂
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
⊢ (∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
rw [differentiableAt_iff_restrictScalars ℝ (h_diff.comp _ conjCle.differentiableAt)]
case h.h₂
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
g : ℂ →L[ℂ] ℂ
⊢ comp (fderiv ℝ f z) ↑conjCle = fderiv ℝ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
case h.h₂
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
⊢ (∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    ∃ g', restrictScalars ℝ g' = fderiv ℝ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
refine' exists_congr fun g => rfl.congr _
case h.h₂
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
g : ℂ →L[ℂ] ℂ
this : fderiv ℝ (↑(starRingEnd ((fun x => ℂ) z))) (↑(starRingEnd ℂ) z) = ↑conjCle
⊢ comp (fderiv ℝ f z) ↑conjCle = fderiv ℝ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
case h.h₂
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
g : ℂ →L[ℂ] ℂ
⊢ comp (fderiv ℝ f z) ↑conjCle = fderiv ℝ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
have : fderiv ℝ conj (conj z) = _ := conjCle.fderiv
no goals
case h.h₂
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
g : ℂ →L[ℂ] ℂ
this : fderiv ℝ (↑(starRingEnd ((fun x => ℂ) z))) (↑(starRingEnd ℂ) z) = ↑conjCle
⊢ comp (fderiv ℝ f z) ↑conjCle = fderiv ℝ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
simp [fderiv.comp _ h_diff conjCle.differentiableAt, this, conj_conj]
no goals
case h.h₁
E : Type ?u.154957
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ map, restrictScalars ℝ map = fderiv ℝ f z) ↔ DifferentiableAt ℂ f z
rw [differentiableAt_iff_restrictScalars ℝ h_diff]