-- Mathlib/Topology/Instances/Complex.lean
theorem Complex.subfield_eq_of_closed {K : Subfield ℂ} (hc : IsClosed (K : Set ℂ)) :
    K = ofRealHom.fieldRange ∨ K = ⊤

Proof state:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ ofReal '' closure (range Rat.cast)

Tactic:
rw [DenseRange.closure_range Rat.isDenseEmbedding_coe_real.dense]

Result:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ ofReal '' univ

Proof state:
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
⊢ closure (range (ofReal ∘ Rat.cast)) ⊆ ↑K

Tactic:
rw [← IsClosed.closure_eq hc]

Result:
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
⊢ closure (range (ofReal ∘ Rat.cast)) ⊆ closure ↑K

Proof state:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))

Tactic:
nth_rw 1 [range_comp]

Result:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ closure (ofReal '' range Rat.cast)

Proof state:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ K = ofRealHom.fieldRange ∨ K = ⊤

Tactic:
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, IntermediateField.coe_toSubalgebra] at this ⊢
  exact this

Result:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ ↑K

Proof state:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ closure (ofReal '' range Rat.cast)

Tactic:
refine subset_trans ?_ (image_closure_subset_closure_image continuous_ofReal)

Result:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ ofReal '' closure (range Rat.cast)

Proof state:
case h
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
⊢ range (ofReal ∘ Rat.cast) ⊆ ↑K

Tactic:
rintro _ ⟨_, rfl⟩

Result:
case h.intro
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
w✝ : ℚ
⊢ (ofReal ∘ Rat.cast) w✝ ∈ ↑K

Proof state:
K : Subfield ℂ
hc : IsClosed ↑K
this✝ : ∀ (y : ℝ), (algebraMap ℝ ℂ) y ∈ ↑K
this : ↑(K.toIntermediateField this✝) = ↑⊥ ∨ ↑(K.toIntermediateField this✝) = ↑⊤
⊢ ↑K = ↑ofRealHom.fieldRange ∨ ↑K = ↑⊤

Tactic:
exact this

Result:
no goals

Proof state:
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal ⊆ ↑K
⊢ K = ofRealHom.fieldRange ∨ K = ⊤

Tactic:
rw [range_subset_iff, ← coe_algebraMap] at this

Result:
K : Subfield ℂ
hc : IsClosed ↑K
this : ∀ (y : ℝ), (algebraMap ℝ ℂ) y ∈ ↑K
⊢ K = ofRealHom.fieldRange ∨ K = ⊤

Proof state:
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
⊢ range ofReal ⊆ ↑K

Tactic:
refine subset_trans this ?_

Result:
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
⊢ closure (range (ofReal ∘ Rat.cast)) ⊆ ↑K

Proof state:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ ↑K

Tactic:
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_ratCast, SetLike.mem_coe, SubfieldClass.ratCast_mem]

Result:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))

Proof state:
case h.intro
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
w✝ : ℚ
⊢ (ofReal ∘ Rat.cast) w✝ ∈ ↑K

Tactic:
simp only [Function.comp_apply, ofReal_ratCast, SetLike.mem_coe, SubfieldClass.ratCast_mem]

Result:
no goals

Proof state:
K : Subfield ℂ
hc : IsClosed ↑K
this✝ : ∀ (y : ℝ), (algebraMap ℝ ℂ) y ∈ ↑K
this : (K.toIntermediateField this✝).toSubalgebra = ⊥ ∨ (K.toIntermediateField this✝).toSubalgebra = ⊤
⊢ K = ofRealHom.fieldRange ∨ K = ⊤

Tactic:
simp_rw [← SetLike.coe_set_eq, IntermediateField.coe_toSubalgebra] at this ⊢

Result:
K : Subfield ℂ
hc : IsClosed ↑K
this✝ : ∀ (y : ℝ), (algebraMap ℝ ℂ) y ∈ ↑K
this : ↑(K.toIntermediateField this✝) = ↑⊥ ∨ ↑(K.toIntermediateField this✝) = ↑⊤
⊢ ↑K = ↑ofRealHom.fieldRange ∨ ↑K = ↑⊤

Proof state:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ ofReal '' univ

Tactic:
simp only [image_univ]

Result:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ range ofReal

Proof state:
K : Subfield ℂ
hc : IsClosed ↑K
⊢ range ofReal ⊆ range ofReal

Tactic:
rfl

Result:
no goals

Proof state:
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
⊢ closure (range (ofReal ∘ Rat.cast)) ⊆ closure ↑K

Tactic:
apply closure_mono

Result:
case h
K : Subfield ℂ
hc : IsClosed ↑K
this : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
⊢ range (ofReal ∘ Rat.cast) ⊆ ↑K

Proof state:
K : Subfield ℂ
hc : IsClosed ↑K
this : ∀ (y : ℝ), (algebraMap ℝ ℂ) y ∈ ↑K
⊢ K = ofRealHom.fieldRange ∨ K = ⊤

Tactic:
have :=
  (Subalgebra.isSimpleOrder_of_finrank finrank_real_complex).eq_bot_or_eq_top
    (Subfield.toIntermediateField K this).toSubalgebra

Result:
K : Subfield ℂ
hc : IsClosed ↑K
this✝ : ∀ (y : ℝ), (algebraMap ℝ ℂ) y ∈ ↑K
this : (K.toIntermediateField this✝).toSubalgebra = ⊥ ∨ (K.toIntermediateField this✝).toSubalgebra = ⊤
⊢ K = ofRealHom.fieldRange ∨ K = ⊤