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 = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrict)
⊢ Continuous (X := ℝ) (Y := ℂ) (⇑ψ₁ : (a : ℝ) → ℂ)

Tactic:
have hψ₁ : Continuous ψ₁ := by
        simpa only [RingHom.coe_comp] using hψ.comp ((continuous_algebraMap ℝ ℂ).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 = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrict)
hψ₁ : Continuous (X := ℝ) (Y := ℂ) (⇑ψ₁ : (a : ℝ) → ℂ)
refine_2 : ∀ (x : ↥K), (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x = (K.subtype : (a : ↥K) → ℂ) x
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun = (⇑K.subtype : (a : ↥K) → ℂ)

Tactic:
ext1 x
-- 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)
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
rsuffices :
  ∃ (r : ℝ),
    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)

Premises used: DFunLike.coe
-- 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)
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)
⊢ Eq (α := ℂ) ((ψ₁ : (a : ℝ) → ℂ) r : ℂ) ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)

Tactic:
have :=
          RingHom.congr_fun (ringHom_eq_ofReal_of_continuous hψ₁) r
-- Module: Mathlib.Topology.Instances.Complex
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 : ℂ)
⊢ 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

Premises used: RingHom.comp_apply
-- Module: Mathlib.Topology.Instances.Complex
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 : ℂ)
⊢ 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
-- Module: Mathlib.Topology.Instances.Complex
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 : ℂ)
⊢ 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

Premises used: RingEquiv.toRingHom_eq_coe
-- Module: Mathlib.Topology.Instances.Complex
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 (α := ℂ)
    ((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:
this
-- Module: Mathlib.Topology.Instances.Complex
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)
h₂ : Eq (α := ℂ) ((K.subtype : (a : ↥K) → ℂ) x : ℂ) ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)
⊢ (↑(↑ψ : ↥K →* ℂ) : OneHom ↥K ℂ).toFun x = (K.subtype : (a : ↥K) → ℂ) x

Tactic:
convert! this using 1
-- Module: Mathlib.Topology.Instances.Complex
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 =
    (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:
(IsDenseInducing.extend_eq di hc.continuous _).symm

Premises used: Classical.epsilon, Set.Mem, setOf, UniformContinuous.continuous, closure, Filter.lim, Set.range, Eq.symm, Set.sInter, 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_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 =
    (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:
exact (IsDenseInducing.extend_eq di hc.continuous _).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_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₁ :
  Eq (α := ℂ) ((K.subtype : (a : ↥K) → ℂ) x : ℂ)
    ((↑((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x)) : ℂ) : ℂ)
⊢ Eq (α := ℂ) ((K.subtype : (a : ↥K) → ℂ) x : ℂ) ((ofRealHom : (a : ℝ) → ℂ) r : ℂ)

Tactic:
rw [← ofRealHom.coe_rangeRestrict, hr]

Premises used: Complex.ofRealHom, RingHom.coe_rangeRestrict
-- Module: Mathlib.Topology.Instances.Complex
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 : ℂ)
    ((↑((j : (a : ↥K.topologicalClosure) → ↥ofRealHom.fieldRange) (ι x)) : ℂ) : ℂ)

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 ι
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
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)
⊢ ∃ (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))

Premises used: SetLike.coe_mem, DFunLike.coe
-- 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)
hψ₁ : Continuous (X := ℝ) (Y := ℂ) (⇑ψ₁ : (a : ℝ) → ℂ)
x : ↥K
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:
⟨r, Subtype.ext hr⟩

Premises used: Exists.intro, Subtype.ext
-- 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)
hψ₁ : Continuous (X := ℝ) (Y := ℂ) (⇑ψ₁ : (a : ℝ) → ℂ)
x : ↥K
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:
exact ⟨r, Subtype.ext hr⟩