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

Goal state before:
pp: R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f + -g) ≤ supDegree D f ⊔ supDegree D g

Tactic:
← supDegree_neg (f := g)

Goal state after:
R' : Type u_2
A : Type u_3
B : Type u_5
inst✝² : Ring R'
inst✝¹ : SemilatticeSup B
inst✝ : OrderBot B
D : A → B
f g : R'[A]
⊢ supDegree D (f + -g) ≤ supDegree D f ⊔ supDegree D (-g)
Module: Mathlib.Algebra.Polynomial.Coeff

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n k : ℕ
⊢ ((X + 1) ^ n).coeff k = ↑(n.choose k)

Tactic:
rw [← C_1, coeff_X_add_C_pow, one_pow, one_mul]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.degree.succ = p.natDegree + 1

Tactic:
rw [degree_eq_natDegree h]

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ (↑p.natDegree).succ = p.natDegree + 1
Module: Mathlib.Algebra.Polynomial.Degree.Defs

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : a = 0
⊢ ((monomial n) a).leadingCoeff = a

pp: case neg
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ ((monomial n) a).leadingCoeff = a

Tactic:
· simp only [ha, (monomial n).map_zero, leadingCoeff_zero]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
a : R
n : ℕ
ha : ¬a = 0
⊢ ((monomial n) a).leadingCoeff = a
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
hp : p ≠ 0
hq : q ≠ 0
⊢ (p * q).natDegree = p.natDegree + q.natDegree

Tactic:
by
  rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree (mul_ne_zero hp hq),
    Nat.cast_add, ← degree_eq_natDegree hp, ← degree_eq_natDegree hq, degree_mul]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.leadingCoeff ^ (n + 1) ≠ 0
⊢ (p ^ (n + 1)).degree = (n + 1) • p.degree

Tactic:
by
    have h₁ : leadingCoeff p ^ n ≠ 0 := fun h₁ => h <| by rw [pow_succ, h₁, zero_mul]
    have h₂ : leadingCoeff (p ^ n) * leadingCoeff p ≠ 0 := by
      rwa [pow_succ, ← leadingCoeff_pow' h₁] at h
    rw [pow_succ, degree_mul' h₂, succ_nsmul, degree_pow' h₁]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
a : R
inst✝ : Semiring R
ha : IsUnit a
p : R[X]
⊢ (C a * p).degree = p.degree

Tactic:
by
  obtain rfl | hp := eq_or_ne p 0
  · simp
  nontriviality R
  rw [degree_mul', degree_C ha.ne_zero]
  · simp
  · simpa [ha.mul_right_eq_zero]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Units

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
| 0

Tactic:
rw [← natDegree_coe_units u]

Goal state after:
R : Type u
inst✝² : Semiring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
u : R[X]ˣ
| (↑u).natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.Monic
⊢ p = 1 → p.natDegree = 0

Tactic:
by rintro rfl; simp

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : Semiring R
inst✝¹ : Semiring S
f : R →+* S
inst✝ : Semiring T
g : S →+* T
p : R[X]
⊢ ∀ (n : ℕ), (map g (map f p)).coeff n = (map (g.comp f) p).coeff n

Tactic:
simp [coeff_map]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
this : (C a).degree < X.degree
⊢ X.degree = 1

Tactic:
degree_X

Goal state after:
R : Type u
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
this : (C a).degree < X.degree
⊢ 1 = 1
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
inst✝² : Add B
inst✝¹ : AddLeftStrictMono B
inst✝ : AddRightStrictMono B
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
hp : Monic D p
hq : q ≠ 0
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
cases subsingleton_or_nontrivial R; · exact (hq (Subsingleton.elim _ _)).elim
  apply supDegree_mul hD hadd ?_ hp.ne_zero hq
  simp_rw [hp, one_mul, Ne, leadingCoeff_eq_zero hD, hq, not_false_eq_true]

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℕ
hn : 0 < n
r : R
⊢ (X ^ n - C r).leadingCoeff = 1

Tactic:
by
  rw [sub_eq_add_neg, ← map_neg C r, leadingCoeff_X_pow_add_C hn]

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

Goal state before:
pp: R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ R[x] = (aeval x).range

Tactic:
← Algebra.map_top,

Goal state after:
R : Type u
A : Type z
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
⊢ R[x] = Subalgebra.map (aeval x) ⊤
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
⊢ f (p.coeff (map f p).natDegree) = f (p.coeff p.natDegree)

Tactic:
natDegree_map_of_leadingCoeff_ne_zero f hf

Goal state after:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
p : R[X]
f : R →+* S
hf : f p.leadingCoeff ≠ 0
⊢ f (p.coeff p.natDegree) = f (p.coeff p.natDegree)
Module: Mathlib.Data.Finsupp.Antidiagonal

Goal state before:
pp: α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
⊢ (u, v) ∈
      image
        (fun x ↦
          match x with
          | ((x, y), z, w) => (x.sumElim z, y.sumElim w))
        (antidiagonal x ×ˢ antidiagonal y) ↔
    (u, v) ∈ antidiagonal (x.sumElim y)

Tactic:
simp only [mem_antidiagonal, mem_image, mem_product, Prod.mk.injEq, Prod.exists]

Goal state after:
α : Type u
inst✝¹ : DecidableEq α
β : Type u_1
inst✝ : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
⊢ (∃ a b a_1 b_1, (a + b = x ∧ a_1 + b_1 = y) ∧ a.sumElim a_1 = u ∧ b.sumElim b_1 = v) ↔ u + v = x.sumElim y
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: A : Type u_3
B : Type u_4
C : Type u_5
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
p : A[X]
⊢ (algebraMap B C) ((algebraMap A B) (p.coeff 0)) = (algebraMap A C) (p.coeff 0)

Tactic:
IsScalarTower.algebraMap_eq A B C,

Goal state after:
A : Type u_3
B : Type u_4
C : Type u_5
inst✝⁶ : CommSemiring A
inst✝⁵ : CommSemiring B
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra A C
inst✝¹ : Algebra B C
inst✝ : IsScalarTower A B C
p : A[X]
⊢ (algebraMap B C) ((algebraMap A B) (p.coeff 0)) = ((algebraMap B C).comp (algebraMap A B)) (p.coeff 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 only [sub_eq_add_neg] using @neLocus_add_right α N _ _ _ _ _ _

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

Goal state before:
pp: case e_a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
⊢ (C.prod fun n e ↦ g₁ n ^ e) = C.prod fun n e ↦ g₂ n ^ e

Tactic:
apply Finset.prod_congr rfl

Goal state after:
case e_a
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
p : MvPolynomial σ R
f : R →+* S₁
g₁ g₂ : σ → S₁
h : ∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → coeff c p ≠ 0 → g₁ i = g₂ i
C : σ →₀ ℕ
hc : C ∈ p.coeff.support
⊢ ∀ x ∈ C.support, (fun n e ↦ g₁ n ^ e) x (C x) = (fun n e ↦ g₂ n ^ e) x (C x)
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 [Finset.mem_add]
        using Finset.add_subset_add_left support_monomial_subset <| support_mul _ _ h

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
m : σ →₀ ℕ
s : σ
p : MvPolynomial σ R
⊢ (if Finsupp.single s 1 ≤ m then coeff (m - Finsupp.single s 1) p * 1 else 0) =
    if s ∈ m.support then coeff (m - Finsupp.single s 1) p else 0

Tactic:
simp_rw [Finsupp.single_le_iff, Finsupp.mem_support_iff, Nat.succ_le_iff, pos_iff_ne_zero,
    mul_one]

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

Goal state before:
pp: case monomial
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
d u : σ →₀ ℕ
r : R
⊢ coeff (Finsupp.mapDomain f d) ((rename f) ((monomial u) r)) = coeff d ((monomial u) r)

Tactic:
rename_monomial,

Goal state after:
case monomial
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
d u : σ →₀ ℕ
r : R
⊢ coeff (Finsupp.mapDomain f d) ((monomial (Finsupp.mapDomain f u)) r) = coeff d ((monomial u) r)
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
h : r ≠ 0
⊢ ((monomial s) r).degrees.toFinset = s.support

Tactic:
degrees_monomial_eq _ _ h,

Goal state after:
R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
h : r ≠ 0
⊢ (toMultiset s).toFinset = s.support
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : DecidableEq σ
i j : σ
inst✝ : Nontrivial R
c : ¬i = j
⊢ degreeOf i (X j) = if i = j then 1 else 0

Tactic:
simp [c, degreeOf_def, degrees_X]

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

Goal state before:
pp: case refine_2.monomial_add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ↑p.coeffs ⊆ range ⇑f → p ∈ range ⇑(map f)
ih : ↑((monomial a) s).coeffs ⊆ range ⇑f → (monomial a) s ∈ range ⇑(map f)
hx : ↑(((monomial a) s).coeffs ∪ p.coeffs) ⊆ range ⇑f
⊢ (monomial a) s + p ∈ range ⇑(map f)

Tactic:
simp only [Finset.coe_union, Set.union_subset_iff] at hx

Goal state after:
case refine_2.monomial_add
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.coeff.support
hs : s ≠ 0
hp : ↑p.coeffs ⊆ range ⇑f → p ∈ range ⇑(map f)
ih : ↑((monomial a) s).coeffs ⊆ range ⇑f → (monomial a) s ∈ range ⇑(map f)
hx : ↑((monomial a) s).coeffs ⊆ range ⇑f ∧ ↑p.coeffs ⊆ range ⇑f
⊢ (monomial a) s + p ∈ range ⇑(map f)
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : CommRing S
f✝ : R →+* S
g f : σ → S
x : σ
⊢ (fun f ↦ ⇑f ∘ X) ((fun f ↦ eval₂Hom (Int.castRingHom S) f) f) x = f x

Tactic:
by simp only [coe_eval₂Hom, Function.comp_apply, eval₂_X]

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

Goal state before:
pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m ↦ (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
have hbb : b ∈ (p + q).support := by
      apply support_sdiff_support_subset_support_add
      rw [Finset.mem_sdiff]
      exact ⟨hb₁, hb⟩

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
b : σ →₀ ℕ
hb₁ : b ∈ p.support
hb₂ : (p.support.sup fun m ↦ (toMultiset m).card) = (toMultiset b).card
hb : b ∉ q.support
hbb : b ∈ (p + q).support
⊢ p.totalDegree ≤ (p + q).totalDegree
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: case e_a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
⊢ ∏ x ∈ d.support, g₁ x ^ d x = ∏ x ∈ d.support, g₂ x ^ d x

Tactic:
apply Finset.prod_congr rfl

Goal state after:
case e_a
R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ : R →+* S
g₁ g₂ : σ → S
p₁ : MvPolynomial σ R
h : ∀ i ∈ p₁.vars, i ∈ p₁.vars → g₁ i = g₂ i
d : σ →₀ ℕ
hd : d ∈ p₁.support
⊢ ∀ x ∈ d.support, g₁ x ^ d x = g₂ x ^ d x
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inl
R : Type u
m n : ℕ
inst✝ : Semiring R
p : R[X]
pn : p.natDegree ≤ n
mno : m * n ≤ m * n
⊢ (p ^ m).coeff (m * n) = if m * n = m * n then p.coeff n ^ m else 0

Tactic:
simpa only [ite_true] using coeff_pow_of_natDegree_le pn

Goal state after:
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : i < p.natTrailingDegree
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

pp: case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0

Tactic:
· rw [coeff_eq_zero_of_lt_natTrailingDegree hi, zero_mul]

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
i j : ℕ
h₁ : (i, j).1 + (i, j).2 = p.natTrailingDegree + q.natTrailingDegree
h₂ : (i, j) ≠ (p.natTrailingDegree, q.natTrailingDegree)
hi : p.natTrailingDegree ≤ i
⊢ p.coeff (i, j).1 * q.coeff (i, j).2 = 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: N a b : ℕ
hab : revAtFun N a = revAtFun N b
⊢ a = b

Tactic:
← @revAtFun_invol N a,

Goal state after:
N a b : ℕ
hab : revAtFun N a = revAtFun N b
⊢ revAtFun N (revAtFun N a) = b
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = (revAt (n + n')) n + (revAt (o + o')) o

Tactic:
revAt_le (le_add_right rfl.le)

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (revAt (o + o')) o
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (revAt (o + o')) o

Tactic:
revAt_le (le_add_right rfl.le)

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)

Tactic:
revAt_le (le_add_right rfl.le)

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + o + (n' + o'))) (n + o) = n + n' - n + (o + o' - o)

Tactic:
revAt_le (le_add_right rfl.le)

Goal state after:
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: N O n o : ℕ
hn : n ≤ N
ho : o ≤ O
⊢ (revAt (N + O)) (n + o) = (revAt N) n + (revAt O) o

Tactic:
rcases Nat.le.dest hn with ⟨n', rfl⟩
  rcases Nat.le.dest ho with ⟨o', rfl⟩
  repeat' rw [revAt_le (le_add_right rfl.le)]
  rw [add_assoc, add_left_comm n' o, ← add_assoc, revAt_le (le_add_right rfl.le)]
  repeat' rw [add_tsub_cancel_left]

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

Goal state before:
pp: case inl
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead.natDegree < f.natDegree
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1

pp: case inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1

Tactic:
· exact Nat.le_sub_one_of_lt h

Goal state after:
case inr
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
⊢ f.eraseLead.natDegree ≤ f.natDegree - 1
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.succ.refine_1.refine_1
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
⊢ 2 ≤ #f.support

Tactic:
exact (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _))).trans hf.ge

Goal state after:
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
⊢ motive f

Tactic:
by
  induction hf : #f.support generalizing f with
  | zero =>
    convert! zero
    simpa [support_eq_empty, card_eq_zero] using hf
  | succ c hc =>
    rw [← eraseLead_add_C_mul_X_pow f]
    cases c
    · convert C_mul_pow f.natDegree f.leadingCoeff ?_ df
      · convert! zero_add (C (leadingCoeff f) * X ^ f.natDegree)
        rw [← card_support_eq_zero, card_support_eraseLead' hf]
      · rw [leadingCoeff_ne_zero, Ne, ← card_support_eq_zero, hf]
        exact zero_ne_one.symm
    refine add f.eraseLead _ ?_ ?_ ?_ ?_
    · refine (eraseLead_natDegree_lt ?_).trans_le (le_of_eq ?_)
      · exact (Nat.succ_le_succ (Nat.succ_le_succ (Nat.zero_le _))).trans hf.ge
      · rw [natDegree_C_mul_X_pow _ _ (leadingCoeff_ne_zero.mpr _)]
        rintro rfl
        simp at hf
    · exact (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree).trans df
    · exact hc _ (eraseLead_natDegree_le_aux.trans df) (card_support_eraseLead' hf)
    · refine C_mul_pow _ _ ?_ df
      rw [Ne, leadingCoeff_eq_zero, ← card_support_eq_zero, hf]
      exact Nat.succ_ne_zero _

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
⊢ (X * p).reverse = p.reverse

Tactic:
by
  rw [commute_X p, reverse_mul_X]

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

Goal state before:
pp: case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ p.degree ≤ (List.map natDegree l).maximum

Tactic:
rw [degree_eq_natDegree h]

Goal state after:
case neg
S : Type u_1
inst✝ : Semiring S
l : List S[X]
p : S[X]
hp : p ∈ l
h : ¬p = 0
⊢ ↑p.natDegree ≤ (List.map natDegree l).maximum
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
h : ∏ i ∈ s, (f i).leadingCoeff ≠ 0
⊢ (∏ i ∈ s, f i).leadingCoeff = ∏ i ∈ s, (f i).leadingCoeff

Tactic:
by
  simpa using leadingCoeff_multiset_prod' (s.1.map f) (by simpa using h)

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

Goal state before:
pp: R : Type u
ι : Type w
s : Finset ι
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
f : ι → R[X]
h : ∀ i ∈ s, f i ≠ 0
⊢ (∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree

Tactic:
nontriviality R
  apply natDegree_prod'
  rw [prod_ne_zero_iff]
  intro x hx; simp [h x hx]

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

Goal state before:
pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ degreeLT R n ≤ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n))

pp: case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n)) ≤ degreeLT R n

Tactic:
· intro p hp
    replace hp := mem_degreeLT.1 hp
    rw [← Polynomial.sum_monomial_eq p, Polynomial.sum]
    refine Submodule.sum_mem _ fun k hk => ?_
    have := WithBot.coe_lt_coe.1 ((Finset.sup_lt_iff <| WithBot.bot_lt_coe n).1 hp k hk)
    rw [← C_mul_X_pow_eq_monomial, C_mul']
    refine Submodule.smul_mem _ _ (Submodule.subset_span <| by grind)

Goal state after:
case a
R : Type u
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℕ
⊢ Submodule.span R ↑(image (fun n ↦ X ^ n) (range n)) ≤ degreeLT R n
Module: Mathlib.Algebra.Algebra.Subalgebra.Operations

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := fun x ↦ ⟨s x, ⋯⟩
l' : ι → ↥S' := fun x ↦ ⟨l x, ⋯⟩
e' : ∑ i ∈ ι', l' i * s' i = 1
⊢ ∑ i ∈ ι', l' i * s' i ∈ Ideal.span (s' '' ↑ι')

Tactic:
apply sum_mem

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
S' : Subalgebra R S
ι : Type u_3
ι' : Finset ι
s l : ι → S
e : ∑ i ∈ ι', l i * s i = 1
hs : ∀ (i : ι), s i ∈ S'
hl : ∀ (i : ι), l i ∈ S'
x : S
n : ι → ℕ
hn : ∀ (i : ι), s i ^ n i • x ∈ S'
s' : ι → ↥S' := ⋯
l' : ι → ↥S' := ⋯
e' : ∑ i ∈ ι', l' i * s' i = 1
⊢ ∀ c ∈ ι', l' c * s' c ∈ Ideal.span (s' '' ↑ι')
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ ∑ x ∈ antidiagonal k, (f a).coeff x.1 * (∏ x ∈ s, f x).coeff x.2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)

Tactic:
apply sum_mem

Goal state after:
case insert
R : Type u
inst✝ : CommSemiring R
ι : Type u_2
f : ι → R[X]
I : Ideal R
n : ι → ℕ
a : ι
s : Finset ι
ha : a ∉ s
hs : (∀ i ∈ s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)) → ∀ (k : ℕ), (s.prod f).coeff k ∈ I ^ (s.sum n - k)
h : ∀ i ∈ insert a s, ∀ (k : ℕ), (f i).coeff k ∈ I ^ (n i - k)
k : ℕ
⊢ ∀ c ∈ antidiagonal k, (f a).coeff c.1 * (∏ x ∈ s, f x).coeff c.2 ∈ I ^ (n a + ∑ x ∈ s, n x - k)
Module: Mathlib.Algebra.Algebra.Subalgebra.Pointwise

Goal state before:
pp: case refine_1.inl
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S T : Subalgebra R A
x✝ : A
hx : x✝ ∈ Algebra.adjoin R (↑S ∪ ↑T)
x : A
hxS : x ∈ ↑S
⊢ x * 1 ∈ toSubmodule S * toSubmodule T

Tactic:
exact Submodule.mul_mem_mul hxS (show (1 : A) ∈ T from one_mem T)

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

Goal state after:
Module: Mathlib.Algebra.CharP.Two

Goal state before:
pp: case inl
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Even n
⊢ ↑n = 0 ↔ True

Tactic:
iff_true

Goal state after:
case inl
R : Type u_1
inst✝ : AddMonoidWithOne R
h₁ : 1 ≠ 0
h₂ : 2 = 0
n : ℕ
hn : Even n
⊢ ↑n = 0
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; rfl

Goal state after:
Module: Mathlib.Data.Nat.Prime.Basic

Goal state before:
pp: a b : ℕ
hdvd : ∀ (p : ℕ), Prime p → p ∣ a → p * a ∣ b
⊢ a ∣ b

Tactic:
by
  obtain rfl | ha := eq_or_ne a 1
  · apply one_dvd
  obtain ⟨p, hp⟩ := exists_prime_and_dvd ha
  exact _root_.trans (dvd_mul_left a p) (hdvd p hp.1 hp.2)

Goal state after: