mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: u : ℕ → ℕ
f : ℕ → ℝ≥0∞
hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : StrictMono u
n k : ℕ
⊢ ↑(u (k + 1)) - ↑(u k) = ↑(u (k + 1) - u k)

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
⊢ 1 < 2

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
m✝ n✝ : ℕ
a✝¹ : 0 < m✝
a✝ : m✝ ≤ n✝
⊢ max m✝ (n + m) ∈ {x | n + m ≤ x}

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: f : ℕ → ℝ
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → 0 b ≤ f b
m : ℕ
hm : ∀ (b : ℕ), m ≤ b → f (b + 1) ≤ f b
m✝ n✝ : ℕ
a✝¹ : 0 < m✝
a✝ : m✝ ≤ n✝
⊢ max n✝ (n + m) ∈ {x | n + m ≤ x}

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: case inl
p : ℝ
hp : 0 ≤ p
⊢ 2 = 0 ∧ 1 - p ≠ 0 ∨ 1 < 2 ∧ 1 - p < 0 ∨ 2 < 1 ∧ 0 < 1 - p ↔ 1 < p

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: p : ℝ
⊢ (Summable fun n ↦ 1 / ↑n ^ p) ↔ 1 < p

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Module.ZLattice.Summable

Goal state before:
pp: E✝ : Type u_1
inst✝⁴ : NormedAddCommGroup E✝
L✝ : Submodule ℤ E✝
ι✝ : Type u_2
b✝ : Basis ι✝ ℤ ↥L✝
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : FiniteDimensional ℝ E
L : Submodule ℤ E
inst✝ : DiscreteTopology ↥L
ι : Type u_2
b : Basis ι ℤ ↥L
H : IsZLattice ℝ L
this✝ : Finite ι
b' : Basis ι ℝ E := Basis.ofZLatticeBasis ℝ L b
e : E ≃L[ℝ] ι → ℝ := (b'.repr ≪≫ₗ Finsupp.linearEquivFunOnFinite ℝ ℝ ι).toContinuousLinearEquiv
this : IsOpen (⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1)
⊢ 0 ∈ ⇑e ⁻¹' Set.univ.pi fun x ↦ Set.Ioo (-1) 1

Tactic:
simp

Goal state after:
Module: Mathlib.Analysis.PSeries

Goal state before:
pp: a s : ℝ
⊢ Nat.cast =ᶠ[atTop] fun n ↦ ‖↑n‖

Tactic:
simp

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

Goal state before:
pp: k : Type u_1
G : Type u_3
inst✝¹ : Monoid G
inst✝ : Semiring k
s : Set G
x : k[G]
⊢ 0 ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d * m'}

Tactic:
simp

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

Goal state before:
pp: k : Type u_1
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : Semiring k
s : Set A
x : k[A]
⊢ 0 ∈ {p | ∀ m ∈ p.coeff.support, ∃ m' ∈ s, ∃ d, m = d + m'}

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f g : ⨁ (x : ι), M
⊢ (f * g).toAddMonoidAlgebra.toDirectSum = (f.toAddMonoidAlgebra * g.toAddMonoidAlgebra).toDirectSum

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Cardinal

Goal state before:
pp: σ : Type u
R : Type v
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
⊢ #(MvPolynomial σ R) = lift.{u, v} #R

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Cardinal

Goal state before:
pp: case inl
σ : Type u
R : Type v
inst✝ : CommSemiring R
a✝ : Nontrivial R
h✝ : IsEmpty σ
⊢ #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Cardinal

Goal state before:
pp: case inr
σ : Type u
R : Type v
inst✝ : CommSemiring R
a✝ : Nontrivial R
h✝ : Nonempty σ
⊢ #(MvPolynomial σ R) ≤ max (max (lift.{u, v} #R) (lift.{v, u} #σ)) ℵ₀

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Cardinal

Goal state before:
pp: σ R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsEmpty σ
⊢ #(MvPolynomial σ R) = #R

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.GetD

Goal state before:
pp: α : Type u
β : Type v
l : List α
x : α
xs : List α
n : ℕ
d : α
i : Fin l.length
⊢ l[i]?.isSome = true

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: M : Type u_1
inst✝¹ : Zero M
inst✝ : DecidablePred fun i ↦ [].getD i 0 ≠ 0
a✝ : ℕ
⊢ [].toFinsupp a✝ = 0 a✝

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: case zero
M : Type u_1
inst✝¹ : Zero M
x : M
inst✝ : DecidablePred fun x_1 ↦ [x].getD x_1 0 ≠ 0
⊢ [x].toFinsupp 0 = (Finsupp.single 0 x) 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: case succ
M : Type u_1
inst✝¹ : Zero M
x : M
inst✝ : DecidablePred fun x_1 ↦ [x].getD x_1 0 ≠ 0
n✝ : ℕ
⊢ [x].toFinsupp (n✝ + 1) = (Finsupp.single 0 x) (n✝ + 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.List.ToFinsupp

Goal state before:
pp: R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst✝¹ : DecidablePred fun x ↦ l₁.getD x 0 ≠ 0
inst✝ : DecidablePred fun x ↦ l₂.getD x 0 ≠ 0
n : ℕ
⊢ (l₁ ++ l₂).toFinsupp n = (l₁.toFinsupp + Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp) n

Tactic:
simp only [toFinsupp_apply, Finsupp.add_apply]

Goal state after:
R : Type u_2
inst✝³ : AddZeroClass R
l₁ l₂ : List R
inst✝² : DecidablePred fun x ↦ (l₁ ++ l₂).getD x 0 ≠ 0
inst✝¹ : DecidablePred fun x ↦ l₁.getD x 0 ≠ 0
inst✝ : DecidablePred fun x ↦ l₂.getD x 0 ≠ 0
n : ℕ
⊢ (l₁ ++ l₂).getD n 0 = l₁.getD n 0 + (Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp) n
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs' : s.support ⊆ a.support
⊢ ∀ i ∈ a.support, a i ^ 0 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
a : α
f : α → ℕ
⊢ (f a + ∑ i ∈ ∅, f i).choose (f a) * multinomial ∅ f = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
s : σ →₀ ℕ
a : σ →₀ R
n : ℕ
hs : (s.sum fun x m ↦ m) = n
hs'' : s.support ⊆ a.support
hs' : ¬a.support.sum ⇑s = n
⊢ ∀ i ∈ a.support, 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
a : σ →₀ R
n : ℕ
x : σ → ℕ
hs : ((indicator a.support fun i x_1 ↦ x i).sum fun x m ↦ m) ≠ n
hx : a.support.sum x = n ∧ ∀ (i : σ), x i ≠ 0 → i ∈ a.support
⊢ ∀ i ∈ a.support, 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ (f a + f b + 1) * (f a + f b).choose (f a) = ((f a).succ + f b).choose (f a).succ * (f a).succ

Tactic:
add_one_mul_choose_eq (f a + f b) (f a),

Goal state after:
α : Type u_1
f : α → ℕ
a b : α
inst✝ : DecidableEq α
h : a ≠ b
⊢ (f a + f b + 1).choose (f a + 1) * (f a + 1) = ((f a).succ + f b).choose (f a).succ * (f a).succ
Module: Mathlib.Algebra.MvPolynomial.Coeff

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
d : σ →₀ ℕ
n : ℕ
⊢ ∑ i, X i = ∑ i, 1 i • X i

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case empty.zero
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
hc : (↑∅).Pairwise (Commute on f)
⊢ (∑ i ∈ ∅, f i) ^ 0 = ∑ k ∈ ∅.piAntidiag 0, ↑(multinomial ∅ k) * ∅.noncommProd (fun i ↦ f i ^ k i) ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case empty.succ
α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
hc : (↑∅).Pairwise (Commute on f)
n✝ : ℕ
⊢ (∑ i ∈ ∅, f i) ^ (n✝ + 1) = ∑ k ∈ ∅.piAntidiag (n✝ + 1), ↑(multinomial ∅ k) * ∅.noncommProd (fun i ↦ f i ^ k i) ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f)) (n : ℕ),
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f)
n : ℕ
p : ℕ × ℕ
g : α → ℕ
⊢ ↑s ⊆ ↑(cons a s has)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f)) (n : ℕ),
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ antidiagonal n,
    ∑ g ∈ s.piAntidiag p.2,
        ↑((g a + p.1 + s.sum g).choose (g a + p.1)) * ↑(multinomial s (g + fun i ↦ if i = a then p.1 else 0)) *
          (f a ^ (g a + p.1) * s.noncommProd (fun i ↦ f i ^ (g i + if i = a then p.1 else 0)) ⋯) =
      ∑ g ∈ s.piAntidiag p.2, ↑(n.choose p.1) * ↑(multinomial s g) * (f a ^ p.1 * s.noncommProd (fun i ↦ f i ^ g i) ⋯)
i : α
hi : i ∈ s
⊢ a ∈ ↑(cons a s has)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
f : α → R
a : α
s : Finset α
has : a ∉ s
ih :
  ∀ (hc : (↑s).Pairwise (Commute on f)) (n : ℕ),
    (∑ i ∈ s, f i) ^ n = ∑ k ∈ s.piAntidiag n, ↑(multinomial s k) * s.noncommProd (fun i ↦ f i ^ k i) ⋯
hc : (↑(cons a s has)).Pairwise (Commute on f)
n : ℕ
this :
  ∀ p ∈ antidiagonal n,
    ∑ g ∈ s.piAntidiag p.2,
        ↑((g a + p.1 + s.sum g).choose (g a + p.1)) * ↑(multinomial s (g + fun i ↦ if i = a then p.1 else 0)) *
          (f a ^ (g a + p.1) * s.noncommProd (fun i ↦ f i ^ (g i + if i = a then p.1 else 0)) ⋯) =
      ∑ g ∈ s.piAntidiag p.2, ↑(n.choose p.1) * ↑(multinomial s g) * (f a ^ p.1 * s.noncommProd (fun i ↦ f i ^ g i) ⋯)
⊢ ↑s ⊆ ↑(cons a s has)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Division

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝¹ : CommRing R
p✝ q✝ : MvPolynomial σ R
inst✝ : IsCancelMulZero R
n✝ : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ),
    Finsupp.degree n = d →
      ∀ (p q : MvPolynomial σ R), p ∣ (monomial n) 1 * q ↔ ∃ m r, m ≤ n ∧ r ∣ q ∧ p = (monomial m) 1 * r
n : σ →₀ ℕ
hn : Finsupp.degree n = d + 1
p q : MvPolynomial σ R
hp : p ∣ (monomial n) 1 * q
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
⊢ Finsupp.degree n' + 1 = Finsupp.degree (n' + Finsupp.single i 1)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Finset

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : OrderBot R
inst✝ : CanonicallyOrderedAdd R
s : Finset ι
f : ι → ℕ
⊢ ↑⊥ = ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Finset

Goal state before:
pp: case empty
R : Type u_1
ι : Type u_2
inst✝³ : LinearOrder R
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : OrderBot R
f : ι → R
a : R
⊢ a * ∅.sup f = ∅.sup fun x ↦ a * f x

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Finset

Goal state before:
pp: case empty
R : Type u_1
ι : Type u_2
inst✝³ : LinearOrder R
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : CanonicallyOrderedAdd R
inst✝ : OrderBot R
f : ι → R
a : R
⊢ ∅.sup f * a = ∅.sup fun x ↦ f x * a

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: case h
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
d : σ →₀ ℕ
r : R
⊢ ∀ i ∈ d.support, X i ^ 0 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (expand 0) (X i) = ((Algebra.ofId R (MvPolynomial σ R)).comp (aeval 1)) (X i)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ (expand 0) f = C ((eval 1) f)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ (expand 1) (X i) = (AlgHom.id R (MvPolynomial σ R)) (X i)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
f : MvPolynomial σ R
⊢ (expand 1) f = f

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
R : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Semiring R
x : α → R
hc : (↑∅).Pairwise (Commute on x)
⊢ (↑↑⟨0, ⋯⟩).countPerms = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → MvPolynomial τ R
i : σ
⊢ ((expand p).comp (bind₁ f)) (X i) = (bind₁ fun i ↦ (expand p) (f i)) (X i)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : σ → τ
i : σ
⊢ ((rename f).comp (expand p)) (X i) = ((expand p).comp (rename f)) (X i)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: case hC
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
x✝ : R
⊢ (((eval₂Hom f g).comp ↑(expand p)).comp C) x✝ = ((eval₂Hom f (g ^ p)).comp C) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: case hX
σ : Type u_1
R : Type u_3
S : Type u_4
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : ℕ
f : R →+* S
g : σ → S
i✝ : σ
⊢ ((eval₂Hom f g).comp ↑(expand p)) (X i✝) = (eval₂Hom f (g ^ p)) (X i✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝² : CommSemiring R
p : ℕ
A : Type u_5
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f : σ → A
i✝ : σ
⊢ ((aeval f).comp (expand p)) (X i✝) = (aeval (f ^ p)) (X i✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
φ : MvPolynomial σ R
i : σ
a : σ →₀ ℕ
⊢ (p • a) i = p * a i

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
⊢ ((expand p) f).totalDegree = f.totalDegree * p

Tactic:
rcases p.eq_zero_or_pos with hp | hp

Goal state after:
case inl
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p = 0
⊢ ((expand p) f).totalDegree = f.totalDegree * p

case inr
σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
⊢ ((expand p) f).totalDegree = f.totalDegree * p
Module: Mathlib.Algebra.MvPolynomial.Expand

Goal state before:
pp: σ : Type u_1
R : Type u_3
inst✝ : CommSemiring R
p : ℕ
f : MvPolynomial σ R
hp : p > 0
hf : ¬f = 0
d : σ →₀ ℕ
⊢ ∀ i ∈ d.support, id 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Polynomial

Goal state before:
pp: case C
R : Type u_1
S : Type u_2
σ : Type u_3
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x : S
f : R →+* Polynomial S
g : σ → Polynomial S
p : MvPolynomial σ R
⊢ ∀ (a : R),
    Polynomial.eval x (eval₂ f g (C a)) =
      eval₂ ((Polynomial.evalRingHom x).comp f) (fun s ↦ Polynomial.eval x (g s)) (C a)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Polynomial

Goal state before:
pp: R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
r : R
⊢ ((eval x).comp ((Polynomial.evalRingHom q).comp (Polynomial.C.comp C))) r = (RingHom.id R) r

Tactic:
simp

Goal state after:
R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
r : R
| r
Module: Mathlib.Algebra.MvPolynomial.Polynomial

Goal state before:
pp: R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
i : Fin (n + 1)
⊢ (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) 0)) = Fin.cases ((eval x) q) x 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Polynomial

Goal state before:
pp: R : Type u_1
n : ℕ
x : Fin n → R
inst✝ : CommSemiring R
f : MvPolynomial (Fin (n + 1)) R
q : MvPolynomial (Fin n) R
i : Fin (n + 1)
⊢ ∀ (i : Fin n),
    (eval x) (Polynomial.eval q (Fin.cases Polynomial.X (fun k ↦ Polynomial.C (X k)) i.succ)) =
      Fin.cases ((eval x) q) x i.succ

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Funext

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ih :
  ∀ {p : MvPolynomial (Fin n) R} (s : Fin n → Set R),
    (∀ (i : Fin n), (s i).Infinite) → (∀ x ∈ Set.univ.pi s, (eval x) p = 0) → p = 0
p : MvPolynomial (Fin (n + 1)) R
s : Fin (n + 1) → Set R
hs : ∀ (i : Fin (n + 1)), (s i).Infinite
h : ∀ x ∈ Set.univ.pi s, (eval x) p = 0
r : R
hr : r ∈ s 0
x : Fin n → R
hx : x ∈ Set.univ.pi fun x ↦ s x.succ
⊢ (eval fun i ↦ Fin.cases ((eval x) (C r)) x i) p = 0

Tactic:
exact h _ fun i _ ↦ i.cases (by simpa [eval_C] using hr) (by simpa using hx)

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
⊢ ∀ i ∈ s, id 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
⊢ ∀ i ∈ s, 0! = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: σ : Type u_1
d : σ →₀ ℕ
s : Finset σ
h : d.support ⊆ s
⊢ (∑ i ∈ s, d i)! / ∏ i ∈ s, (d i)! = (∑ x ∈ s, id (d x))! / ∏ x ∈ s, (d x)!

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommMonoid α
inst✝ : DecidableEq α
l : List α
⊢ ([].toFinsupp.sum fun x a ↦ a) = [].sum

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommMonoid α
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
⊢ ∀ a ∈ (Finsupp.single 0 x).support ∪ (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp).support, 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: α : Type u_1
inst✝¹ : AddCommMonoid α
inst✝ : DecidableEq α
l✝ : List α
x : α
l : List α
⊢ ∀ a ∈ (Finsupp.single 0 x).support ∪ (Finsupp.embDomain (addRightEmbedding 1) l.toFinsupp).support,
    ∀ (b₁ b₂ : α), b₁ + b₂ = b₁ + b₂

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case nil
m : Multiset ℕ
l l' : List ℕ
⊢ [].multinomial = [].multinomial

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case empty
m' : Multiset ℕ
⊢ (0 + m').multinomial = (0 + m').sum.choose (sum 0) * multinomial 0 * m'.multinomial

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case zero
m : Multiset ℕ
⊢ (0 • m).multinomial = (Nat.multinomial (Finset.range 0) fun x ↦ m.sum) * m.multinomial ^ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: m : Multiset ℕ
k : ℕ
hk : (k • m).multinomial = (Nat.multinomial (Finset.range k) fun x ↦ m.sum) * m.multinomial ^ k
⊢ k ∉ Finset.range k

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Nat.Choose.Multinomial

Goal state before:
pp: case empty
⊢ 0 < multinomial 0

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
a : WithBot (σ →₀ ℕ)
⊢ m.toWithBotSyn a ≤ ⊥ ↔ a = ⊥

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder

Goal state before:
pp: case h
⊢ (∀ (j : ℕ),
      (fun x1 x2 ↦ x1 < x2) j 0 → (ofLex (toLex (single 0 1 + single 1 1))) j = (ofLex (toLex (single 0 2))) j) ∧
    (fun {i} x1 x2 ↦ x1 < x2) ((ofLex (toLex (single 0 1 + single 1 1))) 0) ((ofLex (toLex (single 0 2))) 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder

Goal state before:
pp: case h
⊢ (∀ (j : ℕ), (fun x1 x2 ↦ x1 < x2) j 0 → (ofLex (toLex (single 1 1))) j = (ofLex (toLex (single 0 1))) j) ∧
    (fun {i} x1 x2 ↦ x1 < x2) ((ofLex (toLex (single 1 1))) 0) ((ofLex (toLex (single 0 1))) 0)

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder

Goal state before:
pp: case h
⊢ (∀ (j : ℕ), (fun x1 x2 ↦ x1 < x2) j 0 → (ofLex (toLex (single 1 1))) j = (ofLex (toLex (single 0 2))) j) ∧
    (fun {i} x1 x2 ↦ x1 < x2) ((ofLex (toLex (single 1 1))) 0) ((ofLex (toLex (single 0 2))) 0)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder.DegLex

Goal state before:
pp: case a
σ : Type u_1
R : Type u_2
inst✝² : CommSemiring R
f : MvPolynomial σ R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
hf : ¬f = 0
⊢ f.totalDegree ≤ Finsupp.degree (degLex.degree f)

Tactic:
· unfold MvPolynomial.totalDegree
    apply Finset.sup_le
    intro b hb
    exact DegLex.monotone_degree (degLex.le_degree hb)

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

Goal state before:
pp: case inr.empty
R : Type u_1
σ : Type u_2
n : σ
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
ι : Type u_3
f : ι → MvPolynomial σ R
nontrivial : Nontrivial (MvPolynomial σ R)
h : ∀ i ∈ ∅, f i ≠ 0
⊢ degreeOf n (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, degreeOf n (f i)

Tactic:
simp

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

Goal state before:
pp: R : Type u_1
σ : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
i : σ
p : MvPolynomial σ R
n : ℕ
hp : p ≠ 0
⊢ ∑ i_1 ∈ range n, degreeOf i p = n * degreeOf i p

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f g : DegLex (α →₀ ℕ)
⊢ (fun f ↦ toLex (degree (ofDegLex f), toLex (ofDegLex f))) f =
      (fun f ↦ toLex (degree (ofDegLex f), toLex (ofDegLex f))) g →
    f = g

Tactic:
simp

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

Goal state before:
pp: case neg
R : Type u_1
σ : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial σ R
j : σ
c : R
hc : c ∈ R⁰
hp : ¬p = 0
⊢ ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) (C c))).natDegree +
      ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) p)).natDegree =
    ((optionEquivLeft R { b // b ≠ j }) ((renameEquiv R (optionSubtypeNe j).symm) p)).natDegree

Tactic:
simp

Goal state after:
Module: Mathlib.Data.Finsupp.MonomialOrder.DegLex

Goal state before:
pp: case h
α : Type u_1
⊢ (∀ (j : Fin 2),
      (fun x1 x2 ↦ x1 < x2) j 0 →
        (ofLex (toLex (single 0 1) + toLex (single 1 1))) j = (ofLex (toLex (single 0 2))) j) ∧
    (fun {i} x1 x2 ↦ x1 < x2) ((ofLex (toLex (single 0 1) + toLex (single 1 1))) 0) ((ofLex (toLex (single 0 2))) 0)

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
hc : c = 0
⊢ m.toSyn.symm (∅.sup ⇑m.toSyn) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: case neg
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝¹ : CommSemiring R
d : σ →₀ ℕ
c : R
inst✝ : Decidable (c = 0)
hc : ¬c = 0
⊢ m.toSyn.symm ({d}.sup ⇑m.toSyn) = d

Tactic:
simp

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.MonomialOrder

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ (if 1 = 0 then 0 else 0) = 0

Tactic:
simp

Goal state after: