mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.NAry

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

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
hf : ∀ b ∈ t, Injective fun a ↦ f a b
ht : ((fun b ↦ image (fun a ↦ f a b) s) '' ↑t).PairwiseDisjoint id
⊢ #s ∣ #(image₂ (fun b a ↦ f a b) t s)
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:
;

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
x✝ : R[M]
a✝ : M
⊢ ((mapRingEquiv M (e₁.trans e₂)) x✝).coeff a✝ = (((mapRingEquiv M e₁).trans (mapRingEquiv M e₂)) x✝).coeff a✝

Tactic:
;

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]
a✝ : M
⊢ (map f (-x)).coeff a✝ = (-map f x).coeff a✝

Tactic:
;

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]
a✝ : M
⊢ (map f (x - y)).coeff a✝ = (map f x - map f y).coeff a✝

Tactic:
;

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]
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:
;

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.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (s.sup' ⋯ fun i ↦ t.sup' ⋯ fun i' ↦ (g ∘ uncurry f) (i, i')) = s.sup' ⋯ fun x ↦ t.sup' ⋯ fun x_1 ↦ g (f x x_1)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (s.sup' ⋯ fun i ↦ t.sup' ⋯ fun i' ↦ (g ∘ uncurry f) (i, i')) = s.sup' ⋯ fun x ↦ t.sup' ⋯ fun x_1 ↦ g (f x x_1)
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:
;

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.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (t.sup' ⋯ fun i' ↦ s.sup' ⋯ fun i ↦ (g ∘ uncurry f) (i, i')) = t.sup' ⋯ fun y ↦ s.sup' ⋯ fun x ↦ g (f x y)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : SemilatticeSup δ
g : γ → δ
h : (image₂ f s t).Nonempty
⊢ (t.sup' ⋯ fun i' ↦ s.sup' ⋯ fun i ↦ (g ∘ uncurry f) (i, i')) = t.sup' ⋯ fun y ↦ s.sup' ⋯ fun x ↦ g (f x y)
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:
;

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

Tactic:
;

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]
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:
;

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

Tactic:
;

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)
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:
;

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

Tactic:
;

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.Defs

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

Tactic:
;

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

Tactic:
simp [Finsupp.single_add_erase]

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
x : R[M]
a✝ : M
⊢ (erase m x + single m (x.coeff m)).coeff a✝ = x.coeff a✝

Tactic:
;

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.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (s.sup fun i ↦ t.sup fun i' ↦ (g ∘ uncurry f) (i, i')) = s.sup fun x ↦ t.sup fun x_1 ↦ g (f x x_1)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (s.sup fun i ↦ t.sup fun i' ↦ (g ∘ uncurry f) (i, i')) = s.sup fun x ↦ t.sup fun x_1 ↦ g (f x x_1)
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:
;

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.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (t.sup fun i' ↦ s.sup fun i ↦ (g ∘ uncurry f) (i, i')) = t.sup fun y ↦ s.sup fun x ↦ g (f x y)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝¹ : SemilatticeSup δ
inst✝ : OrderBot δ
g : γ → δ
⊢ (t.sup fun i' ↦ s.sup fun i ↦ (g ∘ uncurry f) (i, i')) = t.sup fun y ↦ s.sup fun x ↦ g (f x y)
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:
;

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.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝ : Semiring R
motive : R[M] → Prop
x : R[M]
zero : motive 0
single_add : ∀ (m : M) (r : R) (x : R[M]), m ∉ x.coeff.support → r ≠ 0 → motive x → motive (single m r + x)
⊢ motive (ofCoeff 0)

Tactic:
simpa using zero

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

Tactic:
;

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)
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case h
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
⊢ {p ∈ x.coeff.support ×ˢ y.coeff.support | p.1 * p.2 = m} = {p ∈ s | p.1 ∈ x.coeff.support ∧ p.2 ∈ y.coeff.support}

Tactic:
;

Goal state after:
case h
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
⊢ {p ∈ x.coeff.support ×ˢ y.coeff.support | p.1 * p.2 = m} = {p ∈ s | p.1 ∈ x.coeff.support ∧ p.2 ∈ y.coeff.support}
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case h
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
a✝ : M × M
⊢ a✝ ∈ {p ∈ x.coeff.support ×ˢ y.coeff.support | p.1 * p.2 = m} ↔
    a✝ ∈ {p ∈ s | p.1 ∈ x.coeff.support ∧ p.2 ∈ y.coeff.support}

Tactic:
;

Goal state after:
case h
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
inst✝ : Mul M
x y : R[M]
m : M
s : Finset (M × M)
hs : ∀ {p : M × M}, p ∈ s ↔ p.1 * p.2 = m
F : M × M → R := fun p ↦ if p.1 * p.2 = m then x.coeff p.1 * y.coeff p.2 else 0
a✝ : M × M
⊢ a✝ ∈ {p ∈ x.coeff.support ×ˢ y.coeff.support | p.1 * p.2 = m} ↔
    a✝ ∈ {p ∈ s | p.1 ∈ x.coeff.support ∧ p.2 ∈ y.coeff.support}
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 t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑ht.toFinset)
u : Finset V
_hust : ↑u ⊆ s ∪ ↑ht.toFinset
hsu : s ⊆ ↑u
Eq : u.card = ht.toFinset.card
this : s.Finite
⊢ this.toFinset.card ≤ u.card

Tactic:
;

Goal state after:
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s t : Set V
ht : t.Finite
hs : LinearIndepOn K id s
hst : s ⊆ ↑(span K t)
this✝ : s ⊆ ↑(span K ↑ht.toFinset)
u : Finset V
_hust : ↑u ⊆ s ∪ ↑ht.toFinset
hsu : s ⊆ ↑u
Eq : u.card = ht.toFinset.card
this : s.Finite
⊢ this.toFinset.card ≤ u.card
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:
;

Goal state after:
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✝
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ᵐᵒᵖ
⊢ unop (MonoidAlgebra.opRingEquiv.symm (single x r)) = unop (op (single (unop x) (unop r)))

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_2
inst✝¹ : Semiring R
inst✝ : Mul M
r : Rᵐᵒᵖ
x : Mᵐᵒᵖ
⊢ unop (MonoidAlgebra.opRingEquiv.symm (single x r)) = unop (op (single (unop x) (unop r)))
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:
;

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
r : R
m : M
inst✝ : Mul M
hm : ∀ (m' : M), Commute m m'
hr : ∀ (r' : R), Commute r r'
x : R[M]
m' : M
r' : R
⊢ ((AddMonoidHom.mulLeft (single m r)).comp (singleAddHom m')) r' =
    ((AddMonoidHom.mulRight (single m r)).comp (singleAddHom m')) r'

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_4
inst✝¹ : Semiring R
r : R
m : M
inst✝ : Mul M
hm : ∀ (m' : M), Commute m m'
hr : ∀ (r' : R), Commute r r'
x : R[M]
m' : M
r' : R
⊢ ((AddMonoidHom.mulLeft (single m r)).comp (singleAddHom m')) r' =
    ((AddMonoidHom.mulRight (single m r)).comp (singleAddHom m')) r'
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case h
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₂
m' : M
a✝ : m' ∈ x.coeff.support
⊢ (if m' * m = m₁ then x.coeff m' * r else 0) = if m' = m₂ then x.coeff m' * r else 0

Tactic:
;

Goal state after:
case h
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₂
m' : M
a✝ : m' ∈ x.coeff.support
⊢ (if m' * m = m₁ then x.coeff m' * r else 0) = if m' = m₂ then x.coeff m' * r else 0
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case h
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₂
m' : M
a✝ : m' ∈ x.coeff.support
⊢ (if m * m' = m₁ then r * x.coeff m' else 0) = if m' = m₂ then r * x.coeff m' else 0

Tactic:
;

Goal state after:
case h
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₂
m' : M
a✝ : m' ∈ x.coeff.support
⊢ (if m * m' = m₁ then r * x.coeff m' else 0) = if m' = m₂ then r * x.coeff m' else 0
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 a✝ : M
⊢ (single (a * b) 1).coeff a✝ = (single a 1 * single b 1).coeff a✝

Tactic:
;

Goal state after:
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 a✝ : M
⊢ (single (a * b) 1).coeff a✝ = (single a 1 * single b 1).coeff a✝
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
a✝ : M
⊢ ((uniqueRingEquiv M).symm r).coeff a✝ = (single 1 r).coeff a✝

Tactic:
;

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : Monoid M
inst✝ : Subsingleton M
r : R
a✝ : M
⊢ ((uniqueRingEquiv M).symm r).coeff a✝ = (single 1 r).coeff a✝
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:
;

Goal state after:
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✝
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.coeff.sum fun m₁ r₁ ↦ y.coeff.sum fun m₂ r₂ ↦ if m₁ * m₂ = g then r₁ * r₂ else 0) =
    x.coeff.sum fun h r ↦ r * y.coeff (h⁻¹ * g)

Tactic:
;

Goal state after:
R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g : G
⊢ (x.coeff.sum fun m₁ r₁ ↦ y.coeff.sum fun m₂ r₂ ↦ if m₁ * m₂ = g then r₁ * r₂ else 0) =
    x.coeff.sum fun h r ↦ r * y.coeff (h⁻¹ * g)
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case h
R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g m₁ : G
a✝ : m₁ ∈ x.coeff.support
⊢ (y.coeff.sum fun m₂ r₂ ↦ if m₁ * m₂ = g then x.coeff m₁ * r₂ else 0) = x.coeff m₁ * y.coeff (m₁⁻¹ * g)

Tactic:
;

Goal state after:
case h
R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g m₁ : G
a✝ : m₁ ∈ x.coeff.support
⊢ (y.coeff.sum fun m₂ r₂ ↦ if m₁ * m₂ = g then x.coeff m₁ * r₂ else 0) = x.coeff m₁ * y.coeff (m₁⁻¹ * g)
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
⊢ (y.coeff.sum fun x' v' ↦ x.coeff.sum fun x v ↦ if x * x' = g then v * v' else 0) =
    y.coeff.sum fun h r ↦ x.coeff (g * h⁻¹) * r

Tactic:
;

Goal state after:
R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g : G
⊢ (y.coeff.sum fun x' v' ↦ x.coeff.sum fun x v ↦ if x * x' = g then v * v' else 0) =
    y.coeff.sum fun h r ↦ x.coeff (g * h⁻¹) * r
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: case h
R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g x' : G
a✝ : x' ∈ y.coeff.support
⊢ (x.coeff.sum fun x v ↦ if x * x' = g then v * y.coeff x' else 0) = x.coeff (g * x'⁻¹) * y.coeff x'

Tactic:
;

Goal state after:
case h
R : Type u_1
G : Type u_3
inst✝¹ : Semiring R
inst✝ : Group G
x y : R[G]
g x' : G
a✝ : x' ∈ y.coeff.support
⊢ (x.coeff.sum fun x v ↦ if x * x' = g then v * y.coeff x' else 0) = x.coeff (g * x'⁻¹) * y.coeff x'
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:
prod_cons,

Goal state after:
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)
⊢ single (m i) (r i) * ∏ x ∈ s, single (m x) (r x) = single (∏ i ∈ cons i s hi, m i) (∏ i ∈ cons i s hi, r i)