-- Mathlib/Analysis/Complex/Conformal.lean
theorem isConformalMap_iff_is_complex_or_conj_linear :
    IsConformalMap g ↔
      ((∃ map : ℂ →L[ℂ] ℂ, map.restrictScalars ℝ = g) ∨
          ∃ map : ℂ →L[ℂ] ℂ, map.restrictScalars ℝ = g ∘L ↑conjCLE) ∧
        g ≠ 0

Proof state:
case mpr
g : ℂ →L[ℝ] ℂ
⊢ ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = g.comp ↑conjCLE) ∧ g ≠ 0 → IsConformalMap g

Tactic:
rintro ⟨⟨map, rfl⟩ | ⟨map, hmap⟩, h₂⟩

Result:
case mpr.intro.inl.intro
map : ℂ →L[ℂ] ℂ
h₂ : restrictScalars ℝ map ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)

case mpr.intro.inr.intro
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g.comp ↑conjCLE
⊢ IsConformalMap g

Proof state:
case mpr.intro.inr.intro
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g.comp ↑conjCLE
minor₁ : g = (restrictScalars ℝ map).comp ↑conjCLE
w : map = 0
⊢ (restrictScalars ℝ map).comp ↑conjCLE = 0

Tactic:
simp only [w, restrictScalars_zero, zero_comp]

Result:
no goals

Proof state:
case mpr.intro.inr.intro
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g.comp ↑conjCLE
⊢ IsConformalMap g

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]

Result:
case mpr.intro.inr.intro
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g.comp ↑conjCLE
minor₁ : g = (restrictScalars ℝ map).comp ↑conjCLE
⊢ IsConformalMap g

Proof state:
g : ℂ →L[ℝ] ℂ
⊢ IsConformalMap g ↔ ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = g.comp ↑conjCLE) ∧ g ≠ 0

Tactic:
constructor

Result:
case mp
g : ℂ →L[ℝ] ℂ
⊢ IsConformalMap g → ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = g.comp ↑conjCLE) ∧ g ≠ 0

case mpr
g : ℂ →L[ℝ] ℂ
⊢ ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = g.comp ↑conjCLE) ∧ g ≠ 0 → IsConformalMap g

Proof state:
case mpr.intro.inl.intro
map : ℂ →L[ℂ] ℂ
h₂ : restrictScalars ℝ map ≠ 0
⊢ map ≠ 0

Tactic:
contrapose! h₂ with w

Result:
case mpr.intro.inl.intro
map : ℂ →L[ℂ] ℂ
w : map = 0
⊢ restrictScalars ℝ map = 0

Proof state:
case h
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g.comp ↑conjCLE
x✝ : ℂ
⊢ g x✝ = ((restrictScalars ℝ map).comp ↑conjCLE) x✝

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

Result:
no goals

Proof state:
case mpr.intro.inl.intro
map : ℂ →L[ℂ] ℂ
w : map = 0
⊢ restrictScalars ℝ map = 0

Tactic:
simp only [w, restrictScalars_zero]

Result:
no goals

Proof state:
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g.comp ↑conjCLE
⊢ g = (restrictScalars ℝ map).comp ↑conjCLE

Tactic:
ext1

Result:
case h
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g.comp ↑conjCLE
x✝ : ℂ
⊢ g x✝ = ((restrictScalars ℝ map).comp ↑conjCLE) x✝

Proof state:
case mp
g : ℂ →L[ℝ] ℂ
⊢ IsConformalMap g → ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = g.comp ↑conjCLE) ∧ g ≠ 0

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

Result:
no goals

Proof state:
case mpr.intro.inr.intro
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
h₂ : (restrictScalars ℝ map).comp ↑conjCLE ≠ 0
hmap : restrictScalars ℝ map = g.comp ↑conjCLE
minor₁ : g = (restrictScalars ℝ map).comp ↑conjCLE
⊢ IsConformalMap ((restrictScalars ℝ map).comp ↑conjCLE)

Tactic:
refine isConformalMap_complex_linear_conj ?_

Result:
case mpr.intro.inr.intro
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
h₂ : (restrictScalars ℝ map).comp ↑conjCLE ≠ 0
hmap : restrictScalars ℝ map = g.comp ↑conjCLE
minor₁ : g = (restrictScalars ℝ map).comp ↑conjCLE
⊢ map ≠ 0

Proof state:
case mpr.intro.inr.intro
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
h₂ : (restrictScalars ℝ map).comp ↑conjCLE ≠ 0
hmap : restrictScalars ℝ map = g.comp ↑conjCLE
minor₁ : g = (restrictScalars ℝ map).comp ↑conjCLE
⊢ map ≠ 0

Tactic:
contrapose! h₂ with w

Result:
case mpr.intro.inr.intro
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g.comp ↑conjCLE
minor₁ : g = (restrictScalars ℝ map).comp ↑conjCLE
w : map = 0
⊢ (restrictScalars ℝ map).comp ↑conjCLE = 0

Proof state:
case mpr.intro.inr.intro
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = g.comp ↑conjCLE
minor₁ : g = (restrictScalars ℝ map).comp ↑conjCLE
⊢ IsConformalMap g

Tactic:
rw [minor₁] at h₂ ⊢

Result:
case mpr.intro.inr.intro
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
h₂ : (restrictScalars ℝ map).comp ↑conjCLE ≠ 0
hmap : restrictScalars ℝ map = g.comp ↑conjCLE
minor₁ : g = (restrictScalars ℝ map).comp ↑conjCLE
⊢ IsConformalMap ((restrictScalars ℝ map).comp ↑conjCLE)

Proof state:
case mpr.intro.inl.intro
map : ℂ →L[ℂ] ℂ
h₂ : restrictScalars ℝ map ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)

Tactic:
refine isConformalMap_complex_linear ?_

Result:
case mpr.intro.inl.intro
map : ℂ →L[ℂ] ℂ
h₂ : restrictScalars ℝ map ≠ 0
⊢ map ≠ 0