awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
g : ℂ →L[ℝ] ℂ
h : IsConformalMap g
rcases :
  ∀ (c : ℝ) (li : ℂ →ₗᵢ[ℝ] ℂ),
    (∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = c • li.toContinuousLinearMap) ∨
      ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = (c • li.toContinuousLinearMap) ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
⊢ (∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g) ∨
    ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)

Tactic:
rcases h with ⟨c, -, li, rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
h :
  ∀ (x : ℂ),
    Eq (α := ℂ) (((li.toLinearIsometryEquiv ⋯).toLinearIsometry : (a : ℂ) → ℂ) x : ℂ) ((li : (a : ℂ) → ℂ) x : ℂ)
⊢ (li.toLinearIsometryEquiv ⋯).toLinearIsometry = li

Tactic:
ext1
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
x : ℂ
⊢ Eq (α := ℂ) (((li.toLinearIsometryEquiv ⋯).toLinearIsometry : (a : ℂ) → ℂ) x : ℂ) ((li : (a : ℂ) → ℂ) x : ℂ)

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
obtain :
  ∀ (li : ℂ ≃ₗᵢ[ℝ] ℂ),
    (∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = c • li.toLinearIsometry.toContinuousLinearMap) ∨
      ∃ (map : ℂ →L[ℂ] ℂ),
        restrictScalars ℝ map = (c • li.toLinearIsometry.toContinuousLinearMap) ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
⊢ (∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = c • li.toContinuousLinearMap) ∨
    ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = (c • li.toContinuousLinearMap) ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)

Tactic:
obtain ⟨li, rfl⟩ : ∃ li' : ℂ ≃ₗᵢ[ℝ] ℂ, li'.toLinearIsometry = li :=
    ⟨li.toLinearIsometryEquiv rfl, by ext1; rfl⟩

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
c : ℝ
li : ℂ ≃ₗᵢ[ℝ] ℂ
inl :
  ∀ (a : Circle),
    (∃ (map : ℂ →L[ℂ] ℂ),
        restrictScalars ℝ map =
          HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
            (LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))) ∨
      ∃ (map : ℂ →L[ℂ] ℂ),
        restrictScalars ℝ map =
          HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
              (LinearIsometry.toContinuousLinearMap
                (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))) ∘SL
            (↑conjCLE : ℂ →L[ℝ] ℂ)
inr :
  ∀ (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[ℝ] ℂ)
⊢ (∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = c • li.toLinearIsometry.toContinuousLinearMap) ∨
    ∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map = (c • li.toLinearIsometry.toContinuousLinearMap) ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)

Tactic:
rcases linear_isometry_complex li with ⟨a, rfl | rfl⟩

Premises used: linear_isometry_complex, rfl
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
c : ℝ
a : Circle
⊢ (∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map =
        HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
          (LinearIsometry.toContinuousLinearMap
            (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))) ∨
    ∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map =
        HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
            (LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))) ∘SL
          (↑conjCLE : ℂ →L[ℝ] ℂ)

Tactic:
Or.inl ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, ?_⟩

Premises used: ContinuousLinearMap.id, Exists.intro, HSMul.hSMul, Or.inl, Complex, Subtype.val
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
c : ℝ
a : Circle
inl :
  restrictScalars ℝ (c • HSMul.hSMul (β := ℂ →L[ℂ] ℂ) (↑a : ℂ) (ContinuousLinearMap.id ℂ ℂ)) =
    HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
      (LinearIsometry.toContinuousLinearMap
        (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))
⊢ (∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map =
        HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
          (LinearIsometry.toContinuousLinearMap
            (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))) ∨
    ∃ (map : ℂ →L[ℂ] ℂ),
      restrictScalars ℝ map =
        HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
            (LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))) ∘SL
          (↑conjCLE : ℂ →L[ℝ] ℂ)

Tactic:
refine Or.inl ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, ?_⟩

Premises used: Or.inl
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
c : ℝ
a : Circle
inl :
  ∀ (x : ℂ),
    Eq (α := ℂ)
      ((restrictScalars ℝ (c • HSMul.hSMul (β := ℂ →L[ℂ] ℂ) (↑a : ℂ) (ContinuousLinearMap.id ℂ ℂ)) : (a : ℂ) → ℂ) x : ℂ)
      ((HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
              (LinearIsometry.toContinuousLinearMap
                (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))) :
            (a : ℂ) → ℂ)
          x :
        ℂ)
⊢ restrictScalars ℝ (c • HSMul.hSMul (β := ℂ →L[ℂ] ℂ) (↑a : ℂ) (ContinuousLinearMap.id ℂ ℂ)) =
    HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
      (LinearIsometry.toContinuousLinearMap
        (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)))

Tactic:
ext1
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
c : ℝ
a : Circle
x : ℂ
⊢ Eq (α := ℂ)
    ((restrictScalars ℝ (c • HSMul.hSMul (β := ℂ →L[ℂ] ℂ) (↑a : ℂ) (ContinuousLinearMap.id ℂ ℂ)) : (a : ℂ) → ℂ) x : ℂ)
    ((HSMul.hSMul (β := ℂ →L[ℝ] ℂ) c
            (LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))) :
          (a : ℂ) → ℂ)
        x :
      ℂ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Conformal
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[ℝ] ℂ)

Tactic:
Or.inr ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, ?_⟩

Premises used: ContinuousLinearMap.id, Exists.intro, HSMul.hSMul, Complex, Subtype.val, Or.inr
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
c : ℝ
a : Circle
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[ℝ] ℂ)
⊢ (∃ (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[ℝ] ℂ)

Tactic:
refine Or.inr ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, ?_⟩

Premises used: Or.inr
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
c : ℝ
a : Circle
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 :
        ℂ)
⊢ 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:
ext1
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
c : ℝ
a : Circle
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:
simp
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
g : ℂ →L[ℝ] ℂ
mp :
  IsConformalMap g →
    ((∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g) ∨
        ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) ∧
      g ≠ 0
mpr :
  ((∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g) ∨
        ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) ∧
      g ≠ 0 →
    IsConformalMap g
⊢ IsConformalMap g ↔
    ((∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g) ∨
        ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) ∧
      g ≠ 0

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
g : ℂ →L[ℝ] ℂ
⊢ IsConformalMap g →
    ((∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g) ∨
        ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) ∧
      g ≠ 0

Tactic:
fun h => ⟨h.is_complex_or_conj_linear, h.ne_zero⟩

Premises used: IsConformalMap.is_complex_or_conj_linear, IsConformalMap.ne_zero, And.intro
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
g : ℂ →L[ℝ] ℂ
⊢ IsConformalMap g →
    ((∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g) ∨
        ∃ (map : ℂ →L[ℂ] ℂ), restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) ∧
      g ≠ 0

Tactic:
exact fun h => ⟨h.is_complex_or_conj_linear, h.ne_zero⟩
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
map : ℂ →L[ℂ] ℂ
h₂ : Ne (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) 0
⊢ IsConformalMap (restrictScalars ℝ map)

Tactic:
isConformalMap_complex_linear ?_

Premises used: isConformalMap_complex_linear
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
map : ℂ →L[ℂ] ℂ
h₂ : Ne (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) 0
mpr : map ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)

Tactic:
refine isConformalMap_complex_linear ?_

Premises used: isConformalMap_complex_linear
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
map : ℂ →L[ℂ] ℂ
h₂ : Ne (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) 0
mpr : ∀ (w : map = 0), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) 0
⊢ map ≠ 0

Tactic:
contrapose h₂ with w
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
map : ℂ →L[ℂ] ℂ
w : map = 0
⊢ Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) 0

Tactic:
simp only [w, restrictScalars_zero]

Premises used: ContinuousLinearMap.restrictScalars_zero
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
h :
  ∀ (x : ℂ),
    Eq (α := ℂ) ((g : (a : ℂ) → ℂ) x : ℂ) ((restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ) : (a : ℂ) → ℂ) x : ℂ)
⊢ g = restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)

Tactic:
ext1
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
x : ℂ
⊢ Eq (α := ℂ) ((g : (a : ℂ) → ℂ) x : ℂ) ((restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ) : (a : ℂ) → ℂ) x : ℂ)

Tactic:
simp only [hmap, coe_comp', ContinuousLinearEquiv.coe_coe, Function.comp_apply,
          conjCLE_apply, starRingEnd_self_apply]

Premises used: ContinuousLinearMap.coe_comp', Complex.conjCLE_apply, Function.comp_apply, ContinuousLinearEquiv.coe_coe, starRingEnd_self_apply
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
⊢ 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]
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
minor₁ : g = restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
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[ℝ] ℂ))
⊢ IsConformalMap g

Tactic:
rw [minor₁] at h₂ ⊢
-- Module: Mathlib.Analysis.Complex.Conformal
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[ℝ] ℂ))

Tactic:
isConformalMap_complex_linear_conj ?_

Premises used: isConformalMap_complex_linear_conj
-- Module: Mathlib.Analysis.Complex.Conformal
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[ℝ] ℂ)
mpr : map ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))

Tactic:
refine isConformalMap_complex_linear_conj ?_

Premises used: isConformalMap_complex_linear_conj
-- Module: Mathlib.Analysis.Complex.Conformal
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[ℝ] ℂ)
mpr : ∀ (w : map = 0), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) 0
⊢ map ≠ 0

Tactic:
contrapose h₂ with w
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
minor₁ : g = restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)
w : map = 0
⊢ Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ)) 0

Tactic:
simp only [w, restrictScalars_zero, zero_comp]

Premises used: ContinuousLinearMap.zero_comp, ContinuousLinearMap.restrictScalars_zero
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
rw : IsConformalMap (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))
⊢ ConformalAt f z

Tactic:
rw [conformalAt_iff_isConformalMap_fderiv, (h.hasFDerivAt.restrictScalars ℝ).fderiv]

Premises used: Real, HasFDerivAt.restrictScalars, conformalAt_iff_isConformalMap_fderiv, DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
nonzero : Ne (α := ℂ →L[ℂ] E) (fderiv ℂ f z) 0
⊢ IsConformalMap (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))

Tactic:
apply isConformalMap_complex_linear

Premises used: isConformalMap_complex_linear
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ Ne (α := ℂ →L[ℂ] E) (fderiv ℂ f z) 0

Tactic:
simpa only [Ne, ContinuousLinearMap.ext_ring_iff]

Premises used: Ne, ContinuousLinearMap.ext_ring_iff
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
f : ℂ → ℂ
z : ℂ
rw :
  IsConformalMap (fderiv ℝ f z) ↔
    (DifferentiableAt ℂ f z ∨
        DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ)
          ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)) ∧
      Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
⊢ ConformalAt 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]

Premises used: conformalAt_iff_isConformalMap_fderiv
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
f : ℂ → ℂ
z : ℂ
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
⊢ IsConformalMap (fderiv ℝ f z) ↔
    (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]

Premises used: isConformalMap_iff_is_complex_or_conj_linear
-- Module: Mathlib.Analysis.Complex.Conformal
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 : ℂ))
⊢ ((∃ (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:
apply and_congr_left

Premises used: and_congr_left
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
⊢ DifferentiableAt ℝ f z

Tactic:
have h_diff := h.imp_symm fderiv_zero_of_not_differentiableAt
-- Module: Mathlib.Analysis.Complex.Conformal
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
h₂ :
  (∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))) ↔
    DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) 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 : ℂ)

Tactic:
apply or_congr

Premises used: or_congr
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
h_diff : DifferentiableAt ℝ f z
h₁ h₂ :
  (∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z)) ↔
    ∃ (g' : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ g') (fderiv ℝ f z)
⊢ (∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z)) ↔ DifferentiableAt ℂ f z

Tactic:
rw [differentiableAt_iff_restrictScalars ℝ h_diff]

Premises used: Real, differentiableAt_iff_restrictScalars
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
h_diff : DifferentiableAt ℝ f z
⊢ DifferentiableAt ℝ f ((starRingEnd ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ))

Tactic:
rw [← conj_conj z] at h_diff

Premises used: Complex.conj_conj
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
h_diff : DifferentiableAt ℝ f ((starRingEnd ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ))
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))
⊢ (∃ (map : ℂ →L[ℂ] ℂ), Eq (α := ℂ →L[ℝ] ℂ) (restrictScalars ℝ map) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))) ↔
    DifferentiableAt ℂ (E := ℂ) (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) : ℂ → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ)

Tactic:
rw [differentiableAt_iff_restrictScalars ℝ (h_diff.comp _ conjCLE.differentiableAt)]

Premises used: Real, ContinuousLinearEquiv.differentiableAt, Complex.conjCLE, DifferentiableAt.comp, differentiableAt_iff_restrictScalars
-- Module: Mathlib.Analysis.Complex.Conformal
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))

Tactic:
exists_congr fun g => rfl.congr ?_

Premises used: Eq.congr, exists_congr, rfl
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
h_diff : DifferentiableAt ℝ f ((starRingEnd ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ))
h₁ :
  ∀ (g : ℂ →L[ℂ] ℂ),
    Eq (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))
      (fderiv ℝ (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))

Tactic:
refine exists_congr fun g => rfl.congr ?_

Premises used: Eq.congr, exists_congr, rfl
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
h_diff : DifferentiableAt ℝ f ((starRingEnd ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ))
g : ℂ →L[ℂ] ℂ
⊢ fderiv ℝ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) = (↑conjCLE : ℂ →L[ℝ] ℂ)

Tactic:
have : fderiv ℝ conj (conj z) = _ := conjCLE.fderiv
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
f : ℂ → ℂ
z : ℂ
h : Ne (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z) 0
h_diff : DifferentiableAt ℝ f ((starRingEnd ℂ : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z : ℂ))
g : ℂ →L[ℂ] ℂ
this : fderiv ℝ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) z) = (↑conjCLE : ℂ →L[ℝ] ℂ)
⊢ Eq (α := ℂ →L[ℝ] ℂ) (fderiv ℝ f z ∘SL (↑conjCLE : ℂ →L[ℝ] ℂ))
    (fderiv ℝ (f ∘ (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ)) ((starRingEnd ℂ : (a : ℂ) → ℂ) z))

Tactic:
simp [fderiv_comp _ h_diff conjCLE.differentiableAt, this]

Premises used: ContinuousLinearEquiv.differentiableAt, fderiv_comp, Complex.conjCLE