awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 : Completion α
a : α
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) 0 = (↑a : Completion α)
have rw : HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑0 : Completion α) = (↑a : Completion α)
Tactic: rw [← coe_zero, ← coe_add, add_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 : Completion α
a : α
rw : HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑0 : Completion α) = (↑a : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) 0 = (↑a : Completion α)
have rw₁ : Eq (α := Completion α) (↑(a + 0) : Completion α) (↑a : Completion α)
Tactic: rw [← coe_zero, ← coe_add, add_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 : Completion α
a : α
rw : HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑0 : Completion α) = (↑a : Completion α)
rw₁ : Eq (α := Completion α) (↑(a + 0) : Completion α) (↑a : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) 0 = (↑a : Completion α)
have rw₂ : Eq (α := Completion α) (↑a : Completion α) (↑a : Completion α)
Tactic: rw [← coe_zero, ← coe_add, add_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 : Completion α
a : α
⊢ HSMul.hSMul (α := ℕ) (β := Completion α) 0 (↑a : Completion α) = 0
have rw : Eq (α := Completion α) (↑(HSMul.hSMul (α := ℕ) 0 a) : Completion α) 0
Tactic: rw [← coe_smul, ← coe_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 : Completion α
a : α
rw : Eq (α := Completion α) (↑(HSMul.hSMul (α := ℕ) 0 a) : Completion α) 0
⊢ HSMul.hSMul (α := ℕ) (β := Completion α) 0 (↑a : Completion α) = 0
have rw₁ : Eq (α := Completion α) (↑(HSMul.hSMul (α := ℕ) 0 a) : Completion α) (↑0 : Completion α)
Tactic: rw [← coe_smul, ← coe_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 : Completion α
a : α
rw : Eq (α := Completion α) (↑(HSMul.hSMul (α := ℕ) 0 a) : Completion α) 0
rw₁ : Eq (α := Completion α) (↑(HSMul.hSMul (α := ℕ) 0 a) : Completion α) (↑0 : Completion α)
⊢ HSMul.hSMul (α := ℕ) (β := Completion α) 0 (↑a : Completion α) = 0
have rw₂ : Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) (↑0 : Completion α)
Tactic: rw [← coe_smul, ← coe_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
n : ℕ
a_1 : Completion α
a : α
⊢ HSMul.hSMul (β := Completion α) (n + 1) (↑a : Completion α) =
    HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α)
have rw : (↑((n + 1) • a) : Completion α) = HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α)
Tactic: rw [← coe_smul, succ_nsmul, coe_add, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
n : ℕ
a_1 : Completion α
a : α
rw : (↑((n + 1) • a) : Completion α) = HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α)
⊢ HSMul.hSMul (β := Completion α) (n + 1) (↑a : Completion α) =
    HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α)
have rw₁ : (↑(n • a + a) : Completion α) = HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α)
Tactic: rw [← coe_smul, succ_nsmul, coe_add, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
n : ℕ
a_1 : Completion α
a : α
rw : (↑((n + 1) • a) : Completion α) = HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α)
rw₁ : (↑(n • a + a) : Completion α) = HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α)
⊢ HSMul.hSMul (β := Completion α) (n + 1) (↑a : Completion α) =
    HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α)
have rw₂ : HAdd.hAdd (α := Completion α) (↑(n • a) : Completion α) (↑a : Completion α) =
  HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α)
Tactic: rw [← coe_smul, succ_nsmul, coe_add, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
n : ℕ
a_1 : Completion α
a : α
rw : (↑((n + 1) • a) : Completion α) = HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α)
rw₁ : (↑(n • a + a) : Completion α) = HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α)
rw₂ :
  HAdd.hAdd (α := Completion α) (↑(n • a) : Completion α) (↑a : Completion α) =
    HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α)
⊢ HSMul.hSMul (β := Completion α) (n + 1) (↑a : Completion α) =
    HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α)
have rw₃ : HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α) =
  HSMul.hSMul (β := Completion α) n (↑a : Completion α) + (↑a : Completion α)
Tactic: rw [← coe_smul, succ_nsmul, coe_add, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 : Completion α
a : α
⊢ HSMul.hSMul (α := ℤ) (β := Completion α) 0 (↑a : Completion α) = 0
have rw : Eq (α := Completion α) (↑(HSMul.hSMul (α := ℤ) 0 a) : Completion α) 0
Tactic: rw [← coe_smul, ← coe_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 : Completion α
a : α
rw : Eq (α := Completion α) (↑(HSMul.hSMul (α := ℤ) 0 a) : Completion α) 0
⊢ HSMul.hSMul (α := ℤ) (β := Completion α) 0 (↑a : Completion α) = 0
have rw₁ : Eq (α := Completion α) (↑(HSMul.hSMul (α := ℤ) 0 a) : Completion α) (↑0 : Completion α)
Tactic: rw [← coe_smul, ← coe_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 : Completion α
a : α
rw : Eq (α := Completion α) (↑(HSMul.hSMul (α := ℤ) 0 a) : Completion α) 0
rw₁ : Eq (α := Completion α) (↑(HSMul.hSMul (α := ℤ) 0 a) : Completion α) (↑0 : Completion α)
⊢ HSMul.hSMul (α := ℤ) (β := Completion α) 0 (↑a : Completion α) = 0
have rw₂ : Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) (↑0 : Completion α)
Tactic: rw [← coe_smul, ← coe_zero, zero_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
n : ℕ
a_1 : Completion α
a : α
⊢ HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α) =
    HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α)
have rw : (↑(HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a) : Completion α) =
  HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α)
Tactic: rw [← coe_smul, show (n.succ : ℤ) • a = (n : ℤ) • a + a from
              SubNegMonoid.zsmul_succ' n a, coe_add, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
n : ℕ
a_1 : Completion α
a : α
rw :
  (↑(HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a) : Completion α) =
    HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α)
⊢ HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α) =
    HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α)
have rw₁ : (↑(HSMul.hSMul (α := ℤ) (↑n : ℤ) a + a) : Completion α) =
  HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α)
Tactic: rw [← coe_smul, show (n.succ : ℤ) • a = (n : ℤ) • a + a from
              SubNegMonoid.zsmul_succ' n a, coe_add, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
n : ℕ
a_1 : Completion α
a : α
rw :
  (↑(HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a) : Completion α) =
    HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α)
rw₁ :
  (↑(HSMul.hSMul (α := ℤ) (↑n : ℤ) a + a) : Completion α) =
    HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α)
⊢ HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α) =
    HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α)
have rw₂ : HAdd.hAdd (α := Completion α) (↑(HSMul.hSMul (α := ℤ) (↑n : ℤ) a) : Completion α) (↑a : Completion α) =
  HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α)
Tactic: rw [← coe_smul, show (n.succ : ℤ) • a = (n : ℤ) • a + a from
              SubNegMonoid.zsmul_succ' n a, coe_add, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
n : ℕ
a_1 : Completion α
a : α
rw :
  (↑(HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a) : Completion α) =
    HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α)
rw₁ :
  (↑(HSMul.hSMul (α := ℤ) (↑n : ℤ) a + a) : Completion α) =
    HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α)
rw₂ :
  HAdd.hAdd (α := Completion α) (↑(HSMul.hSMul (α := ℤ) (↑n : ℤ) a) : Completion α) (↑a : Completion α) =
    HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α)
⊢ HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α) =
    HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α)
have rw₃ : HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α) =
  HSMul.hSMul (α := ℤ) (β := Completion α) (↑n : ℤ) (↑a : Completion α) + (↑a : Completion α)
Tactic: rw [← coe_smul, show (n.succ : ℤ) • a = (n : ℤ) • a + a from
              SubNegMonoid.zsmul_succ' n a, coe_add, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
n : ℕ
a_1 : Completion α
a : α
⊢ HSMul.hSMul (β := Completion α) (Int.negSucc n) (↑a : Completion α) =
    -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α)
have rw : (↑(Int.negSucc n • a) : Completion α) = -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α)
Tactic: rw [← coe_smul, show (Int.negSucc n) • a = -((n.succ : ℤ) • a) from
              SubNegMonoid.zsmul_neg' n a, coe_neg, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
n : ℕ
a_1 : Completion α
a : α
rw : (↑(Int.negSucc n • a) : Completion α) = -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α)
⊢ HSMul.hSMul (β := Completion α) (Int.negSucc n) (↑a : Completion α) =
    -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α)
have rw₁ : (↑(-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a) : Completion α) =
  -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α)
Tactic: rw [← coe_smul, show (Int.negSucc n) • a = -((n.succ : ℤ) • a) from
              SubNegMonoid.zsmul_neg' n a, coe_neg, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
n : ℕ
a_1 : Completion α
a : α
rw : (↑(Int.negSucc n • a) : Completion α) = -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α)
rw₁ :
  (↑(-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a) : Completion α) =
    -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α)
⊢ HSMul.hSMul (β := Completion α) (Int.negSucc n) (↑a : Completion α) =
    -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α)
have rw₂ : -(↑(HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a) : Completion α) =
  -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α)
Tactic: rw [← coe_smul, show (Int.negSucc n) • a = -((n.succ : ℤ) • a) from
              SubNegMonoid.zsmul_neg' n a, coe_neg, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
n : ℕ
a_1 : Completion α
a : α
rw : (↑(Int.negSucc n • a) : Completion α) = -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α)
rw₁ :
  (↑(-HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a) : Completion α) =
    -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α)
rw₂ :
  -(↑(HSMul.hSMul (α := ℤ) (↑n.succ : ℤ) a) : Completion α) =
    -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α)
⊢ HSMul.hSMul (β := Completion α) (Int.negSucc n) (↑a : Completion α) =
    -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α)
have rw₃ : -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α) =
  -HSMul.hSMul (α := ℤ) (β := Completion α) (↑n.succ : ℤ) (↑a : Completion α)
Tactic: rw [← coe_smul, show (Int.negSucc n) • a = -((n.succ : ℤ) • a) from
              SubNegMonoid.zsmul_neg' n a, coe_neg, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a_1 : Completion α
a : α
⊢ HAdd.hAdd (α := Completion α) (-(↑a : Completion α)) (↑a : Completion α) = 0
have rw_mod_cast : Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) 0
Tactic: rw_mod_cast [neg_add_cancel]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M_1 : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
M : Type u_5
inst_3 : Monoid M
inst_4 : DistribMulAction M α
inst_5 : UniformContinuousConstSMul M α
r : M
⊢ HSMul.hSMul (β := Completion α) r 0 = 0
have rw : HSMul.hSMul (β := Completion α) r (↑0 : Completion α) = (↑0 : Completion α)
Tactic: rw [← coe_zero, ← coe_smul, smul_zero r]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M_1 : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
M : Type u_5
inst_3 : Monoid M
inst_4 : DistribMulAction M α
inst_5 : UniformContinuousConstSMul M α
r : M
rw : HSMul.hSMul (β := Completion α) r (↑0 : Completion α) = (↑0 : Completion α)
⊢ HSMul.hSMul (β := Completion α) r 0 = 0
have rw₁ : Eq (α := Completion α) (↑(HSMul.hSMul (β := α) r 0) : Completion α) (↑0 : Completion α)
Tactic: rw [← coe_zero, ← coe_smul, smul_zero r]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M_1 : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
M : Type u_5
inst_3 : Monoid M
inst_4 : DistribMulAction M α
inst_5 : UniformContinuousConstSMul M α
r : M
rw : HSMul.hSMul (β := Completion α) r (↑0 : Completion α) = (↑0 : Completion α)
rw₁ : Eq (α := Completion α) (↑(HSMul.hSMul (β := α) r 0) : Completion α) (↑0 : Completion α)
⊢ HSMul.hSMul (β := Completion α) r 0 = 0
have rw₂ : Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) (↑0 : Completion α)
Tactic: rw [← coe_zero, ← coe_smul, smul_zero r]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
a b : Completion α
x y : α
⊢ HAdd.hAdd (α := Completion α) (↑x : Completion α) (↑y : Completion α) =
    HAdd.hAdd (α := Completion α) (↑y : Completion α) (↑x : Completion α)
have rw : (↑(x + y) : Completion α) = HAdd.hAdd (α := Completion α) (↑y : Completion α) (↑x : Completion α)
Tactic: rw [← coe_add, ← coe_add, add_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
a b : Completion α
x y : α
rw : (↑(x + y) : Completion α) = HAdd.hAdd (α := Completion α) (↑y : Completion α) (↑x : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑x : Completion α) (↑y : Completion α) =
    HAdd.hAdd (α := Completion α) (↑y : Completion α) (↑x : Completion α)
have rw₁ : Eq (α := Completion α) (↑(x + y) : Completion α) (↑(y + x) : Completion α)
Tactic: rw [← coe_add, ← coe_add, add_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
a b : Completion α
x y : α
rw : (↑(x + y) : Completion α) = HAdd.hAdd (α := Completion α) (↑y : Completion α) (↑x : Completion α)
rw₁ : Eq (α := Completion α) (↑(x + y) : Completion α) (↑(y + x) : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑x : Completion α) (↑y : Completion α) =
    HAdd.hAdd (α := Completion α) (↑y : Completion α) (↑x : Completion α)
have rw₂ : Eq (α := Completion α) (↑(y + x) : Completion α) (↑(y + x) : Completion α)
Tactic: rw [← coe_add, ← coe_add, add_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
inst_3 : Semiring R
inst_4 : Module R α
inst_5 : UniformContinuousConstSMul R α
a b : R
x : α
⊢ HSMul.hSMul (β := Completion α) (a + b) (↑x : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
have rw : (↑((a + b) • x) : Completion α) =
  HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
Tactic: rw [← coe_smul, add_smul, coe_add, coe_smul, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
inst_3 : Semiring R
inst_4 : Module R α
inst_5 : UniformContinuousConstSMul R α
a b : R
x : α
rw :
  (↑((a + b) • x) : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
⊢ HSMul.hSMul (β := Completion α) (a + b) (↑x : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
have rw₁ : (↑(a • x + b • x) : Completion α) =
  HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
Tactic: rw [← coe_smul, add_smul, coe_add, coe_smul, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
inst_3 : Semiring R
inst_4 : Module R α
inst_5 : UniformContinuousConstSMul R α
a b : R
x : α
rw :
  (↑((a + b) • x) : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
rw₁ :
  (↑(a • x + b • x) : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
⊢ HSMul.hSMul (β := Completion α) (a + b) (↑x : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
have rw₂ : HAdd.hAdd (α := Completion α) (↑(a • x) : Completion α) (↑(b • x) : Completion α) =
  HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
Tactic: rw [← coe_smul, add_smul, coe_add, coe_smul, coe_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.GroupCompletion (goal)
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddCommGroup α
inst_2 : IsUniformAddGroup α
inst_3 : Semiring R
inst_4 : Module R α
inst_5 : UniformContinuousConstSMul R α
a b : R
x : α
rw :
  (↑((a + b) • x) : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
rw₁ :
  (↑(a • x + b • x) : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
rw₂ :
  HAdd.hAdd (α := Completion α) (↑(a • x) : Completion α) (↑(b • x) : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
⊢ HSMul.hSMul (β := Completion α) (a + b) (↑x : Completion α) =
    HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
have rw₃ : HSMul.hSMul (β := Completion α) a (↑x : Completion α) + (↑(b • x) : Completion α) =
  HSMul.hSMul (β := Completion α) a (↑x : Completion α) + HSMul.hSMul (β := Completion α) b (↑x : Completion α)
Tactic: rw [← coe_smul, add_smul, coe_add, coe_smul, coe_smul]