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)
⊢ Eq (α := Filter (↥K × ↥K))
    (Filter.comap (β := ↥K.topologicalClosure × ↥K.topologicalClosure) (fun (x : ↥K × ↥K) ↦ (ι x.1, ι x.2))
      (uniformity ↥K.topologicalClosure))
    (uniformity ↥K)
have 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 ℂ))
Tactic: rw [uniformity_subtype, uniformity_subtype, Filter.comap_comap]
-- 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)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
      Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
have ui : IsUniformInducing ι
Tactic: have ui : IsUniformInducing ι :=
    ⟨by
      rw [uniformity_subtype, uniformity_subtype, Filter.comap_comap]
      congr ⟩
-- 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 ι
refine_2 :
  (↑(↑ψ : ↥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_1 : DenseRange ι
Tactic: let di := ui.isDenseInducing (?_ : DenseRange ι)
-- 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
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
      Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
have hψ : Continuous (Y := ℂ) (sorry.extend (⇑ψ : (a : ↥K) → ℂ))
Tactic: haveI hψ := (uniformContinuous_uniformly_extend ui di.dense hc).continuous
-- 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) → ℂ))
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
      Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
have 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) → ℂ)
Tactic: rcases Complex.subfield_eq_of_closed (Subfield.isClosed_topologicalClosure K) 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) → ℂ))
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) → ℂ)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ) ∨
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun =
      Function.comp (β := ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ) (⇑K.subtype : (a : ↥K) → ℂ)
have 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) → ℂ)
Tactic: rcases Complex.subfield_eq_of_closed (Subfield.isClosed_topologicalClosure K) 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 = ofRealHom.fieldRange
⊢ (↑(↑ψ : ↥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 (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 = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrict)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ)
have hψ₁ : Continuous (X := ℝ) (Y := ℂ) (⇑ψ₁ : (a : ℝ) → ℂ)
Tactic: have hψ₁ : Continuous ψ₁ := by
        simpa only [RingHom.coe_comp] using hψ.comp ((continuous_algebraMap ℝ ℂ).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 = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrict)
hψ₁ : Continuous (X := ℝ) (Y := ℂ) (⇑ψ₁ : (a : ℝ) → ℂ)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ)
have refine_2 : ∀ (x : ↥K), (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x = (K.subtype : (a : ↥K) → ℂ) x
Tactic: ext1 x
-- 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
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x = (K.subtype : (a : ↥K) → ℂ) x
have refine_2 : ∀ (r : ℝ)
  (hr :
    Eq (α := ↥ofRealHom.range) ((ofRealHom.rangeRestrict : (a : ℝ) → ↥ofRealHom.range) r : ↥ofRealHom.range)
      ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x) : ↥ofRealHom.fieldRange)),
  (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x = (K.subtype : (a : ↥K) → ℂ) x
Tactic: rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ofRealHom.rangeRestrict r = j (ι x)
-- 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
refine_2 :
  ∀ (r : ℝ)
    (hr :
      Eq (α := ↥ofRealHom.range) ((ofRealHom.rangeRestrict : (a : ℝ) → ↥ofRealHom.range) r : ↥ofRealHom.range)
        ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x) : ↥ofRealHom.fieldRange)),
    (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x = (K.subtype : (a : ↥K) → ℂ) x
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x = (K.subtype : (a : ↥K) → ℂ) x
have rsuffices : ∃ (r : ℝ),
  Eq (α := ↥ofRealHom.range) ((ofRealHom.rangeRestrict : (a : ℝ) → ↥ofRealHom.range) r : ↥ofRealHom.range)
    ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x) : ↥ofRealHom.fieldRange)
Tactic: rsuffices ⟨r, hr⟩ : ∃ r : ℝ, ofRealHom.rangeRestrict r = 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 = 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 : ℝ
hr :
  Eq (α := ↥ofRealHom.range) ((ofRealHom.rangeRestrict : (a : ℝ) → ↥ofRealHom.range) r : ↥ofRealHom.range)
    ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x) : ↥ofRealHom.fieldRange)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x = (K.subtype : (a : ↥K) → ℂ) x
have this₁ : Eq (α := ℂ) ((ψ₁ : (a : ℝ) → ℂ) r : ℂ) ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)
Tactic: have :=
          RingHom.congr_fun (ringHom_eq_ofReal_of_continuous hψ₁) r
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (hypothesis)
Goal:
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous (α := ↥K) (β := ℂ) (⇑ψ : (a : ↥K) → ℂ)
this_1 : IsTopologicalDivisionRing ℂ := ⋯
this_2 : 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 : ℝ
hr :
  Eq (α := ↥ofRealHom.range) ((ofRealHom.rangeRestrict : (a : ℝ) → ↥ofRealHom.range) r : ↥ofRealHom.range)
    ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x) : ↥ofRealHom.fieldRange)
this : Eq (α := ℂ) ((ψ₁ : (a : ℝ) → ℂ) r : ℂ) ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x = (K.subtype : (a : ↥K) → ℂ) x
have this₁ : Eq (α := ℂ)
  ((extψ : (a : ↥K.topologicalClosure) → ℂ)
      ((j.symm.toRingHom : (a : ↥ofRealHom.fieldRange) → ↥K.topologicalClosure)
          ((ofRealHom.rangeRestrict : (a : ℝ) → ↥ofRealHom.fieldRange) r) :
        ↥K.topologicalClosure) :
    ℂ)
  ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)
Tactic: rw [RingHom.comp_apply, RingHom.comp_apply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (hypothesis)
Goal:
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous (α := ↥K) (β := ℂ) (⇑ψ : (a : ↥K) → ℂ)
this_1 : IsTopologicalDivisionRing ℂ := ⋯
this_2 : 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 : ℝ
hr :
  Eq (α := ↥ofRealHom.range) ((ofRealHom.rangeRestrict : (a : ℝ) → ↥ofRealHom.range) r : ↥ofRealHom.range)
    ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x) : ↥ofRealHom.fieldRange)
this :
  Eq (α := ℂ)
    ((extψ : (a : ↥K.topologicalClosure) → ℂ)
        ((j.symm.toRingHom : (a : ↥ofRealHom.fieldRange) → ↥K.topologicalClosure)
            ((ofRealHom.rangeRestrict : (a : ℝ) → ↥ofRealHom.fieldRange) r) :
          ↥K.topologicalClosure) :
      ℂ)
    ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x = (K.subtype : (a : ↥K) → ℂ) x
have this₁ : Eq (α := ℂ)
  ((extψ : (a : ↥K.topologicalClosure) → ℂ)
      ((j.symm.toRingHom : (a : ↥ofRealHom.fieldRange) → ↥K.topologicalClosure)
          ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x)) :
        ↥K.topologicalClosure) :
    ℂ)
  ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)
Tactic: erw [hr] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (hypothesis)
Goal:
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous (α := ↥K) (β := ℂ) (⇑ψ : (a : ↥K) → ℂ)
this_1 : IsTopologicalDivisionRing ℂ := ⋯
this_2 : 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 : ℝ
hr :
  Eq (α := ↥ofRealHom.range) ((ofRealHom.rangeRestrict : (a : ℝ) → ↥ofRealHom.range) r : ↥ofRealHom.range)
    ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x) : ↥ofRealHom.fieldRange)
this :
  Eq (α := ℂ)
    ((extψ : (a : ↥K.topologicalClosure) → ℂ)
        ((j.symm.toRingHom : (a : ↥ofRealHom.fieldRange) → ↥K.topologicalClosure)
            ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x)) :
          ↥K.topologicalClosure) :
      ℂ)
    ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x = (K.subtype : (a : ↥K) → ℂ) x
have this₁ : Eq (α := ℂ)
  ((extψ : (a : ↥K.topologicalClosure) → ℂ)
      (((↑j.symm : ↥ofRealHom.fieldRange →+* ↥K.topologicalClosure) :
            (a : ↥ofRealHom.fieldRange) → ↥K.topologicalClosure)
          ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x)) :
        ↥K.topologicalClosure) :
    ℂ)
  ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)
Tactic: rw [RingEquiv.toRingHom_eq_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Instances.Complex (goal)
Goal:
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous (α := ↥K) (β := ℂ) (⇑ψ : (a : ↥K) → ℂ)
this_1 : IsTopologicalDivisionRing ℂ := ⋯
this_2 : 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 : ℝ
hr :
  Eq (α := ↥ofRealHom.range) ((ofRealHom.rangeRestrict : (a : ℝ) → ↥ofRealHom.range) r : ↥ofRealHom.range)
    ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x) : ↥ofRealHom.fieldRange)
this :
  Eq (α := ℂ)
    ((extψ : (a : ↥K.topologicalClosure) → ℂ)
        (((↑j.symm : ↥ofRealHom.fieldRange →+* ↥K.topologicalClosure) :
              (a : ↥ofRealHom.fieldRange) → ↥K.topologicalClosure)
            ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x)) :
          ↥K.topologicalClosure) :
      ℂ)
    ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x = (K.subtype : (a : ↥K) → ℂ) x
have h₁ : (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x =
  (extψ : (a : ↥K.topologicalClosure) → ℂ)
    (((↑j.symm : ↥ofRealHom.fieldRange →+* ↥K.topologicalClosure) : (a : ↥ofRealHom.fieldRange) → ↥K.topologicalClosure)
        ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x)) :
      ↥K.topologicalClosure)
Tactic: convert! this 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_2 : 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 : ℝ
hr :
  Eq (α := ↥ofRealHom.range) ((ofRealHom.rangeRestrict : (a : ℝ) → ↥ofRealHom.range) r : ↥ofRealHom.range)
    ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x) : ↥ofRealHom.fieldRange)
this :
  Eq (α := ℂ)
    ((extψ : (a : ↥K.topologicalClosure) → ℂ)
        (((↑j.symm : ↥ofRealHom.fieldRange →+* ↥K.topologicalClosure) :
              (a : ↥ofRealHom.fieldRange) → ↥K.topologicalClosure)
            ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x)) :
          ↥K.topologicalClosure) :
      ℂ)
    ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)
h₁ :
  (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x =
    (extψ : (a : ↥K.topologicalClosure) → ℂ)
      (((↑j.symm : ↥ofRealHom.fieldRange →+* ↥K.topologicalClosure) :
            (a : ↥ofRealHom.fieldRange) → ↥K.topologicalClosure)
          ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x)) :
        ↥K.topologicalClosure)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x = (K.subtype : (a : ↥K) → ℂ) x
have h₂ : Eq (α := ℂ) ((K.subtype : (a : ↥K) → ℂ) x : ℂ) ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)
Tactic: convert! this 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_2 : 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 : ℝ
hr :
  Eq (α := ↥ofRealHom.range) ((ofRealHom.rangeRestrict : (a : ℝ) → ↥ofRealHom.range) r : ↥ofRealHom.range)
    ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x) : ↥ofRealHom.fieldRange)
this :
  Eq (α := ℂ)
    ((extψ : (a : ↥K.topologicalClosure) → ℂ)
        (((↑j.symm : ↥ofRealHom.fieldRange →+* ↥K.topologicalClosure) :
              (a : ↥ofRealHom.fieldRange) → ↥K.topologicalClosure)
            ((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x)) :
          ↥K.topologicalClosure) :
      ℂ)
    ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)
⊢ Eq (α := ℂ) ((K.subtype : (a : ↥K) → ℂ) x : ℂ) ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)
have h₁ : Eq (α := ℂ) ((K.subtype : (a : ↥K) → ℂ) x : ℂ)
  ((↑((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x)) : ℂ) : ℂ)
Tactic: rw [← ofRealHom.coe_rangeRestrict, hr]