mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ comapDomain f hf (single (f m) r) = single m r

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

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

Tactic:
ext

Goal state after:
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✝
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
f : N →ₙ* O
g : M →ₙ* N
⊢ mapDomainNonUnitalRingHom R (f.comp g) = (mapDomainNonUnitalRingHom R f).comp (mapDomainNonUnitalRingHom R g)

Tactic:
ext

Goal state after:
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
f : N →ₙ* O
g : M →ₙ* N
x✝ : R[M]
a✝ : O
⊢ ((mapDomainNonUnitalRingHom R (f.comp g)) x✝).coeff a✝ =
    (((mapDomainNonUnitalRingHom R f).comp (mapDomainNonUnitalRingHom R g)) x✝).coeff a✝
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]
⊢ (fun x ↦ mapDomain (⇑e.symm) x) ((fun x ↦ mapDomain (⇑e) x) x) = x

Tactic:
ext

Goal state after:
ι : 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✝
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]
⊢ (fun x ↦ mapDomain (⇑e) x) ((fun x ↦ mapDomain (⇑e.symm) x) x) = x

Tactic:
ext

Goal state after:
ι : 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✝
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]
⊢ mapDomain (⇑e) (x + y) = mapDomain (⇑e) x + mapDomain (⇑e) y

Tactic:
ext

Goal state after:
ι : 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✝
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
N : Type u_7
inst✝² : Semiring R
inst✝¹ : Mul M
inst✝ : Mul N
e : M ≃ N
x : R[M]
⊢ ((mapDomainAddEquiv R e) x).coeff = equivMapDomain e x.coeff

Tactic:
ext

Goal state after:
R : Type u_3
M : Type u_6
N : Type u_7
inst✝² : Semiring R
inst✝¹ : Mul M
inst✝ : Mul N
e : M ≃ N
x : R[M]
a✝ : N
⊢ ((mapDomainAddEquiv R e) x).coeff a✝ = (equivMapDomain e x.coeff) a✝
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
⊢ mapDomainAddEquiv R (e₁.trans e₂) = (mapDomainAddEquiv R e₁).trans (mapDomainAddEquiv R e₂)

Tactic:
ext

Goal state after:
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✝
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]
⊢ map (↑e.symm) (map (↑e) x) = x

Tactic:
ext

Goal state after:
ι : 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✝
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]
⊢ map (↑e) (map (↑e.symm) x) = x

Tactic:
ext

Goal state after:
ι : 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✝
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
⊢ mapAddEquiv M (e₁.trans e₂) = (mapAddEquiv M e₁).trans (mapAddEquiv M e₂)

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Mul M
f : R →+* S
x y : R[M]
⊢ map (↑f) (x * y) = map (↑f) x * map (↑f) y

Tactic:
ext

Goal state after:
R : Type u_3
S : Type u_4
M : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Mul M
f : R →+* S
x y : R[M]
a✝ : M
⊢ (map (↑f) (x * y)).coeff a✝ = (map (↑f) x * map (↑f) y).coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Mul M
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 [mul_def, sum_mapRange_index, map_finsuppSum, single_apply, apply_ite]

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

Goal state before:
pp: R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
⊢ mapDomainRingHom R (MonoidHom.id M) = RingHom.id R[M]

Tactic:
ext

Goal state after:
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✝

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✝
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
f : N →* O
g : M →* N
⊢ mapDomainRingHom R (f.comp g) = (mapDomainRingHom R f).comp (mapDomainRingHom R g)

Tactic:
ext

Goal state after:
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✝

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✝
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
S : Type u_4
M : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Monoid M
f : R →+* S
⊢ map (↑f) 1 = 1

Tactic:
ext

Goal state after:
R : Type u_3
S : Type u_4
M : Type u_6
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Monoid M
f : R →+* S
a✝ : M
⊢ (map (↑f) 1).coeff a✝ = (coeff 1) a✝
Module: Mathlib.Algebra.MonoidAlgebra.MapDomain

Goal state before:
pp: R : Type u_3
M : Type u_6
inst✝¹ : Semiring R
inst✝ : Monoid M
⊢ mapRingHom M (RingHom.id R) = RingHom.id R[M]

Tactic:
ext

Goal state after:
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✝

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✝
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
f : S →+* T
g : R →+* S
⊢ mapRingHom M (f.comp g) = (mapRingHom M f).comp (mapRingHom M g)

Tactic:
ext

Goal state after:
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✝

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✝
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
⊢ mapDomainRingEquiv R (e₁.trans e₂) = (mapDomainRingEquiv R e₁).trans (mapDomainRingEquiv R e₂)

Tactic:
ext

Goal state after:
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✝
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
⊢ mapRingEquiv M (e₁.trans e₂) = (mapRingEquiv M e₁).trans (mapRingEquiv M e₂)

Tactic:
ext

Goal state after:
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✝
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]
⊢ map f (-x) = -map f x

Tactic:
ext

Goal state after:
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✝
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]
⊢ map f (x - y) = map f x - map f y

Tactic:
ext

Goal state after:
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✝
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]
⊢ (fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Multiplicative.toAdd) x.coeff))
      ((fun x ↦ MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff)) x) =
    x

Tactic:
ext

Goal state after:
ι : 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✝
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)
⊢ (fun x ↦ MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff))
      ((fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Multiplicative.toAdd) x.coeff)) x) =
    x

Tactic:
ext

Goal state after:
ι : 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✝
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 y : R[M]
⊢ MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) (x * y).coeff) =
    MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff) *
      MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) y.coeff)

Tactic:
ext

Goal state after:
ι : 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 y : R[M]
a✝ : Multiplicative M
⊢ (MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) (x * y).coeff)).coeff a✝ =
    (MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) x.coeff) *
          MonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Multiplicative.ofAdd) y.coeff)).coeff
      a✝
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
⊢ erase m 0 = 0

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_4
inst✝ : Semiring R
m a✝ : M
⊢ (erase m 0).coeff a✝ = (coeff 0) a✝
Module: Mathlib.Algebra.MonoidAlgebra.Defs

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

Tactic:
ext

Goal state after:
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✝
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]
⊢ (fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Additive.toMul) x.coeff))
      ((fun x ↦ AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff)) x) =
    x

Tactic:
ext

Goal state after:
ι : 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✝
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 • single m r = single m (a • r)

Tactic:
ext

Goal state after:
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✝
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)
⊢ (fun x ↦ AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff))
      ((fun x ↦ ofCoeff (Finsupp.mapDomain (⇑Additive.toMul) x.coeff)) x) =
    x

Tactic:
ext

Goal state after:
ι : 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✝
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
⊢ single m (r₁ + r₂) = single m r₁ + single m r₂

Tactic:
ext

Goal state after:
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✝
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 y : R[M]
⊢ AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) (x * y).coeff) =
    AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff) *
      AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) y.coeff)

Tactic:
ext

Goal state after:
ι : 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 y : R[M]
a✝ : Additive M
⊢ (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) (x * y).coeff)).coeff a✝ =
    (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) x.coeff) *
          AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (⇑Additive.ofMul) y.coeff)).coeff
      a✝
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
x : R[M]
⊢ single m (x.coeff m) + erase m x = x

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
x : R[M]
a✝ : M
⊢ (single m (x.coeff m) + erase m x).coeff a✝ = x.coeff a✝
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
x : R[M]
⊢ erase m x + single m (x.coeff m) = x

Tactic:
ext

Goal state after:
R : Type u_1
M : Type u_4
inst✝ : Semiring R
m : M
x : R[M]
a✝ : M
⊢ (erase m x + single m (x.coeff m)).coeff a✝ = x.coeff a✝
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
⊢ f = (f.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom

Tactic:
ext

Goal state after:
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✝
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
⊢ g = (g.comp coeffAddEquiv.symm.toAddMonoidHom).comp coeffAddEquiv.toAddMonoidHom

Tactic:
ext

Goal state after:
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✝
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
⊢ (toAdditive R M) (single m r) = AddMonoidAlgebra.single (Additive.ofMul m) r

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.Algebra.MonoidAlgebra.Defs

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

Tactic:
ext

Goal state after:
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✝
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: ι : Type u_14
α : ι → Type u_15
β : ι → Type u_16
γ : ι → Type u_17
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → α i → β i → γ i
s : (i : ι) → Finset (α i)
t : (i : ι) → Finset (β i)
⊢ (piFinset fun i ↦ image₂ (f i) (s i) (t i)) = image₂ (fun a b i ↦ f i (a i) (b i)) (piFinset s) (piFinset t)

Tactic:
ext

Goal state after:
ι : Type u_14
α : ι → Type u_15
β : ι → Type u_16
γ : ι → Type u_17
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (γ i)
f : (i : ι) → α i → β i → γ i
s : (i : ι) → Finset (α i)
t : (i : ι) → Finset (β i)
a✝ : (a : ι) → γ a
⊢ (a✝ ∈ piFinset fun i ↦ image₂ (f i) (s i) (t i)) ↔ a✝ ∈ image₂ (fun a b i ↦ f i (a i) (b i)) (piFinset s) (piFinset t)