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

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Add M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : Multiplicative M →ₙ* A
a₁ a₂ : R[M]
⊢ (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp coeffAddEquiv.toAddMonoidHom)).toFun
      (a₁ * a₂) =
    (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp coeffAddEquiv.toAddMonoidHom)).toFun
        a₁ *
      (↑((liftAddHom fun x ↦ (smulAddHom R A).flip (f (Multiplicative.ofAdd x))).comp
              coeffAddEquiv.toAddMonoidHom)).toFun
        a₂

Tactic:
simpa using

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
A : Type u_4
B : Type u_5
C : Type u_6
M : Type u_7
N : Type u_8
O : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Add M
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
f : Multiplicative M →ₙ* A
a₁ a₂ : R[M]
⊢ (a₁.coeff.sum fun a b ↦
      a₂.coeff.sum fun a_1 b_1 ↦ (b * b_1) • (f (Multiplicative.ofAdd a) * f (Multiplicative.ofAdd a_1))) =
    a₂.coeff.sum fun a c ↦
      a₁.coeff.sum fun a_1 c_1 ↦ (c_1 * c) • (f (Multiplicative.ofAdd a_1) * f (Multiplicative.ofAdd a))
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p * X).coeff (n + 1) = p.coeff n

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (p * X).coeff (n + 1) = p.coeff n
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
⊢ (C a * X).natDegree = 1

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
ha : a ≠ 0
⊢ (C a * X).natDegree = 1
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).degree ≤ ↑n

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).degree ≤ ↑n
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).support ⊆ p.support

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ p.support.erase n ⊆ p.support
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case mp
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
h : (↑m).coeff 0 = (↑n).coeff 0
⊢ m = n

Tactic:
simpa using

Goal state after:
case mp
m n : ℕ
R : Type u_1
inst✝¹ : Semiring R
inst✝ : CharZero R
h : (↑m).coeff 0 = (↑n).coeff 0
⊢ m = n
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: case mp
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : (↑m).coeff 0 = (↑n).coeff 0
⊢ m = n

Tactic:
simpa using

Goal state after:
case mp
m n : ℤ
R : Type u_1
inst✝¹ : Ring R
inst✝ : CharZero R
h : (↑m).coeff 0 = (↑n).coeff 0
⊢ m = n
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
a : R
⊢ (C a * X).leadingCoeff = a

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
a : R
⊢ (C a * X).leadingCoeff = a
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).leadingCoeff = 1

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
⊢ (X ^ n).leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ X.leadingCoeff = 1

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ X.leadingCoeff = 1
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ f.degree < ↑n ↔ ∀ (m : ℕ), n ≤ m → f.coeff m = 0

Tactic:
simp only [degree, Finset.sup_lt_iff (WithBot.bot_lt_coe n), mem_support_iff,
    WithBot.coe_lt_coe, ← @not_le ℕ, max_eq_sup_coe, Nat.cast_withBot, Ne, not_imp_not]

Goal state after:
Module: Mathlib.Data.Nat.WithBot

Goal state before:
pp: x : WithBot ℕ
⊢ ¬x < 1 ↔ ¬x ≤ 0

Tactic:
simpa using

Goal state after:
x : WithBot ℕ
⊢ 1 ≤ x ↔ 0 < x
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
a : A
h : supDegree D q < D a
ha : a ∈ p.coeff.support
he : supDegree D p = D a
⊢ a ∈ (p + q).coeff.support

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
p q : R[A]
D : A → B
inst✝ : AddZeroClass A
a : A
h : supDegree D q < D a
ha : a ∈ p.coeff.support
he : supDegree D p = D a
⊢ ¬p.coeff a = 0
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
⊢ supDegree D (∑ x ∈ s.erase i, f x) < supDegree D (f i)

Tactic:
refine supDegree_sum_lt ?_ (fun j hj => ?_)

Goal state after:
case neg.refine_1
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
⊢ (s.erase i).Nonempty

case neg.refine_2
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
i : ι
f : ι → R[A]
inst✝ : AddZeroClass A
hi : i ∈ s
hmax : ∀ j ∈ s, j ≠ i → supDegree D (f j) < supDegree D (f i)
hs : (s.erase i).Nonempty
j : ι
hj : j ∈ s.erase i
⊢ supDegree D (f j) < supDegree D (f i)
Module: Mathlib.Algebra.Polynomial.Degree.Units

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
a p : R[X]
hp : p.Monic
hap : C (a.coeff 0) ∣ p
h : a.degree ≤ 0
⊢ IsUnit (C (a.coeff 0))

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
a p : R[X]
hp : p.Monic
hap : C (a.coeff 0) ∣ p
h : a.degree ≤ 0
⊢ IsUnit (a.coeff 0)
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C b).degree < (C a * X).degree

Tactic:
simpa using

Goal state after:
R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C b).degree < 1
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p✝ p q : R[X]
hp : eval₂ C X p = p
hq : eval₂ C X q = q
⊢ eval₂ C X (p + q) = p + q

Tactic:
by simp [hp, hq]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R✝ : Type u
S : Type v
T : Type w
ι✝ : Type y
a b : R✝
m n✝ : ℕ
inst✝³ : Semiring R✝
p✝ q✝ r : R✝[X]
inst✝² : Semiring S
f : R✝ →+* S
ι : Type ?u.38
inst✝¹ : Finite ι
R : ι → Type u_1
inst✝ : (i : ι) → Semiring (R i)
p q : ((i : ι) → R i)[X]
h : (RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i)) p = (RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i)) q
n : ℕ
i : ι
⊢ p.coeff n i = q.coeff n i

Tactic:
simpa using

Goal state after:
R✝ : Type u
S : Type v
T : Type w
ι✝ : Type y
a b : R✝
m n✝ : ℕ
inst✝³ : Semiring R✝
p✝ q✝ r : R✝[X]
inst✝² : Semiring S
f : R✝ →+* S
ι : Type ?u.38
inst✝¹ : Finite ι
R : ι → Type u_1
inst✝ : (i : ι) → Semiring (R i)
p q : ((i : ι) → R i)[X]
h : (RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i)) p = (RingHom.pi fun i ↦ mapRingHom (Pi.evalRingHom R i)) q
n : ℕ
i : ι
⊢ p.coeff n i = q.coeff n i
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
h : X ^ n + C a = 1
⊢ n = 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
h : X ^ n + C a = 1
⊢ n = 0
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
h : Function.Injective (map f)
r r' : R
eq : f r = f r'
⊢ r = r'

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
h : Function.Injective (map f)
r r' : R
eq : f r = f r'
⊢ r = r'
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
h✝ : Function.Surjective (map f)
s : S
p : R[X]
h : map f p = C s
⊢ f (p.coeff 0) = s

Tactic:
simpa using

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
h✝ : Function.Surjective (map f)
s : S
p : R[X]
h : map f p = C s
⊢ f (p.coeff 0) = s
Module: Mathlib.Algebra.Polynomial.Monomial

Goal state before:
pp: R : Type u
a b : R
m✝ n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Nontrivial R
m n : ℕ
h : (fun i ↦ (monomial i) 1) m = (fun i ↦ (monomial i) 1) n
⊢ m = n

Tactic:
simpa using

Goal state after:
R : Type u
a b : R
m✝ n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Nontrivial R
m n : ℕ
h : (fun i ↦ (monomial i) 1) m = (fun i ↦ (monomial i) 1) n
⊢ m = n
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case mp
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
h' : ∀ (i : κ), (embDomain f g₁) i ≤ (embDomain f g₂) i
x : ι
⊢ g₁ x ≤ g₂ x

Tactic:
simpa using

Goal state after:
case mp
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
h' : ∀ (i : κ), (embDomain f g₁) i ≤ (embDomain f g₂) i
x : ι
⊢ g₁ x ≤ g₂ x
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case mpr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
h : g₁ ≤ g₂
⊢ embDomain f g₁ ≤ embDomain f g₂

Tactic:
simp [Finsupp.le_def, embDomain_apply, apply_dite₂, Finsupp.le_def.mp h]

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι → κ
h : Function.Injective f
g₁ g₂ : ι →₀ α
⊢ mapDomain f g₁ ≤ mapDomain f g₂ ↔ g₁ ≤ g₂

Tactic:
simpa using

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι → κ
h : Function.Injective f
g₁ g₂ : ι →₀ α
⊢ mapDomain f g₁ ≤ mapDomain f g₂ ↔ g₁ ≤ g₂
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
f : ι → κ
h : Function.Injective f
g₁ g₂ : ι →₀ α
⊢ mapDomain f g₁ < mapDomain f g₂ ↔ g₁ < g₂

Tactic:
simpa using

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
f : ι → κ
h : Function.Injective f
g₁ g₂ : ι →₀ α
⊢ mapDomain f g₁ < mapDomain f g₂ ↔ g₁ < g₂
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedAddMonoid α
f : ι → κ
g : ι →₀ α
hg : 0 ≤ g
⊢ 0 ≤ mapDomain f g

Tactic:
simpa using

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedAddMonoid α
f : ι → κ
g : ι →₀ α
hg : 0 ≤ g
⊢ 0 ≤ mapDomain f g
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedAddMonoid α
f : ι → κ
g : ι →₀ α
hg : g ≤ 0
⊢ mapDomain f g ≤ 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : Preorder α
inst✝ : IsOrderedAddMonoid α
f : ι → κ
g : ι →₀ α
hg : g ≤ 0
⊢ mapDomain f g ≤ 0
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case inr
α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
H : f a ≠ 0
⊢ a ∈ f.support

Tactic:
simpa using

Goal state after:
case inr
α : Type u_5
M : Type u_6
N : Type u_7
inst✝³ : Zero M
inst✝² : AddCommMonoid N
inst✝¹ : PartialOrder N
inst✝ : IsOrderedAddMonoid N
f : α →₀ M
g : α → M → N
h : 0 ≤ fun x1 x2 ↦ g x1 x2
a : α
H : f a ≠ 0
⊢ ¬f a = 0
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q p' q' : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
hpq' : p'.comp q' = X
hqp' : q'.comp p' = X
h : p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp'
⊢ p = p'

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
p q p' q' : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
hpq' : p'.comp q' = X
hqp' : q'.comp p' = X
h : p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp'
⊢ p = p'
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p q p' q' : R[X]
hpq : p.comp q = X
hqp : q.comp p = X
hpq' : p'.comp q' = X
hqp' : q'.comp p' = X
h : p = p'
⊢ p.algEquivOfCompEqX q hpq hqp = p'.algEquivOfCompEqX q' hpq' hqp'

Tactic:
by ext1; simp [h]

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝¹ : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst✝ : (i : ι) → LinearOrder (β i)
hxy : toLex x ≤ toLex y
h : ∀ (j : ι), j < i → x j = y j
⊢ x i ≤ y i

Tactic:
contrapose! hxy
  apply not_le_of_gt
  use i
  aesop

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
β : ι → Type u_2
inst✝¹ : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst✝ : (i : ι) → LinearOrder (β i)
hxy : toColex x ≤ toColex y
h : ∀ (j : ι), j > i → x j = y j
⊢ x i ≤ y i

Tactic:
contrapose! hxy
  apply not_le_of_gt
  use i
  aesop

Goal state after:
Module: Mathlib.Order.PiLex

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝² : Preorder ι
inst✝¹ : DecidableEq ι
inst✝ : LT α
f : ι → α
i j : ι
h₁ : i ≤ j
h₂ : f j < f i
⊢ (fun {i} x1 x2 ↦ x1 < x2) (toLex (f ∘ ⇑(Equiv.swap i j)) i) (toLex f i)

Tactic:
simpa using

Goal state after:
ι : Type u_1
α : Type u_3
inst✝² : Preorder ι
inst✝¹ : DecidableEq ι
inst✝ : LT α
f : ι → α
i j : ι
h₁ : i ≤ j
h₂ : f j < f i
⊢ f j < f i
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommRing R
p q : R[X]
x✝¹ : Invertible 1 := invertibleOne
x✝ : Invertible (-1) := invertibleNeg 1
⊢ p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommRing R
p q : R[X]
x✝¹ : Invertible 1 := invertibleOne
x✝ : Invertible (-1) := invertibleNeg 1
⊢ p ∣ q.comp (-X) ↔ p.comp (-X) ∣ q
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case C
R : Type u
A : Type z
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
q : Submodule R M
m : M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hm : m ∈ q
a✝ : A
hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a✝) q
a : R
⊢ (aeval a✝) (C a) • m ∈ q

Tactic:
simpa using

Goal state after:
case C
R : Type u
A : Type z
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
q : Submodule R M
m : M
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
hm : m ∈ q
a✝ : A
hq : q ≤ Submodule.comap ((Algebra.lsmul R R M) a✝) q
a : R
⊢ a • m ∈ q
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
a : α
⊢ a ∈ f.neLocus g ↔ f a ≠ g a

Tactic:
simpa using

Goal state after:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
a : α
⊢ f a ≠ g a → f a ≠ 0 ∨ g a ≠ 0
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝⁴ : DecidableEq α
M : α → Type u_3
inst✝³ : (a : α) → Zero (N a)
inst✝² : (a : α) → Zero (M a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (M a)
f g : Π₀ (a : α), N a
F : (a : α) → N a → M a
F0 : ∀ (a : α), F a 0 = 0
a : α
⊢ a ∈ (mapRange F F0 f).neLocus (mapRange F F0 g) → a ∈ f.neLocus g

Tactic:
simpa using

Goal state after:
α : Type u_1
N : α → Type u_2
inst✝⁴ : DecidableEq α
M : α → Type u_3
inst✝³ : (a : α) → Zero (N a)
inst✝² : (a : α) → Zero (M a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (M a)
f g : Π₀ (a : α), N a
F : (a : α) → N a → M a
F0 : ∀ (a : α), F a 0 = 0
a : α
⊢ f a = g a → F a (f a) = F a (g a)
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
this : ∀ (i : ℕ), P.coeff i • Q = 0
⊢ Q.leadingCoeff • P = 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
this : ∀ (i : ℕ), P.coeff i • Q = 0
⊢ ∀ (n : ℕ), P.coeff n * Q.leadingCoeff = 0
Module: Mathlib.Data.DFinsupp.NeLocus

Goal state before:
pp: α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f₁ f₂ g : Π₀ (a : α), N a
⊢ (f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂

Tactic:
simpa using

Goal state after:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f₁ f₂ g : Π₀ (a : α), N a
⊢ (f₁ + -g).neLocus (f₂ + -g) = f₁.neLocus f₂
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
P : R[X]
⊢ P ∈ R[X]⁰ ↔ ∀ (a : R), a • P = 0 → a = 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
P : R[X]
⊢ P ∈ R[X]⁰ ↔ ∀ (a : R), a • P = 0 → a = 0
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hp : p.coeff n ∈ R⁰
r : R
hr : r • p = 0
⊢ r * p.coeff n = 0

Tactic:
simpa using

Goal state after:
R : Type u
inst✝ : CommSemiring R
p : R[X]
n : ℕ
hp : p.coeff n ∈ R⁰
r : R
hr : r • p = 0
⊢ r * p.coeff n = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case refine_1
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
A : Type u_2
inst✝ : Semiring A
f g : MvPolynomial σ R →+* A
hC : ∀ (r : R), f (C r) = g (C r)
hX : ∀ (i : σ), f (X i) = g (X i)
x : R
⊢ (f.comp singleZeroRingHom) x = (g.comp singleZeroRingHom) x

Tactic:
exact hC _

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
α : Type u_2
inst✝ : DecidableEq σ
s : Finset α
f : α → MvPolynomial σ R
⊢ (∑ x ∈ s, f x).support ⊆ s.biUnion fun x ↦ (f x).support

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
α : Type u_2
inst✝ : DecidableEq σ
s : Finset α
f : α → MvPolynomial σ R
⊢ (∑ i ∈ s, (f i).coeff).support ⊆ s.biUnion fun x ↦ (f x).coeff.support
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : σ →₀ ℕ
p : MvPolynomial σ R
s : R
ha : a ∉ p.support
hs : s ≠ 0
⊢ Disjoint ((monomial a) s).support p.support

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : σ →₀ ℕ
p : MvPolynomial σ R
s : R
ha : a ∉ p.support
hs : s ≠ 0
⊢ coeff a p = 0
Module: Mathlib.Data.Finsupp.Lex

Goal state before:
pp: case h.left
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ ∀ d < a, (single b 1) d = (single a 1) d

pp: case h.right
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (single b 1) a < (single a 1) a

Tactic:
· intro d hd
    simp only [Finsupp.single_eq_of_ne hd.ne, Finsupp.single_eq_of_ne (hd.trans h).ne]

Goal state after:
case h.right
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a < b
⊢ (single b 1) a < (single a 1) a
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : NeZero n
m : σ →₀ ℕ
a : R
i : σ
H : m + Finsupp.single i n = 0
⊢ False

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
n : ℕ
inst✝ : NeZero n
m : σ →₀ ℕ
a : R
i : σ
H : m + Finsupp.single i n = 0
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
s s' : σ
n : ℕ
⊢ coeff (Finsupp.single s' n) (X s) = if n = 1 ∧ s = s' then 1 else 0

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
s s' : σ
n : ℕ
⊢ coeff (Finsupp.single s' n) (X s) = if s = s' ∧ n = 1 then 1 else 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : m ∈ (p * (monomial s) r).support
⊢ ∃ j ∈ p.support, j + s = m

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
h : m ∈ (p * (monomial s) r).support
⊢ ∃ j, ¬coeff j p = 0 ∧ j + s = m
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
C : (σ →₀ ℕ) → R
hc : ∀ (i : σ →₀ ℕ), coeff i φ = r * C i
⊢ MvPolynomial.C r ∣ φ

Tactic:
classical
      let c' : (σ →₀ ℕ) → R := fun i => if i ∈ φ.support then C i else 0
      let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      apply MvPolynomial.ext
      intro i
      simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [notMem_support_iff] at hi
        rwa [mul_zero]

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

Goal state before:
pp: case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
r : R
φ : MvPolynomial σ R
⊢ (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) → C r ∣ φ

Tactic:
intro h
    choose C hc using h
    classical
      let c' : (σ →₀ ℕ) → R := fun i => if i ∈ φ.support then C i else 0
      let ψ : MvPolynomial σ R := ∑ i ∈ φ.support, monomial i (c' i)
      use ψ
      apply MvPolynomial.ext
      intro i
      simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']
      split_ifs with hi
      · rw [hc]
      · rw [notMem_support_iff] at hi
        rwa [mul_zero]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Subsingleton R
p : MvPolynomial σ R
⊢ p.coeffs = ∅

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Subsingleton R
p : MvPolynomial σ R
⊢ p = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
n : ℕ
⊢ (p ^ n).degrees ≤ n • p.degrees

Tactic:
simpa using

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
n : ℕ
⊢ (p ^ n).degrees ≤ n • p.degrees
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
h : ∀ (i_1 : σ →₀ ℕ), (if i = i_1 then x else 0) ∈ M
⊢ x ∈ M

Tactic:
simpa using

Goal state after:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
i : σ →₀ ℕ
x : S
h : ∀ (i_1 : σ →₀ ℕ), (if i = i_1 then x else 0) ∈ M
⊢ x ∈ M
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
x : S
⊢ C x ∈ coeffsIn σ M ↔ x ∈ M

Tactic:
simpa using

Goal state after:
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Module R S
M : Submodule R S
x : S
⊢ C x ∈ coeffsIn σ M ↔ x ∈ M