awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformFilterBasis (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mp : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₁ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₁ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₂ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₂ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₃ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₃ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
have mp₄ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
Tactic: constructor <;> rintro ⟨h', h⟩ <;> refine ⟨h', ?_⟩ <;> [rwa [← this]; rwa [this]]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformFilterBasis (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mp : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₁ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₁ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₂ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₂ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₃ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₃ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₄ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
have mpr₄ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), Cauchy F
Tactic: constructor <;> rintro ⟨h', h⟩ <;> refine ⟨h', ?_⟩ <;> [rwa [← this]; rwa [this]]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformFilterBasis (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mp : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₁ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₁ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₂ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₂ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₃ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₃ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₄ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₄ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), Cauchy F
mp₅ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₅ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), Cauchy F
mp₆ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₆ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), Cauchy F
mp₇ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₇ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), Cauchy F
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
have mp₈ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
Tactic: constructor <;> rintro ⟨h', h⟩ <;> refine ⟨h', ?_⟩ <;> [rwa [← this]; rwa [this]]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformFilterBasis (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mp : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₁ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₁ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₂ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₂ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₃ : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₃ : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
mp₄ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₄ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), Cauchy F
mp₅ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₅ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), Cauchy F
mp₆ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₆ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), Cauchy F
mp₇ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mpr₇ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), Cauchy F
mp₈ : ∀ (h' : F.NeBot) (h : F ×ˢ F ≤ uniformity G), ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
have mpr₈ : ∀ (h' : F.NeBot) (h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U), F ×ˢ F ≤ uniformity G
Tactic: constructor <;> rintro ⟨h', h⟩ <;> refine ⟨h', ?_⟩ <;> [rwa [← this]; rwa [this]]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformFilterBasis (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this : IsUniformAddGroup G
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
have suffices : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
Tactic: suffices F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ᵉ (x ∈ M) (y ∈ M), y - x ∈ U by
    constructor <;> rintro ⟨h', h⟩ <;> refine ⟨h', ?_⟩ <;> [rwa [← this]; rwa [this]]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformFilterBasis (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this : IsUniformAddGroup G
⊢ F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
have rw : LE.le (α := Filter G) (map (fun (x : G × G) ↦ x.2 - x.1) (F ×ˢ F)) (nhds 0) ↔
  ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
Tactic: rw [uniformity_eq_comap_nhds_zero G, ← map_le_iff_le_comap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformMulAction (hypothesis)
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : SMul M X
inst_3 : SMul N X
inst_4 : SMul M N
inst_5 : UniformContinuousConstSMul M X
inst_6 : UniformContinuousConstSMul N X
inst_7 : IsScalarTower M N X
m : M
n : N
x : Completion X
⊢ (m • n) • x = m • n • x
have this : Eq.{x + 1} (α := Completion X → Completion X)
  (Function.comp (β := Completion X) (Completion.map fun (x : X) ↦ m • x) (Completion.map fun (x : X) ↦ n • x))
  (Completion.map ((fun (x : X) ↦ m • x) ∘ fun (x : X) ↦ n • x))
Tactic: have : _ = (_ : Completion X → Completion X) :=
      map_comp (uniformContinuous_const_smul m) (uniformContinuous_const_smul n)
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformMulAction (goal)
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : SMul M X
inst_3 : SMul N X
inst_4 : SMul M N
inst_5 : UniformContinuousConstSMul M X
inst_6 : UniformContinuousConstSMul N X
inst_7 : IsScalarTower M N X
m : M
n : N
x : Completion X
this :
  Eq.{x + 1} (α := Completion X → Completion X)
    (Function.comp (β := Completion X) (Completion.map fun (x : X) ↦ m • x) (Completion.map fun (x : X) ↦ n • x))
    (Completion.map ((fun (x : X) ↦ m • x) ∘ fun (x : X) ↦ n • x))
⊢ (m • n) • x = m • n • x
have refine : (m • n) • x = Completion.map ((fun (x : X) ↦ m • x) ∘ fun (x : X) ↦ n • x) x
Tactic: refine Eq.trans ?_ (congr_fun this.symm x)
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformMulAction (hypothesis)
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : SMul M X
inst_3 : SMul N X
inst_4 : SMulCommClass M N X
inst_5 : UniformContinuousConstSMul M X
inst_6 : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
⊢ m • n • x = n • m • x
have hmn : m • n • x = Function.comp (β := Completion X) (Completion.map (SMul.smul m)) (Completion.map (SMul.smul n)) x
Tactic: have hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x := rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformMulAction (hypothesis)
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : SMul M X
inst_3 : SMul N X
inst_4 : SMulCommClass M N X
inst_5 : UniformContinuousConstSMul M X
inst_6 : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = Function.comp (β := Completion X) (Completion.map (SMul.smul m)) (Completion.map (SMul.smul n)) x
⊢ m • n • x = n • m • x
have hnm : n • m • x = Function.comp (β := Completion X) (Completion.map (SMul.smul n)) (Completion.map (SMul.smul m)) x
Tactic: have hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x := rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformMulAction (goal)
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : SMul M X
inst_3 : SMul N X
inst_4 : SMulCommClass M N X
inst_5 : UniformContinuousConstSMul M X
inst_6 : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = Function.comp (β := Completion X) (Completion.map (SMul.smul m)) (Completion.map (SMul.smul n)) x
hnm : n • m • x = Function.comp (β := Completion X) (Completion.map (SMul.smul n)) (Completion.map (SMul.smul m)) x
⊢ m • n • x = n • m • x
have rw : Eq (α := Completion X) (Completion.map (SMul.smul m ∘ SMul.smul n) x) (Completion.map (SMul.smul n ∘ SMul.smul m) x)
Tactic: rw [hmn, hnm, map_comp, map_comp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformMulAction (goal)
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : SMul M X
inst_3 : SMul N X
inst_4 : SMulCommClass M N X
inst_5 : UniformContinuousConstSMul M X
inst_6 : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = Function.comp (β := Completion X) (Completion.map (SMul.smul m)) (Completion.map (SMul.smul n)) x
hnm : n • m • x = Function.comp (β := Completion X) (Completion.map (SMul.smul n)) (Completion.map (SMul.smul m)) x
rw :
  Eq (α := Completion X) (Completion.map (SMul.smul m ∘ SMul.smul n) x) (Completion.map (SMul.smul n ∘ SMul.smul m) x)
⊢ m • n • x = n • m • x
have hg : UniformContinuous.{x, x} (α := X) (SMul.smul n)
Tactic: rw [hmn, hnm, map_comp, map_comp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformMulAction (goal)
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : SMul M X
inst_3 : SMul N X
inst_4 : SMulCommClass M N X
inst_5 : UniformContinuousConstSMul M X
inst_6 : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = Function.comp (β := Completion X) (Completion.map (SMul.smul m)) (Completion.map (SMul.smul n)) x
hnm : n • m • x = Function.comp (β := Completion X) (Completion.map (SMul.smul n)) (Completion.map (SMul.smul m)) x
rw :
  Eq (α := Completion X) (Completion.map (SMul.smul m ∘ SMul.smul n) x) (Completion.map (SMul.smul n ∘ SMul.smul m) x)
hg : UniformContinuous.{x, x} (α := X) (SMul.smul n)
⊢ m • n • x = n • m • x
have hf : UniformContinuous.{x, x} (α := X) (SMul.smul m)
Tactic: rw [hmn, hnm, map_comp, map_comp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformMulAction (goal)
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : Monoid M
inst_3 : MulAction M X
inst_4 : UniformContinuousConstSMul M X
a : X
⊢ HSMul.hSMul.{v, x, x} (α := M) (β := Completion X) 1 (↑a : Completion X) = (↑a : Completion X)
have rw : Eq (α := Completion X) (↑(HSMul.hSMul.{v, x, x} (α := M) 1 a) : Completion X) (↑a : Completion X)
Tactic: rw [← coe_smul, one_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformMulAction (goal)
Goal:
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : Monoid M
inst_3 : MulAction M X
inst_4 : UniformContinuousConstSMul M X
a : X
rw : Eq (α := Completion X) (↑(HSMul.hSMul.{v, x, x} (α := M) 1 a) : Completion X) (↑a : Completion X)
⊢ HSMul.hSMul.{v, x, x} (α := M) (β := Completion X) 1 (↑a : Completion X) = (↑a : Completion X)
have rw₁ : Eq (α := Completion X) (↑a : Completion X) (↑a : Completion X)
Tactic: rw [← coe_smul, one_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (hypothesis)
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ (P := α) AddMonoidHom.mul toCompl
⊢ Continuous (Y := Completion α) fun (p : Completion α × Completion α) ↦ p.1 * p.2
have this : Continuous (Y := Completion α) fun (p : α × α) ↦
  (((m : (a : α) → α →+ Completion α) p.1 : α →+ Completion α) : (a : α) → Completion α) p.2
Tactic: have : Continuous fun p : α × α => m p.1 p.2 := (continuous_coe α).comp continuous_mul
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformRing (hypothesis)
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ (P := α) AddMonoidHom.mul toCompl
this :
  Continuous (Y := Completion α) fun (p : α × α) ↦
    (((m : (a : α) → α →+ Completion α) p.1 : α →+ Completion α) : (a : α) → Completion α) p.2
⊢ Continuous (Y := Completion α) fun (p : Completion α × Completion α) ↦ p.1 * p.2
have di : IsDenseInducing.{u_1, u_1} (α := α) (β := Completion α) (⇑toCompl : (a : α) → Completion α)
Tactic: have di : IsDenseInducing (toCompl : α → Completion α) := isDenseInducing_coe
-- 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 : α
⊢ HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) * (↑c : Completion α) =
    (↑a : Completion α) * HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
have rw : HMul.hMul (α := Completion α) (↑(a * b) : Completion α) (↑c : Completion α) =
  (↑a : Completion α) * HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
Tactic: rw [← coe_mul, ← coe_mul, ← coe_mul, ← coe_mul, mul_assoc]
-- 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 α) =
    (↑a : Completion α) * HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
⊢ HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) * (↑c : Completion α) =
    (↑a : Completion α) * HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
have rw₁ : (↑(a * b * c) : Completion α) =
  (↑a : Completion α) * HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
Tactic: rw [← coe_mul, ← coe_mul, ← coe_mul, ← coe_mul, mul_assoc]
-- 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 α) =
    (↑a : Completion α) * HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₁ :
  (↑(a * b * c) : Completion α) =
    (↑a : Completion α) * HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
⊢ HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) * (↑c : Completion α) =
    (↑a : Completion α) * HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
have rw₂ : (↑(a * b * c) : Completion α) = HMul.hMul (α := Completion α) (↑a : Completion α) (↑(b * c) : Completion α)
Tactic: rw [← coe_mul, ← coe_mul, ← coe_mul, ← coe_mul, mul_assoc]
-- 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 α) =
    (↑a : Completion α) * HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₁ :
  (↑(a * b * c) : Completion α) =
    (↑a : Completion α) * HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₂ : (↑(a * b * c) : Completion α) = HMul.hMul (α := Completion α) (↑a : Completion α) (↑(b * c) : Completion α)
⊢ HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) * (↑c : Completion α) =
    (↑a : Completion α) * HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
have rw₃ : Eq (α := Completion α) (↑(a * b * c) : Completion α) (↑(a * (b * c)) : Completion α)
Tactic: rw [← coe_mul, ← coe_mul, ← coe_mul, ← coe_mul, mul_assoc]
-- 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 α) =
    (↑a : Completion α) * HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₁ :
  (↑(a * b * c) : Completion α) =
    (↑a : Completion α) * HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
rw₂ : (↑(a * b * c) : Completion α) = HMul.hMul (α := Completion α) (↑a : Completion α) (↑(b * c) : Completion α)
rw₃ : Eq (α := Completion α) (↑(a * b * c) : Completion α) (↑(a * (b * c)) : Completion α)
⊢ HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α) * (↑c : Completion α) =
    (↑a : Completion α) * HMul.hMul (α := Completion α) (↑b : Completion α) (↑c : Completion α)
have rw₄ : Eq (α := Completion α) (↑(a * (b * c)) : Completion α) (↑(a * (b * c)) : Completion α)
Tactic: rw [← coe_mul, ← coe_mul, ← coe_mul, ← coe_mul, mul_assoc]
-- 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 α) 1 (↑a : Completion α) = (↑a : Completion α)
have rw : HMul.hMul (α := Completion α) (↑1 : Completion α) (↑a : Completion α) = (↑a : Completion α)
Tactic: rw [← coe_one, ← coe_mul, one_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 : Completion α
a : α
rw : HMul.hMul (α := Completion α) (↑1 : Completion α) (↑a : Completion α) = (↑a : Completion α)
⊢ HMul.hMul (α := Completion α) 1 (↑a : Completion α) = (↑a : Completion α)
have rw₁ : Eq (α := Completion α) (↑(1 * a) : Completion α) (↑a : Completion α)
Tactic: rw [← coe_one, ← coe_mul, one_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 : Completion α
a : α
rw : HMul.hMul (α := Completion α) (↑1 : Completion α) (↑a : Completion α) = (↑a : Completion α)
rw₁ : Eq (α := Completion α) (↑(1 * a) : Completion α) (↑a : Completion α)
⊢ HMul.hMul (α := Completion α) 1 (↑a : Completion α) = (↑a : Completion α)
have rw₂ : Eq (α := Completion α) (↑a : Completion α) (↑a : Completion α)
Tactic: rw [← coe_one, ← coe_mul, one_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 : Completion α
a : α
⊢ HMul.hMul (α := Completion α) (↑a : Completion α) 1 = (↑a : Completion α)
have rw : HMul.hMul (α := Completion α) (↑a : Completion α) (↑1 : Completion α) = (↑a : Completion α)
Tactic: rw [← coe_one, ← coe_mul, mul_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 α
a_1 : Completion α
a : α
rw : HMul.hMul (α := Completion α) (↑a : Completion α) (↑1 : Completion α) = (↑a : Completion α)
⊢ HMul.hMul (α := Completion α) (↑a : Completion α) 1 = (↑a : Completion α)
have rw₁ : Eq (α := Completion α) (↑(a * 1) : Completion α) (↑a : Completion α)
Tactic: rw [← coe_one, ← coe_mul, mul_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 α
a_1 : Completion α
a : α
rw : HMul.hMul (α := Completion α) (↑a : Completion α) (↑1 : Completion α) = (↑a : Completion α)
rw₁ : Eq (α := Completion α) (↑(a * 1) : Completion α) (↑a : Completion α)
⊢ HMul.hMul (α := Completion α) (↑a : Completion α) 1 = (↑a : Completion α)
have rw₂ : Eq (α := Completion α) (↑a : Completion α) (↑a : Completion α)
Tactic: rw [← coe_one, ← coe_mul, mul_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 α
a_1 : Completion α
a : α
⊢ HMul.hMul (α := Completion α) 0 (↑a : Completion α) = 0
have rw : HMul.hMul (α := Completion α) (↑0 : Completion α) (↑a : Completion α) = (↑0 : Completion α)
Tactic: rw [← coe_zero, ← coe_mul, zero_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 : Completion α
a : α
rw : HMul.hMul (α := Completion α) (↑0 : Completion α) (↑a : Completion α) = (↑0 : Completion α)
⊢ HMul.hMul (α := Completion α) 0 (↑a : Completion α) = 0
have rw₁ : Eq (α := Completion α) (↑(0 * a) : Completion α) (↑0 : Completion α)
Tactic: rw [← coe_zero, ← coe_mul, zero_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 : Completion α
a : α
rw : HMul.hMul (α := Completion α) (↑0 : Completion α) (↑a : Completion α) = (↑0 : Completion α)
rw₁ : Eq (α := Completion α) (↑(0 * a) : Completion α) (↑0 : Completion α)
⊢ HMul.hMul (α := Completion α) 0 (↑a : Completion α) = 0
have rw₂ : Eq.{u_1 + 1} (α := Completion α) (↑0 : Completion α) (↑0 : Completion α)
Tactic: rw [← coe_zero, ← coe_mul, zero_mul]