awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
c : ℝ
a : Circle
⊢ (∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map =
        HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
          (LinearIsometry.toContinuousLinearMap
            (LinearIsometryEquiv.toLinearIsometry (conjLIE.trans ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))))) ∨
    ∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map =
        HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
            (LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry (conjLIE.trans ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))) ∘SL
          (↑conjCLE : ℂ →L[ℝ] ℂ)
have inr : restrictScalars ℝ (c • HSMul.hSMul (β := ℂ →L[ℂ] ℂ) (↑a : ℂ) (ContinuousLinearMap.id ℂ ℂ)) =
  HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
      (LinearIsometry.toContinuousLinearMap
        (LinearIsometryEquiv.toLinearIsometry (conjLIE.trans ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))) ∘SL
    (↑conjCLE : ℂ →L[ℝ] ℂ)
Tactic: refine Or.inr ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
c : ℝ
a : Circle
⊢ restrictScalars ℝ (c • HSMul.hSMul (β := ℂ →L[ℂ] ℂ) (↑a : ℂ) (ContinuousLinearMap.id ℂ ℂ)) =
    HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
        (LinearIsometry.toContinuousLinearMap
          (LinearIsometryEquiv.toLinearIsometry (conjLIE.trans ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))) ∘SL
      (↑conjCLE : ℂ →L[ℝ] ℂ)
have inr : ∀ (x : ℂ),
  Eq (α := ℂ)
    ((restrictScalars ℝ (c • HSMul.hSMul (β := ℂ →L[ℂ] ℂ) (↑a : ℂ) (ContinuousLinearMap.id ℂ ℂ)) : (a : ℂ) → ℂ) x : ℂ)
    ((HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
              (LinearIsometry.toContinuousLinearMap
                (LinearIsometryEquiv.toLinearIsometry (conjLIE.trans ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))) ∘SL
            (↑conjCLE : ℂ →L[ℝ] ℂ) :
          (a : ℂ) → ℂ)
        x :
      ℂ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
g : ℂ →L[ℝ] ℂ
⊢ IsConformalMap g ↔
    ((∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g) ∨
        ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) ∧
      g ≠ 0
have mp : IsConformalMap g →
  ((∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g) ∨
      ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) ∧
    g ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
g : ℂ →L[ℝ] ℂ
mp :
  IsConformalMap g →
    ((∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g) ∨
        ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) ∧
      g ≠ 0
⊢ IsConformalMap g ↔
    ((∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g) ∨
        ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) ∧
      g ≠ 0
have mpr : ((∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g) ∨
      ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) ∧
    g ≠ 0 →
  IsConformalMap g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
map : ℂ →L[ℂ] ℂ
h₂ : Ne (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) 0
⊢ IsConformalMap (restrictScalars ℝ map)
have mpr : map ≠ 0
Tactic: refine isConformalMap_complex_linear ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
map : ℂ →L[ℂ] ℂ
h₂ : Ne (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) 0
⊢ map ≠ 0
have mpr : ∀ (w : map = 0), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) 0
Tactic: contrapose h₂ with w
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
⊢ g = restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
have h : ∀ (x : ℂ),
  Eq (α := ℂ) ((g : (a : ℂ) → ℂ) x : ℂ) ((restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ) : (a : ℂ) → ℂ) x : ℂ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (hypothesis)
Goal:
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
⊢ IsConformalMap g
have minor₁ : g = restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
Tactic: have minor₁ : g = map.restrictScalars ℝ ∘L ↑conjCLE := by
        ext1
        simp only [hmap, coe_comp', ContinuousLinearEquiv.coe_coe, Function.comp_apply,
          conjCLE_apply, starRingEnd_self_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
minor₁ : g = restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
⊢ IsConformalMap g
have mpr : ∀ (h₂ : Ne (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) 0)
  (hmap : restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))
  (minor₁ : g = restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)),
  IsConformalMap (restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))
Tactic: rw [minor₁] at h₂ ⊢
Cleared hypotheses: h₂, hmap, minor₁
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
h₂ : Ne (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) 0
hmap : restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
minor₁ : g = restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
⊢ IsConformalMap (restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))
have mpr : map ≠ 0
Tactic: refine isConformalMap_complex_linear_conj ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
h₂ : Ne (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) 0
hmap : restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
minor₁ : g = restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
⊢ map ≠ 0
have mpr : ∀ (w : map = 0), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) 0
Tactic: contrapose h₂ with w
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ ConformalAt f z
have rw : IsConformalMap (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))
Tactic: rw [conformalAt_iff_isConformalMap_fderiv, (h.hasFDerivAt.restrictScalars ℝ).fderiv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ IsConformalMap (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))
have nonzero : Ne (α := ℂ →L[ℂ] E) (fderiv ℂ f z) 0
Tactic: apply isConformalMap_complex_linear
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
f : ℂ → ℂ
z : ℂ
⊢ ConformalAt f z ↔
    (DifferentiableAt ℂ f z ∨
        DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)) ∧
      Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
have rw : IsConformalMap (fderiv ℝ f z) ↔
  (DifferentiableAt ℂ f z ∨
      DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)) ∧
    Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
Tactic: rw [conformalAt_iff_isConformalMap_fderiv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
f : ℂ → ℂ
z : ℂ
⊢ IsConformalMap (fderiv ℝ f z) ↔
    (DifferentiableAt ℂ f z ∨
        DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)) ∧
      Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
have rw : ((∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z)) ∨
      ∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))) ∧
    Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0 ↔
  (DifferentiableAt ℂ f z ∨
      DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)) ∧
    Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
Tactic: rw [isConformalMap_iff_is_complex_or_conj_linear]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
f : ℂ → ℂ
z : ℂ
⊢ ((∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z)) ∨
        ∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))) ∧
      Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0 ↔
    (DifferentiableAt ℂ f z ∨
        DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)) ∧
      Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
have h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0 →
  (((∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z)) ∨
      ∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))) ↔
    DifferentiableAt ℂ f z ∨
      DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ))
Tactic: apply and_congr_left
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (hypothesis)
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
⊢ ((∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z)) ∨
      ∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))) ↔
    DifferentiableAt ℂ f z ∨
      DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)
have h_diff : DifferentiableAt ℝ f z
Tactic: have h_diff := h.imp_symm fderiv_zero_of_not_differentiableAt
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
h_diff : DifferentiableAt ℝ f z
⊢ ((∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z)) ∨
      ∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))) ↔
    DifferentiableAt ℂ f z ∨
      DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)
have h₁ : (∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z)) ↔ DifferentiableAt ℂ f z
Tactic: apply or_congr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
h_diff : DifferentiableAt ℝ f z
h₁ : (∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z)) ↔ DifferentiableAt ℂ f z
⊢ ((∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z)) ∨
      ∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))) ↔
    DifferentiableAt ℂ f z ∨
      DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)
have h₂ : (∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))) ↔
  DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)
Tactic: apply or_congr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z)) ↔ DifferentiableAt ℂ f z
have h₁ : (∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z)) ↔
  ∃ (g' : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ g') (fderiv ℝ f z)
Tactic: rw [differentiableAt_iff_restrictScalars ℝ h_diff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (hypothesis)
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))) ↔
    DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)
have h_diff₁ : DifferentiableAt ℝ f ((starRingEnd ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ))
Tactic: rw [← conj_conj z] at h_diff
Cleared hypotheses: h_diff
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
h_diff : DifferentiableAt ℝ f ((starRingEnd ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ))
⊢ (∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))) ↔
    DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)
have h₁ : (∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))) ↔
  ∃ (g' : ℂ →L[ℂ] ℂ),
    Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ g')
      (fderiv ℝ (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ)) ((starRingEnd ℂ : (a : ℂ) → ℂ) z))
Tactic: rw [differentiableAt_iff_restrictScalars ℝ (h_diff.comp _ conjCLE.differentiableAt)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
h_diff : DifferentiableAt ℝ f ((starRingEnd ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ))
⊢ (∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))) ↔
    ∃ (g' : ℂ →L[ℂ] ℂ),
      Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ g')
        (fderiv ℝ (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ)) ((starRingEnd ℂ : (a : ℂ) → ℂ) z))
have h₁ : ∀ (g : ℂ →L[ℂ] ℂ),
  Eq (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))
    (fderiv ℝ (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ)) ((starRingEnd ℂ : (a : ℂ) → ℂ) z))
Tactic: refine exists_congr fun g => rfl.congr ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (hypothesis)
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
h_diff : DifferentiableAt ℝ f ((starRingEnd ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ))
g : ℂ →L[ℂ] ℂ
⊢ Eq (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))
    (fderiv ℝ (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ)) ((starRingEnd ℂ : (a : ℂ) → ℂ) z))
have this : fderiv ℝ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) = (↑conjCLE : ℂ →L[ℝ] ℂ)
Tactic: have : fderiv ℝ conj (conj z) = _ := conjCLE.fderiv
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
a b : ℂ
⊢ (ℓ : (a : ℂ) → E) (a • b) = HSMul.hSMul (β := E) a ((ℓ : (a : ℂ) → E) b : E)
have rw : (ℓ : (a : ℂ) → E) (((↑a.re : ℂ) + (↑a.im : ℂ) • I) • ((↑b.re : ℂ) + (↑b.im : ℂ) • I)) =
  HSMul.hSMul (β := E) ((↑a.re : ℂ) + (↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.re : ℂ) + (↑b.im : ℂ) • I) : E)
Tactic: rw [← re_add_im a, ← re_add_im b, ← smul_eq_mul _ I, ← smul_eq_mul _ I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
a b : ℂ
⊢ (ℓ : (a : ℂ) → E) (((↑a.re : ℂ) + (↑a.im : ℂ) • I) • ((↑b.re : ℂ) + (↑b.im : ℂ) • I)) =
    HSMul.hSMul (β := E) ((↑a.re : ℂ) + (↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.re : ℂ) + (↑b.im : ℂ) • I) : E)
have t₀ : ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I
Tactic: have t₀ : ((a.im : ℂ) • I) • (b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I := by
    simp only [smul_eq_mul, ofReal_mul, ← mul_assoc, mul_comm _ I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
a b : ℂ
t₀ : ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I
⊢ (ℓ : (a : ℂ) → E) (((↑a.re : ℂ) + (↑a.im : ℂ) • I) • ((↑b.re : ℂ) + (↑b.im : ℂ) • I)) =
    HSMul.hSMul (β := E) ((↑a.re : ℂ) + (↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.re : ℂ) + (↑b.im : ℂ) • I) : E)
have t₁ : ((↑a.im : ℂ) • I) • (↑b.im : ℂ) • I = HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1
Tactic: have t₁ : ((a.im : ℂ) • I) • (b.im : ℂ) • I = (↑(- a.im * b.im) : ℂ) • (1 : ℂ) := by
    simp [mul_mul_mul_comm _ I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
a b : ℂ
t₀ : ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I
t₁ : ((↑a.im : ℂ) • I) • (↑b.im : ℂ) • I = HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1
⊢ (ℓ : (a : ℂ) → E) (((↑a.re : ℂ) + (↑a.im : ℂ) • I) • ((↑b.re : ℂ) + (↑b.im : ℂ) • I)) =
    HSMul.hSMul (β := E) ((↑a.re : ℂ) + (↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.re : ℂ) + (↑b.im : ℂ) • I) : E)
have simp : HAdd.hAdd (α := E) (β := E) ((ℓ : (a : ℂ) → E) ((↑a.re : ℂ) • (↑b.re : ℂ)) : E)
      ((ℓ : (a : ℂ) → E) ((↑(a.im * b.re) : ℂ) • I) : E) +
    HAdd.hAdd (α := E) (β := E) ((ℓ : (a : ℂ) → E) ((↑a.re : ℂ) • (↑b.im : ℂ) • I) : E)
      ((ℓ : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1) : E) =
  HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
    (HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E) +
      HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E))
Tactic: simp only [add_smul, smul_add, ℓ.map_add, t₀, t₁]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
a b : ℂ
t₀ : ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I
t₁ : ((↑a.im : ℂ) • I) • (↑b.im : ℂ) • I = HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1
⊢ HAdd.hAdd (α := E) (β := E) ((ℓ : (a : ℂ) → E) ((↑a.re : ℂ) • (↑b.re : ℂ)) : E)
        ((ℓ : (a : ℂ) → E) ((↑(a.im * b.re) : ℂ) • I) : E) +
      HAdd.hAdd (α := E) (β := E) ((ℓ : (a : ℂ) → E) ((↑a.re : ℂ) • (↑b.im : ℂ) • I) : E)
        ((ℓ : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1) : E) =
    HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
        HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      (HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E) +
        HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E))
have rw : HAdd.hAdd (β := E) (HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E))
      ((ℓ : (a : ℂ) → E) ((↑(a.im * b.re) : ℂ) • I) : E) +
    HAdd.hAdd (α := E) (β := E) ((ℓ : (a : ℂ) → E) ((↑a.re : ℂ) • (↑b.im : ℂ) • I) : E)
      ((ℓ : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1) : E) =
  HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
    (HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E) +
      HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E))
Tactic: rw [Complex.coe_smul, ℓ.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
a b : ℂ
t₀ : ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I
t₁ : ((↑a.im : ℂ) • I) • (↑b.im : ℂ) • I = HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1
⊢ HAdd.hAdd (β := E) (HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E))
        ((ℓ : (a : ℂ) → E) ((↑(a.im * b.re) : ℂ) • I) : E) +
      HAdd.hAdd (α := E) (β := E) ((ℓ : (a : ℂ) → E) ((↑a.re : ℂ) • (↑b.im : ℂ) • I) : E)
        ((ℓ : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1) : E) =
    HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
        HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      (HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E) +
        HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E))
have rw : HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      HSMul.hSMul (β := E) (a.im * b.re) ((ℓ : (a : ℂ) → E) I : E) +
    HAdd.hAdd (α := E) (β := E) ((ℓ : (a : ℂ) → E) ((↑a.re : ℂ) • (↑b.im : ℂ) • I) : E)
      ((ℓ : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1) : E) =
  HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
    (HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E) +
      HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E))
Tactic: rw [Complex.coe_smul, ℓ.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
a b : ℂ
t₀ : ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I
t₁ : ((↑a.im : ℂ) • I) • (↑b.im : ℂ) • I = HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1
⊢ HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
        HSMul.hSMul (β := E) (a.im * b.re) ((ℓ : (a : ℂ) → E) I : E) +
      HAdd.hAdd (α := E) (β := E) ((ℓ : (a : ℂ) → E) ((↑a.re : ℂ) • (↑b.im : ℂ) • I) : E)
        ((ℓ : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1) : E) =
    HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
        HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      (HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E) +
        HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E))
have rw : HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      HSMul.hSMul (β := E) (a.im * b.re) ((ℓ : (a : ℂ) → E) I : E) +
    HAdd.hAdd (β := E) (HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E))
      ((ℓ : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1) : E) =
  HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
    (HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E) +
      HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E))
Tactic: rw [Complex.coe_smul, ℓ.map_smul]