mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set V
t✝¹ : Finset V
hs : LinearIndepOn K id s
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s → s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ ↑t = ∅
this : s ⊆ ↑(span K ↑(s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
Eq : u.card = (s' ∪ t).card
hb₁u : b₁ ∉ u
⊢ ↑u ⊆ ↑(insert b₁ u)

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
hf : Injective f
a✝ : M
⊢ (comapDomain f hf 0).coeff a✝ = (coeff 0) a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: case empty
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ a ∈ ∅, Injective (f a)
hs : ((fun a ↦ image (f a) t) '' ↑∅).PairwiseDisjoint id
⊢ #t ∣ #(image₂ f ∅ t)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f✝ : M → N
a : M
r : R
f : M → N
hf : Injective f
⊢ comapDomain f hf 0 = 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Semiring T
f✝ : M → N
a : M
r : R
f : M → N
hf : Injective f
⊢ ∀ (x y : R[N]), comapDomain f hf (x + y) = comapDomain f hf x + comapDomain f hf y

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝ : Semiring R
f : M → N
hf : Injective f
m : M
r : R
a✝ : M
⊢ (comapDomain f hf (single (f m) r)).coeff a✝ = (single m r).coeff a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Mul M
x✝ : R[M]
a✝ : M
⊢ ((mapDomainNonUnitalRingHom R (MulHom.id M)) x✝).coeff a✝ = ((NonUnitalRingHom.id R[M]) x✝).coeff a✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M ≃ N
x : R[M]
a✝ : M
⊢ ((fun x ↦ mapDomain (⇑e.symm) x) ((fun x ↦ mapDomain (⇑e) x) x)).coeff a✝ = x.coeff a✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M ≃ N
x : R[N]
a✝ : N
⊢ ((fun x ↦ mapDomain (⇑e) x) ((fun x ↦ mapDomain (⇑e.symm) x) x)).coeff a✝ = x.coeff a✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : M ≃ N
x y : R[M]
a✝ : N
⊢ (mapDomain (⇑e) (x + y)).coeff a✝ = (mapDomain (⇑e) x + mapDomain (⇑e) y).coeff a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst✝³ : Semiring R
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul O
e₁ : M ≃ N
e₂ : N ≃ O
x✝ : R[M]
a✝ : O
⊢ ((mapDomainAddEquiv R (e₁.trans e₂)) x✝).coeff a✝ =
    (((mapDomainAddEquiv R e₁).trans (mapDomainAddEquiv R e₂)) x✝).coeff a✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : R ≃+ S
x : R[M]
a✝ : M
⊢ (map (↑e.symm) (map (↑e) x)).coeff a✝ = x.coeff a✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : Semiring T
f : M → N
a : M
r : R
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul O
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
e : R ≃+ S
x : S[M]
a✝ : M
⊢ (map (↑e) (map (↑e.symm) x)).coeff a✝ = x.coeff a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Semiring T
inst✝ : Mul M
e₁ : R ≃+ S
e₂ : S ≃+ T
x✝ : R[M]
a✝ : M
⊢ ((mapAddEquiv M (e₁.trans e₂)) x✝).coeff a✝ = (((mapAddEquiv M e₁).trans (mapAddEquiv M e₂)) x✝).coeff a✝

Tactic:
simp

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

Goal state before:
pp: case h₁
R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
r✝ : R
a✝ : M
⊢ ((mapDomainRingHom R (MonoidHom.id M)) (single 1 r✝)).coeff a✝ = ((RingHom.id R[M]) (single 1 r✝)).coeff a✝

Tactic:
simp

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

Goal state before:
pp: case h_of
R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
m✝ a✝ : M
⊢ ((mapDomainRingHom R (MonoidHom.id M)) (single m✝ 1)).coeff a✝ = ((RingHom.id R[M]) (single m✝ 1)).coeff a✝

Tactic:
simp

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

Goal state before:
pp: case h₁
R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst✝³ : Semiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : N →* O
g : M →* N
r✝ : R
a✝ : O
⊢ ((mapDomainRingHom R (f.comp g)) (single 1 r✝)).coeff a✝ =
    (((mapDomainRingHom R f).comp (mapDomainRingHom R g)) (single 1 r✝)).coeff a✝

Tactic:
simp

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

Goal state before:
pp: case h_of
R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst✝³ : Semiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
f : N →* O
g : M →* N
m✝ : M
a✝ : O
⊢ ((mapDomainRingHom R (f.comp g)) (single m✝ 1)).coeff a✝ =
    (((mapDomainRingHom R f).comp (mapDomainRingHom R g)) (single m✝ 1)).coeff a✝

Tactic:
simp

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

Goal state before:
pp: case h₁
R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
r✝ : R
a✝ : M
⊢ ((mapRingHom M (RingHom.id R)) (single 1 r✝)).coeff a✝ = ((RingHom.id R[M]) (single 1 r✝)).coeff a✝

Tactic:
simp

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

Goal state before:
pp: case h_of
R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
m✝ a✝ : M
⊢ ((mapRingHom M (RingHom.id R)) (single m✝ 1)).coeff a✝ = ((RingHom.id R[M]) (single m✝ 1)).coeff a✝

Tactic:
simp

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

Goal state before:
pp: case h₁
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Semiring T
inst✝ : Monoid M
f : S →+* T
g : R →+* S
r✝ : R
a✝ : M
⊢ ((mapRingHom M (f.comp g)) (single 1 r✝)).coeff a✝ = (((mapRingHom M f).comp (mapRingHom M g)) (single 1 r✝)).coeff a✝

Tactic:
simp

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

Goal state before:
pp: case h_of
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Semiring T
inst✝ : Monoid M
f : S →+* T
g : R →+* S
m✝ a✝ : M
⊢ ((mapRingHom M (f.comp g)) (single m✝ 1)).coeff a✝ = (((mapRingHom M f).comp (mapRingHom M g)) (single m✝ 1)).coeff a✝

Tactic:
simp

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

Goal state before:
pp: case h₁
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ ∀ (r : R), ((mapDomainRingHom R ↑e).comp (mapDomainRingHom R ↑e.symm)) (single 1 r) = (RingHom.id R[N]) (single 1 r)

Tactic:
simp

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

Goal state before:
pp: case h_of
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ ∀ (m : N), ((mapDomainRingHom R ↑e).comp (mapDomainRingHom R ↑e.symm)) (single m 1) = (RingHom.id R[N]) (single m 1)

Tactic:
simp

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

Goal state before:
pp: case h₁
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ ∀ (r : R), ((mapDomainRingHom R ↑e.symm).comp (mapDomainRingHom R ↑e)) (single 1 r) = (RingHom.id R[M]) (single 1 r)

Tactic:
simp

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

Goal state before:
pp: case h_of
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : M ≃* N
⊢ ∀ (m : M), ((mapDomainRingHom R ↑e.symm).comp (mapDomainRingHom R ↑e)) (single m 1) = (RingHom.id R[M]) (single m 1)

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
O : Type u_8
inst✝³ : Semiring R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e₁ : M ≃* N
e₂ : N ≃* O
x✝ : R[M]
a✝ : O
⊢ ((mapDomainRingEquiv R (e₁.trans e₂)) x✝).coeff a✝ =
    (((mapDomainRingEquiv R e₁).trans (mapDomainRingEquiv R e₂)) x✝).coeff a✝

Tactic:
simp

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

Goal state before:
pp: case h₁
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ ∀ (r : S), ((mapRingHom M ↑e).comp (mapRingHom M ↑e.symm)) (single 1 r) = (RingHom.id S[M]) (single 1 r)

Tactic:
simp

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

Goal state before:
pp: case h_of
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ ∀ (m : M), ((mapRingHom M ↑e).comp (mapRingHom M ↑e.symm)) (single m 1) = (RingHom.id S[M]) (single m 1)

Tactic:
simp

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

Goal state before:
pp: case h₁
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ ∀ (r : R), ((mapRingHom M ↑e.symm).comp (mapRingHom M ↑e)) (single 1 r) = (RingHom.id R[M]) (single 1 r)

Tactic:
simp

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

Goal state before:
pp: case h_of
ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝⁵ : Semiring R
inst✝⁴ : Semiring S
inst✝³ : Semiring T
f : M → N
a : M
r : R
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid O
e : R ≃+* S
⊢ ∀ (m : M), ((mapRingHom M ↑e.symm).comp (mapRingHom M ↑e)) (single m 1) = (RingHom.id R[M]) (single m 1)

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : Semiring T
inst✝ : Monoid M
e₁ : R ≃+* S
e₂ : S ≃+* T
x✝ : R[M]
a✝ : M
⊢ ((mapRingEquiv M (e₁.trans e₂)) x✝).coeff a✝ = (((mapRingEquiv M e₁).trans (mapRingEquiv M e₂)) x✝).coeff a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+ S
x : R[M]
a✝ : M
⊢ (map f (-x)).coeff a✝ = (-map f x).coeff a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+ S
x y : R[M]
a✝ : M
⊢ (map f (x - y)).coeff a✝ = (map f x - map f y).coeff a✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Add M
x : R[M]
a✝ : M
⊢ ((fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Multiplicative.toAdd) x.coeff))
          ((fun x ↦ MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff)) x)).coeff
      a✝ =
    x.coeff a✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Add M
x : MonoidAlgebra R (Multiplicative M)
a✝ : Multiplicative M
⊢ ((fun x ↦ MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff))
          ((fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Multiplicative.toAdd) x.coeff)) x)).coeff
      a✝ =
    x.coeff a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m a✝ : M
⊢ (erase m 0).coeff a✝ = (coeff 0) a✝

Tactic:
simp

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
r : R
a✝ : M
⊢ (erase m (single m r)).coeff a✝ = (coeff 0) a✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Mul M
x : R[M]
a✝ : M
⊢ ((fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Additive.toMul) x.coeff))
          ((fun x ↦ AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff)) x)).coeff
      a✝ =
    x.coeff a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
A : Type u_8
inst✝ : SMulZeroClass A R
a : A
m : M
r : R
a✝ : M
⊢ (a • single m r).coeff a✝ = (single m (a • r)).coeff a✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
F : Type u_2
R : Type u_3
S : Type u_4
T : Type u_5
M : Type u_6
N : Type u_7
O : Type u_8
inst✝¹ : Semiring R
inst✝ : Mul M
x : AddMonoidAlgebra R (Additive M)
a✝ : Additive M
⊢ ((fun x ↦ AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff))
          ((fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Additive.toMul) x.coeff)) x)).coeff
      a✝ =
    x.coeff a✝

Tactic:
simp

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
r₁ r₂ : R
a✝ : M
⊢ (single m (r₁ + r₂)).coeff a✝ = (single m r₁ + single m r₂).coeff a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Mul M
m : M
r : R
a✝ : Additive M
⊢ ((toAdditive R M) (single m r)).coeff a✝ = (AddMonoidAlgebra.single (Additive.ofMul m) r).coeff a✝

Tactic:
simp

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

Goal state before:
pp: case e'_2
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
x✝ : R[M]
⊢ f x✝ = ((f.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom) x✝

Tactic:
simp

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

Goal state before:
pp: case e'_3
R : Type u_1
M : Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : AddZeroClass N
f g : R[M] →+ N
h : ∀ (m : M) (r : R), f (single m r) = g (single m r)
this : f.comp coeffAddEquiv.symm.toAddMonoidHom = g.comp coeffAddEquiv.symm.toAddMonoidHom
x✝ : R[M]
⊢ g x✝ = ((g.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom) x✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
f : R[M]
a✝ : M
⊢ (f.coeff.sum single).coeff a✝ = f.coeff a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝³ : DecidableEq γ
f : α → β → γ
s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(image2 f s t)
⊢ ↑(image2 f s t).toFinset = ↑(image₂ f s.toFinset t.toFinset)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
s : Set α
t : Set β
f : α → β → γ
hs : s.Finite
ht : t.Finite
hf : (image2 f s t).Finite
⊢ ↑hf.toFinset = ↑(image₂ f hs.toFinset ht.toFinset)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
r : R
x : M
a✝ : Mᵐᵒᵖ
⊢ (MonoidAlgebra.opRingEquiv (op (single x r))).coeff a✝ = (single (op x) (op r)).coeff a✝

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
r : Rᵐᵒᵖ
x : Mᵐᵒᵖ
a✝ : M
⊢ (unop (MonoidAlgebra.opRingEquiv.symm (single x r))).coeff a✝ = (unop (op (single (unop x) (unop r)))).coeff a✝

Tactic:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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
m₁ : M
n₁ : N
r₁ : R
m₂ : M
n₂ : N
r₂ : R
a✝¹ : M
a✝ : N
⊢ ((((((AddMonoidHom.mul.compr₂ curryAddEquiv.toAddMonoidHom).comp (singleAddHom (m₁, n₁))) r₁).comp
                (singleAddHom (m₂, n₂)))
              r₂).coeff
          a✝¹).coeff
      a✝ =
    (((((((AddMonoidHom.mul.comp curryAddEquiv.toAddMonoidHom).compl₂ curryAddEquiv.toAddMonoidHom).comp
                      (singleAddHom (m₁, n₁)))
                    r₁).comp
                (singleAddHom (m₂, n₂)))
              r₂).coeff
          a✝¹).coeff
      a✝

Tactic:
simp

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:
simp

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:
simp

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
a✝ : M
⊢ (single m (-r)).coeff a✝ = (-single m r).coeff a✝

Tactic:
simp

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
a✝ : M
⊢ (single m (r - s)).coeff a✝ = (single m r - single m s).coeff a✝

Tactic:
simp

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✝¹ * x✝ = a0 * b0
⊢ x✝¹ = a0 ∧ x✝ = b0

Tactic:
exact h ha hb k

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
s : Finset α
p : α → Prop
inst✝ : DecidablePred p
a✝ : α
⊢ a✝ ∈ ({x ∈ s | p x})⁻¹ ↔ a✝ ∈ {x ∈ s⁻¹ | p x⁻¹}

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : InvolutiveInv α
p : α → Prop
inst✝¹ : Fintype α
inst✝ : DecidablePred p
⊢ ↑{x | p x}⁻¹ = {x | p x⁻¹}

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
inst✝¹ : InvolutiveInv α
inst✝ : Fintype α
a✝ : α
⊢ a✝ ∈ univ⁻¹ ↔ a✝ ∈ univ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : InvolutiveInv α
s t : Finset α
⊢ ↑(s ∩ t)⁻¹ = ↑(s⁻¹ ∩ t⁻¹)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
hs : s.Nonempty
⊢ (s ^ 0).Nonempty

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case mp.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ (s ^ 0).Nonempty

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Finset.Basic

Goal state before:
pp: case hab
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s t : Finset α
n : ℕ
⊢ s ∩ t ⊆ s

Tactic:
simp

Goal state after: