awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
a : α
⊢ Eq.{u + 1} (α := Completion β)
    (((mapRingHom f hf : RingHom.{u_1, u} (Completion α) (Completion β)) : (a : Completion α) → Completion β)
        (↑a : Completion α) :
      Completion β)
    ((↑((f : (a : α) → β) a) : Completion β) : Completion β)
have rw : Eq.{u + 1} (α := Completion β) (Completion.map (⇑f : (a : α) → β) (↑a : Completion α) : Completion β)
  ((↑((f : (a : α) → β) a) : Completion β) : Completion β)
Tactic: rw [mapRingHom_apply, map_coe (uniformContinuous_addMonoidHom_of_continuous hf)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
a : α
rw :
  Eq.{u + 1} (α := Completion β) (Completion.map (⇑f : (a : α) → β) (↑a : Completion α) : Completion β)
    ((↑((f : (a : α) → β) a) : Completion β) : Completion β)
⊢ Eq.{u + 1} (α := Completion β)
    (((mapRingHom f hf : RingHom.{u_1, u} (Completion α) (Completion β)) : (a : Completion α) → Completion β)
        (↑a : Completion α) :
      Completion β)
    ((↑((f : (a : α) → β) a) : Completion β) : Completion β)
have rw₁ : Eq.{u + 1} (α := Completion β) ((↑((f : (a : α) → β) a) : Completion β) : Completion β)
  ((↑((f : (a : α) → β) a) : Completion β) : Completion β)
Tactic: rw [mapRingHom_apply, map_coe (uniformContinuous_addMonoidHom_of_continuous hf)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
A : Type u_2
inst : Ring A
inst_1 : UniformSpace A
inst_2 : IsUniformAddGroup A
inst_3 : IsTopologicalRing A
R : Type u_3
inst_4 : CommSemiring R
inst_5 : Algebra R A
inst_6 : UniformContinuousConstSMul R A
r : R
⊢ Eq.{u_2 + 1} (α := Completion A → Completion A) (Completion.map fun (x : A) ↦ r • x) fun (x : Completion A) ↦
    HMul.hMul (α := Completion A) ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) x
have h : ∀ (x : Completion A),
  Completion.map (fun (x : A) ↦ r • x) x =
    HMul.hMul (α := Completion A) ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
A : Type u_2
inst : Ring A
inst_1 : UniformSpace A
inst_2 : IsUniformAddGroup A
inst_3 : IsTopologicalRing A
R : Type u_3
inst_4 : CommSemiring R
inst_5 : Algebra R A
inst_6 : UniformContinuousConstSMul R A
r : R
x : Completion A
⊢ Completion.map (fun (x : A) ↦ r • x) x =
    HMul.hMul (α := Completion A) ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) x
have h : IsClosed.{u_2} (X := Completion A)
  {a : Completion A |
    Completion.map (fun (x : A) ↦ r • x) a =
      HMul.hMul (α := Completion A) ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) a}
Tactic: refine Completion.induction_on x ?_ fun a => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
A : Type u_2
inst : Ring A
inst_1 : UniformSpace A
inst_2 : IsUniformAddGroup A
inst_3 : IsTopologicalRing A
R : Type u_3
inst_4 : CommSemiring R
inst_5 : Algebra R A
inst_6 : UniformContinuousConstSMul R A
r : R
x : Completion A
h :
  IsClosed.{u_2} (X := Completion A)
    {a : Completion A |
      Completion.map (fun (x : A) ↦ r • x) a =
        HMul.hMul (α := Completion A) ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) a}
⊢ Completion.map (fun (x : A) ↦ r • x) x =
    HMul.hMul (α := Completion A) ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) x
have h₁ : ∀ (a : A),
  Completion.map (fun (x : A) ↦ r • x) (↑a : Completion A) =
    HMul.hMul (α := Completion A) (β := Completion A)
      ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) (↑a : Completion A)
Tactic: refine Completion.induction_on x ?_ fun a => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
A : Type u_2
inst : Ring A
inst_1 : UniformSpace A
inst_2 : IsUniformAddGroup A
inst_3 : IsTopologicalRing A
R : Type u_3
inst_4 : CommSemiring R
inst_5 : Algebra R A
inst_6 : UniformContinuousConstSMul R A
r : R
x : Completion A
a : A
⊢ Completion.map (fun (x : A) ↦ r • x) (↑a : Completion A) =
    HMul.hMul (α := Completion A) (β := Completion A)
      ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) (↑a : Completion A)
have h : (↑(r • a) : Completion A) =
  HMul.hMul (α := Completion A) (β := Completion A)
    ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) (↑a : Completion A)
Tactic: simp_rw [map_coe (uniformContinuous_const_smul r) a, Algebra.smul_def, coe_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
A : Type u_2
inst : Ring A
inst_1 : UniformSpace A
inst_2 : IsUniformAddGroup A
inst_3 : IsTopologicalRing A
R : Type u_3
inst_4 : CommSemiring R
inst_5 : Algebra R A
inst_6 : UniformContinuousConstSMul R A
r : R
x : Completion A
a : A
h :
  (↑(r • a) : Completion A) =
    HMul.hMul (α := Completion A) (β := Completion A)
      ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) (↑a : Completion A)
⊢ Completion.map (fun (x : A) ↦ r • x) (↑a : Completion A) =
    HMul.hMul (α := Completion A) (β := Completion A)
      ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) (↑a : Completion A)
have h₁ : (↑(HMul.hMul (α := A) ((algebraMap R A : (a : R) → A) r : A) a) : Completion A) =
  HMul.hMul (α := Completion A) (β := Completion A)
    ((↑((algebraMap R A : (a : R) → A) r) : Completion A) : Completion A) (↑a : Completion A)
Tactic: simp_rw [map_coe (uniformContinuous_const_smul r) a, Algebra.smul_def, coe_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
R : Type u_2
inst_8 : CommRing R
inst_9 : UniformSpace R
inst_10 : IsUniformAddGroup R
inst_11 : IsTopologicalRing R
a_1 b_1 : Completion R
a b : R
⊢ HMul.hMul (α := Completion R) (↑a : Completion R) (↑b : Completion R) =
    HMul.hMul (α := Completion R) (↑b : Completion R) (↑a : Completion R)
have rw : (↑(a * b) : Completion R) = HMul.hMul (α := Completion R) (↑b : Completion R) (↑a : Completion R)
Tactic: rw [← coe_mul, ← coe_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
R : Type u_2
inst_8 : CommRing R
inst_9 : UniformSpace R
inst_10 : IsUniformAddGroup R
inst_11 : IsTopologicalRing R
a_1 b_1 : Completion R
a b : R
rw : (↑(a * b) : Completion R) = HMul.hMul (α := Completion R) (↑b : Completion R) (↑a : Completion R)
⊢ HMul.hMul (α := Completion R) (↑a : Completion R) (↑b : Completion R) =
    HMul.hMul (α := Completion R) (↑b : Completion R) (↑a : Completion R)
have rw₁ : Eq (α := Completion R) (↑(a * b) : Completion R) (↑(b * a) : Completion R)
Tactic: rw [← coe_mul, ← coe_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
β : Type u
inst_4 : UniformSpace β
inst_5 : Ring β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
f : α →+* β
hf : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
R : Type u_2
inst_8 : CommRing R
inst_9 : UniformSpace R
inst_10 : IsUniformAddGroup R
inst_11 : IsTopologicalRing R
a_1 b_1 : Completion R
a b : R
rw : (↑(a * b) : Completion R) = HMul.hMul (α := Completion R) (↑b : Completion R) (↑a : Completion R)
rw₁ : Eq (α := Completion R) (↑(a * b) : Completion R) (↑(b * a) : Completion R)
⊢ HMul.hMul (α := Completion R) (↑a : Completion R) (↑b : Completion R) =
    HMul.hMul (α := Completion R) (↑b : Completion R) (↑a : Completion R)
have rw₂ : Eq (α := Completion R) (↑(b * a) : Completion R) (↑(b * a) : Completion R)
Tactic: rw [← coe_mul, ← coe_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α_1 : Type u_1
α : Type u_2
inst : Ring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalRing α
x y : α
⊢ (inseparableSetoid α : α → α → Prop) x y ↔ (Submodule.quotientRel ⊥.closure : α → α → Prop) x y
have rw : (Submodule.quotientRel ⊥.closure : α → α → Prop) x y ↔ (Submodule.quotientRel ⊥.closure : α → α → Prop) x y
Tactic: rw [inseparableSetoid_ring]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α_1 : Type u_1
α : Type u_2
inst : Ring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalRing α
⊢ Relator.LiftFun.{u_2 + 1, u_2 + 1, u_2 + 1, u_2 + 1} (α := α) (⇑(inseparableSetoid α) : α → α → Prop)
    (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop) id id
have rw : Relator.LiftFun.{u_2 + 1, u_2 + 1, u_2 + 1, u_2 + 1} (α := α) (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop)
  (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop) id id
Tactic: rw [inseparableSetoid_ring]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α_1 : Type u_1
α : Type u_2
inst : Ring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalRing α
⊢ Relator.LiftFun.{u_2 + 1, u_2 + 1, u_2 + 1, u_2 + 1} (α := α) (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop)
    (⇑(inseparableSetoid α) : α → α → Prop) id id
have rw : Relator.LiftFun.{u_2 + 1, u_2 + 1, u_2 + 1, u_2 + 1} (α := α) (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop)
  (⇑(Submodule.quotientRel ⊥.closure) : α → α → Prop) id id
Tactic: rw [inseparableSetoid_ring]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
⊢ Eq.{u_3 + 1} (α := γ) (⋯.extend (⇑f : (a : α) → γ) 1) 1
have h : Eq.{u_2 + 1} (α := β) (1 : β) ((i : (a : α) → β) 1 : β)
Tactic: convert! IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Eq.{u_2 + 1} (α := β) (1 : β) ((i : (a : α) → β) 1 : β)
⊢ Eq.{u_3 + 1} (α := γ) (⋯.extend (⇑f : (a : α) → γ) 1) 1
have h₁ : Eq.{u_3 + 1} (α := γ) (1 : γ) ((f : (a : α) → γ) 1 : γ)
Tactic: convert! IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (hypothesis)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
⊢ ∀ (x y : β),
    ⋯.extend (⇑f : (a : α) → γ) (x * y) =
      HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) x) (⋯.extend (⇑f : (a : α) → γ) y)
have h : Continuous.{u_2, u_3} (Y := γ) (sorry.extend (⇑f : (a : α) → γ))
Tactic: have h := (uniformContinuous_uniformly_extend ue dr hf).continuous
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
⊢ ∀ (x y : β),
    ⋯.extend (⇑f : (a : α) → γ) (x * y) =
      HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) x) (⋯.extend (⇑f : (a : α) → γ) y)
have refine_1 : ∀ (x y : β),
  IsClosed.{u_2} (X := β × β)
    {q : β × β |
      sorry.extend (⇑f : (a : α) → γ) (q.1 * q.2) =
        HMul.hMul (α := γ) (sorry.extend (⇑f : (a : α) → γ) q.1) (sorry.extend (⇑f : (a : α) → γ) q.2)}
Tactic: refine fun x y => DenseRange.induction_on₂ dr ?_ (fun a b => ?_) x y
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
refine_1 :
  ∀ (x y : β),
    IsClosed.{u_2} (X := β × β)
      {q : β × β |
        ⋯.extend (⇑f : (a : α) → γ) (q.1 * q.2) =
          HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) q.1) (⋯.extend (⇑f : (a : α) → γ) q.2)}
⊢ ∀ (x y : β),
    ⋯.extend (⇑f : (a : α) → γ) (x * y) =
      HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) x) (⋯.extend (⇑f : (a : α) → γ) y)
have refine_2 : ∀ (x y : β) (a b : α),
  sorry.extend (⇑f : (a : α) → γ) (HMul.hMul (α := β) (β := β) ((i : (a : α) → β) a : β) ((i : (a : α) → β) b : β)) =
    HMul.hMul (α := γ) (sorry.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
      (sorry.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))
Tactic: refine fun x y => DenseRange.induction_on₂ dr ?_ (fun a b => ?_) x y
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
x y : β
a b : α
⊢ ⋯.extend (⇑f : (a : α) → γ) (HMul.hMul (α := β) (β := β) ((i : (a : α) → β) a : β) ((i : (a : α) → β) b : β)) =
    HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
      (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))
have refine_2 : sorry.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) (a * b)) =
  HMul.hMul (α := γ) (sorry.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
    (sorry.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))
Tactic: simp_rw [← i.map_mul, IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous _,
        ← f.map_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
x y : β
a b : α
refine_2 :
  ⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) (a * b)) =
    HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
      (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))
⊢ ⋯.extend (⇑f : (a : α) → γ) (HMul.hMul (α := β) (β := β) ((i : (a : α) → β) a : β) ((i : (a : α) → β) b : β)) =
    HMul.hMul (α := γ) (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
      (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))
have refine_2₁ : (f : (a : α) → γ) (a * b) = HMul.hMul (α := γ) (β := γ) ((f : (a : α) → γ) a : γ) ((f : (a : α) → γ) b : γ)
Tactic: simp_rw [← i.map_mul, IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous _,
        ← f.map_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
⊢ Eq.{u_3 + 1} (α := γ) (⋯.extend (⇑f : (a : α) → γ) 0) 0
have h : Eq.{u_2 + 1} (α := β) (0 : β) ((i : (a : α) → β) 0 : β)
Tactic: convert! IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Eq.{u_2 + 1} (α := β) (0 : β) ((i : (a : α) → β) 0 : β)
⊢ Eq.{u_3 + 1} (α := γ) (⋯.extend (⇑f : (a : α) → γ) 0) 0
have h₁ : Eq.{u_3 + 1} (α := γ) (0 : γ) ((f : (a : α) → γ) 0 : γ)
Tactic: convert! IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (hypothesis)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
⊢ ∀ (x y : β),
    ⋯.extend (⇑f : (a : α) → γ) (x + y) =
      HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) x) (⋯.extend (⇑f : (a : α) → γ) y)
have h : Continuous.{u_2, u_3} (Y := γ) (sorry.extend (⇑f : (a : α) → γ))
Tactic: have h := (uniformContinuous_uniformly_extend ue dr hf).continuous
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
⊢ ∀ (x y : β),
    ⋯.extend (⇑f : (a : α) → γ) (x + y) =
      HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) x) (⋯.extend (⇑f : (a : α) → γ) y)
have refine_1 : ∀ (x y : β),
  IsClosed.{u_2} (X := β × β)
    {q : β × β |
      sorry.extend (⇑f : (a : α) → γ) (q.1 + q.2) =
        HAdd.hAdd (α := γ) (sorry.extend (⇑f : (a : α) → γ) q.1) (sorry.extend (⇑f : (a : α) → γ) q.2)}
Tactic: refine fun x y => DenseRange.induction_on₂ dr ?_ (fun a b => ?_) x y
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
refine_1 :
  ∀ (x y : β),
    IsClosed.{u_2} (X := β × β)
      {q : β × β |
        ⋯.extend (⇑f : (a : α) → γ) (q.1 + q.2) =
          HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) q.1) (⋯.extend (⇑f : (a : α) → γ) q.2)}
⊢ ∀ (x y : β),
    ⋯.extend (⇑f : (a : α) → γ) (x + y) =
      HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) x) (⋯.extend (⇑f : (a : α) → γ) y)
have refine_2 : ∀ (x y : β) (a b : α),
  sorry.extend (⇑f : (a : α) → γ) (HAdd.hAdd (α := β) (β := β) ((i : (a : α) → β) a : β) ((i : (a : α) → β) b : β)) =
    HAdd.hAdd (α := γ) (sorry.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
      (sorry.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))
Tactic: refine fun x y => DenseRange.induction_on₂ dr ?_ (fun a b => ?_) x y
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Semiring α
β : Type u_2
inst_2 : UniformSpace β
inst_3 : Semiring β
inst_4 : IsTopologicalSemiring β
γ : Type u_3
inst_5 : UniformSpace γ
inst_6 : Semiring γ
inst_7 : IsTopologicalSemiring γ
inst_8 : T2Space γ
inst_9 : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : IsUniformInducing.{u_1, u_2} (α := α) (β := β) (⇑i : (a : α) → β)
dr : DenseRange.{u_2, u_1} (X := β) (α := α) (⇑i : (a : α) → β)
hf : UniformContinuous.{u_1, u_3} (α := α) (β := γ) (⇑f : (a : α) → γ)
h : Continuous.{u_2, u_3} (Y := γ) (⋯.extend (⇑f : (a : α) → γ))
x y : β
a b : α
⊢ ⋯.extend (⇑f : (a : α) → γ) (HAdd.hAdd (α := β) (β := β) ((i : (a : α) → β) a : β) ((i : (a : α) → β) b : β)) =
    HAdd.hAdd (α := γ) (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
      (⋯.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))
have refine_2 : sorry.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) (a + b)) =
  HAdd.hAdd (α := γ) (sorry.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) a))
    (sorry.extend (⇑f : (a : α) → γ) ((i : (a : α) → β) b))
Tactic: simp_rw [← i.map_add, IsDenseInducing.extend_eq (ue.isDenseInducing dr) hf.continuous _,
        ← f.map_add]