K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ ↑K
K : Subfield ℂ
hc : IsClosed ↑K
⊢ K = RingHom.fieldRange ofReal ∨ K = ⊤
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
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ ↑K
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]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ closure (ofReal' '' range Rat.cast)
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
nth_rw 1 [range_comp]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ ofReal' '' closure (range Rat.cast)
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ closure (ofReal' '' range Rat.cast)
refine' subset_trans _ (image_closure_subset_closure_image continuous_ofReal)
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ ofReal' '' univ
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ ofReal' '' closure (range Rat.cast)
rw [DenseRange.closure_range Rat.denseEmbedding_coe_real.dense]
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ range ofReal'
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ ofReal' '' univ
simp only [image_univ]
no goals
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal' ⊆ range ofReal'
rfl
K : Subfield ℂ
hc : IsClosed ↑K
this : ∀ (y : ℝ), ↑(algebraMap ℝ ℂ) y ∈ ↑K
⊢ K = RingHom.fieldRange ofReal ∨ K = ⊤
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ ↑K
⊢ K = RingHom.fieldRange ofReal ∨ K = ⊤
rw [range_subset_iff, ← coe_algebraMap] at this
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 = ⊤
K : Subfield ℂ
hc : IsClosed ↑K
this : ∀ (y : ℝ), ↑(algebraMap ℝ ℂ) y ∈ ↑K
⊢ K = RingHom.fieldRange ofReal ∨ K = ⊤
have :=
  (Subalgebra.isSimpleOrder_of_finrank finrank_real_complex).eq_bot_or_eq_top
    (Subfield.toIntermediateField K this).toSubalgebra
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 = ↑⊤
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 = ⊤
simp_rw [← SetLike.coe_set_eq] at this⊢
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) = ↑⊥
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 = ↑⊤
convert this using 2
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'
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) = ↑⊥
simp only [RingHom.coe_fieldRange, Algebra.coe_bot, coe_algebraMap]
no goals
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'
rfl
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ closure (range (ofReal' ∘ Rat.cast)) ⊆ ↑K
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ range ofReal' ⊆ ↑K
refine' subset_trans this _
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ closure (range (ofReal' ∘ Rat.cast)) ⊆ closure ↑K
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ closure (range (ofReal' ∘ Rat.cast)) ⊆ ↑K
rw [← IsClosed.closure_eq hc]
case h
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ range (ofReal' ∘ Rat.cast) ⊆ ↑K
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ closure (range (ofReal' ∘ Rat.cast)) ⊆ closure ↑K
apply closure_mono
case h.intro
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
w✝ : ℚ
⊢ (ofReal' ∘ Rat.cast) w✝ ∈ ↑K
case h
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
⊢ range (ofReal' ∘ Rat.cast) ⊆ ↑K
rintro _ ⟨_, rfl⟩
no goals
case h.intro
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal' ⊆ closure (range (ofReal' ∘ Rat.cast))
w✝ : ℚ
⊢ (ofReal' ∘ Rat.cast) w✝ ∈ ↑K
simp only [Function.comp_apply, ofReal_rat_cast, SetLike.mem_coe, SubfieldClass.coe_rat_mem]