awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
⊢ Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)

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

Premises used: Continuous.comp, Continuous.subtype_mk, continuous_id, RingHom.coe_comp
-- 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 = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
⊢ Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)

Tactic:
have hψ₁ : Continuous ψ₁ := by
        simpa only [RingHom.coe_comp] using hψ.comp (continuous_id.subtype_mk _)
-- 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 = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)
refine_2 :
  ∀ (h : ψ₁ = RingHom.id ℂ),
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
      (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
        Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
refine_2₁ :
  ∀ (h : ψ₁ = starRingEnd ℂ),
    (↑(↑ψ : ↥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 ringHom_eq_id_or_conj_of_continuous hψ₁ with h | h

Premises used: Complex.ringHom_eq_id_or_conj_of_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) → ℂ))
h_1 : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h_1).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)
h : ψ₁ = RingHom.id ℂ
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_1 : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h_1).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)
h : ψ₁ = RingHom.id ℂ
refine_2 : ∀ (z : ↥K), (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun z = (K.subtype : (a : ↥K) → ℂ) z
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ)

Tactic:
ext1 z
-- 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_1 : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h_1).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)
h : ψ₁ = RingHom.id ℂ
z : ↥K
⊢ Eq (α := ℂ) ((ψ₁ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) ((RingHom.id ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ)

Tactic:
RingHom.congr_fun h z

Premises used: RingHom.congr_fun, Subtype.val
-- 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_1 : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h_1).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)
h : ψ₁ = RingHom.id ℂ
z : ↥K
h₁ : (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun z = (ψ₁ : (a : ℂ) → ℂ) (↑z : ℂ)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun z = (K.subtype : (a : ↥K) → ℂ) z

Tactic:
convert! RingHom.congr_fun h z using 1

Premises used: RingHom.congr_fun, Subtype.val
-- 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_1 : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h_1).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)
h : ψ₁ = RingHom.id ℂ
z : ↥K
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun z = (ψ₁ : (a : ℂ) → ℂ) (↑z : ℂ)

Tactic:
(IsDenseInducing.extend_eq di hc.continuous z).symm

Premises used: Classical.epsilon, Set.Mem, Set.univ, setOf, UniformContinuous.continuous, Filter.lim, Eq.symm, Filter.limUnder, IsDenseInducing.extend, IsDenseInducing.extend_eq
-- 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_1 : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h_1).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)
h : ψ₁ = RingHom.id ℂ
z : ↥K
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun z = (ψ₁ : (a : ℂ) → ℂ) (↑z : ℂ)

Tactic:
exact (IsDenseInducing.extend_eq di hc.continuous z).symm

Premises used: UniformContinuous.continuous, Eq.symm, IsDenseInducing.extend_eq
-- 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_1 : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h_1).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)
h : ψ₁ = starRingEnd ℂ
refine_2 :
  (↑(↑ψ : ↥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:
right
-- 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_1 : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h_1).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)
h : ψ₁ = starRingEnd ℂ
refine_2 :
  ∀ (z : ↥K),
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun z =
      Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ) z
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
    Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)

Tactic:
ext1 z
-- 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_1 : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h_1).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)
h : ψ₁ = starRingEnd ℂ
z : ↥K
⊢ Eq (α := ℂ) ((ψ₁ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) (↑z : ℂ) : ℂ)

Tactic:
RingHom.congr_fun h z

Premises used: RingHom.congr_fun, Subtype.val
-- 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_1 : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h_1).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)
h : ψ₁ = starRingEnd ℂ
z : ↥K
h₁ : (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun z = (ψ₁ : (a : ℂ) → ℂ) (↑z : ℂ)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun z =
    Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ) z

Tactic:
convert! RingHom.congr_fun h z using 1

Premises used: RingHom.congr_fun, Subtype.val
-- 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_1 : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h_1).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)
h : ψ₁ = starRingEnd ℂ
z : ↥K
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun z = (ψ₁ : (a : ℂ) → ℂ) (↑z : ℂ)

Tactic:
(IsDenseInducing.extend_eq di hc.continuous z).symm

Premises used: Classical.epsilon, Set.Mem, Set.univ, setOf, UniformContinuous.continuous, Filter.lim, Eq.symm, Filter.limUnder, IsDenseInducing.extend, IsDenseInducing.extend_eq
-- 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_1 : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ :=
  extψ.comp ((RingEquiv.subfieldCongr h_1).symm.toRingHom.comp (RingEquiv.toRingHom (RingEquiv.symm Subfield.topEquiv)))
hψ₁ : Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)
h : ψ₁ = starRingEnd ℂ
z : ↥K
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun z = (ψ₁ : (a : ℂ) → ℂ) (↑z : ℂ)

Tactic:
exact (IsDenseInducing.extend_eq di hc.continuous z).symm

Premises used: UniformContinuous.continuous, Eq.symm, IsDenseInducing.extend_eq
-- 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 ι
x : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) }
⊢ (↑x : ℂ) ∈ closure (id '' (↑K : Set ℂ))

Tactic:
x.prop

Premises used: Subtype.prop
-- 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 ι
x : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) }
h : (↑K.topologicalClosure : Set ℂ) = closure (id '' (↑K : Set ℂ))
⊢ (↑x : ℂ) ∈ (↑K.topologicalClosure : Set ℂ)

Tactic:
convert! x.prop

Premises used: Subtype.prop
-- 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 ι
x : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) }
h : (↑K.topologicalClosure : Set ℂ) = closure (↑K : Set ℂ)
⊢ (↑K.topologicalClosure : Set ℂ) = closure (id '' (↑K : Set ℂ))

Tactic:
simp only [id, Set.image_id']

Premises used: Set.image_id', id
-- 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 ι
x : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) }
⊢ (↑K.topologicalClosure : Set ℂ) = closure (↑K : Set ℂ)

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)
ui : IsUniformInducing ι
j : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) } → (↑(↑K.topologicalClosure : Set ℂ) : Type) :=
  fun (x : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) }) ↦
    Subtype.mk (p := fun (x : ℂ) ↦ x ∈ (↑K.topologicalClosure : Set ℂ)) (↑x : ℂ) ⋯
⊢ Continuous j

Tactic:
fun_prop
-- 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 ι
j : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) } → (↑(↑K.topologicalClosure : Set ℂ) : Type) :=
  fun (x : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) }) ↦
    Subtype.mk (p := fun (x : ℂ) ↦ x ∈ (↑K.topologicalClosure : Set ℂ)) (↑x : ℂ) ⋯
refine_1 : Function.Surjective j
⊢ DenseRange ι

Tactic:
convert!
      DenseRange.comp (Function.Surjective.denseRange _) (IsDenseEmbedding.id.subtype (· ∈ K)).dense
        (by fun_prop : Continuous j)

Premises used: IsDenseEmbedding.toIsDenseInducing, Membership.mem, IsDenseEmbedding.id, Function.Surjective.denseRange, IsDenseInducing.dense, IsDenseEmbedding.subtype, DenseRange.comp
-- 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 ι
j : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) } → (↑(↑K.topologicalClosure : Set ℂ) : Type) :=
  fun (x : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) }) ↦
    Subtype.mk (p := fun (x : ℂ) ↦ x ∈ (↑K.topologicalClosure : Set ℂ)) (↑x : ℂ) ⋯
y : ℂ
hy : y ∈ (↑K.topologicalClosure : Set ℂ)
⊢ y ∈ (↑K.topologicalClosure : Set ℂ)

Tactic:
hy
-- 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 ι
j : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) } → (↑(↑K.topologicalClosure : Set ℂ) : Type) :=
  fun (x : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) }) ↦
    Subtype.mk (p := fun (x : ℂ) ↦ x ∈ (↑K.topologicalClosure : Set ℂ)) (↑x : ℂ) ⋯
y : ℂ
hy : y ∈ (↑K.topologicalClosure : Set ℂ)
h : closure (id '' {x : ℂ | x ∈ K}) = (↑K.topologicalClosure : Set ℂ)
⊢ Membership.mem (γ := Set ℂ) (closure (id '' {x : ℂ | x ∈ K})) y

Tactic:
convert! hy
-- 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 ι
j : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) } → (↑(↑K.topologicalClosure : Set ℂ) : Type) :=
  fun (x : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) }) ↦
    Subtype.mk (p := fun (x : ℂ) ↦ x ∈ (↑K.topologicalClosure : Set ℂ)) (↑x : ℂ) ⋯
y : ℂ
hy : y ∈ (↑K.topologicalClosure : Set ℂ)
h : closure {x : ℂ | x ∈ K} = (↑K.topologicalClosure : Set ℂ)
⊢ closure (id '' {x : ℂ | x ∈ K}) = (↑K.topologicalClosure : Set ℂ)

Tactic:
simp only [id, Set.image_id']

Premises used: Set.image_id', id
-- 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 ι
j : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) } → (↑(↑K.topologicalClosure : Set ℂ) : Type) :=
  fun (x : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) }) ↦
    Subtype.mk (p := fun (x : ℂ) ↦ x ∈ (↑K.topologicalClosure : Set ℂ)) (↑x : ℂ) ⋯
y : ℂ
hy : y ∈ (↑K.topologicalClosure : Set ℂ)
⊢ closure {x : ℂ | x ∈ K} = (↑K.topologicalClosure : Set ℂ)

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)
ui : IsUniformInducing ι
j : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) } → (↑(↑K.topologicalClosure : Set ℂ) : Type) :=
  fun (x : { x : ℂ // x ∈ closure (id '' (↑K : Set ℂ)) }) ↦
    Subtype.mk (p := fun (x : ℂ) ↦ x ∈ (↑K.topologicalClosure : Set ℂ)) (↑x : ℂ) ⋯
y : ℂ
hy : y ∈ (↑K.topologicalClosure : Set ℂ)
w : { x : ℂ // Membership.mem (γ := Set ℂ) (closure (id '' {x : ℂ | x ∈ K})) x }
h :
  j (Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Set ℂ) (closure (id '' {x : ℂ | x ∈ K})) x) y ⋯) =
    Subtype.mk (p := fun (x : ℂ) ↦ x ∈ (↑K.topologicalClosure : Set ℂ)) y hy
⊢ ∃ (a : { x : ℂ // Membership.mem (γ := Set ℂ) (closure (id '' {x : ℂ | x ∈ K})) x }),
    j a = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ (↑K.topologicalClosure : Set ℂ)) y hy

Tactic:
use
      ⟨y, by
        convert! hy
        simp only [id, Set.image_id']
        rfl ⟩
-- Module: Mathlib.Topology.Instances.Discrete
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
rw : ∀ (a : α), IsCountablyGenerated (pure a)
⊢ ∀ (a : α), (nhds a).IsCountablyGenerated

Tactic:
rw [nhds_discrete]

Premises used: nhds_discrete
-- Module: Mathlib.Topology.Instances.Discrete
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
⊢ ∀ (a : α), IsCountablyGenerated (pure a)

Tactic:
isCountablyGenerated_pure

Premises used: Filter.isCountablyGenerated_pure
-- Module: Mathlib.Topology.Instances.Discrete
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
⊢ ∀ (a : α), IsCountablyGenerated (pure a)

Tactic:
exact isCountablyGenerated_pure

Premises used: Filter.isCountablyGenerated_pure