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 α
a_1 : Completion α
a : α
⊢ HMul.hMul (α := Completion α) (↑a : Completion α) 0 = 0
have rw : HMul.hMul (α := Completion α) (↑a : Completion α) (↑0 : Completion α) = (↑0 : Completion α)
Tactic: rw [← coe_zero, ← coe_mul, mul_zero]
-- 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 α
a_1 : Completion α
a : α
rw : HMul.hMul (α := Completion α) (↑a : Completion α) (↑0 : Completion α) = (↑0 : Completion α)
⊢ HMul.hMul (α := Completion α) (↑a : Completion α) 0 = 0
have rw₁ : Eq (α := Completion α) (↑(a * 0) : Completion α) (↑0 : Completion α)
Tactic: rw [← coe_zero, ← coe_mul, mul_zero]
-- 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 α
a_1 : Completion α
a : α
rw : HMul.hMul (α := Completion α) (↑a : Completion α) (↑0 : Completion α) = (↑0 : Completion α)
rw₁ : Eq (α := Completion α) (↑(a * 0) : Completion α) (↑0 : Completion α)
⊢ HMul.hMul (α := Completion α) (↑a : Completion α) 0 = 0
have rw₂ : Eq.{u_1 + 1} (α := Completion α) (↑0 : Completion α) (↑0 : Completion α)
Tactic: rw [← coe_zero, ← coe_mul, mul_zero]
-- 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 α
a_1 b_1 c_1 : Completion α
a b c : α
⊢ (↑a : Completion α) * HAdd.hAdd (α := Completion α) (↑b : Completion α) (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
have rw : HMul.hMul (α := Completion α) (↑a : Completion α) (↑(b + c) : Completion α) =
  HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
Tactic: rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, mul_add]
-- 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 α
a_1 b_1 c_1 : Completion α
a b c : α
rw :
  HMul.hMul (α := Completion α) (↑a : Completion α) (↑(b + c) : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
⊢ (↑a : Completion α) * HAdd.hAdd (α := Completion α) (↑b : Completion α) (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
have rw₁ : (↑(a * (b + c)) : Completion α) =
  HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
Tactic: rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, mul_add]
-- 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 α
a_1 b_1 c_1 : Completion α
a b c : α
rw :
  HMul.hMul (α := Completion α) (↑a : Completion α) (↑(b + c) : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
rw₁ :
  (↑(a * (b + c)) : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
⊢ (↑a : Completion α) * HAdd.hAdd (α := Completion α) (↑b : Completion α) (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
have rw₂ : (↑(a * (b + c)) : Completion α) =
  (↑(a * b) : Completion α) + HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
Tactic: rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, mul_add]
-- 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 α
a_1 b_1 c_1 : Completion α
a b c : α
rw :
  HMul.hMul (α := Completion α) (↑a : Completion α) (↑(b + c) : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
rw₁ :
  (↑(a * (b + c)) : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
rw₂ :
  (↑(a * (b + c)) : Completion α) =
    (↑(a * b) : Completion α) + HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
⊢ (↑a : Completion α) * HAdd.hAdd (α := Completion α) (↑b : Completion α) (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
have rw₃ : (↑(a * (b + c)) : Completion α) = HAdd.hAdd (α := Completion α) (↑(a * b) : Completion α) (↑(a * c) : Completion α)
Tactic: rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, mul_add]
-- 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 α
a_1 b_1 c_1 : Completion α
a b c : α
rw :
  HMul.hMul (α := Completion α) (↑a : Completion α) (↑(b + c) : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
rw₁ :
  (↑(a * (b + c)) : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
rw₂ :
  (↑(a * (b + c)) : Completion α) =
    (↑(a * b) : Completion α) + HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
rw₃ :
  (↑(a * (b + c)) : Completion α) = HAdd.hAdd (α := Completion α) (↑(a * b) : Completion α) (↑(a * c) : Completion α)
⊢ (↑a : Completion α) * HAdd.hAdd (α := Completion α) (↑b : Completion α) (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
have rw₄ : Eq (α := Completion α) (↑(a * (b + c)) : Completion α) (↑(a * b + a * c) : Completion α)
Tactic: rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, mul_add]
-- 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 α
a_1 b_1 c_1 : Completion α
a b c : α
rw :
  HMul.hMul (α := Completion α) (↑a : Completion α) (↑(b + c) : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
rw₁ :
  (↑(a * (b + c)) : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
rw₂ :
  (↑(a * (b + c)) : Completion α) =
    (↑(a * b) : Completion α) + HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
rw₃ :
  (↑(a * (b + c)) : Completion α) = HAdd.hAdd (α := Completion α) (↑(a * b) : Completion α) (↑(a * c) : Completion α)
rw₄ : Eq (α := Completion α) (↑(a * (b + c)) : Completion α) (↑(a * b + a * c) : Completion α)
⊢ (↑a : Completion α) * HAdd.hAdd (α := Completion α) (↑b : Completion α) (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) +
      HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α)
have rw₅ : Eq (α := Completion α) (↑(a * b + a * c) : Completion α) (↑(a * b + a * c) : Completion α)
Tactic: rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, mul_add]
-- 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 α
a_1 b_1 c_1 : Completion α
a b c : α
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α) * (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
have rw : HMul.hMul (α := Completion α) (↑(a + b) : Completion α) (↑c : Completion α) =
  HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
    HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
Tactic: rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, add_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 α
a_1 b_1 c_1 : Completion α
a b c : α
rw :
  HMul.hMul (α := Completion α) (↑(a + b) : Completion α) (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α) * (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
have rw₁ : (↑((a + b) * c) : Completion α) =
  HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
    HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
Tactic: rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, add_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 α
a_1 b_1 c_1 : Completion α
a b c : α
rw :
  HMul.hMul (α := Completion α) (↑(a + b) : Completion α) (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₁ :
  (↑((a + b) * c) : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α) * (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
have rw₂ : (↑((a + b) * c) : Completion α) =
  (↑(a * c) : Completion α) + HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
Tactic: rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, add_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 α
a_1 b_1 c_1 : Completion α
a b c : α
rw :
  HMul.hMul (α := Completion α) (↑(a + b) : Completion α) (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₁ :
  (↑((a + b) * c) : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₂ :
  (↑((a + b) * c) : Completion α) =
    (↑(a * c) : Completion α) + HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α) * (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
have rw₃ : (↑((a + b) * c) : Completion α) = HAdd.hAdd (α := Completion α) (↑(a * c) : Completion α) (↑(b * c) : Completion α)
Tactic: rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, add_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 α
a_1 b_1 c_1 : Completion α
a b c : α
rw :
  HMul.hMul (α := Completion α) (↑(a + b) : Completion α) (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₁ :
  (↑((a + b) * c) : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₂ :
  (↑((a + b) * c) : Completion α) =
    (↑(a * c) : Completion α) + HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₃ :
  (↑((a + b) * c) : Completion α) = HAdd.hAdd (α := Completion α) (↑(a * c) : Completion α) (↑(b * c) : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α) * (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
have rw₄ : Eq (α := Completion α) (↑((a + b) * c) : Completion α) (↑(a * c + b * c) : Completion α)
Tactic: rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, add_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 α
a_1 b_1 c_1 : Completion α
a b c : α
rw :
  HMul.hMul (α := Completion α) (↑(a + b) : Completion α) (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₁ :
  (↑((a + b) * c) : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₂ :
  (↑((a + b) * c) : Completion α) =
    (↑(a * c) : Completion α) + HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₃ :
  (↑((a + b) * c) : Completion α) = HAdd.hAdd (α := Completion α) (↑(a * c) : Completion α) (↑(b * c) : Completion α)
rw₄ : Eq (α := Completion α) (↑((a + b) * c) : Completion α) (↑(a * c + b * c) : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α) * (↑c : Completion α) =
    HMul.hMul (α := Completion α) (↑a : Completion α) (↑c : Completion α) +
      HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
have rw₅ : Eq (α := Completion α) (↑(a * c + b * c) : Completion α) (↑(a * c + b * c) : Completion α)
Tactic: rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, add_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_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Eq.{u + 1} (α := β) (Completion.extension.{u_1, u} (α := α) (⇑f : (a : α) → β) 1) 1
have rw : Eq.{u + 1} (α := β) (Completion.extension.{u_1, u} (α := α) (⇑f : (a : α) → β) (↑1 : Completion α)) 1
Tactic: rw [← coe_one, extension_coe hf, f.map_one]
-- 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_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
rw : Eq.{u + 1} (α := β) (Completion.extension.{u_1, u} (α := α) (⇑f : (a : α) → β) (↑1 : Completion α)) 1
⊢ Eq.{u + 1} (α := β) (Completion.extension.{u_1, u} (α := α) (⇑f : (a : α) → β) 1) 1
have rw₁ : Eq.{u + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)
Tactic: rw [← coe_one, extension_coe hf, f.map_one]
-- 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_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
rw : Eq.{u + 1} (α := β) (Completion.extension.{u_1, u} (α := α) (⇑f : (a : α) → β) (↑1 : Completion α)) 1
rw₁ : Eq.{u + 1} (α := β) ((f : (a : α) → β) 1 : β) (1 : β)
⊢ Eq.{u + 1} (α := β) (Completion.extension.{u_1, u} (α := α) (⇑f : (a : α) → β) 1) 1
have rw₂ : Eq.{u + 1} (α := β) 1 1
Tactic: rw [← coe_one, extension_coe hf, f.map_one]
-- 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_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
a_1 b_1 : Completion α
a b : α
⊢ Completion.extension (⇑f : (a : α) → β) (HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α)) =
    HMul.hMul (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
have simp_rw : Completion.extension (⇑f : (a : α) → β) (↑(a * b) : Completion α) =
  HMul.hMul (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
    (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
Tactic: simp_rw [← coe_mul, extension_coe hf, f.map_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_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
a_1 b_1 : Completion α
a b : α
simp_rw :
  Completion.extension (⇑f : (a : α) → β) (↑(a * b) : Completion α) =
    HMul.hMul (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
⊢ Completion.extension (⇑f : (a : α) → β) (HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α)) =
    HMul.hMul (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
have simp_rw₁ : (f : (a : α) → β) (a * b) = HMul.hMul (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
Tactic: simp_rw [← coe_mul, extension_coe hf, f.map_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_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ Eq.{u + 1} (α := β) (Completion.extension.{u_1, u} (α := α) (⇑f : (a : α) → β) 0) 0
have simp_rw : Eq.{u + 1} (α := β) (Completion.extension.{u_1, u} (α := α) (⇑f : (a : α) → β) (↑0 : Completion α)) 0
Tactic: simp_rw [← coe_zero, extension_coe hf, f.map_zero]
-- 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_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
simp_rw : Eq.{u + 1} (α := β) (Completion.extension.{u_1, u} (α := α) (⇑f : (a : α) → β) (↑0 : Completion α)) 0
⊢ Eq.{u + 1} (α := β) (Completion.extension.{u_1, u} (α := α) (⇑f : (a : α) → β) 0) 0
have simp_rw₁ : Eq.{u + 1} (α := β) ((f : (a : α) → β) 0 : β) (0 : β)
Tactic: simp_rw [← coe_zero, extension_coe hf, f.map_zero]
-- 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_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
a_1 b_1 : Completion α
a b : α
⊢ Completion.extension (⇑f : (a : α) → β) (HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α)) =
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
have simp_rw : Completion.extension (⇑f : (a : α) → β) (↑(a + b) : Completion α) =
  HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
    (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
Tactic: simp_rw [← coe_add, extension_coe hf, f.map_add]
-- 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_1 : Continuous.{u_1, u} (X := α) (Y := β) (⇑f : (a : α) → β)
inst_8 : CompleteSpace β
inst_9 : T0Space β
hf' : Continuous.{u_1, u} (X := α) (Y := β) (⇑(↑f : α →+ β) : (a : α) → β)
hf : UniformContinuous.{u_1, u} (α := α) (β := β) (⇑f : (a : α) → β)
a_1 b_1 : Completion α
a b : α
simp_rw :
  Completion.extension (⇑f : (a : α) → β) (↑(a + b) : Completion α) =
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
⊢ Completion.extension (⇑f : (a : α) → β) (HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α)) =
    HAdd.hAdd (α := β) (Completion.extension (⇑f : (a : α) → β) (↑a : Completion α))
      (Completion.extension (⇑f : (a : α) → β) (↑b : Completion α))
have simp_rw₁ : (f : (a : α) → β) (a + b) = HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
Tactic: simp_rw [← coe_add, extension_coe hf, f.map_add]