mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m' * m = m₁ ↔ m' = m₂
⊢ (x.coeff.sum fun m' r' ↦ if m' = m₂ then r' * r else 0) = x.coeff m₂ * r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m' * m = m₁ ↔ m' = m₂
⊢ (x * single m r).coeff m₁ = x.coeff m₂ * r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m * m' = m₁ ↔ m' = m₂
⊢ (single m r * x).coeff m₁ = x.coeff.sum fun m' r' ↦ if m * m' = m₁ then r * r' else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m * m' = m₁ ↔ m' = m₂
⊢ (x.coeff.sum fun m' r' ↦ if m * m' = m₁ then r * r' else 0) = x.coeff.sum fun m' r' ↦ if m' = m₂ then r * r' else 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m * m' = m₁ ↔ m' = m₂
⊢ (x.coeff.sum fun m' r' ↦ if m' = m₂ then r * r' else 0) = r * x.coeff m₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
x : R[M]
r : R
m m₁ : M
inst✝ : Mul M
m₂ : M
H : ∀ m' ∈ x.coeff.support, m * m' = m₁ ↔ m' = m₂
⊢ (single m r * x).coeff m₁ = r * x.coeff m₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
m m' : M
inst✝ : Mul M
r : R
x : R[M]
h : ∀ (d : M), d * m ≠ m'
⊢ (x * single m r).coeff m' = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
m m' : M
inst✝ : Mul M
r : R
x : R[M]
h : ∀ (d : M), m * d ≠ m'
⊢ (single m r * x).coeff m' = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul A
f g : R[A]
a0 b0 : A
h : UniqueMul f.coeff.support g.coeff.support a0 b0
⊢ (f * g).coeff (a0 * b0) = f.coeff a0 * g.coeff b0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
r : R
g g' : M
x : R[M]
h : ¬∃ d, g' = d * g
⊢ ∀ (d : M), d * g ≠ g'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
r : R
g g' : M
x : R[M]
h : ¬∃ d, g' = g * d
⊢ ∀ (d : M), g * d ≠ g'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : NoZeroDivisors R
inst✝¹ : Mul A
inst✝ : UniqueProds A
a b : R[A]
hab : a * b = 0
⊢ a = 0 ∨ b = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
G : Type u_3
M✝ : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝³ : Semiring R✝
x y : R✝[M✝]
r r₁ r₂ : R✝
m m' m₁ m₂ m₁' m₂' : M✝
inst✝² : Mul M✝
R : Type u_8
M : Type u_9
inst✝¹ : Semiring R
inst✝ : Mul M
a b : M
⊢ single (a * b) 1 = single a 1 * single b 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : Semigroup M
⊢ ∀ (a b c : R[M]), a * b * c = a * (b * c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : MulOneClass M
⊢ ∀ (a : R[M]), 1 * a = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : MulOneClass M
⊢ ∀ (a : R[M]), a * 1 = a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : MulOneClass M
⊢ single 1 ↑0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : MulOneClass M
⊢ ∀ (n : ℕ), single 1 ↑(n + 1) = single 1 ↑n + 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : MulOneClass M
x : R[M]
r : R
m : M
⊢ ∀ m' ∈ x.coeff.support, m' * 1 = m ↔ m' = m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : MulOneClass M
x : R[M]
r : R
m : M
⊢ ∀ m' ∈ x.coeff.support, 1 * m' = m ↔ m' = m

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : MulOneClass M
inst✝ : Nontrivial R
a b : M
h : (of R M) a = (of R M) b
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : MulOneClass M
_a _b : R × M
⊢ single (_a * _b).2 (_a * _b).1 = single _a.2 _a.1 * single _b.2 _b.1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝ : MulOneClass M
⊢ ∀ (x y : R), (↑(singleAddHom 1)).toFun (x * y) = (↑(singleAddHom 1)).toFun x * (↑(singleAddHom 1)).toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : MulOneClass M
inst✝ : Semiring S
f g : R[M] →+* S
h₁ : ∀ (r : R), f (single 1 r) = g (single 1 r)
h_of : ∀ (m : M), f (single m 1) = g (single m 1)
m : M
r : R
⊢ ((fun f ↦ ↑f) f) (single m r) = ((fun f ↦ ↑f) g) (single m r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : MulOneClass M
inst✝ : Semiring S
f g : R[M] →+* S
h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom
h_of : (↑f).comp (of R M) = (↑g).comp (of R M)
⊢ ∀ (r : R), f (single 1 r) = g (single 1 r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : MulOneClass M
inst✝ : Semiring S
f g : R[M] →+* S
h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom
h_of : (↑f).comp (of R M) = (↑g).comp (of R M)
⊢ ∀ (m : M), f (single m 1) = g (single m 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Monoid M
m : M
r : R
⊢ single m r ^ 0 = single (m ^ 0) (r ^ 0)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Monoid M
m : M
r : R
n : ℕ
⊢ single m r ^ (n + 1) = single (m ^ (n + 1)) (r ^ (n + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Monoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((MonoidAlgebra.of R M) m)
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
⊢ motive (ofCoeff 0)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Monoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((MonoidAlgebra.of R M) m)
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
m : M
r : R
⊢ motive (ofCoeff (Finsupp.single m r))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ ∀ (a : R), IsUnit (singleOneRingHom a) → IsUnit a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝³ : Semiring R
x✝ y✝ : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Subsingleton M
x y : R[M]
⊢ (coeffAddEquiv.trans (uniqueAddEquiv 1)).toFun (x * y) =
    (coeffAddEquiv.trans (uniqueAddEquiv 1)).toFun x * (coeffAddEquiv.trans (uniqueAddEquiv 1)).toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Subsingleton M
r : R
⊢ (uniqueRingEquiv M).symm r = single 1 r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Subsingleton M
r : R
m : M
⊢ ((uniqueRingEquiv M).symm r).coeff m = r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Monoid N
m : M
n : N
r : R
⊢ curryAddEquiv (single (m, n) r) = single m (single n r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Monoid N
m : M
n : N
r : R
⊢ curryAddEquiv.symm (single m (single n r)) = single (m, n) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ AddMonoidHom.mul.compr₂ curryAddEquiv.toAddMonoidHom =
    (AddMonoidHom.mul.comp curryAddEquiv.toAddMonoidHom).compl₂ curryAddEquiv.toAddMonoidHom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Monoid N
m : M
n : N
r : R
⊢ curryRingEquiv (single (m, n) r) = single m (single n r)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
N : Type u_5
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Monoid N
m : M
n : N
r : R
⊢ curryRingEquiv.symm (single m (single n r)) = single (m, n) r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : IsCancelMul M
x : R[M]
r : R
m m' : M
⊢ ∀ m'_1 ∈ x.coeff.support, m'_1 * m = m' * m ↔ m'_1 = m'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : IsCancelMul M
x : R[M]
r : R
m m' : M
⊢ ∀ m'_1 ∈ x.coeff.support, m * m'_1 = m * m' ↔ m'_1 = m'

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x : R[G]
r : R
g h : G
⊢ ∀ m' ∈ x.coeff.support, m' * g = h ↔ m' = h * g⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x : R[G]
r : R
g h : G
⊢ ∀ m' ∈ x.coeff.support, g * m' = h ↔ m' = g⁻¹ * h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g : G
⊢ (x * y).coeff g = x.coeff.sum fun h r ↦ r * y.coeff (h⁻¹ * g)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : f.coeff af * g₂.coeff ag = f.coeff af * g₁.coeff ag
this : g₂.coeff ag = g₁.coeff ag
eq : f * erase ag g₁ + f * single ag (g₁.coeff ag) = f * erase ag g₂ + f * single ag (g₁.coeff ag)
⊢ erase ag g₁ + single ag (g₁.coeff ag) = erase ag g₂ + single ag (g₁.coeff ag)

Tactic:
add_right_cancel_iff

Goal state after:
case H.inr
R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f g₁ g₂ : R[A]
ih :
  ∀ s ∈ g₁.coeff.support ∪ g₂.coeff.support,
    ∀ {g₁_1 g₂_1 : R[A]},
      (fun x ↦ f * x) g₁_1 = (fun x ↦ f * x) g₂_1 →
        g₁_1.coeff.support ∪ g₂_1.coeff.support = (g₁.coeff.support ∪ g₂.coeff.support).erase s → g₁_1 = g₂_1
h✝ : (g₁.coeff.support ∪ g₂.coeff.support).Nonempty
hf : f.coeff.support.Nonempty
af : A
haf : af ∈ f.coeff.support
ag : A
hag : ag ∈ g₁.coeff.support ∪ g₂.coeff.support
uniq : UniqueMul f.coeff.support (g₁.coeff.support ∪ g₂.coeff.support) af ag
h : f.coeff af * g₂.coeff ag = f.coeff af * g₁.coeff ag
this : g₂.coeff ag = g₁.coeff ag
eq : f * erase ag g₁ = f * erase ag g₂
⊢ erase ag g₁ + single ag (g₁.coeff ag) = erase ag g₂ + single ag (g₁.coeff ag)
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g : G
⊢ (x * y).coeff g = y.coeff.sum fun h r ↦ x.coeff (g * h⁻¹) * r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CommSemigroup M
f g : R[M]
⊢ f * g = g * f

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
ι : Type u_7
inst✝¹ : CommSemiring R
inst✝ : CommMonoid M
s✝ : Finset ι
m : ι → M
r : ι → R
i : ι
s : Finset ι
hi : i ∉ s
ih : ∏ i ∈ s, single (m i) (r i) = single (∏ i ∈ s, m i) (∏ i ∈ s, r i)
⊢ ∏ i ∈ cons i s hi, single (m i) (r i) = single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Ring R
m : M
r : R
⊢ single m (-r) = -single m r

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Ring R
m : M
r s : R
⊢ single m (r - s) = single m r - single m s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Ring R
inst✝ : MulOneClass M
n : ℕ
⊢ single 1 ↑↑n = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝¹ : Ring R
inst✝ : MulOneClass M
n : ℕ
⊢ single 1 ↑(Int.negSucc n) = -↑(n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R✝ : Type u_1
S : Type u_2
G : Type u_3
M✝ : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R✝
R : Type u_8
M : Type u_9
inst✝¹ : Semiring R
inst✝ : Add M
⊢ ∀ (x y : Multiplicative M),
    single (Multiplicative.toAdd (x * y)) 1 = single (Multiplicative.toAdd x) 1 * single (Multiplicative.toAdd y) 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : AddZeroClass M
a b : Multiplicative M
h : (of R M) a = (of R M) b
⊢ a = b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : AddMonoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((AddMonoidAlgebra.of R M) (Multiplicative.ofAdd m))
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
⊢ motive (ofCoeff 0)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : AddMonoid M
motive : R[M] → Prop
x : R[M]
of : ∀ (m : M), motive ((AddMonoidAlgebra.of R M) (Multiplicative.ofAdd m))
add : ∀ (x y : R[M]), motive x → motive y → motive (x + y)
smul : ∀ (r : R) (x : R[M]), motive x → motive (r • x)
m : M
r : R
⊢ motive (ofCoeff (Finsupp.single m r))

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
⊢ g₁ = g₂

Tactic:
classical
    induction hg : g₁.coeff.support ∪ g₂.coeff.support
      using Finset.eraseInduction generalizing g₁ g₂ with
    | _ s ih =>
    obtain h | h := s.eq_empty_or_nonempty <;> subst s
    · simp_all
    simp only [ne_eq, ← coeff_eq_zero, ← support_nonempty_iff] at hf
    obtain ⟨af, haf, ag, hag, uniq⟩ := UniqueProds.uniqueMul_of_nonempty hf h
    have h := coeff_mul_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_left)
    dsimp only at eq
    rw [eq, coeff_mul_mul_of_uniqueMul (uniq.mono subset_rfl Finset.subset_union_right)] at h
    have := mul_left_cancel₀ (mem_support_iff.mp haf) h
    rw [← g₁.erase_add_single ag, ← g₂.erase_add_single ag, this] at eq ⊢
    simp_rw [mul_add, add_right_cancel_iff] at eq
    rw [ih ag hag eq]
    simp [Finset.erase_union_distrib]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : Semiring R
inst✝³ : IsCancelAdd R
inst✝² : IsLeftCancelMulZero R
inst✝¹ : Mul A
inst✝ : UniqueProds A
f : R[A]
hf : f ≠ 0
g₁ g₂ : R[A]
eq : (fun x ↦ f * x) g₁ = (fun x ↦ f * x) g₂
⊢ g₁ = g₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
⊢ a • 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
x y : R
⊢ a • (x + y) = a • x + a • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionSemiring R
a : ℚ≥0
x y : R
⊢ (a • x) • y = a • x • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionRing R
a : ℚ
⊢ a • 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionRing R
a : ℚ
x y : R
⊢ a • (x + y) = a • x + a • y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Ring.Action.Rat

Goal state before:
pp: R : Type u_1
inst✝ : DivisionRing R
a : ℚ
x y : R
⊢ (a • x) • y = a • x • y

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
r : α → α → Prop
inst✝⁷ : DecidableRel r
inst✝⁶ : IsTrans α r
inst✝⁵ : Std.Antisymm r
inst✝⁴ : Std.Total r
r' : β → β → Prop
inst✝³ : DecidableRel r'
inst✝² : IsTrans β r'
inst✝¹ : Std.Antisymm r'
inst✝ : Std.Total r'
l : List α
h : ∀ (a : α), a ∈ Quot.mk (⇑(isSetoid α)) l → ∀ (b : α), b ∈ Quot.mk (⇑(isSetoid α)) l → (r a b ↔ r' (f a) (f b))
⊢ ∀ (a : α), a ∈ l → ∀ (b : α), b ∈ l → decide (r a b) = decide (r' (f a) (f b))

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sort

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s : Multiset α
r : α → α → Prop
inst✝⁷ : DecidableRel r
inst✝⁶ : IsTrans α r
inst✝⁵ : Std.Antisymm r
inst✝⁴ : Std.Total r
r' : β → β → Prop
inst✝³ : DecidableRel r'
inst✝² : IsTrans β r'
inst✝¹ : Std.Antisymm r'
inst✝ : Std.Total r'
hs : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → (r a b ↔ r' (f a) (f b))
⊢ List.map f (s.sort r) = (map f s).sort r'

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sort

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
⊢ (∀ (b : α), b ∈ s → r a b) → (a ::ₘ s).sort r = a :: s.sort r

Tactic:
by

Goal state after:
Module: Mathlib.Data.Multiset.Sort

Goal state before:
pp: α : Type u_1
a : α
s : Multiset α
r : α → α → Prop
inst✝³ : DecidableRel r
inst✝² : IsTrans α r
inst✝¹ : Std.Antisymm r
inst✝ : Std.Total r
⊢ a ∈ s.sort r ↔ a ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : Subsingleton G
⊢ UniqueMul A B a0 b0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
hA : A.Nonempty
hB : B.Nonempty
hA1 : #A ≤ 1
hB1 : #B ≤ 1
⊢ ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x✝¹ x✝ : G
ha : x✝¹ ∈ A
hb : x✝ ∈ B
k : x✝¹ ≠ a0 ∨ x✝ ≠ b0
⊢ x✝¹ * x✝ ≠ a0 * b0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ {ab | ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = a0 * b0}.Subsingleton

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
x✝ : UniqueMul A B a0 b0
⊢ ∀ (y : G × G), (fun ab ↦ ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0) y → y = (a0, b0)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
aA : a0 ∈ A
bB : b0 ∈ B
h : ∃! ab, ab ∈ A ×ˢ B ∧ ab.1 * ab.2 = a0 * b0
⊢ ∀ (x : G × G),
    x ∈ A ×ˢ B ∧ x.1 * x.2 = a0 * b0 → (∀ (y : G × G), y ∈ A ×ˢ B ∧ y.1 * y.2 = a0 * b0 → y = x) → UniqueMul A B a0 b0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Mul G
A B : Finset G
a0 b0 : G
inst✝ : DecidableEq G
ha0 : a0 ∈ A
hb0 : b0 ∈ B
⊢ UniqueMul A B a0 b0 ↔ #({p ∈ A ×ˢ B | p.1 * p.2 = a0 * b0}) ≤ 1

Tactic:
by

Goal state after: