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

case mpr
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
⊢ ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = comp g ↑conjCle) ∧ g ≠ 0 → IsConformalMap g
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
⊢ IsConformalMap g ↔ ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = comp g ↑conjCle) ∧ g ≠ 0
constructor
no goals
case mp
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
⊢ IsConformalMap g → ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = comp g ↑conjCle) ∧ g ≠ 0
exact fun h => ⟨h.is_complex_or_conj_linear, h.ne_zero⟩
case mpr.intro.inl.intro
f : ℂ → ℂ
z : ℂ
map : ℂ →L[ℂ] ℂ
h₂ : restrictScalars ℝ map ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)

case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = comp g ↑conjCle
⊢ IsConformalMap g
case mpr
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
⊢ ((∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = comp g ↑conjCle) ∧ g ≠ 0 → IsConformalMap g
rintro ⟨⟨map, rfl⟩ | ⟨map, hmap⟩, h₂⟩
case mpr.intro.inl.intro
f : ℂ → ℂ
z : ℂ
map : ℂ →L[ℂ] ℂ
h₂ : restrictScalars ℝ map ≠ 0
⊢ map ≠ 0
case mpr.intro.inl.intro
f : ℂ → ℂ
z : ℂ
map : ℂ →L[ℂ] ℂ
h₂ : restrictScalars ℝ map ≠ 0
⊢ IsConformalMap (restrictScalars ℝ map)
refine' isConformalMap_complex_linear _
case mpr.intro.inl.intro
f : ℂ → ℂ
z : ℂ
map : ℂ →L[ℂ] ℂ
w : map = 0
⊢ restrictScalars ℝ map = 0
case mpr.intro.inl.intro
f : ℂ → ℂ
z : ℂ
map : ℂ →L[ℂ] ℂ
h₂ : restrictScalars ℝ map ≠ 0
⊢ map ≠ 0
contrapose! h₂ with w
no goals
case mpr.intro.inl.intro
f : ℂ → ℂ
z : ℂ
map : ℂ →L[ℂ] ℂ
w : map = 0
⊢ restrictScalars ℝ map = 0
simp only [w, restrictScalars_zero]
case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = comp g ↑conjCle
minor₁ : g = comp (restrictScalars ℝ map) ↑conjCle
⊢ IsConformalMap g
case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = comp g ↑conjCle
⊢ IsConformalMap g
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]
case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
h₂ : comp (restrictScalars ℝ map) ↑conjCle ≠ 0
hmap : restrictScalars ℝ map = comp g ↑conjCle
minor₁ : g = comp (restrictScalars ℝ map) ↑conjCle
⊢ IsConformalMap (comp (restrictScalars ℝ map) ↑conjCle)
case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = comp g ↑conjCle
minor₁ : g = comp (restrictScalars ℝ map) ↑conjCle
⊢ IsConformalMap g
rw [minor₁] at h₂⊢
case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
h₂ : comp (restrictScalars ℝ map) ↑conjCle ≠ 0
hmap : restrictScalars ℝ map = comp g ↑conjCle
minor₁ : g = comp (restrictScalars ℝ map) ↑conjCle
⊢ map ≠ 0
case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
h₂ : comp (restrictScalars ℝ map) ↑conjCle ≠ 0
hmap : restrictScalars ℝ map = comp g ↑conjCle
minor₁ : g = comp (restrictScalars ℝ map) ↑conjCle
⊢ IsConformalMap (comp (restrictScalars ℝ map) ↑conjCle)
refine' isConformalMap_complex_linear_conj _
case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = comp g ↑conjCle
minor₁ : g = comp (restrictScalars ℝ map) ↑conjCle
w : map = 0
⊢ comp (restrictScalars ℝ map) ↑conjCle = 0
case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
h₂ : comp (restrictScalars ℝ map) ↑conjCle ≠ 0
hmap : restrictScalars ℝ map = comp g ↑conjCle
minor₁ : g = comp (restrictScalars ℝ map) ↑conjCle
⊢ map ≠ 0
contrapose! h₂ with w
no goals
case mpr.intro.inr.intro
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = comp g ↑conjCle
minor₁ : g = comp (restrictScalars ℝ map) ↑conjCle
w : map = 0
⊢ comp (restrictScalars ℝ map) ↑conjCle = 0
simp only [w, restrictScalars_zero, zero_comp]
case h
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = comp g ↑conjCle
x✝ : ℂ
⊢ ↑g x✝ = ↑(comp (restrictScalars ℝ map) ↑conjCle) x✝
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = comp g ↑conjCle
⊢ g = comp (restrictScalars ℝ map) ↑conjCle
ext1
no goals
case h
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
h₂ : g ≠ 0
map : ℂ →L[ℂ] ℂ
hmap : restrictScalars ℝ map = comp g ↑conjCle
x✝ : ℂ
⊢ ↑g x✝ = ↑(comp (restrictScalars ℝ map) ↑conjCle) x✝
simp only [hmap, coe_comp', ContinuousLinearEquiv.coe_coe, Function.comp_apply,
  conjCle_apply, starRingEnd_self_apply]