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

Proof state:
case intro.intro.intro.intro.intro.inl
c : ℝ
a : Circle
⊢ restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ) = c • (rotation a).toLinearIsometry.toContinuousLinearMap

Tactic:
ext1

Result:
case intro.intro.intro.intro.intro.inl.h
c : ℝ
a : Circle
x✝ : ℂ
⊢ (restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ)) x✝ =
    (c • (rotation a).toLinearIsometry.toContinuousLinearMap) x✝

Proof state:
case intro.intro.intro.intro.intro.inl.h
c : ℝ
a : Circle
x✝ : ℂ
⊢ (restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ)) x✝ =
    (c • (rotation a).toLinearIsometry.toContinuousLinearMap) x✝

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro.intro
c : ℝ
li : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ (∃ map, restrictScalars ℝ map = c • li.toLinearIsometry.toContinuousLinearMap) ∨
    ∃ map, restrictScalars ℝ map = (c • li.toLinearIsometry.toContinuousLinearMap).comp ↑conjCLE

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

Result:
case intro.intro.intro.intro.intro.inl
c : ℝ
a : Circle
⊢ (∃ map, restrictScalars ℝ map = c • (rotation a).toLinearIsometry.toContinuousLinearMap) ∨
    ∃ map, restrictScalars ℝ map = (c • (rotation a).toLinearIsometry.toContinuousLinearMap).comp ↑conjCLE

case intro.intro.intro.intro.intro.inr
c : ℝ
a : Circle
⊢ (∃ map, restrictScalars ℝ map = c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap) ∨
    ∃ map,
      restrictScalars ℝ map = (c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap).comp ↑conjCLE

Proof state:
case intro.intro.intro
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
⊢ (∃ map, restrictScalars ℝ map = c • li.toContinuousLinearMap) ∨
    ∃ map, restrictScalars ℝ map = (c • li.toContinuousLinearMap).comp ↑conjCLE

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

Result:
case intro.intro.intro.intro
c : ℝ
li : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ (∃ map, restrictScalars ℝ map = c • li.toLinearIsometry.toContinuousLinearMap) ∨
    ∃ map, restrictScalars ℝ map = (c • li.toLinearIsometry.toContinuousLinearMap).comp ↑conjCLE

Proof state:
case intro.intro.intro.intro.intro.inr.h
c : ℝ
a : Circle
x✝ : ℂ
⊢ (restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ)) x✝ =
    ((c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap).comp ↑conjCLE) x✝

Tactic:
simp

Result:
no goals

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

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

Result:
case intro.intro.intro
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
⊢ (∃ map, restrictScalars ℝ map = c • li.toContinuousLinearMap) ∨
    ∃ map, restrictScalars ℝ map = (c • li.toContinuousLinearMap).comp ↑conjCLE

Proof state:
case intro.intro.intro.intro.intro.inr
c : ℝ
a : Circle
⊢ restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ) =
    (c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap).comp ↑conjCLE

Tactic:
ext1

Result:
case intro.intro.intro.intro.intro.inr.h
c : ℝ
a : Circle
x✝ : ℂ
⊢ (restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ)) x✝ =
    ((c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap).comp ↑conjCLE) x✝

Proof state:
case intro.intro.intro.intro.intro.inl
c : ℝ
a : Circle
⊢ (∃ map, restrictScalars ℝ map = c • (rotation a).toLinearIsometry.toContinuousLinearMap) ∨
    ∃ map, restrictScalars ℝ map = (c • (rotation a).toLinearIsometry.toContinuousLinearMap).comp ↑conjCLE

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

Result:
case intro.intro.intro.intro.intro.inl
c : ℝ
a : Circle
⊢ restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ) = c • (rotation a).toLinearIsometry.toContinuousLinearMap

Proof state:
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
⊢ (li.toLinearIsometryEquiv ⋯).toLinearIsometry = li

Tactic:
ext1

Result:
case h
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
x✝ : ℂ
⊢ (li.toLinearIsometryEquiv ⋯).toLinearIsometry x✝ = li x✝

Proof state:
case intro.intro.intro.intro.intro.inr
c : ℝ
a : Circle
⊢ (∃ map, restrictScalars ℝ map = c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap) ∨
    ∃ map,
      restrictScalars ℝ map = (c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap).comp ↑conjCLE

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

Result:
case intro.intro.intro.intro.intro.inr
c : ℝ
a : Circle
⊢ restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ) =
    (c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap).comp ↑conjCLE

Proof state:
case h
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
x✝ : ℂ
⊢ (li.toLinearIsometryEquiv ⋯).toLinearIsometry x✝ = li x✝

Tactic:
rfl

Result:
no goals