awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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)
hψ₁ : Continuous (X := ℝ) (Y := ℂ) (⇑ψ₁ : (a : ℝ) → ℂ)
x : ↥K
⊢ ∃ (r : ℝ),
    Eq (α := ↥ofRealHom.range) ((ofRealHom.rangeRestrict : (a : ℝ) → ↥ofRealHom.range) r : ↥ofRealHom.range)
      ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x) : ↥ofRealHom.fieldRange)
have obtain : ∀ (r : ℝ)
  (hr :
    Eq (α := ℂ) ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)
      ((↑((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x)) : ℂ) : ℂ)),
  ∃ (r : ℝ),
    Eq (α := ↥ofRealHom.range) ((ofRealHom.rangeRestrict : (a : ℝ) → ↥ofRealHom.range) r : ↥ofRealHom.range)
      ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x) : ↥ofRealHom.fieldRange)
Tactic: obtain ⟨r, hr⟩ := SetLike.coe_mem (j (ι x))
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (hypothesis)
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)))
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
      Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
have hψ₁ : Continuous (X := ℂ) (Y := ℂ) (⇑ψ₁ : (a : ℂ) → ℂ)
Tactic: have hψ₁ : Continuous ψ₁ := by
        simpa only [RingHom.coe_comp] using hψ.comp (continuous_id.subtype_mk _)
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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 : ℂ) → ℂ)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
      Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
have 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) → ℂ)
Tactic: rcases ringHom_eq_id_or_conj_of_continuous hψ₁ with h | h
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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) → ℂ)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
      Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
have refine_2₁ : ∀ (h : ψ₁ = starRingEnd ℂ),
  (↑(↑ψ : ↥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
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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 ℂ
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
      Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
have refine_2 : (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ)
Tactic: left
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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 ℂ
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ)
have refine_2 : ∀ (z : ↥K), (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun z = (K.subtype : (a : ↥K) → ℂ) z
Tactic: ext1 z
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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 = (K.subtype : (a : ↥K) → ℂ) z
have h₁ : (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun z = (ψ₁ : (a : ℂ) → ℂ) (↑z : ℂ)
Tactic: convert! RingHom.congr_fun h z using 1
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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 ℂ
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
      Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
have refine_2 : (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
  Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
Tactic: right
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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 ℂ
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
    Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
have refine_2 : ∀ (z : ↥K),
  (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun z =
    Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ) z
Tactic: ext1 z
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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 =
    Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ) z
have h₁ : (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun z = (ψ₁ : (a : ℂ) → ℂ) (↑z : ℂ)
Tactic: convert! RingHom.congr_fun h z using 1
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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 : ℂ) ∈ (↑K.topologicalClosure : Set ℂ)
have h : (↑K.topologicalClosure : Set ℂ) = closure (id '' (↑K : Set ℂ))
Tactic: convert! x.prop
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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 (id '' (↑K : Set ℂ))
have h : (↑K.topologicalClosure : Set ℂ) = closure (↑K : Set ℂ)
Tactic: simp only [id, Set.image_id']
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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 : ℂ) ⋯
⊢ DenseRange ι
have refine_1 : Function.Surjective j
Tactic: convert!
      DenseRange.comp (Function.Surjective.denseRange _) (IsDenseEmbedding.id.subtype (· ∈ K)).dense
        (by fun_prop : Continuous j)
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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 ℂ)
⊢ Membership.mem (γ := Set ℂ) (closure (id '' {x : ℂ | x ∈ K})) y
have h : closure (id '' {x : ℂ | x ∈ K}) = (↑K.topologicalClosure : Set ℂ)
Tactic: convert! hy
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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 (id '' {x : ℂ | x ∈ K}) = (↑K.topologicalClosure : Set ℂ)
have h : closure {x : ℂ | x ∈ K} = (↑K.topologicalClosure : Set ℂ)
Tactic: simp only [id, Set.image_id']
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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 ℂ)
⊢ ∃ (a : { x : ℂ // Membership.mem (γ := Set ℂ) (closure (id '' {x : ℂ | x ∈ K})) x }),
    j a = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ (↑K.topologicalClosure : Set ℂ)) y hy
have w : { x : ℂ // Membership.mem (γ := Set ℂ) (closure (id '' {x : ℂ | x ∈ K})) x }
Tactic: use
      ⟨y, by
        convert! hy
        simp only [id, Set.image_id']
        rfl ⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
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 }
⊢ ∃ (a : { x : ℂ // Membership.mem (γ := Set ℂ) (closure (id '' {x : ℂ | x ∈ K})) x }),
    j a = Subtype.mk (p := fun (x : ℂ) ↦ x ∈ (↑K.topologicalClosure : Set ℂ)) y hy
have h : j (Subtype.mk (p := fun (x : ℂ) ↦ Membership.mem (γ := Set ℂ) (closure (id '' {x : ℂ | x ∈ K})) x) y sorry) =
  Subtype.mk (p := fun (x : ℂ) ↦ x ∈ (↑K.topologicalClosure : Set ℂ)) y hy
Tactic: use
      ⟨y, by
        convert! hy
        simp only [id, Set.image_id']
        rfl ⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.Discrete (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : DiscreteTopology α
⊢ ∀ (a : α), (nhds a).IsCountablyGenerated
have rw : ∀ (a : α), IsCountablyGenerated (pure a)
Tactic: rw [nhds_discrete]
-- Lean 4 proof step from Mathlib.Topology.Instances.Discrete (hypothesis)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : SuccOrder α
x : TopologicalSpace α := Preorder.topology α
⊢ ⊥ = Preorder.topology α
have this : OrderTopology α
Tactic: have : OrderTopology α := ⟨rfl⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.Discrete (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : PredOrder α
inst_3 : SuccOrder α
⊢ DiscreteTopology α ↔ OrderTopology α
have refine : ∀ (h : DiscreteTopology α), inst = Preorder.topology α
Tactic: refine ⟨fun h ↦ ⟨?_⟩, fun h ↦ .of_predOrder_succOrder⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.Discrete (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : PredOrder α
inst_3 : SuccOrder α
h : DiscreteTopology α
⊢ inst = Preorder.topology α
have rw : ⊥ = Preorder.topology α
Tactic: rw [h.eq_bot, LinearOrder.bot_topologicalSpace_eq_preorderTopology]
-- Lean 4 proof step from Mathlib.Topology.Instances.Discrete (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LinearOrder α
inst_2 : PredOrder α
inst_3 : SuccOrder α
h : DiscreteTopology α
rw : ⊥ = Preorder.topology α
⊢ inst = Preorder.topology α
have rw₁ : Preorder.topology α = Preorder.topology α
Tactic: rw [h.eq_bot, LinearOrder.bot_topologicalSpace_eq_preorderTopology]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.ENatENNReal (goal)
Goal:
⊢ Continuous toENNReal
have refine_1 : ∀ (a : ENNReal), IsOpen (toENNReal ⁻¹' Set.Ioi a)
Tactic: refine OrderTopology.continuous_iff.mpr fun a ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.ENatENNReal (goal)
Goal:
refine_1 : ∀ (a : ENNReal), IsOpen (toENNReal ⁻¹' Set.Ioi a)
⊢ Continuous toENNReal
have refine_2 : ∀ (a : ENNReal), IsOpen (toENNReal ⁻¹' Set.Iio a)
Tactic: refine OrderTopology.continuous_iff.mpr fun a ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
b : ℝ≥0∞
⊢ IsOpen (Ico 0 b)
have rw : IsOpen (Iio b)
Tactic: rw [ENNReal.Ico_eq_Iio]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
⊢ Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 a)
have nth_rewrite : Tendsto ofNNReal (𝓝 a.toNNReal) (𝓝 (↑a.toNNReal : ℝ≥0∞))
Tactic: nth_rewrite 2 [← coe_toNNReal ha]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_4
l : Filter α
x : ℝ≥0
f : ℝ≥0∞ → α
⊢ Tendsto f (𝓝 (↑x : ℝ≥0∞)) l ↔ Tendsto (f ∘ ofNNReal) (𝓝 x) l
have rw : Tendsto f (map ofNNReal (𝓝 x)) l ↔ Tendsto (f ∘ ofNNReal) (𝓝 x) l
Tactic: rw [nhds_coe, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_4
l : Filter α
x : ℝ≥0
f : ℝ≥0∞ → α
rw : Tendsto f (map ofNNReal (𝓝 x)) l ↔ Tendsto (f ∘ ofNNReal) (𝓝 x) l
⊢ Tendsto f (𝓝 (↑x : ℝ≥0∞)) l ↔ Tendsto (f ∘ ofNNReal) (𝓝 x) l
have rw₁ : Tendsto (f ∘ ofNNReal) (𝓝 x) l ↔ Tendsto (f ∘ ofNNReal) (𝓝 x) l
Tactic: rw [nhds_coe, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a : ℝ≥0∞
ha : a ≠ ∞
⊢ Tendsto ENNReal.toNNReal (𝓝 a) (𝓝 a.toNNReal)
have lift : ∀ (a : ℝ≥0), Tendsto ENNReal.toNNReal (𝓝 (↑a : ℝ≥0∞)) (𝓝 (↑a : ℝ≥0∞).toNNReal)
Tactic: lift a to ℝ≥0 using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
a : ℝ≥0
⊢ Tendsto ENNReal.toNNReal (𝓝 (↑a : ℝ≥0∞)) (𝓝 (↑a : ℝ≥0∞).toNNReal)
have rw : Tendsto (ENNReal.toNNReal ∘ ofNNReal) (𝓝 a) (𝓝 (↑a : ℝ≥0∞).toNNReal)
Tactic: rw [nhds_coe, tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ∞
hf : ∀ (x : α), f x ≠ ∞
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal) ↔ Tendsto f u (𝓝 a)
have refine : ∀ (h : Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal)), Tendsto f u (𝓝 a)
Tactic: refine ⟨fun h => ?_, fun h => (ENNReal.tendsto_toNNReal ha).comp h⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
u : Filter α
ha : a ≠ ∞
hf : ∀ (x : α), f x ≠ ∞
h : Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a.toNNReal)
⊢ Tendsto f u (𝓝 a)
have rw : Tendsto ((fun (x : ℝ≥0) ↦ (↑x : ℝ≥0∞)) ∘ ENNReal.toNNReal ∘ f) u (𝓝 a)
Tactic: rw [← coe_comp_toNNReal_comp hf]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
f : α → ℝ≥0∞
u : Filter α
a : ℝ≥0
hf : ∀ (x : α), f x ≠ ∞
⊢ Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 a) ↔ Tendsto f u (𝓝 (↑a : ℝ≥0∞))
have rw : Tendsto (ENNReal.toNNReal ∘ f) u (𝓝 (↑a : ℝ≥0∞).toNNReal) ↔ Tendsto f u (𝓝 (↑(↑a : ℝ≥0∞).toNNReal : ℝ≥0∞))
Tactic: rw [← toNNReal_coe a]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
l : Filter α
f g : α → ℝ≥0∞
hfi : ∀ᶠ (x : α) in l, f x ≠ ∞
hgi : ∀ᶠ (x : α) in l, g x ≠ ∞
hfg : l.EventuallyEq (β := ℝ) (fun (x : α) ↦ (f x).toReal) fun (x : α) ↦ (g x).toReal
⊢ f =ᶠ[l] g
have h : ∀ (a : α) (hfx : f a ≠ ∞) (hgx : g a ≠ ∞), (f a).toReal = (g a).toReal → f a = g a
Tactic: filter_upwards [hfi, hgi, hfg] with _ hfx hgx _
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
a b : ℝ≥0∞
r : ℝ≥0
x ε : ℝ≥0∞
⊢ (↑{a : ℝ≥0∞ | a < ∞} : Type) ≃ₜ ℝ≥0
have refine : Eq (α := Set ℝ≥0∞) {a : ℝ≥0∞ | a < ∞} {a : ℝ≥0∞ | a ≠ ∞}
Tactic: refine (Homeomorph.setCongr ?_).trans neTopHomeomorphNNReal
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
m : α → ℝ≥0∞
f : Filter α
h : ∀ (n : ℕ), ∀ᶠ (a : α) in f, (↑n : ℝ≥0∞) < m a
x : ℝ≥0
n : ℕ
hn : x < (↑n : ℝ≥0)
x_1 : α
⊢ (↑x : ℝ≥0∞) < (↑n : ℝ≥0∞)
have rwa : (↑x : ℝ≥0∞) < (↑(↑n : ℝ≥0) : ℝ≥0∞)
Tactic: rwa [← ENNReal.coe_natCast, coe_lt_coe]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
α : Type u_1
f : α → ℝ≥0
l : Filter α
⊢ Tendsto (β := ℝ≥0∞) (fun (x : α) ↦ (↑(f x) : ℝ≥0∞)) l (𝓝 ∞) ↔ Tendsto f l atTop
have rw : (∀ (x : ℝ≥0), ∀ᶠ (a : α) in l, (↑x : ℝ≥0∞) < (↑(f a) : ℝ≥0∞)) ↔ ∀ (i : ℝ≥0), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i
Tactic: rw [tendsto_nhds_top_iff_nnreal, atTop_basis_Ioi.tendsto_right_iff]
-- Lean 4 proof step from Mathlib.Topology.Instances.ENNReal.Lemmas (goal)
Goal:
x : ℝ≥0∞
xt : x ≠ ∞
⊢ (𝓝 x).HasBasis (fun (x : ℝ≥0∞) ↦ x ≠ 0) fun (ε : ℝ≥0∞) ↦ Icc (x - ε) (x + ε)
have inl : ∀ (xt : Ne (α := ℝ≥0∞) 0 ∞), HasBasis (α := ℝ≥0∞) (𝓝 0) (fun (x : ℝ≥0∞) ↦ x ≠ 0) fun (ε : ℝ≥0∞) ↦ Icc (0 - ε) (0 + ε)
Tactic: rcases eq_zero_or_pos x with rfl | x0
Cleared hypotheses: x, xt