mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: case mul_X
R : Type u
S₁ : Type v
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
k : S₁ →+* S₂
f : R →+* S₁
g : σ → S₁
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p) → k (eval₂ f g (p * X n)) = eval₂ k (⇑k ∘ g) ((map f) (p * X n))

Tactic:
intro p s hp
    rw [eval₂_mul, k.map_mul, (map f).map_mul, eval₂_mul, map_X, hp, eval₂_X, eval₂_X, comp_apply]

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

Goal state before:
pp: case mul_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p : MvPolynomial S₂ R
s : S₂
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
⊢ eval₂ C (⇑(map f) ∘ g) ((map f) p) * (map f) (g s) = eval₂ C (⇑(map f) ∘ g) ((map f) p) * (⇑(map f) ∘ g) s

Tactic:
comp_apply

Goal state after:
case mul_X
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p✝ p : MvPolynomial S₂ R
s : S₂
hp : (map f) (eval₂ C g p) = eval₂ C (⇑(map f) ∘ g) ((map f) p)
⊢ eval₂ C (⇑(map f) ∘ g) ((map f) p) * (map f) (g s) = eval₂ C (⇑(map f) ∘ g) ((map f) p) * (map f) (g s)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ degrees 0 = 0

Tactic:
← C_0

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ (C 0).degrees = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ degrees 0 = 0

Tactic:
rw [← C_0]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ (C 0).degrees = 0
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✝ : Algebra R S
M : Submodule R S
⊢ coeffsIn σ M ^ 0 ≤ coeffsIn σ (M ^ 0)

Tactic:
simpa using ⟨1, map_one _⟩

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : R
x : σ
⊢ degreeOf x (C a) = 0

Tactic:
by
  classical simp [degreeOf_def, degrees_C]

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

Goal state before:
pp: case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
⊢ (φ ^ (n + 1)).vars ⊆ φ.vars

Tactic:
rw [pow_succ']

Goal state after:
case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
⊢ (φ * φ ^ n).vars ⊆ φ.vars
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
⊢ (-p).degrees = p.degrees

Tactic:
rw [degrees, support_neg]; rfl

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
f : MvPolynomial σ R
h : i ≠ j
⊢ degreeOf i (f * X j) = degreeOf i f

Tactic:
by
  classical
  simp only [degreeOf_eq_sup i, support_mul_X, Finset.sup_map]
  congr
  ext
  simp only [Finsupp.single, addRightEmbedding_apply, coe_mk,
    Pi.add_apply, comp_apply, Finsupp.coe_add, Pi.single_eq_of_ne h, add_zero]

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

Goal state before:
pp: case e'_4
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ 1 = Multiset.count j {j}

Tactic:
rw [Multiset.count_singleton_self]

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

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
inst✝² : Algebra R S₁
f : σ → S₁
B : Type u_2
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
φ : S₁ →ₐ[R] B
p : MvPolynomial σ R
⊢ φ ((aeval f) p) = (⇑φ ∘ ⇑(aeval f)) p

Tactic:
comp_apply

Goal state after:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
inst✝² : Algebra R S₁
f : σ → S₁
B : Type u_2
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
φ : S₁ →ₐ[R] B
p : MvPolynomial σ R
⊢ φ ((aeval f) p) = φ ((aeval f) p)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : CommSemiring S
f : R →+* S
⊢ ((map f) p).vars ⊆ p.vars

Tactic:
classical simp [vars_def, Multiset.subset_of_le degrees_map_le]

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

Goal state before:
pp: case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
h : p ≠ 0
k : ℕ
hk : degreeOf i (p * X i ^ k) = degreeOf i p + k
⊢ degreeOf i (p * X i ^ (k + 1)) = degreeOf i p + (k + 1)

Tactic:
have : p * X i ^ k ≠ 0 := by
      rcases ne_zero_iff.mp h with ⟨s, hs⟩
      refine ne_zero_iff.mpr ⟨s + Finsupp.single i k, ?_⟩
      rwa [X_pow_eq_monomial, coeff_mul_monomial, mul_one]
    rw [pow_add, pow_one, ← mul_assoc,
      (degreeOf_mul_X_eq_degreeOf_add_one_iff i _).mpr this, hk, add_assoc]

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

Goal state before:
pp: case neg.h₁
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬constantCoeff p = 0
⊢ 0 ∉ p.support → (f (coeff 0 p) * Finsupp.prod 0 fun i k ↦ g i ^ k) = 0

Tactic:
rw [constantCoeff_eq, coeff, ← Ne, ← Finsupp.mem_support_iff] at h0

Goal state after:
case neg.h₁
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : 0 ∈ p.coeff.support
⊢ 0 ∉ p.support → (f (coeff 0 p) * Finsupp.prod 0 fun i k ↦ g i ^ k) = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ totalDegree 0 = 0

Tactic:
← C_0

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ (C 0).totalDegree = 0
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ totalDegree 0 = 0

Tactic:
rw [← C_0]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
⊢ (C 0).totalDegree = 0
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : 0 ∉ p.coeff.support
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ ¬d = 0

Tactic:
rintro rfl

Goal state after:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : 0 ∉ p.coeff.support
hd : 0 ∈ p.support
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬0 ∉ p.coeff.support
d : σ →₀ ℕ
hd : d ∈ p.support
hd0 : d ≠ 0
⊢ ¬d = 0

Tactic:
rintro rfl

Goal state after:
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
h0 : ¬0 ∉ p.coeff.support
hd : 0 ∈ p.support
hd0 : 0 ≠ 0
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
⊢ p = C (coeff 0 p)

Tactic:
ext m

Goal state after:
case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
m : σ →₀ ℕ
⊢ coeff m p = coeff m (C (coeff 0 p))
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p = 0 → p.coeff p.natTrailingDegree = 0

Tactic:
rintro rfl

Goal state after:
case mpr
R : Type u
inst✝ : Semiring R
⊢ coeff 0 (natTrailingDegree 0) = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
i : ℕ
⊢ f.eraseLead.coeff i = if i = f.natDegree then 0 else f.coeff i

Tactic:
by
  simp only [eraseLead, coeff_erase]

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

Goal state before:
pp: case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
n : ℕ
nd : ¬n = p.natDegree
⊢ ¬n = (p + q).natDegree

Tactic:
rintro rfl

Goal state after:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : q.degree < p.degree
nd : ¬(p + q).natDegree = p.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
n : ℕ
nd : ¬n = q.natDegree
⊢ ¬n = (p + q).natDegree

Tactic:
rintro rfl

Goal state after:
case neg.hnc
R : Type u_1
inst✝ : Semiring R
p q : R[X]
pq : p.degree < q.degree
nd : ¬(p + q).natDegree = q.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
h4 : map f p ≠ 0
⊢ (map f p).coeff p.natDegree ≠ 0

Tactic:
← h3,

Goal state after:
case inr
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p ≠ 0
h2 : (map f p).degree = p.degree
h3 : (map f p).natDegree = p.natDegree
h4 : map f p ≠ 0
⊢ (map f p).coeff (map f p).natDegree ≠ 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
f : R[X]
df : f.natDegree ≤ N
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
hf : #f.support = n✝ + 1 + 1
⊢ f ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝ : Semiring R
motive : R[X] → Prop
N : ℕ
zero : motive 0
C_mul_pow : ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → motive (C r * X ^ n)
add : ∀ (f g : R[X]), f.natDegree < g.natDegree → g.natDegree ≤ N → motive f → motive g → motive (f + g)
n✝ : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = n✝ + 1 → motive f
df : natDegree 0 ≤ N
hf : #(support 0) = n✝ + 1 + 1
⊢ False
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff (f.natDegree - 0) = f.leadingCoeff

Tactic:
tsub_zero,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.coeff f.natDegree = f.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.natDegree + q.natDegree = (q * p).natDegree

Tactic:
Polynomial.natDegree_mul',

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ p.natDegree + q.natDegree = q.natDegree + p.natDegree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
hp : p.Monic
q : R[X]
h : ¬q = 0
⊢ q.leadingCoeff * p.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse.natTrailingDegree = 0

Tactic:
natTrailingDegree_eq_zero,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.reverse = 0 ∨ f.reverse.coeff 0 ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
m : Fin n →₀ ℕ
hjmi : j ≠ cons (j 0) m
⊢ m ≠ j.tail

Tactic:
rintro rfl

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
j : Fin (n + 1) →₀ ℕ
r : R
hjmi : j ≠ cons (j 0) j.tail
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
⊢ Finset.image (cons i) (((finSuccEquiv R n) f).coeff i).support = {m ∈ f.support | m 0 = i}

Tactic:
ext m

Goal state after:
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ m ∈ Finset.image (cons i) (((finSuccEquiv R n) f).coeff i).support ↔ m ∈ {m ∈ f.support | m 0 = i}
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
⊢ (∃ x, ¬coeff (cons i x) f = 0 ∧ cons i x = m) → coeff m f ≠ 0 ∧ m 0 = i

Tactic:
grind [cons_zero]

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

Goal state before:
pp: case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0
⊢ (a * t.prod).natDegree = a.natDegree + (Multiset.map (fun f ↦ f.natDegree) t).sum

Tactic:
Polynomial.natDegree_mul',

Goal state after:
case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0
⊢ a.natDegree + t.prod.natDegree = a.natDegree + (Multiset.map (fun f ↦ f.natDegree) t).sum

case refine_2
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0 → t.prod.natDegree = (Multiset.map (fun f ↦ f.natDegree) t).sum
ht : a.leadingCoeff * (Multiset.map (fun f ↦ f.leadingCoeff) t).prod ≠ 0
⊢ a.leadingCoeff * t.prod.leadingCoeff ≠ 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
p : R[X]
hm : p.Monic
hnd : p.natDegree = 2
h✝ : Nontrivial R
⊢ p ≠ 1

Tactic:
rintro rfl

Goal state after:
case inr
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
h✝ : Nontrivial R
hm : Monic 1
hnd : natDegree 1 = 2
⊢ False
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
n : ℕ
this : (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) + y ^ n = x ^ n
⊢ (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ n

Tactic:
rw [← this, add_sub_cancel_right]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ -q.coeff q.natDegree = 1

Tactic:
show q.coeff q.natDegree = -1 from hq,

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ - -1 = 1
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
⊢ (p - q).Monic

Tactic:
by
  have : (-q).coeff (-q).natDegree = 1 := by
    rw [natDegree_neg, coeff_neg, show q.coeff q.natDegree = -1 from hq, neg_neg]
  rw [sub_eq_add_neg]
  apply Monic.add_of_right this
  rwa [degree_neg]

Goal state after:
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
r : R
p a b : ℕ
h : a ∣ b
hp₀ : p = 0
hb₀ : ¬b = 0
⊢ a ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u_1
inst✝ : Ring R
r : R
p b : ℕ
hp₀ : p = 0
hb₀ : ¬b = 0
h : 0 ∣ b
⊢ False
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → p * q = 0

Tactic:
rintro rfl

Goal state after:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ p * 0 = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
⊢ q = 0 → q * p = 0

Tactic:
rintro rfl

Goal state after:
case mpr
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
⊢ 0 * p = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (X ^ n + ↑p).natDegree = n

Tactic:
rw [natDegree_add_eq_left_of_degree_lt]

Goal state after:
R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (X ^ n).natDegree = n

R : Type u
S : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
p : ↥(degreeLT R n)
⊢ (↑p).degree < (X ^ n).degree
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: case inl.inr
A : Type w
B : Type u₁
C : Type u_1
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
x : Finset C
hx : Algebra.adjoin A ↑x = ⊤
y : Finset C
hy : span B ↑y = ⊤
f : C → C → B
h✝ : ∀ (x : C), Function.support (f x) ⊆ ↑y
hf : ∀ (x : C), ∑ a ∈ y, f x a • a = x
s : Finset B := image₂ f (x ∪ y * y) y
hxy : ∀ xi ∈ x, xi ∈ span ↥(Algebra.adjoin A ↑s) ↑(insert 1 y)
yj : C
hyj : yj ∈ ↑y
⊢ yj ∈ ↑(span (↥(Algebra.adjoin A ↑s)) (insert 1 ↑y))

Tactic:
exact subset_span (Set.mem_insert_of_mem _ hyj)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f : R[X]
hf : ∀ (n : ℕ), f.coeff n ∈ I
n : ℕ
x✝ : n ∈ f.support
⊢ X ^ n * C (f.coeff n) ∈ map C I

Tactic:
exact (I.map C : Ideal R[X]).mul_mem_left _ (mem_map_of_mem _ (hf n))

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.inl
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree < ↑n
⊢ Polynomial.leadingCoeff 0 = p.coeff n

Tactic:
rw [leadingCoeff_zero, eq_comm]

Goal state after:
case mp.inl
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
p : R[X]
hpdeg✝ : p.degree ≤ ↑n
hpI : p ∈ I.ofPolynomial
hpdeg : p.degree < ↑n
⊢ p.coeff n = 0
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mpr
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
n : ℕ
x : R
⊢ (∃ p ∈ I, p.degree ≤ ↑n ∧ p.leadingCoeff = x) → ∃ y, (y.degree ≤ ↑n ∧ y ∈ I.ofPolynomial) ∧ y.coeff n = x

Tactic:
· rintro ⟨p, hpI, hpdeg, rfl⟩
    have : natDegree p + (n - natDegree p) = n :=
      add_tsub_cancel_of_le (natDegree_le_of_degree_le hpdeg)
    refine ⟨p * X ^ (n - natDegree p), ⟨?_, I.mul_mem_right _ hpI⟩, ?_⟩
    · apply le_trans (degree_mul_le _ _) _
      apply le_trans (add_le_add degree_le_natDegree (degree_X_pow_le _)) _
      rw [← Nat.cast_add, this]
    · rw [Polynomial.leadingCoeff, ← coeff_mul_X_pow p (n - natDegree p), this]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommRing R
r : R
hr : Prime r
a b : MvPolynomial σ R
hd : C r ∣ a * b
⊢ C r ∣ a ∨ C r ∣ b

Tactic:
by
      obtain ⟨s, a', b', rfl, rfl⟩ := exists_finset_rename₂ a b
      rw [← algebraMap_eq] at hd
      have : algebraMap R _ r ∣ a' * b' := by
        convert! _root_.map_dvd (killCompl Subtype.val_injective) hd
        · simp
        · simp
      rw [← rename_C ((↑) : s → σ)]
      let f := (rename (R := R) ((↑) : s → σ)).toRingHom
      exact (((prime_C_iff_of_fintype s).2 hr).2.2 a' b' this).imp (map_dvd f) (map_dvd f)

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
p : R[X]
hp : p ∈ I
hn : p.natDegree = k
h : N < k
⊢ p ≠ 0

Tactic:
rintro rfl

Goal state after:
R : Type u
inst✝ : CommRing R
inst : IsNoetherianRing R
I : Ideal R[X]
M : Submodule R R := ⋯.min (Set.range I.leadingCoeffNth) ⋯
hm : M ∈ Set.range I.leadingCoeffNth
N : ℕ
HN : I.leadingCoeffNth N = M
s : Finset R[X]
hs : Submodule.span R ↑s = I.degreeLE ↑N
hm2 : ∀ (k : ℕ), I.leadingCoeffNth k ≤ M
hs2 : ∀ {x : R[X]}, x ∈ I.degreeLE ↑N → x ∈ Ideal.span ↑s
this : Submodule.span R[X] ↑s = Ideal.span ↑s
k : ℕ
ih : ∀ m < k, ∀ ⦃p : R[X]⦄, p ∈ I → p.natDegree = m → p ∈ Ideal.span ↑s
h : N < k
hp : 0 ∈ I
hn : natDegree 0 = k
⊢ False
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
f : R[M]
⊢ ∃ a, (MvPolynomial.aeval fun s ↦ of' R M ↑s) a = f

Tactic:
induction f using induction_on with
  | of m =>
    have : m ∈ closure S := hS.symm ▸ mem_top _
    refine AddSubmonoid.closure_induction (fun m hm => ?_) ?_ ?_ this
    · exact ⟨MvPolynomial.X ⟨m, hm⟩, MvPolynomial.aeval_X _ _⟩
    · exact ⟨1, map_one _⟩
    · rintro m₁ m₂ _ _ ⟨P₁, hP₁⟩ ⟨P₂, hP₂⟩
      exact
        ⟨P₁ * P₂, by
          rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single,
            one_mul]; rfl⟩
  | add f g ihf ihg =>
    rcases ihf with ⟨P, rfl⟩
    rcases ihg with ⟨Q, rfl⟩
    exact ⟨P + Q, map_add _ _ _⟩
  | smul r f ih =>
    rcases ih with ⟨P, rfl⟩
    exact ⟨r • P, map_smul _ _ _⟩

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
m : ℕ
h : a ≡ b [ZMOD n]
⊢ a ^ m ≡ b ^ m [ZMOD n]

Tactic:
by
  induction m with
  | zero => simp
  | succ d hd => rw [pow_succ, pow_succ]; exact hd.mul h

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: n a b : ℤ
⊢ a ≡ b - n [ZMOD n] ↔ a ≡ b [ZMOD n]

Tactic:
by
  rw [← modEq_add_modulus_iff, sub_add_cancel]

Goal state after:
Module: Mathlib.Data.Int.ModEq

Goal state before:
pp: a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ ↑z.natAbs < b ∧ ↑z.natAbs ≡ a [ZMOD b]

Tactic:
constructor <;> rw [natAbs_of_nonneg hz1]

Goal state after:
case left
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ z < b

case right
a b : ℤ
hb : 0 < b
z : ℤ
hz1 : 0 ≤ z
hz2 : z < b
hz3 : z ≡ a [ZMOD b]
⊢ z ≡ a [ZMOD b]
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: case inr
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
this : ∀ (R : Type u_1) [inst : AddMonoidWithOne R] (p : ℕ) [CharP R p] {a b : ℕ}, a ≡ b [MOD p] → a ≤ b → ↑a = ↑b
hle : ¬a ≤ b
⊢ ↑a = ↑b

pp: R✝ : Type u_1
inst✝² : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
hle : a ≤ b
⊢ ↑a = ↑b

Tactic:
· exact (this R p h.symm (le_of_not_ge hle)).symm

Goal state after:
R✝ : Type u_1
inst✝² : AddMonoidWithOne R✝
p✝ a✝ b✝ : ℕ
R : Type u_1
inst✝¹ : AddMonoidWithOne R
p : ℕ
inst✝ : CharP R p
a b : ℕ
h : a ≡ b [MOD p]
hle : a ≤ b
⊢ ↑a = ↑b
Module: Mathlib.Algebra.CharP.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ ¬2 = 0

Tactic:
(by norm_cast : (2 : R) = (2 : ℕ)),

Goal state after:
R : Type u_2
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hR : ringChar R ≠ 2
⊢ ¬↑2 = 0
Module: Mathlib.RingTheory.Ideal.Quotient.Operations

Goal state before:
pp: case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
⊢ ker f = I → ker f ≤ I

Tactic:
rintro rfl

Goal state after:
case mpr
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : (ker f).IsTwoSided
H : ∀ a ∈ ker f, f a = 0
⊢ ker f ≤ ker f
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: p a : ℕ
hp : Prime p
a1 : a ≠ 1
⊢ p = a → a ∣ p

Tactic:
rintro rfl

Goal state after:
p : ℕ
hp : Prime p
a1 : p ≠ 1
⊢ p ∣ p