awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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
⊢ 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)
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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

Tactic:
Eq.trans ?_ (congr_fun this.symm x)

Premises used: congr_fun, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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))
refine : (m • n) • x = Completion.map ((fun (x : X) ↦ m • x) ∘ fun (x : X) ↦ n • x) x
⊢ (m • n) • x = m • n • x

Tactic:
refine Eq.trans ?_ (congr_fun this.symm x)

Premises used: congr_fun, Eq.symm, Eq.trans
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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 = Completion.map ((fun (x : X) ↦ m • x) ∘ fun (x : X) ↦ n • x) x

Tactic:
congr_arg (fun f => Completion.map f x) (funext (smul_assoc _ _))

Premises used: UniformSpace.Completion.map, smul_assoc, congr_arg, funext
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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 = Completion.map ((fun (x : X) ↦ m • x) ∘ fun (x : X) ↦ n • x) x

Tactic:
exact congr_arg (fun f => Completion.map f x) (funext (smul_assoc _ _))

Premises used: UniformSpace.Completion.map, smul_assoc, congr_arg, funext
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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 = 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
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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
⊢ 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
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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)
hf hg₁ : UniformContinuous.{x, x} (α := X) (SMul.smul m)
hf₁ : UniformContinuous.{x, x} (α := X) (SMul.smul n)
⊢ m • n • x = n • m • x

Tactic:
rw [hmn, hnm, map_comp, map_comp]

Premises used: UniformSpace.Completion.map_comp
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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
⊢ Eq (α := Completion X) (Completion.map (SMul.smul m ∘ SMul.smul n) x) (Completion.map (SMul.smul n ∘ SMul.smul m) x)

Tactic:
congr_arg (fun f => Completion.map f x) (funext (smul_comm _ _))

Premises used: UniformSpace.Completion.map, congr_arg, funext, SMulCommClass.smul_comm
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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
⊢ Eq (α := Completion X) (Completion.map (SMul.smul m ∘ SMul.smul n) x) (Completion.map (SMul.smul n ∘ SMul.smul m) x)

Tactic:
exact congr_arg (fun f => Completion.map f x) (funext (smul_comm _ _))

Premises used: UniformSpace.Completion.map, congr_arg, funext, SMulCommClass.smul_comm
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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
⊢ UniformContinuous.{x, x} (α := X) (SMul.smul n)

Tactic:
uniformContinuous_const_smul _

Premises used: UniformContinuousConstSMul.uniformContinuous_const_smul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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
⊢ UniformContinuous.{x, x} (α := X) (SMul.smul n)

Tactic:
exact uniformContinuous_const_smul _

Premises used: UniformContinuousConstSMul.uniformContinuous_const_smul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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
⊢ UniformContinuous.{x, x} (α := X) (SMul.smul m)

Tactic:
uniformContinuous_const_smul _

Premises used: UniformContinuousConstSMul.uniformContinuous_const_smul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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
⊢ UniformContinuous.{x, x} (α := X) (SMul.smul m)

Tactic:
exact uniformContinuous_const_smul _

Premises used: UniformContinuousConstSMul.uniformContinuous_const_smul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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.{v, x} Mᵐᵒᵖ X
inst_4 : IsCentralScalar M X
⊢ IsCentralScalar.{v, x} M (Completion X)

Tactic:
⟨fun c a => (congr_arg fun f => Completion.map f a) <| funext (op_smul_eq_smul c)⟩

Premises used: UniformSpace.Completion.map, congr_arg, funext, IsCentralScalar.mk, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
Goal:
M : Type v
X : Type x
inst : UniformSpace X
inst_1 : SMul M X
inst_2 : UniformContinuousConstSMul M X
c : M
x : X
⊢ (↑(c • x) : Completion X) = HSMul.hSMul (β := Completion X) c (↑x : Completion X)

Tactic:
(map_coe (uniformContinuous_const_smul c) x).symm

Premises used: UniformSpace.Completion.map_coe, Eq.symm, UniformContinuousConstSMul.uniformContinuous_const_smul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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
x y : M
a : X
⊢ HSMul.hSMul (β := Completion X) (x * y) (↑a : Completion X) =
    x • HSMul.hSMul (β := Completion X) y (↑a : Completion X)

Tactic:
simp only [← coe_smul, mul_smul]

Premises used: UniformSpace.Completion.coe_smul, SemigroupAction.mul_smul
-- Module: Mathlib.Topology.Algebra.UniformMulAction
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)
rw₁ rw₂ : Eq (α := Completion X) (↑a : Completion X) (↑a : Completion X)
⊢ HSMul.hSMul.{v, x, x} (α := M) (β := Completion X) 1 (↑a : Completion X) = (↑a : Completion X)

Tactic:
rw [← coe_smul, one_smul]

Premises used: one_smul, UniformSpace.Completion.coe_smul
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
⊢ Eq.{u_1 + 1} (α := Completion α) (↑1 : Completion α) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : T0Space α
x : α
⊢ Eq (α := Completion α) (↑x : Completion α) 1 ↔ x = 1

Tactic:
Completion.coe_inj

Premises used: UniformSpace.Completion.coe_inj
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
a b : α
⊢ (↑(a * b) : Completion α) = HMul.hMul (α := Completion α) (↑a : Completion α) (↑b : Completion α)

Tactic:
((isDenseInducing_coe.prodMap isDenseInducing_coe).extend_eq
      ((continuous_coe α).comp (@continuous_mul α _ _ _)) (a, b)).symm

Premises used: UniformSpace.Completion.coe', Classical.epsilon, Set.Mem, continuous_mul, Continuous.comp, Prod.mk, Prod.map, UniformSpace.Completion.continuous_coe, SeparationQuotient.mk, Filter.lim, IsDenseInducing.prodMap, Eq.symm, Filter.limUnder, IsDenseInducing.extend, UniformSpace.Completion.isDenseInducing_coe, IsDenseInducing.extend_eq
-- Module: Mathlib.Topology.Algebra.UniformRing
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 : α × α) ↦
    (((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
-- Module: Mathlib.Topology.Algebra.UniformRing
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
⊢ IsDenseInducing.{u_1, u_1} (α := α) (β := Completion α) (⇑toCompl : (a : α) → Completion α)

Tactic:
have di : IsDenseInducing (toCompl : α → Completion α) := isDenseInducing_coe
-- Module: Mathlib.Topology.Algebra.UniformRing
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
di : IsDenseInducing.{u_1, u_1} (α := α) (β := Completion α) (⇑toCompl : (a : α) → Completion α)
⊢ Continuous (Y := Completion α) fun (p : Completion α × Completion α) ↦ p.1 * p.2

Tactic:
(di.extend_Z_bilin di this :)

Premises used: UniformSpace.Completion.coe', Classical.epsilon, Set.Mem, IsDenseInducing.extend_Z_bilin, SeparationQuotient.mk, Filter.lim, Filter.limUnder, IsDenseInducing.extend
-- Module: Mathlib.Topology.Algebra.UniformRing
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
di : IsDenseInducing.{u_1, u_1} (α := α) (β := Completion α) (⇑toCompl : (a : α) → Completion α)
⊢ Continuous (Y := Completion α) fun (p : Completion α × Completion α) ↦ p.1 * p.2

Tactic:
exact (di.extend_Z_bilin di this :)

Premises used: IsDenseInducing.extend_Z_bilin
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
a b c : Completion α
⊢ Continuous (Y := Completion α) fun (x : Completion α × Completion α × Completion α) ↦ x.1 * x.2.1 * x.2.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
a b c : Completion α
⊢ Continuous (Y := Completion α) fun (x : Completion α × Completion α × Completion α) ↦ x.1 * (x.2.1 * x.2.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
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 α)
rw₄ 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 α)

Tactic:
rw [← coe_mul, ← coe_mul, ← coe_mul, ← coe_mul, mul_assoc]

Premises used: mul_assoc, UniformSpace.Completion.coe_mul
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
a : Completion α
⊢ Continuous (X := Completion α) (HMul.hMul (α := Completion α) 1)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
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 α)
rw₂ rw₃ : Eq (α := Completion α) (↑a : Completion α) (↑a : Completion α)
⊢ HMul.hMul (α := Completion α) 1 (↑a : Completion α) = (↑a : Completion α)

Tactic:
rw [← coe_one, ← coe_mul, one_mul]

Premises used: UniformSpace.Completion.coe_mul, one_mul, UniformSpace.Completion.coe_one
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
a : Completion α
⊢ Continuous (Y := Completion α) fun (a : Completion α) ↦ a * 1

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
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 α)
rw₂ rw₃ : Eq (α := Completion α) (↑a : Completion α) (↑a : Completion α)
⊢ HMul.hMul (α := Completion α) (↑a : Completion α) 1 = (↑a : Completion α)

Tactic:
rw [← coe_one, ← coe_mul, mul_one]

Premises used: UniformSpace.Completion.coe_mul, mul_one, UniformSpace.Completion.coe_one
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
a : Completion α
⊢ Continuous (X := Completion α) (HMul.hMul (α := Completion α) 0)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
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 α)
rw₂ rw₃ : Eq.{u_1 + 1} (α := Completion α) (↑0 : Completion α) (↑0 : Completion α)
⊢ HMul.hMul (α := Completion α) 0 (↑a : Completion α) = 0

Tactic:
rw [← coe_zero, ← coe_mul, zero_mul]

Premises used: MulZeroClass.zero_mul, UniformSpace.Completion.coe_zero, UniformSpace.Completion.coe_mul
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
a : Completion α
⊢ Continuous (Y := Completion α) fun (a : Completion α) ↦ a * 0

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
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 α)
rw₂ rw₃ : Eq.{u_1 + 1} (α := Completion α) (↑0 : Completion α) (↑0 : Completion α)
⊢ HMul.hMul (α := Completion α) (↑a : Completion α) 0 = 0

Tactic:
rw [← coe_zero, ← coe_mul, mul_zero]

Premises used: MulZeroClass.mul_zero, UniformSpace.Completion.coe_zero, UniformSpace.Completion.coe_mul
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
a b c : Completion α
⊢ Continuous (Y := Completion α) fun (x : Completion α × Completion α × Completion α) ↦ x.1 * (x.2.1 + x.2.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
a b c : Completion α
⊢ Continuous (Y := Completion α) fun (x : Completion α × Completion α × Completion α) ↦ x.1 * x.2.1 + x.1 * x.2.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformRing
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 α)
rw₅ rw₆ : Eq (α := Completion α) (↑(a * b + a * 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 α)

Tactic:
rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, mul_add]

Premises used: UniformSpace.Completion.coe_mul, mul_add, UniformSpace.Completion.coe_add
-- Module: Mathlib.Topology.Algebra.UniformRing
Goal:
α : Type u_1
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
a b c : Completion α
⊢ Continuous (Y := Completion α) fun (x : Completion α × Completion α × Completion α) ↦ (x.1 + x.2.1) * x.2.2

Tactic:
fun_prop