awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
refine : x ∈ closure[inst_1] (↑(Submonoid.powers x⁻¹) : Set G)
⊢ x ∈ (↑(Submonoid.topologicalClosure (Submonoid.closure s)) : Set G)

Tactic:
refine closure_mono (Submonoid.powers_le.2 (Submonoid.subset_closure <| Set.mem_inv.1 hx)) ?_

Premises used: Iff.mpr, closure_mono, Iff.mp, Submonoid.subset_closure, Submonoid.powers_le, Set.mem_inv
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
rw : Membership.mem (γ := Subgroup G) (Subgroup.topologicalClosure (Subgroup.zpowers x⁻¹)) x⁻¹
⊢ x ∈ closure[inst_1] (↑(Submonoid.powers x⁻¹) : Set G)

Tactic:
rw [Submonoid.coe_powers, ← closure_range_zpow_eq_pow, ← Subgroup.coe_zpowers,
    ← Subgroup.topologicalClosure_coe, SetLike.mem_coe, ← inv_mem_iff]

Premises used: inv_mem_iff, Subgroup.topologicalClosure_coe, SetLike.mem_coe, closure_range_zpow_eq_pow, Subgroup.coe_zpowers, Submonoid.coe_powers
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ Membership.mem (γ := Subgroup G) (Subgroup.topologicalClosure (Subgroup.zpowers x⁻¹)) x⁻¹

Tactic:
subset_closure <| Subgroup.mem_zpowers _

Premises used: Set.Mem, subset_closure, setOf, Subgroup.mem_zpowers, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
s : Set G
x : G
hx : x ∈ s⁻¹
⊢ Membership.mem (γ := Subgroup G) (Subgroup.topologicalClosure (Subgroup.zpowers x⁻¹)) x⁻¹

Tactic:
exact subset_closure <| Subgroup.mem_zpowers _

Premises used: subset_closure, Subgroup.mem_zpowers
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
s : Set G
⊢ closure[inst_1] (↑(Submonoid.closure s) : Set G) = closure[inst_1] (↑(Subgroup.closure s) : Set G)

Tactic:
congrArg SetLike.coe (topologicalClosure_subgroupClosure_toSubmonoid s).symm

Premises used: congrArg, Set.Mem, setOf, topologicalClosure_subgroupClosure_toSubmonoid, SetLike.coe, closure, Eq.symm, Set.sInter
-- Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : CompactSpace G
inst_3 : IsTopologicalGroup G
s : Set G
⊢ Dense (↑(Submonoid.closure s) : Set G) ↔ Dense (↑(Subgroup.closure s) : Set G)

Tactic:
simp only [dense_iff_closure_eq, closure_submonoidClosure_eq_closure_subgroupClosure]

Premises used: dense_iff_closure_eq, closure_submonoidClosure_eq_closure_subgroupClosure
-- Module: Mathlib.Topology.Algebra.Group.TopologicalAbelianization
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
⊢ Subgroup.Normal (Subgroup.topologicalClosure (commutator G))

Tactic:
Subgroup.is_normal_topologicalClosure (commutator G)

Premises used: commutator, Subgroup.is_normal_topologicalClosure
-- Module: Mathlib.Topology.Algebra.Group.TopologicalAbelianization
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x y : G_ab G
a b : G
⊢ (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆

Tactic:
group
-- Module: Mathlib.Topology.Algebra.Group.TopologicalAbelianization
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x y : G_ab G
a b : G
⊢ (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆

Tactic:
have h : (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆ := by group
-- Module: Mathlib.Topology.Algebra.Group.TopologicalAbelianization
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x y : G_ab G
a b : G
h : (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆
rw : Membership.mem (γ := Subgroup G) (Subgroup.topologicalClosure (commutator G)) ⁅b⁻¹, a⁻¹⁆
⊢ Membership.mem (γ := Subgroup G) (Subgroup.topologicalClosure (commutator G))
    (HMul.hMul (α := G) ((fun (x1 x2 : G) ↦ x1 * x2) a b)⁻¹ ((fun (x1 x2 : G) ↦ x1 * x2) b a))

Tactic:
rw [h]
-- Module: Mathlib.Topology.Algebra.Group.TopologicalAbelianization
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x y : G_ab G
a b : G
h : (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆
⊢ Membership.mem (γ := Subgroup G) (Subgroup.topologicalClosure (commutator G)) ⁅b⁻¹, a⁻¹⁆

Tactic:
Subgroup.le_topologicalClosure _ (Subgroup.commutator_mem_commutator
            (Subgroup.mem_top b⁻¹) (Subgroup.mem_top a⁻¹))

Premises used: Subgroup.le_topologicalClosure, Subgroup.commutator_mem_commutator, Inv.inv, Subgroup.mem_top
-- Module: Mathlib.Topology.Algebra.Group.TopologicalAbelianization
Goal:
G : Type u_1
inst : Group G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
x y : G_ab G
a b : G
h : (a * b)⁻¹ * (b * a) = ⁅b⁻¹, a⁻¹⁆
⊢ Membership.mem (γ := Subgroup G) (Subgroup.topologicalClosure (commutator G)) ⁅b⁻¹, a⁻¹⁆

Tactic:
exact Subgroup.le_topologicalClosure _ (Subgroup.commutator_mem_commutator
            (Subgroup.mem_top b⁻¹) (Subgroup.mem_top a⁻¹))

Premises used: Subgroup.le_topologicalClosure, Subgroup.commutator_mem_commutator, Inv.inv, Subgroup.mem_top
-- Module: Mathlib.Topology.Algebra.Group.Units
Goal:
M : Type u_1
inst : TopologicalSpace M
inst_1 : Monoid M
U : Submonoid M
hU : IsOpen (↑U : Set M)
⊢ IsOpen (↑U.units : Set Mˣ)

Tactic:
(hU.preimage Units.continuous_val).inter (hU.preimage Units.continuous_coe_inv)

Premises used: Set.Mem, Units.continuous_val, setOf, Set.inter, Set.preimage, IsOpen.inter, Units.continuous_coe_inv, IsOpen.preimage
-- Module: Mathlib.Topology.Algebra.Group.Units
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Monoid M
inst_3 : Monoid N
f : M ≃ₜ* N
⊢ (mapContinuousMulEquiv f).symm = mapContinuousMulEquiv f.symm

Tactic:
rfl

Premises used: Units.mapEquiv, ContinuousMulEquiv.symm, Equiv.symm, MulEquiv.symm, rfl, Units.mapContinuousMulEquiv
-- Module: Mathlib.Topology.Algebra.Group.Units
Goal:
M : Type u_1
N : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace N
inst_2 : Monoid M
inst_3 : Monoid N
f : M ≃ₜ* N
⊢ (↑(mapContinuousMulEquiv f) : Mˣ ≃* Nˣ) = mapEquiv (↑f : M ≃* N)

Tactic:
rfl

Premises used: Units.mapEquiv, MulEquivClass.toMulEquiv, EquivLike.toEquiv, rfl
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
α : Type u_3
inst : UniformSpace α
inst_1 : Zero α
⊢ Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
α : Type u_3
inst : UniformSpace α
inst_1 : Zero α
inst_2 : T0Space α
x : α
⊢ Eq (α := Completion α) (↑x : Completion α) 0 ↔ x = 0

Tactic:
Completion.coe_inj

Premises used: UniformSpace.Completion.coe_inj
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : MonoidWithZero M
inst_2 : Zero α
inst_3 : MulActionWithZero M α
inst_4 : UniformContinuousConstSMul M α
r : M
rw : HSMul.hSMul (β := Completion α) r (↑0 : Completion α) = (↑0 : Completion α)
rw₁ : Eq (α := Completion α) (↑(HSMul.hSMul (β := α) r 0) : Completion α) (↑0 : Completion α)
rw₂ rw₃ : Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) (↑0 : Completion α)
⊢ HSMul.hSMul (β := Completion α) r 0 = 0

Tactic:
rw [← coe_zero, ← coe_smul, MulActionWithZero.smul_zero r]

Premises used: MulActionWithZero.smul_zero, UniformSpace.Completion.coe_zero, UniformSpace.Completion.coe_smul
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : MonoidWithZero M
inst_2 : Zero α
inst_3 : MulActionWithZero M α
inst_4 : UniformContinuousConstSMul M α
a : α
rw : Eq (α := Completion α) (↑(HSMul.hSMul.{u_1, u_3, u_3} (α := M) 0 a) : Completion α) 0
rw₁ : Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := Completion α) 0 0
⊢ HSMul.hSMul.{u_1, u_3, u_3} (α := M) (β := Completion α) 0 (↑a : Completion α) = 0

Tactic:
rw [← coe_smul, zero_smul, coe_zero]

Premises used: UniformSpace.Completion.coe_zero, zero_smul, UniformSpace.Completion.coe_smul
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
α : Type u_3
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a : α
⊢ Eq (α := Completion α) (↑(-a) : Completion α) (-(↑a : Completion α))

Tactic:
(map_coe uniformContinuous_neg a).symm

Premises used: uniformContinuous_neg, UniformSpace.Completion.map_coe, Eq.symm
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
α : Type u_3
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a b : α
⊢ (↑(a - b) : Completion α) = HSub.hSub (α := Completion α) (↑a : Completion α) (↑b : Completion α)

Tactic:
(map₂_coe_coe a b Sub.sub uniformContinuous_sub).symm

Premises used: UniformSpace.Completion.map₂_coe_coe, uniformContinuous_sub, Sub.sub, Eq.symm
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
α : Type u_3
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a b : α
⊢ (↑(a + b) : Completion α) = HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α)

Tactic:
(map₂_coe_coe a b (· + ·) uniformContinuous_add).symm

Premises used: uniformContinuous_add, UniformSpace.Completion.map₂_coe_coe, HAdd.hAdd, Eq.symm
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a b c : Completion α
⊢ Continuous (Y := Completion α) fun (x : Completion α × Completion α × Completion α) ↦ x.2.1

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
a b c : Completion α
⊢ Continuous (Y := Completion α) fun (x : Completion α × Completion α × Completion α) ↦ x.2.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 b_1 c_1 : Completion α
a b c : α
rw_mod_cast rw_mod_cast₁ rw_mod_cast₂ rw_mod_cast₃ rw_mod_cast₄ rw_mod_cast₅ :
  Eq (α := Completion α) (↑(a + b + c) : Completion α) (↑(a + (b + c)) : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α) + (↑c : Completion α) =
    (↑a : Completion α) + HAdd.hAdd (α := Completion α) (↑b : Completion α) (↑c : Completion α)

Tactic:
rw_mod_cast [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 b_1 c_1 : Completion α
a b c : α
repeat' repeat'₁ repeat'₂ repeat'₃ repeat'₄ repeat'₅ :
  Eq (α := Completion α) (↑(a + b + c) : Completion α) (↑(a + (b + c)) : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α) + (↑c : Completion α) =
    (↑a : Completion α) + HAdd.hAdd (α := Completion α) (↑b : Completion α) (↑c : Completion α)

Tactic:
repeat' rw_mod_cast [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α) (↑0 : Completion α) (↑a : Completion α) = (↑a : Completion α)
rw₁ : Eq (α := Completion α) (↑(0 + a) : Completion α) (↑a : Completion α)
rw₂ rw₃ : Eq (α := Completion α) (↑a : Completion α) (↑a : Completion α)
⊢ HAdd.hAdd (α := Completion α) 0 (↑a : Completion α) = (↑a : Completion α)

Tactic:
rw [← coe_zero, ← coe_add, zero_add]

Premises used: zero_add, UniformSpace.Completion.coe_zero, UniformSpace.Completion.coe_add
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α)
rw₂ rw₃ : Eq (α := Completion α) (↑a : Completion α) (↑a : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑a : Completion α) 0 = (↑a : Completion α)

Tactic:
rw [← coe_zero, ← coe_add, add_zero]

Premises used: UniformSpace.Completion.coe_zero, add_zero, UniformSpace.Completion.coe_add
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α)
rw₂ rw₃ : Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) (↑0 : Completion α)
⊢ HSMul.hSMul (α := ℕ) (β := Completion α) 0 (↑a : Completion α) = 0

Tactic:
rw [← coe_smul, ← coe_zero, zero_smul]

Premises used: UniformSpace.Completion.coe_zero, zero_smul, UniformSpace.Completion.coe_smul
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α)
rw₃ rw₄ :
  HSMul.hSMul (β := 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 α)

Tactic:
rw [← coe_smul, succ_nsmul, coe_add, coe_smul]

Premises used: UniformSpace.Completion.coe_smul, UniformSpace.Completion.coe_add, succ_nsmul
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α)
rw₂ rw₃ : Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) (↑0 : Completion α)
⊢ HSMul.hSMul (α := ℤ) (β := Completion α) 0 (↑a : Completion α) = 0

Tactic:
rw [← coe_smul, ← coe_zero, zero_smul]

Premises used: UniformSpace.Completion.coe_zero, zero_smul, UniformSpace.Completion.coe_smul
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α)
rw₃ rw₄ :
  HSMul.hSMul (α := ℤ) (β := Completion α) (↑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 α)

Tactic:
rw [← coe_smul, show (n.succ : ℤ) • a = (n : ℤ) • a + a from
              SubNegMonoid.zsmul_succ' n a, coe_add, coe_smul]

Premises used: SubNegMonoid.zsmul_succ', UniformSpace.Completion.coe_smul, UniformSpace.Completion.coe_add
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α)
rw₃ rw₄ :
  -HSMul.hSMul (α := ℤ) (β := Completion α) (↑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 α)

Tactic:
rw [← coe_smul, show (Int.negSucc n) • a = -((n.succ : ℤ) • a) from
              SubNegMonoid.zsmul_neg' n a, coe_neg, coe_smul]

Premises used: UniformSpace.Completion.coe_neg, UniformSpace.Completion.coe_smul, SubNegMonoid.zsmul_neg'
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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_mod_cast : Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) 0
⊢ HAdd.hAdd (α := Completion α) (-(↑a : Completion α)) (↑a : Completion α) = 0

Tactic:
rw_mod_cast [neg_add_cancel]

Premises used: neg_add_cancel
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 : α
⊢ Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) 0

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
⊢ IsUniformAddGroup.{u_3} (Completion α)

Tactic:
⟨uniformContinuous_map₂ Sub.sub⟩

Premises used: UniformSpace.Completion.uniformContinuous_map₂, Sub.sub, IsUniformAddGroup.mk
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α)
rw₂ rw₃ : Eq.{u_3 + 1} (α := Completion α) (↑0 : Completion α) (↑0 : Completion α)
⊢ HSMul.hSMul (β := Completion α) r 0 = 0

Tactic:
rw [← coe_zero, ← coe_smul, smul_zero r]

Premises used: smul_zero, UniformSpace.Completion.coe_zero, UniformSpace.Completion.coe_smul
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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
x y : Completion α
a b : α
⊢ r • HAdd.hAdd (α := Completion α) (↑a : Completion α) (↑b : Completion α) =
    HSMul.hSMul (β := Completion α) r (↑a : Completion α) + HSMul.hSMul (β := Completion α) r (↑b : Completion α)

Tactic:
simp only [← coe_add, ← coe_smul, smul_add]

Premises used: UniformSpace.Completion.coe_smul, smul_add, UniformSpace.Completion.coe_add
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
α : Type u_3
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
⊢ Continuous.{u_3, u_3} (X := α) (Y := Completion α) (⇑toCompl : (a : α) → Completion α)

Tactic:
continuous_coe α

Premises used: UniformSpace.Completion.coe', UniformSpace.Completion.continuous_coe, SeparationQuotient.mk
-- Module: Mathlib.Topology.Algebra.GroupCompletion
Goal:
α : Type u_3
inst : UniformSpace α
inst_1 : AddGroup α
inst_2 : IsUniformAddGroup α
⊢ IsDenseInducing.{u_3, u_3} (α := α) (β := Completion α) (⇑toCompl : (a : α) → Completion α)

Tactic:
isDenseInducing_coe

Premises used: UniformSpace.Completion.coe', SeparationQuotient.mk, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α
⊢ Continuous (Y := Completion α) fun (x : Completion α × Completion α) ↦ x.1 + x.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α
⊢ Continuous (Y := Completion α) fun (x : Completion α × Completion α) ↦ x.2 + x.1

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 : α
change :
  HAdd.hAdd (α := Completion α) (↑x : Completion α) (↑y : Completion α) =
    HAdd.hAdd (α := Completion α) (↑y : Completion α) (↑x : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑x : Completion α) (↑y : Completion α) =
    HAdd.hAdd (α := Completion α) (↑y : Completion α) (↑x : Completion α)

Tactic:
change (x : Completion α) + ↑y = ↑y + ↑x

Premises used: UniformSpace.Completion.coe'
-- Module: Mathlib.Topology.Algebra.GroupCompletion
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 α)
rw₂ rw₃ : Eq (α := Completion α) (↑(y + x) : Completion α) (↑(y + x) : Completion α)
⊢ HAdd.hAdd (α := Completion α) (↑x : Completion α) (↑y : Completion α) =
    HAdd.hAdd (α := Completion α) (↑y : Completion α) (↑x : Completion α)

Tactic:
rw [← coe_add, ← coe_add, add_comm]

Premises used: add_comm, UniformSpace.Completion.coe_add