awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun (x_1 : ℕ) ↦ x) Filter.atTop (nhds x)

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun (x_1 : ℕ) ↦ x) Filter.atTop (nhds x)

Tactic:
exact tendsto_const_nhds

Premises used: tendsto_const_nhds
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
hx : x ∈ cantorSet
⊢ LE.le (α := ℕ → ℝ) (fun (n : ℕ) ↦ x - HPow.hPow (α := ℝ) 3⁻¹ n) fun (n : ℕ) ↦
    ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i

Tactic:
fun _ ↦ le_ofDigits_cantorToTernary_sum hx

Premises used: cantorToTernary, le_ofDigits_cantorToTernary_sum, Stream'.get, Stream'.map
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
hx : x ∈ cantorSet
⊢ LE.le (α := ℕ → ℝ) (fun (n : ℕ) ↦ x - HPow.hPow (α := ℝ) 3⁻¹ n) fun (n : ℕ) ↦
    ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i

Tactic:
exact fun _ ↦ le_ofDigits_cantorToTernary_sum hx

Premises used: le_ofDigits_cantorToTernary_sum
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
hx : x ∈ cantorSet
⊢ LE.le (α := ℕ → ℝ) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) fun (x_1 : ℕ) ↦ x

Tactic:
fun _ ↦ ofDigits_cantorToTernary_sum_le hx

Premises used: cantorToTernary, ofDigits_cantorToTernary_sum_le, Stream'.get, Stream'.map
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
hx : x ∈ cantorSet
⊢ LE.le (α := ℕ → ℝ) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) fun (x_1 : ℕ) ↦ x

Tactic:
exact fun _ ↦ ofDigits_cantorToTernary_sum_le hx

Premises used: ofDigits_cantorToTernary_sum_le
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
h :
  ∀ (x : ℝ),
    x ∈ cantorSet ↔ Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (a : ℕ → Fin 3), (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x} x
⊢ cantorSet = {x : ℝ | ∃ (a : ℕ → Fin 3), (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x}

Tactic:
ext x
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
⊢ x ∈ cantorSet ↔ Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (a : ℕ → Fin 3), (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x} x

Tactic:
⟨fun h ↦ ?_, fun ⟨a, ha⟩ ↦ ?_⟩

Premises used: Membership.mem, _private.0.cantorSet_eq_zero_two_ofDigits.match_1, cantorSet, Iff.intro
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
h :
  ∀ (h : x ∈ cantorSet),
    Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (a : ℕ → Fin 3), (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x} x
h₁ :
  Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (a : ℕ → Fin 3), (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x} x →
    ∀ (a : ℕ → Fin 3) (ha : (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x), x ∈ cantorSet
⊢ x ∈ cantorSet ↔ Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (a : ℕ → Fin 3), (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x} x

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨a, ha⟩ ↦ ?_⟩
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
h : x ∈ cantorSet
h₁ : (∀ (i : ℕ), cantorToTernary x i ≠ 1) ∧ ofDigits (cantorToTernary x) = x
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (a : ℕ → Fin 3), (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x} x

Tactic:
use cantorToTernary x

Premises used: cantorToTernary
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
h : x ∈ cantorSet
⊢ (∀ (i : ℕ), cantorToTernary x i ≠ 1) ∧ ofDigits (cantorToTernary x) = x

Tactic:
⟨fun _ ↦ cantorToTernary_ne_one, ofDigits_cantorToTernary h⟩

Premises used: ofDigits_cantorToTernary, cantorToTernary_ne_one, And.intro
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
h : x ∈ cantorSet
⊢ (∀ (i : ℕ), cantorToTernary x i ≠ 1) ∧ ofDigits (cantorToTernary x) = x

Tactic:
exact ⟨fun _ ↦ cantorToTernary_ne_one, ofDigits_cantorToTernary h⟩
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
h_1 : Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (a : ℕ → Fin 3), (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x} x
a : ℕ → Fin 3
ha : (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x
h : ofDigits a ∈ cantorSet
⊢ x ∈ cantorSet

Tactic:
rw [← ha.right]

Premises used: And.right
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (a : ℕ → Fin 3), (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x} x
a : ℕ → Fin 3
ha : (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x
⊢ ofDigits a ∈ cantorSet

Tactic:
ofDigits_zero_two_sequence_mem_cantorSet ha.left

Premises used: ofDigits_zero_two_sequence_mem_cantorSet, And.left
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
h : Membership.mem (γ := Set ℝ) {x : ℝ | ∃ (a : ℕ → Fin 3), (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x} x
a : ℕ → Fin 3
ha : (∀ (i : ℕ), a i ≠ 1) ∧ ofDigits a = x
⊢ ofDigits a ∈ cantorSet

Tactic:
exact ofDigits_zero_two_sequence_mem_cantorSet ha.left

Premises used: ofDigits_zero_two_sequence_mem_cantorSet, And.left
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
hx : x ∈ cantorSet
simp : (ofDigits (b := 3) fun (i : ℕ) ↦ bif (cantorToBinary x).get i then 2 else 0) = x
⊢ (fun (y : ℕ → Bool) ↦
        Subtype.mk (p := fun (x : ℝ) ↦ x ∈ cantorSet) (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0) ⋯)
      ((fun (x : (↑cantorSet : Type)) ↦
          (match (motive := (↑cantorSet : Type) → ℕ → Bool) x with
            | ⟨x, h⟩ => (cantorToBinary x).get :
            ℕ → Bool))
        (Subtype.mk (p := fun (x : ℝ) ↦ x ∈ cantorSet) x hx)) =
    Subtype.mk (p := fun (x : ℝ) ↦ x ∈ cantorSet) x hx

Tactic:
simp only [Fin.isValue, Subtype.mk.injEq]

Premises used: Fin.isValue, Subtype.mk.injEq
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
hx : x ∈ cantorSet
⊢ (ofDigits (b := 3) fun (i : ℕ) ↦ bif (cantorToBinary x).get i then 2 else 0) = x

Tactic:
ofDigits_cantorToTernary hx

Premises used: ofDigits_cantorToTernary, cantorToTernary, Stream'.get, Stream'.map
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
x : ℝ
hx : x ∈ cantorSet
⊢ (ofDigits (b := 3) fun (i : ℕ) ↦ bif (cantorToBinary x).get i then 2 else 0) = x

Tactic:
exact ofDigits_cantorToTernary hx

Premises used: ofDigits_cantorToTernary
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
y : ℕ → Bool
set :
  let x := ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0;
  (cantorToBinary x).get = y
⊢ (cantorToBinary (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0)).get = y

Tactic:
set x := @ofDigits 3 (fun i ↦ cond (y i) 2 0)

Premises used: cond, Real.ofDigits, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
y : ℕ → Bool
x : ℝ := ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0
⊢ ofDigits (cantorToTernary (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0)).get =
    ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0

Tactic:
have := ofDigits_cantorToTernary (ofDigits_bool_to_fin_three_mem_cantorSet y)
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
y : ℕ → Bool
x : ℝ := ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0
this :
  ofDigits (cantorToTernary (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0)).get =
    ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0
apply :
  ∀
    (this :
      (cantorToTernary (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0)).get = fun (i : ℕ) ↦
        bif y i then 2 else 0),
    (cantorToBinary x).get = y
ha : ∀ (n : ℕ), (cantorToTernary (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0)).get n ≠ 1
hb : ∀ (n : ℕ), Ne (α := Fin 3) (bif y n then 2 else 0) 1
⊢ (cantorToBinary x).get = y

Tactic:
apply ofDigits_zero_two_sequence_unique at this

Premises used: ofDigits_zero_two_sequence_unique
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
y : ℕ → Bool
x : ℝ := ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0
this :
  ofDigits (cantorToTernary (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0)).get =
    ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0
⊢ ∀ (n : ℕ), (cantorToTernary (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0)).get n ≠ 1

Tactic:
fun n ↦ cantorToTernary_ne_one

Premises used: cantorToTernary_ne_one
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
y : ℕ → Bool
x : ℝ := ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0
this :
  ofDigits (cantorToTernary (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0)).get =
    ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0
⊢ ∀ (n : ℕ), (cantorToTernary (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0)).get n ≠ 1

Tactic:
exact fun n ↦ cantorToTernary_ne_one

Premises used: cantorToTernary_ne_one
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
y : ℕ → Bool
x : ℝ := ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0
this :
  ofDigits (cantorToTernary (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0)).get =
    ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0
⊢ ∀ (n : ℕ), Ne (α := Fin 3) (bif y n then 2 else 0) 1

Tactic:
grind
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
y : ℕ → Bool
x : ℝ := ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0
this :
  (cantorToTernary (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0)).get = fun (i : ℕ) ↦ bif y i then 2 else 0
h : ∀ (n : ℕ), (cantorToBinary x).get n = y n
⊢ (cantorToBinary x).get = y

Tactic:
ext n
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
y : ℕ → Bool
x : ℝ := ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0
this :
  (cantorToTernary (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0)).get = fun (i : ℕ) ↦ bif y i then 2 else 0
n : ℕ
⊢ (cantorToTernary (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0)).get n = bif y n then 2 else 0

Tactic:
apply congrFun (a := n) at this

Premises used: congrFun
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
y : ℕ → Bool
x : ℝ := ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0
n : ℕ
this : (cantorToTernary (ofDigits (b := 3) fun (i : ℕ) ↦ bif y i then 2 else 0)).get n = bif y n then 2 else 0
⊢ (cantorToBinary x).get n = y n

Tactic:
grind [cantorToTernary, Stream'.get_map]

Premises used: cantorToTernary, Stream'.get_map
-- Module: Mathlib.Topology.Instances.CantorSet
Goal:
⊢ Continuous (Y := ℕ → Fin 3) fun (x : ℕ → Bool) (i : ℕ) ↦ bif x i then 2 else 0

Tactic:
fun_prop
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
this : range ofReal ⊆ (↑K : Set ℂ)
⊢ ∀ (y : ℝ), Membership.mem (α := ℂ) (↑K : Set ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ)

Tactic:
rw [range_subset_iff, ← coe_algebraMap] at this

Premises used: Complex.coe_algebraMap, Set.range_subset_iff
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
this : ∀ (y : ℝ), Membership.mem (α := ℂ) (↑K : Set ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ)
⊢ (K.toIntermediateField this).toSubalgebra = ⊥ ∨ (K.toIntermediateField this).toSubalgebra = ⊤

Tactic:
have :=
      (Subalgebra.isSimpleOrder_of_finrank finrank_real_complex).eq_bot_or_eq_top
        (Subfield.toIntermediateField K this).toSubalgebra
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
this_1 : ∀ (y : ℝ), Membership.mem (α := ℂ) (↑K : Set ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ)
this : (K.toIntermediateField this_1).toSubalgebra = ⊥ ∨ (K.toIntermediateField this_1).toSubalgebra = ⊤
simp_rw :
  ∀
    (this :
      (↑(K.toIntermediateField this_1) : Set ℂ) = (↑⊥ : Set ℂ) ∨
        (↑(K.toIntermediateField this_1) : Set ℂ) = (↑⊤ : Set ℂ)),
    (↑K : Set ℂ) = (↑ofRealHom.fieldRange : Set ℂ) ∨ (↑K : Set ℂ) = (↑⊤ : Set ℂ)
⊢ K = ofRealHom.fieldRange ∨ K = ⊤

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

Premises used: IntermediateField.coe_toSubalgebra, SetLike.coe_set_eq
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
this_1 : ∀ (y : ℝ), Membership.mem (α := ℂ) (↑K : Set ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ)
this :
  (↑(K.toIntermediateField this_1) : Set ℂ) = (↑⊥ : Set ℂ) ∨ (↑(K.toIntermediateField this_1) : Set ℂ) = (↑⊤ : Set ℂ)
⊢ (↑K : Set ℂ) = (↑ofRealHom.fieldRange : Set ℂ) ∨ (↑K : Set ℂ) = (↑⊤ : Set ℂ)

Tactic:
this
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
this_1 : ∀ (y : ℝ), Membership.mem (α := ℂ) (↑K : Set ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) y : ℂ)
this :
  (↑(K.toIntermediateField this_1) : Set ℂ) = (↑⊥ : Set ℂ) ∨ (↑(K.toIntermediateField this_1) : Set ℂ) = (↑⊤ : Set ℂ)
⊢ (↑K : Set ℂ) = (↑ofRealHom.fieldRange : Set ℂ) ∨ (↑K : Set ℂ) = (↑⊤ : Set ℂ)

Tactic:
exact this
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
suffices : range ofReal ⊆ (↑K : Set ℂ)
⊢ 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
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
this : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
⊢ range ofReal ⊆ (↑K : Set ℂ)

Tactic:
subset_trans this ?_

Premises used: subset_trans
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
this : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
refine : closure (range (ofReal ∘ Rat.cast)) ⊆ (↑K : Set ℂ)
⊢ range ofReal ⊆ (↑K : Set ℂ)

Tactic:
refine subset_trans this ?_

Premises used: subset_trans
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
this : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
rw : closure (range (ofReal ∘ Rat.cast)) ⊆ closure (↑K : Set ℂ)
⊢ closure (range (ofReal ∘ Rat.cast)) ⊆ (↑K : Set ℂ)

Tactic:
rw [← IsClosed.closure_eq hc]

Premises used: IsClosed.closure_eq
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
this : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
h : range (ofReal ∘ Rat.cast) ⊆ (↑K : Set ℂ)
⊢ closure (range (ofReal ∘ Rat.cast)) ⊆ closure (↑K : Set ℂ)

Tactic:
apply closure_mono

Premises used: closure_mono
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
this : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
w : ℚ
⊢ (ofReal ∘ Rat.cast) w ∈ (↑K : Set ℂ)

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

Premises used: SubfieldClass.ratCast_mem, SetLike.mem_coe, Function.comp_apply, Complex.ofReal_ratCast
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
suffices : range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))
⊢ range ofReal ⊆ (↑K : Set ℂ)

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]
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
nth_rw : range ofReal ⊆ closure (ofReal '' range Rat.cast)
⊢ range ofReal ⊆ closure (range (ofReal ∘ Rat.cast))

Tactic:
nth_rw 1 [range_comp]

Premises used: Set.range_comp
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
⊢ range ofReal ⊆ closure (ofReal '' range Rat.cast)

Tactic:
subset_trans ?_ (image_closure_subset_closure_image continuous_ofReal)

Premises used: subset_trans, Complex.continuous_ofReal, image_closure_subset_closure_image
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
refine : range ofReal ⊆ ofReal '' closure (range Rat.cast)
⊢ range ofReal ⊆ closure (ofReal '' range Rat.cast)

Tactic:
refine subset_trans ?_ (image_closure_subset_closure_image continuous_ofReal)

Premises used: subset_trans, Complex.continuous_ofReal, image_closure_subset_closure_image
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
rw : range ofReal ⊆ ofReal '' univ
⊢ range ofReal ⊆ ofReal '' closure (range Rat.cast)

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

Premises used: IsDenseEmbedding.toIsDenseInducing, Rat.isDenseEmbedding_coe_real, DenseRange.closure_range, IsDenseInducing.dense
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
simp : range ofReal ⊆ range ofReal
⊢ range ofReal ⊆ ofReal '' univ

Tactic:
simp only [image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
hc : IsClosed (↑K : Set ℂ)
⊢ range ofReal ⊆ range ofReal

Tactic:
rfl
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous (α := ↥K) (β := ℂ) (⇑ψ : (a : ↥K) → ℂ)
this_1 : IsTopologicalDivisionRing ℂ := ⋯
this : IsTopologicalRing ↥K.topologicalClosure := ⋯
ι : ↥K → ↥K.topologicalClosure := (⇑(Subfield.inclusion ⋯) : (a : ↥K) → ↥K.topologicalClosure)
rw :
  Eq (α := Filter (↥K × ↥K))
    (Filter.comap
      ((fun (q : ↥K.topologicalClosure × ↥K.topologicalClosure) ↦ ((↑q.1 : ℂ), (↑q.2 : ℂ))) ∘ fun (x : ↥K × ↥K) ↦
        (ι x.1, ι x.2))
      (uniformity ℂ))
    (Filter.comap (fun (q : ↥K × ↥K) ↦ ((↑q.1 : ℂ), (↑q.2 : ℂ))) (uniformity ℂ))
⊢ Eq (α := Filter (↥K × ↥K))
    (Filter.comap (β := ↥K.topologicalClosure × ↥K.topologicalClosure) (fun (x : ↥K × ↥K) ↦ (ι x.1, ι x.2))
      (uniformity ↥K.topologicalClosure))
    (uniformity ↥K)

Tactic:
rw [uniformity_subtype, uniformity_subtype, Filter.comap_comap]

Premises used: Filter.comap_comap, uniformity_subtype
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous (α := ↥K) (β := ℂ) (⇑ψ : (a : ↥K) → ℂ)
this_1 : IsTopologicalDivisionRing ℂ := ⋯
this : IsTopologicalRing ↥K.topologicalClosure := ⋯
ι : ↥K → ↥K.topologicalClosure := (⇑(Subfield.inclusion ⋯) : (a : ↥K) → ↥K.topologicalClosure)
⊢ Eq (α := Filter (↥K × ↥K))
    (Filter.comap
      ((fun (q : ↥K.topologicalClosure × ↥K.topologicalClosure) ↦ ((↑q.1 : ℂ), (↑q.2 : ℂ))) ∘ fun (x : ↥K × ↥K) ↦
        (ι x.1, ι x.2))
      (uniformity ℂ))
    (Filter.comap (fun (q : ↥K × ↥K) ↦ ((↑q.1 : ℂ), (↑q.2 : ℂ))) (uniformity ℂ))

Tactic:
congr
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous (α := ↥K) (β := ℂ) (⇑ψ : (a : ↥K) → ℂ)
this_1 : IsTopologicalDivisionRing ℂ := ⋯
this : IsTopologicalRing ↥K.topologicalClosure := ⋯
ι : ↥K → ↥K.topologicalClosure := (⇑(Subfield.inclusion ⋯) : (a : ↥K) → ↥K.topologicalClosure)
⊢ IsUniformInducing ι

Tactic:
have ui : IsUniformInducing ι :=
    ⟨by
      rw [uniformity_subtype, uniformity_subtype, Filter.comap_comap]
      congr ⟩
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous (α := ↥K) (β := ℂ) (⇑ψ : (a : ↥K) → ℂ)
this_1 : IsTopologicalDivisionRing ℂ := ⋯
this : IsTopologicalRing ↥K.topologicalClosure := ⋯
ι : ↥K → ↥K.topologicalClosure := (⇑(Subfield.inclusion ⋯) : (a : ↥K) → ↥K.topologicalClosure)
ui : IsUniformInducing ι
refine_2 :
  (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
      Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
refine_1 : DenseRange ι
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
      Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)

Tactic:
let di := ui.isDenseInducing (?_ : DenseRange ι)
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous (α := ↥K) (β := ℂ) (⇑ψ : (a : ↥K) → ℂ)
this_1 : IsTopologicalDivisionRing ℂ := ⋯
this : IsTopologicalRing ↥K.topologicalClosure := ⋯
ι : ↥K → ↥K.topologicalClosure := (⇑(Subfield.inclusion ⋯) : (a : ↥K) → ↥K.topologicalClosure)
ui : IsUniformInducing ι
di : IsDenseInducing ι := ⋯
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
⊢ Continuous (Y := ℂ) (⋯.extend (⇑ψ : (a : ↥K) → ℂ))

Tactic:
haveI hψ := (uniformContinuous_uniformly_extend ui di.dense hc).continuous
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous (α := ↥K) (β := ℂ) (⇑ψ : (a : ↥K) → ℂ)
this_1 : IsTopologicalDivisionRing ℂ := ⋯
this : IsTopologicalRing ↥K.topologicalClosure := ⋯
ι : ↥K → ↥K.topologicalClosure := (⇑(Subfield.inclusion ⋯) : (a : ↥K) → ↥K.topologicalClosure)
ui : IsUniformInducing ι
di : IsDenseInducing ι := ⋯
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (Y := ℂ) (⋯.extend (⇑ψ : (a : ↥K) → ℂ))
refine_2 :
  ∀ (h : K.topologicalClosure = ofRealHom.fieldRange),
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
      (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
        Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
refine_2₁ :
  ∀ (h : K.topologicalClosure = ⊤),
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
      (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
        Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
      Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)

Tactic:
rcases Complex.subfield_eq_of_closed (Subfield.isClosed_topologicalClosure K) with h | h

Premises used: Subfield.isClosed_topologicalClosure, Complex.subfield_eq_of_closed
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous (α := ↥K) (β := ℂ) (⇑ψ : (a : ↥K) → ℂ)
this_1 : IsTopologicalDivisionRing ℂ := ⋯
this : IsTopologicalRing ↥K.topologicalClosure := ⋯
ι : ↥K → ↥K.topologicalClosure := (⇑(Subfield.inclusion ⋯) : (a : ↥K) → ↥K.topologicalClosure)
ui : IsUniformInducing ι
di : IsDenseInducing ι := ⋯
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (Y := ℂ) (⋯.extend (⇑ψ : (a : ↥K) → ℂ))
h : K.topologicalClosure = ofRealHom.fieldRange
refine_2 : (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
      Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)

Tactic:
left
-- Module: Mathlib.Topology.Instances.Complex
Goal:
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous (α := ↥K) (β := ℂ) (⇑ψ : (a : ↥K) → ℂ)
this_1 : IsTopologicalDivisionRing ℂ := ⋯
this : IsTopologicalRing ↥K.topologicalClosure := ⋯
ι : ↥K → ↥K.topologicalClosure := (⇑(Subfield.inclusion ⋯) : (a : ↥K) → ↥K.topologicalClosure)
ui : IsUniformInducing ι
di : IsDenseInducing ι := ⋯
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (Y := ℂ) (⋯.extend (⇑ψ : (a : ↥K) → ℂ))
h : K.topologicalClosure = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrict)
⊢ Continuous (X := ℝ) (Y := ℂ) (⇑ψ₁ : (a : ℝ) → ℂ)

Tactic:
simpa only [RingHom.coe_comp] using hψ.comp ((continuous_algebraMap ℝ ℂ).subtype_mk _)

Premises used: Real, Continuous.comp, continuous_algebraMap, Continuous.subtype_mk, RingHom.coe_comp, Complex