[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ K = RingHom.fieldRange ofReal ∨ K = ⊤
[PROOFSTEP]
suffices range (ofReal' : ℝ → ℂ) ⊆ K
  by
  rw [range_subset_iff, ← coe_algebraMap] at this 
  have :=
    (Subalgebra.isSimpleOrder_of_finrank finrank_real_complex).eq_bot_or_eq_top
      (Subfield.toIntermediateField K this).toSubalgebra
  simp_rw [← SetLike.coe_set_eq] at this ⊢
  convert this using 2
  simp only [RingHom.coe_fieldRange, Algebra.coe_bot, coe_algebraMap]
  rfl
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ ↑K
⊢ K = RingHom.fieldRange ofReal ∨ K = ⊤
[PROOFSTEP]
rw [range_subset_iff, ← coe_algebraMap] at this 
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
this : ∀ (y : ℝ), ↑(algebraMap ℝ ℂ) y ∈ ↑K
⊢ K = RingHom.fieldRange ofReal ∨ K = ⊤
[PROOFSTEP]
have :=
  (Subalgebra.isSimpleOrder_of_finrank finrank_real_complex).eq_bot_or_eq_top
    (Subfield.toIntermediateField K this).toSubalgebra
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
this✝ : ∀ (y : ℝ), ↑(algebraMap ℝ ℂ) y ∈ ↑K
this : (Subfield.toIntermediateField K this✝).toSubalgebra = ⊥ ∨ (Subfield.toIntermediateField K this✝).toSubalgebra = ⊤
⊢ K = RingHom.fieldRange ofReal ∨ K = ⊤
[PROOFSTEP]
simp_rw [← SetLike.coe_set_eq] at this ⊢
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
this✝ : ∀ (y : ℝ), ↑(algebraMap ℝ ℂ) y ∈ ↑K
this :
  ↑(Subfield.toIntermediateField K this✝).toSubalgebra = ↑⊥ ∨ ↑(Subfield.toIntermediateField K this✝).toSubalgebra = ↑⊤
⊢ ↑K = ↑(RingHom.fieldRange ofReal) ∨ ↑K = ↑⊤
[PROOFSTEP]
convert this using 2
[GOAL]
case h.e'_1.h.e'_3
K : Subfield ℂ
hc : IsClosed ↑K
this✝ : ∀ (y : ℝ), ↑(algebraMap ℝ ℂ) y ∈ ↑K
this :
  ↑(Subfield.toIntermediateField K this✝).toSubalgebra = ↑⊥ ∨ ↑(Subfield.toIntermediateField K this✝).toSubalgebra = ↑⊤
⊢ ↑(RingHom.fieldRange ofReal) = ↑⊥
[PROOFSTEP]
simp only [RingHom.coe_fieldRange, Algebra.coe_bot, coe_algebraMap]
[GOAL]
case h.e'_1.h.e'_3
K : Subfield ℂ
hc : IsClosed ↑K
this✝ : ∀ (y : ℝ), ↑(algebraMap ℝ ℂ) y ∈ ↑K
this :
  ↑(Subfield.toIntermediateField K this✝).toSubalgebra = ↑⊥ ∨ ↑(Subfield.toIntermediateField K this✝).toSubalgebra = ↑⊤
⊢ range ↑ofReal = range ofReal'
[PROOFSTEP]
rfl
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ ↑K
[PROOFSTEP]
suffices range (ofReal' : ℝ → ℂ) ⊆ closure (Set.range ((ofReal' : ℝ → ℂ) ∘ ((↑) : ℚ → ℝ)))
  by
  refine' subset_trans this _
  rw [← IsClosed.closure_eq hc]
  apply closure_mono
  rintro _ ⟨_, rfl⟩
  simp only [Function.comp_apply, ofReal_rat_cast, SetLike.mem_coe, SubfieldClass.coe_rat_mem]
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ range ofReal' ⊆ ↑K
[PROOFSTEP]
refine' subset_trans this _
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ closure (range (ofReal' ∘ Rat.cast)) ⊆ ↑K
[PROOFSTEP]
rw [← IsClosed.closure_eq hc]
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ closure (range (ofReal' ∘ Rat.cast)) ⊆ closure ↑K
[PROOFSTEP]
apply closure_mono
[GOAL]
case h
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ range (ofReal' ∘ Rat.cast) ⊆ ↑K
[PROOFSTEP]
rintro _ ⟨_, rfl⟩
[GOAL]
case h.intro
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
w✝ : ℚ
⊢ (ofReal' ∘ Rat.cast) w✝ ∈ ↑K
[PROOFSTEP]
simp only [Function.comp_apply, ofReal_rat_cast, SetLike.mem_coe, SubfieldClass.coe_rat_mem]
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
[PROOFSTEP]
nth_rw 1 [range_comp]
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ closure (ofReal' '' range Rat.cast)
[PROOFSTEP]
refine' subset_trans _ (image_closure_subset_closure_image continuous_ofReal)
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ ofReal' '' closure (range Rat.cast)
[PROOFSTEP]
rw [DenseRange.closure_range Rat.denseEmbedding_coe_real.dense]
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ ofReal' '' univ
[PROOFSTEP]
simp only [image_univ]
[GOAL]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ range ofReal'
[PROOFSTEP]
rfl
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
letI : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
letI : TopologicalRing K.topologicalClosure := Subring.instTopologicalRing K.topologicalClosure.toSubring
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
set ι : K → K.topologicalClosure := ⇑(Subfield.inclusion K.le_topologicalClosure)
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
have ui : UniformInducing ι :=
  ⟨by
    erw [uniformity_subtype, uniformity_subtype, Filter.comap_comap]
    congr⟩
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
⊢ Filter.comap (fun x => (ι x.fst, ι x.snd)) (uniformity { x // x ∈ Subfield.topologicalClosure K }) =
    uniformity { x // x ∈ K }
[PROOFSTEP]
erw [uniformity_subtype, uniformity_subtype, Filter.comap_comap]
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
⊢ Filter.comap ((fun q => (↑q.fst, ↑q.snd)) ∘ fun x => (ι x.fst, ι x.snd)) (uniformity ℂ) =
    Filter.comap (fun q => (↑q.fst, ↑q.snd)) (uniformity ℂ)
[PROOFSTEP]
congr
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
let di := ui.denseInducing (?_ : DenseRange ι)
[GOAL]
case refine_2
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
let extψ := DenseInducing.extendRingHom ui di.dense hc
[GOAL]
case refine_2
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
haveI hψ := (uniformContinuous_uniformly_extend ui di.dense hc).continuous
[GOAL]
case refine_2
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
cases' Complex.subfield_eq_of_closed (Subfield.isClosed_topologicalClosure K) with h h
[GOAL]
case refine_2.inl
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
left
[GOAL]
case refine_2.inl.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
⊢ ψ.toFun = ↑(Subfield.subtype K)
[PROOFSTEP]
let j := RingEquiv.subfieldCongr h
[GOAL]
case refine_2.inl.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
⊢ ψ.toFun = ↑(Subfield.subtype K)
[PROOFSTEP]
let ψ₁ :=
  RingHom.comp extψ
    (RingHom.comp j.symm.toRingHom ofReal.rangeRestrict)
      -- porting note: was `by continuity!` and was used inline
[GOAL]
case refine_2.inl.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
⊢ ψ.toFun = ↑(Subfield.subtype K)
[PROOFSTEP]
have hψ₁ : Continuous ψ₁ := by simpa only [RingHom.coe_comp] using hψ.comp ((continuous_algebraMap ℝ ℂ).subtype_mk _)
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
⊢ Continuous ↑ψ₁
[PROOFSTEP]
simpa only [RingHom.coe_comp] using hψ.comp ((continuous_algebraMap ℝ ℂ).subtype_mk _)
[GOAL]
case refine_2.inl.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
⊢ ψ.toFun = ↑(Subfield.subtype K)
[PROOFSTEP]
ext1 x
[GOAL]
case refine_2.inl.h.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
⊢ OneHom.toFun (↑↑ψ) x = ↑(Subfield.subtype K) x
[PROOFSTEP]
rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ofReal.rangeRestrict r = j (ι x)
[GOAL]
case refine_2.inl.h.h.intro
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
r : ℝ
hr : ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
⊢ OneHom.toFun (↑↑ψ) x = ↑(Subfield.subtype K) x
[PROOFSTEP]
have := RingHom.congr_fun (ringHom_eq_ofReal_of_continuous hψ₁) r
[GOAL]
case refine_2.inl.h.h.intro
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝¹ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this✝ : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
r : ℝ
hr : ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
this : ↑ψ₁ r = ↑ofReal r
⊢ OneHom.toFun (↑↑ψ) x = ↑(Subfield.subtype K) x
[PROOFSTEP]
rw [RingHom.comp_apply, RingHom.comp_apply, hr, RingEquiv.toRingHom_eq_coe] at this 
[GOAL]
case refine_2.inl.h.h.intro
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝¹ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this✝ : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
r : ℝ
hr : ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
this : ↑extψ (↑↑(RingEquiv.symm j) (↑j (ι x))) = ↑ofReal r
⊢ OneHom.toFun (↑↑ψ) x = ↑(Subfield.subtype K) x
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_2
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝¹ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this✝ : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
r : ℝ
hr : ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
this : ↑extψ (↑↑(RingEquiv.symm j) (↑j (ι x))) = ↑ofReal r
⊢ OneHom.toFun (↑↑ψ) x = ↑extψ (↑↑(RingEquiv.symm j) (↑j (ι x)))
[PROOFSTEP]
exact (DenseInducing.extend_eq di hc.continuous _).symm
[GOAL]
case h.e'_3
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝¹ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this✝ : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
r : ℝ
hr : ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
this : ↑extψ (↑↑(RingEquiv.symm j) (↑j (ι x))) = ↑ofReal r
⊢ ↑(Subfield.subtype K) x = ↑ofReal r
[PROOFSTEP]
rw [← ofReal.coe_rangeRestrict, hr]
[GOAL]
case h.e'_3
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝¹ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this✝ : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
r : ℝ
hr : ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
this : ↑extψ (↑↑(RingEquiv.symm j) (↑j (ι x))) = ↑ofReal r
⊢ ↑(Subfield.subtype K) x = ↑(↑j (ι x))
[PROOFSTEP]
rfl
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
⊢ ∃ r, ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
[PROOFSTEP]
obtain ⟨r, hr⟩ := SetLike.coe_mem (j (ι x))
[GOAL]
case intro
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = RingHom.fieldRange ofReal
j : { x // x ∈ Subfield.topologicalClosure K } ≃+* { x // x ∈ RingHom.fieldRange ofReal } := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := RingHom.comp extψ (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm j)) (RingHom.rangeRestrict ofReal))
hψ₁ : Continuous ↑ψ₁
x : { x // x ∈ K }
r : ℝ
hr : ↑ofReal r = ↑(↑j (ι x))
⊢ ∃ r, ↑(RingHom.rangeRestrict ofReal) r = ↑j (ι x)
[PROOFSTEP]
exact ⟨r, Subtype.ext hr⟩
[GOAL]
case refine_2.inr
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = ⊤
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
let ψ₁ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.subfieldCongr h).symm.toRingHom (@Subfield.topEquiv ℂ _).symm.toRingHom)
      -- porting note: was `by continuity!` and was used inline
[GOAL]
case refine_2.inr
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
have hψ₁ : Continuous ψ₁ := by simpa only [RingHom.coe_comp] using hψ.comp (continuous_id.subtype_mk _)
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
⊢ Continuous ↑ψ₁
[PROOFSTEP]
simpa only [RingHom.coe_comp] using hψ.comp (continuous_id.subtype_mk _)
[GOAL]
case refine_2.inr
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
cases' ringHom_eq_id_or_conj_of_continuous hψ₁ with h h
[GOAL]
case refine_2.inr.inl
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = RingHom.id ℂ
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
left
[GOAL]
case refine_2.inr.inl.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = RingHom.id ℂ
⊢ ψ.toFun = ↑(Subfield.subtype K)
[PROOFSTEP]
ext1 z
[GOAL]
case refine_2.inr.inl.h.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = RingHom.id ℂ
z : { x // x ∈ K }
⊢ OneHom.toFun (↑↑ψ) z = ↑(Subfield.subtype K) z
[PROOFSTEP]
convert RingHom.congr_fun h z using 1
[GOAL]
case h.e'_2
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = RingHom.id ℂ
z : { x // x ∈ K }
⊢ OneHom.toFun (↑↑ψ) z = ↑ψ₁ ↑z
[PROOFSTEP]
exact (DenseInducing.extend_eq di hc.continuous z).symm
[GOAL]
case refine_2.inr.inr
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = starRingEnd ℂ
⊢ ψ.toFun = ↑(Subfield.subtype K) ∨ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
right
[GOAL]
case refine_2.inr.inr.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = starRingEnd ℂ
⊢ ψ.toFun = ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)
[PROOFSTEP]
ext1 z
[GOAL]
case refine_2.inr.inr.h.h
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = starRingEnd ℂ
z : { x // x ∈ K }
⊢ OneHom.toFun (↑↑ψ) z = (↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype K)) z
[PROOFSTEP]
convert RingHom.congr_fun h z using 1
[GOAL]
case h.e'_2
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
di : DenseInducing ι := UniformInducing.denseInducing ui ?refine_1
extψ : { x // x ∈ Subfield.topologicalClosure K } →+* ℂ := DenseInducing.extendRingHom ui (_ : DenseRange ι) hc
hψ : Continuous (DenseInducing.extend (_ : DenseInducing ι) ↑ψ)
h✝ : Subfield.topologicalClosure K = ⊤
ψ₁ : ℂ →+* ℂ :=
  RingHom.comp extψ
    (RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (RingEquiv.subfieldCongr h✝)))
      (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous ↑ψ₁
h : ψ₁ = starRingEnd ℂ
z : { x // x ∈ K }
⊢ OneHom.toFun (↑↑ψ) z = ↑ψ₁ ↑z
[PROOFSTEP]
exact (DenseInducing.extend_eq di hc.continuous z).symm
[GOAL]
case refine_1
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
⊢ DenseRange ι
[PROOFSTEP]
let j : { x // x ∈ closure (id '' {x | (K : Set ℂ) x}) } → (K.topologicalClosure : Set ℂ) := fun x =>
  ⟨x, by
    convert x.prop
    simp only [id.def, Set.image_id']
    rfl⟩
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
x : { x // x ∈ closure (id '' {x | ↑K x}) }
⊢ ↑x ∈ ↑(Subfield.topologicalClosure K)
[PROOFSTEP]
convert x.prop
[GOAL]
case h.e'_5
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
x : { x // x ∈ closure (id '' {x | ↑K x}) }
⊢ ↑(Subfield.topologicalClosure K) = closure (id '' {x | ↑K x})
[PROOFSTEP]
simp only [id.def, Set.image_id']
[GOAL]
case h.e'_5
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
x : { x // x ∈ closure (id '' {x | ↑K x}) }
⊢ ↑(Subfield.topologicalClosure K) = closure {x | ↑K x}
[PROOFSTEP]
rfl
[GOAL]
case refine_1
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
j : { x // x ∈ closure (id '' {x | ↑K x}) } → ↑↑(Subfield.topologicalClosure K) :=
  fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(Subfield.topologicalClosure K)) }
⊢ DenseRange ι
[PROOFSTEP]
convert
  DenseRange.comp (Function.Surjective.denseRange _) (DenseEmbedding.subtype denseEmbedding_id (K : Set ℂ)).dense
    (by continuity : Continuous j)
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
j : { x // x ∈ closure (id '' {x | ↑K x}) } → ↑↑(Subfield.topologicalClosure K) :=
  fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(Subfield.topologicalClosure K)) }
⊢ Continuous j
[PROOFSTEP]
continuity
[GOAL]
case refine_1
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
j : { x // x ∈ closure (id '' {x | ↑K x}) } → ↑↑(Subfield.topologicalClosure K) :=
  fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(Subfield.topologicalClosure K)) }
⊢ Function.Surjective j
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case refine_1.mk
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
j : { x // x ∈ closure (id '' {x | ↑K x}) } → ↑↑(Subfield.topologicalClosure K) :=
  fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(Subfield.topologicalClosure K)) }
y : ℂ
hy : y ∈ ↑(Subfield.topologicalClosure K)
⊢ ∃ a, j a = { val := y, property := hy }
[PROOFSTEP]
use⟨y, by
    convert hy
    simp only [id.def, Set.image_id']
    rfl⟩
[GOAL]
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
j : { x // x ∈ closure (id '' {x | ↑K x}) } → ↑↑(Subfield.topologicalClosure K) :=
  fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(Subfield.topologicalClosure K)) }
y : ℂ
hy : y ∈ ↑(Subfield.topologicalClosure K)
⊢ y ∈ closure (id '' {x | ↑K x})
[PROOFSTEP]
convert hy
[GOAL]
case h.e'_5
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
j : { x // x ∈ closure (id '' {x | ↑K x}) } → ↑↑(Subfield.topologicalClosure K) :=
  fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(Subfield.topologicalClosure K)) }
y : ℂ
hy : y ∈ ↑(Subfield.topologicalClosure K)
⊢ closure (id '' {x | ↑K x}) = ↑(Subfield.topologicalClosure K)
[PROOFSTEP]
simp only [id.def, Set.image_id']
[GOAL]
case h.e'_5
K : Subfield ℂ
ψ : { x // x ∈ K } →+* ℂ
hc : UniformContinuous ↑ψ
this✝ : TopologicalDivisionRing ℂ := TopologicalDivisionRing.mk
this : TopologicalRing { x // x ∈ Subfield.topologicalClosure K } :=
  Subring.instTopologicalRing (Subfield.topologicalClosure K).toSubring
ι : { x // x ∈ K } → { x // x ∈ Subfield.topologicalClosure K } :=
  ↑(Subfield.inclusion (_ : K ≤ Subfield.topologicalClosure K))
ui : UniformInducing ι
j : { x // x ∈ closure (id '' {x | ↑K x}) } → ↑↑(Subfield.topologicalClosure K) :=
  fun x => { val := ↑x, property := (_ : ↑x ∈ ↑(Subfield.topologicalClosure K)) }
y : ℂ
hy : y ∈ ↑(Subfield.topologicalClosure K)
⊢ closure {x | ↑K x} = ↑(Subfield.topologicalClosure K)
[PROOFSTEP]
rfl
