case intro.intro.intro
f : ℂ → ℂ
z : ℂ
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
⊢ (∃ map, restrictScalars ℝ map = c • LinearIsometry.toContinuousLinearMap li) ∨
    ∃ map, restrictScalars ℝ map = ContinuousLinearMap.comp (c • LinearIsometry.toContinuousLinearMap li) ↑conjCle
f : ℂ → ℂ
z : ℂ
g : ℂ →L[ℝ] ℂ
h : IsConformalMap g
⊢ (∃ map, restrictScalars ℝ map = g) ∨ ∃ map, restrictScalars ℝ map = ContinuousLinearMap.comp g ↑conjCle
rcases h with ⟨c, -, li, rfl⟩
case intro.intro.intro.intro
f : ℂ → ℂ
z : ℂ
c : ℝ
li : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ (∃ map, restrictScalars ℝ map = c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry li)) ∨
    ∃ map,
      restrictScalars ℝ map =
        ContinuousLinearMap.comp (c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry li))
          ↑conjCle
case intro.intro.intro
f : ℂ → ℂ
z : ℂ
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
⊢ (∃ map, restrictScalars ℝ map = c • LinearIsometry.toContinuousLinearMap li) ∨
    ∃ map, restrictScalars ℝ map = ContinuousLinearMap.comp (c • LinearIsometry.toContinuousLinearMap li) ↑conjCle
obtain ⟨li, rfl⟩ : ∃ li' : ℂ ≃ₗᵢ[ℝ] ℂ, li'.toLinearIsometry = li :=
  ⟨li.toLinearIsometryEquiv rfl, by ext1; rfl⟩
case intro.intro.intro.intro.intro.inl
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
⊢ (∃ map,
      restrictScalars ℝ map =
        c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry (↑rotation a))) ∨
    ∃ map,
      restrictScalars ℝ map =
        ContinuousLinearMap.comp
          (c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry (↑rotation a))) ↑conjCle

case intro.intro.intro.intro.intro.inr
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
⊢ (∃ map,
      restrictScalars ℝ map =
        c •
          LinearIsometry.toContinuousLinearMap
            (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.trans conjLie (↑rotation a)))) ∨
    ∃ map,
      restrictScalars ℝ map =
        ContinuousLinearMap.comp
          (c •
            LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.trans conjLie (↑rotation a))))
          ↑conjCle
case intro.intro.intro.intro
f : ℂ → ℂ
z : ℂ
c : ℝ
li : ℂ ≃ₗᵢ[ℝ] ℂ
⊢ (∃ map, restrictScalars ℝ map = c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry li)) ∨
    ∃ map,
      restrictScalars ℝ map =
        ContinuousLinearMap.comp (c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry li))
          ↑conjCle
rcases linear_isometry_complex li with ⟨a, rfl | rfl⟩
case h
f : ℂ → ℂ
z : ℂ
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
x✝ : ℂ
⊢ ↑(LinearIsometryEquiv.toLinearIsometry
          (LinearIsometry.toLinearIsometryEquiv li (_ : FiniteDimensional.finrank ℝ ℂ = FiniteDimensional.finrank ℝ ℂ)))
      x✝ =
    ↑li x✝
f : ℂ → ℂ
z : ℂ
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
⊢ LinearIsometryEquiv.toLinearIsometry
      (LinearIsometry.toLinearIsometryEquiv li (_ : FiniteDimensional.finrank ℝ ℂ = FiniteDimensional.finrank ℝ ℂ)) =
    li
ext1
no goals
case h
f : ℂ → ℂ
z : ℂ
c : ℝ
li : ℂ →ₗᵢ[ℝ] ℂ
x✝ : ℂ
⊢ ↑(LinearIsometryEquiv.toLinearIsometry
          (LinearIsometry.toLinearIsometryEquiv li (_ : FiniteDimensional.finrank ℝ ℂ = FiniteDimensional.finrank ℝ ℂ)))
      x✝ =
    ↑li x✝
rfl
case intro.intro.intro.intro.intro.inl
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
⊢ restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ) =
    c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry (↑rotation a))
case intro.intro.intro.intro.intro.inl
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
⊢ (∃ map,
      restrictScalars ℝ map =
        c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry (↑rotation a))) ∨
    ∃ map,
      restrictScalars ℝ map =
        ContinuousLinearMap.comp
          (c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry (↑rotation a))) ↑conjCle
refine' Or.inl ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, _⟩
case intro.intro.intro.intro.intro.inl.h
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
x✝ : ℂ
⊢ ↑(restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ)) x✝ =
    ↑(c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry (↑rotation a))) x✝
case intro.intro.intro.intro.intro.inl
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
⊢ restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ) =
    c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry (↑rotation a))
ext1
no goals
case intro.intro.intro.intro.intro.inl.h
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
x✝ : ℂ
⊢ ↑(restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ)) x✝ =
    ↑(c • LinearIsometry.toContinuousLinearMap (LinearIsometryEquiv.toLinearIsometry (↑rotation a))) x✝
rw [coe_restrictScalars', smul_apply, smul_apply, smul_apply,
  LinearIsometry.coe_toContinuousLinearMap,
  LinearIsometryEquiv.coe_toLinearIsometry, rotation_apply, id_apply, smul_eq_mul]
case intro.intro.intro.intro.intro.inr
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
⊢ restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ) =
    ContinuousLinearMap.comp
      (c •
        LinearIsometry.toContinuousLinearMap
          (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.trans conjLie (↑rotation a))))
      ↑conjCle
case intro.intro.intro.intro.intro.inr
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
⊢ (∃ map,
      restrictScalars ℝ map =
        c •
          LinearIsometry.toContinuousLinearMap
            (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.trans conjLie (↑rotation a)))) ∨
    ∃ map,
      restrictScalars ℝ map =
        ContinuousLinearMap.comp
          (c •
            LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.trans conjLie (↑rotation a))))
          ↑conjCle
refine' Or.inr ⟨c • (a : ℂ) • ContinuousLinearMap.id ℂ ℂ, _⟩
case intro.intro.intro.intro.intro.inr.h
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
x✝ : ℂ
⊢ ↑(restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ)) x✝ =
    ↑(ContinuousLinearMap.comp
          (c •
            LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.trans conjLie (↑rotation a))))
          ↑conjCle)
      x✝
case intro.intro.intro.intro.intro.inr
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
⊢ restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ) =
    ContinuousLinearMap.comp
      (c •
        LinearIsometry.toContinuousLinearMap
          (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.trans conjLie (↑rotation a))))
      ↑conjCle
ext1
no goals
case intro.intro.intro.intro.intro.inr.h
f : ℂ → ℂ
z : ℂ
c : ℝ
a : { x // x ∈ circle }
x✝ : ℂ
⊢ ↑(restrictScalars ℝ (c • ↑a • ContinuousLinearMap.id ℂ ℂ)) x✝ =
    ↑(ContinuousLinearMap.comp
          (c •
            LinearIsometry.toContinuousLinearMap
              (LinearIsometryEquiv.toLinearIsometry (LinearIsometryEquiv.trans conjLie (↑rotation a))))
          ↑conjCle)
      x✝
rw [coe_restrictScalars', smul_apply, smul_apply, comp_apply, smul_apply,
  LinearIsometry.coe_toContinuousLinearMap, LinearIsometryEquiv.coe_toLinearIsometry,
  LinearIsometryEquiv.trans_apply, rotation_apply, id_apply, smul_eq_mul,
  ContinuousLinearEquiv.coe_coe, conjCle_apply, conjLie_apply, conj_conj]