mathlib-initiative/mathlib-tactics huggingface dataset:
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

Goal state after:
ι : Type u_1
β : ι → Type u_2
inst✝¹ : LinearOrder ι
x y : (i : ι) → β i
i : ι
inst✝ : (i : ι) → LinearOrder (β i)
h : ∀ (j : ι), j > i → x j = y j
hxy : y i < x i
⊢ ¬toColex x ≤ toColex y
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: case step.inr
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
⊢ P.coeff l * Q.leadingCoeff = 0

Tactic:
let m := Q.natDegree

Goal state after:
case step.inr
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
⊢ P.coeff l * Q.leadingCoeff = 0
Module: Mathlib.Algebra.Polynomial.AlgebraMap

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
⊢ X.coeff 1 ∈ R⁰

Tactic:
by simp [one_mem]

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

Goal state before:
pp: 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)
⊢ f = g

Tactic:
refine AddMonoidAlgebra.ringHom_ext' ?_ ?_

Goal state after:
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)
⊢ f.comp singleZeroRingHom = g.comp singleZeroRingHom

case refine_2
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)
⊢ (↑f).comp (of R (σ →₀ ℕ)) = (↑g).comp (of R (σ →₀ ℕ))
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✝ p : MvPolynomial σ R
s : σ
hp : k (eval₂ f g p) = eval₂ k (⇑k ∘ g) ((map f) p)
⊢ k (eval₂ f g (p * X s)) = eval₂ k (⇑k ∘ g) ((map f) (p * X s))

Tactic:
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.Basic

Goal state before:
pp: case mp
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
p : MvPolynomial σ S
i : σ →₀ ℕ
⊢ (∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M) → ∀ (i : σ →₀ ℕ), coeff i p ∈ M

Tactic:
rintro hp j

Goal state after:
case mp
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
p : MvPolynomial σ S
i : σ →₀ ℕ
hp : ∀ (i_1 : σ →₀ ℕ), (if i ≤ i_1 then coeff (i_1 - i) p * 1 else 0) ∈ M
j : σ →₀ ℕ
⊢ coeff j p ∈ M
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
hd : 0 ∈ p.support
⊢ toMultiset 0 ≤ (p + q).degrees

Tactic:
toMultiset_zero

Goal state after:
case inl
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
hd : 0 ∈ p.support
⊢ 0 ≤ (p + q).degrees
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case inr.refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ p.degrees

Tactic:
mem_degrees

Goal state after:
case inr.refine_1
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ d, coeff d p ≠ 0 ∧ j ∈ d.support
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case inr.refine_2
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ q.degrees

Tactic:
mem_degrees

Goal state after:
case inr.refine_2
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ d, coeff d q ≠ 0 ∧ j ∈ d.support
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p₁ p₂ : MvPolynomial σ R
⊢ ∃ s q₁ q₂, p₁ = (rename Subtype.val) q₁ ∧ p₂ = (rename Subtype.val) q₂

Tactic:
obtain ⟨s₁, q₁, rfl⟩ := exists_finset_rename p₁
  obtain ⟨s₂, q₂, rfl⟩ := exists_finset_rename p₂
  classical
    use s₁ ∪ s₂
    use rename (fun x ↦ ⟨x, Finset.subset_union_left x.2⟩) q₁
    use rename (fun x ↦ ⟨x, Finset.subset_union_right x.2⟩) q₂
    constructor <;> simp [Function.comp_def]

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

Goal state before:
pp: case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
hx : x ∈ coeffsIn σ M
y : MvPolynomial σ S
hy : y ∈ coeffsIn σ N
⊢ x * y ∈ coeffsIn σ (M * N)

Tactic:
k

Goal state after:
case refine_2
R : Type u_2
S : Type u_3
σ : Type u_4
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M N : Submodule R S
x : MvPolynomial σ S
hx : x ∈ coeffsIn σ M
y : MvPolynomial σ S
hy : y ∈ coeffsIn σ N
k : σ →₀ ℕ
⊢ coeff k (x * y) ∈ M * N
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : σ
k : ℕ
⊢ (Finsupp.single i k) i = k

Tactic:
Finsupp.single_eq_same

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i : σ
k : ℕ
⊢ k = k
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
i : σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degreeOf i (∑ j ∈ s, f j) ≤ s.sup fun j ↦ degreeOf i (f j)

Tactic:
by
  simp_rw [degreeOf_eq_sup]
  exact supDegree_sum_le

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

Goal state before:
pp: case inr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
h✝ : degreeOf i p ≠ degreeOf i q
h : degreeOf i q < degreeOf i p
⊢ max (degreeOf i p) (degreeOf i q) ≤ degreeOf i (p + q)

Tactic:
· simp [degreeOf_add_eq_of_degreeOf_lt h, max_eq_left_of_lt h]

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

Goal state before:
pp: case cons
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
has : a ∉ s
hind : (s.sum f).totalDegree ≤ s.sup fun i ↦ (f i).totalDegree
⊢ ((Finset.cons a s has).sum f).totalDegree ≤ (Finset.cons a s has).sup fun i ↦ (f i).totalDegree

Tactic:
rw [Finset.sum_cons, Finset.sup_cons]
    exact (MvPolynomial.totalDegree_add _ _).trans (max_le_max le_rfl hind)

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ p.coeff (invFun (⇑toLex) (supDegree (⇑toLex) p)) = coeff (ofLex (supDegree (⇑toLex) p)) p

Tactic:
apply congr_arg p.coeff

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
p : MvPolynomial σ R
inst✝ : LinearOrder σ
⊢ invFun (⇑toLex) (supDegree (⇑toLex) p) = ofLex (supDegree (⇑toLex) p)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
by_cases hq : natDegree q = 0
  · exact le_antisymm natDegree_comp_le (by simp [hq])
  apply natDegree_eq_of_le_of_coeff_ne_zero natDegree_comp_le
  rwa [coeff_comp_degree_mul_degree hq]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
⊢ (-p).natTrailingDegree = p.natTrailingDegree

Tactic:
by
  simp [natTrailingDegree]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ #f.eraseLead.support = #f.support - 1

Tactic:
by_cases hf : f = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f = 0
⊢ #f.eraseLead.support = #f.support - 1

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ #f.eraseLead.support = #f.support - 1
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f = 0
⊢ #f.eraseLead.support = #f.support - 1

Tactic:
hf,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f = 0
⊢ #(eraseLead 0).support = #(support 0) - 1
Module: Mathlib.Algebra.Polynomial.Degree.TrailingDegree

Goal state before:
pp: case refine_2.inr.inl
R : Type u
inst✝ : Semiring R
p : R[X]
h₁ : p.Monic
h : p.natDegree ≤ p.natTrailingDegree
⊢ p.coeff p.natDegree = if p.natDegree = p.natDegree then 1 else 0

Tactic:
simpa only [if_pos rfl] using! h₁.leadingCoeff

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

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

Tactic:
nextCoeff_eq_zero,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.natDegree = 0 ∨ 0 < f.natDegree ∧ f.coeff (f.natDegree - 1) = 0
⊢ f.eraseLead.coeff (f.natDegree - 1) = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
P : R[X]
d : σ →₀ ℕ
⊢ P.coeff (d default) = P.coeff ((Finsupp.single default (d default)) default)

Tactic:
Finsupp.single_eq_same

Goal state after:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Unique σ
P : R[X]
d : σ →₀ ℕ
⊢ P.coeff (d default) = P.coeff (d default)
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (optionEquivLeft R S₁) ((monomial m) r) = (Polynomial.monomial (m none)) ((monomial m.some) r)

Tactic:
optionEquivLeft_apply,

Goal state after:
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
m : Option S₁ →₀ ℕ
r : R
⊢ (aeval fun o ↦ o.elim Polynomial.X fun s ↦ Polynomial.C (X s)) ((monomial m) r) =
    (Polynomial.monomial (m none)) ((monomial m.some) r)
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

pp: case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree

Tactic:
· rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C,
      natDegree_C, mul_zero]

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
p q : R[X]
inst✝ : NoZeroDivisors R
q0 : ¬q.natDegree = 0
⊢ (p.comp q).natDegree = p.natDegree * q.natDegree
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ
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)
c : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = c → motive f
f : R[X]
df : f.natDegree ≤ N
hf : #f.support = c + 1
⊢ motive f

Tactic:
← eraseLead_add_C_mul_X_pow f

Goal state after:
case succ
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)
c : ℕ
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = c → motive f
f : R[X]
df : f.natDegree ≤ N
hf : #f.support = c + 1
⊢ motive (f.eraseLead + C f.leadingCoeff * X ^ f.natDegree)
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case succ.zero
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
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → motive f
hf : #f.support = 0 + 1
⊢ f.leadingCoeff ≠ 0

Tactic:
leadingCoeff_ne_zero,

Goal state after:
case succ.zero
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
hc : ∀ (f : R[X]), f.natDegree ≤ N → #f.support = 0 → motive f
hf : #f.support = 0 + 1
⊢ f ≠ 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
c : p = 0
⊢ ((optionEquivLeft R σ) 0).natDegree = degreeOf none 0

Tactic:
map_zero,

Goal state after:
case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial (Option σ) R
c : p = 0
⊢ natDegree 0 = degreeOf none 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case mpr
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = 0 → eval₂ i (⅟x) (reflect N f) = 0

Tactic:
· intro h
    rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
      zero_mul]

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

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

Tactic:
by_cases hf : f = 0

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f = 0
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree

case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.natDegree = f.reverse.natDegree + f.natTrailingDegree
Module: Mathlib.Algebra.Polynomial.Reverse

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

Tactic:
hf,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f = 0
⊢ natDegree 0 = (reverse 0).natDegree + natTrailingDegree 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℕ
r : R
⊢ ((X + C r) ^ n).natDegree = n

Tactic:
by
  rw [(monic_X_add_C r).natDegree_pow, natDegree_X_add_C, mul_one]

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

Goal state before:
pp: case pos
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
⊢ ((finSuccEquiv R n) 0).natDegree = degreeOf 0 0

Tactic:
map_zero,

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
c : f = 0
⊢ natDegree 0 = degreeOf 0 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ f.eraseLead.coeff (k i) ≠ 0

Tactic:
hf,

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
n : ℕ
hn : ∀ {f : R[X]}, #f.support = n → ∃ k x, ∃ (_ : StrictMono k) (_ : ∀ (i : Fin n), x i ≠ 0), f = ∑ i, C (x i) * X ^ k i
f : R[X]
h : #f.support = n + 1
k : Fin n → ℕ
x : Fin n → R
hk : StrictMono k
hx : ∀ (i : Fin n), x i ≠ 0
hf : f.eraseLead = ∑ i, C (x i) * X ^ k i
H : ¬∃ k, k.castSucc = Fin.last n
j : Fin (n + 1)
i : Fin n
hij : i.castSucc < j
hj : ¬∃ j₀, j₀.castSucc = j
⊢ (∑ i, C (x i) * X ^ k i).coeff (k i) ≠ 0
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
this : (-q).coeff (-q).natDegree = 1
⊢ (p + -q).Monic

Tactic:
apply Monic.add_of_right this

Goal state after:
R : Type u
inst✝ : Ring R
p q : R[X]
hq : q.leadingCoeff = -1
hpq : p.degree < q.degree
this : (-q).coeff (-q).natDegree = 1
⊢ p.degree < (-q).degree
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * (y ^ (n - m) * y ^ (m - 1 - j))

Tactic:
rw [← pow_add]

Goal state after:
R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j ∈ range m
⊢ x ^ j * y ^ (n - 1 - j) = x ^ j * y ^ (n - m + (m - 1 - j))
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)
⊢ (↑p).degree < (X ^ n).degree

Tactic:
· simp [mem_degreeLT.1 p.2]

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

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : Semiring R
k : Fin 3 → ℕ
x : Fin 3 → R
hk : StrictMono k
hx : ∀ (i : Fin 3), x i ≠ 0
h : #(∑ i, C (x i) * X ^ k i).support = 3
⊢ ∑ i, C (x i) * X ^ k i = C (x 0) * X ^ k 0 + C (x 1) * X ^ k 1 + C (x 2) * X ^ k 2

Tactic:
rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc, Fin.sum_univ_one]

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
k : Fin 3 → ℕ
x : Fin 3 → R
hk : StrictMono k
hx : ∀ (i : Fin 3), x i ≠ 0
h : #(∑ i, C (x i) * X ^ k i).support = 3
⊢ C (x (Fin.castSucc 0).castSucc) * X ^ k (Fin.castSucc 0).castSucc +
        C (x (Fin.last 1).castSucc) * X ^ k (Fin.last 1).castSucc +
      C (x (Fin.last 2)) * X ^ k (Fin.last 2) =
    C (x 0) * X ^ k 0 + C (x 1) * X ^ k 1 + C (x 2) * X ^ k 2
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.refine_1
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
⊢ (if n = 0 then x else 0) ∈ I

Tactic:
by_cases h : n = 0

Goal state after:
case pos
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : n = 0
⊢ (if n = 0 then x else 0) ∈ I

case neg
R : Type u
inst✝ : CommSemiring R
I : Ideal R
f✝ : R[X]
hf✝ : f✝ ∈ map C I
f : R[X]
hf : f ∈ ⇑C '' ↑I
n : ℕ
x : R
hx : x ∈ ↑I ∧ C x = f
h : ¬n = 0
⊢ (if n = 0 then x else 0) ∈ I
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: 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
hAC : ⊤.FG
hBC : ⊤.FG
⊢ ∃ B₀, B₀.FG ∧ ⊤.FG

Tactic:
obtain ⟨x, hx⟩ := hAC
  obtain ⟨y, hy⟩ := hBC
  have := hy
  simp_rw [eq_top_iff', mem_span_finset] at this
  choose f _ hf using this
  classical
  let s : Finset B := Finset.image₂ f (x ∪ y * y) y
  have hxy :
    ∀ xi ∈ x, xi ∈ span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) :=
    fun xi hxi =>
    hf xi ▸
      sum_mem fun yj hyj =>
        smul_mem (span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C))
          ⟨f xi yj, Algebra.subset_adjoin <| mem_image₂_of_mem (mem_union_left _ hxi) hyj⟩
          (subset_span <| mem_insert_of_mem hyj)
  have hyy :
    span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) *
        span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) ≤
      span (Algebra.adjoin A (↑s : Set B)) (↑(insert 1 y : Finset C) : Set C) := by
    rw [span_mul_span, span_le, coe_insert]
    rintro _ ⟨yi, rfl | hyi, yj, rfl | hyj, rfl⟩ <;> dsimp
    · rw [mul_one]
      exact subset_span (Set.mem_insert _ _)
    · rw [one_mul]
      exact subset_span (Set.mem_insert_of_mem _ hyj)
    · rw [mul_one]
      exact subset_span (Set.mem_insert_of_mem _ hyi)
    · rw [← hf (yi * yj)]
      exact
        SetLike.mem_coe.2
          (sum_mem fun yk hyk =>
            smul_mem (span (Algebra.adjoin A (↑s : Set B)) (insert 1 ↑y : Set C))
              ⟨f (yi * yj) yk,
                Algebra.subset_adjoin <|
                  mem_image₂_of_mem (mem_union_right _ <| mul_mem_mul hyi hyj) hyk⟩
              (subset_span <| Set.mem_insert_of_mem _ hyk : yk ∈ _))
  refine ⟨Algebra.adjoin A (↑s : Set B), Subalgebra.fg_adjoin_finset _, insert 1 y, ?_⟩
  convert! restrictScalars_injective A (Algebra.adjoin A (s : Set B)) C _
  rw [restrictScalars_top, eq_top_iff, ← Algebra.top_toSubmodule, ← hx, Algebra.adjoin_eq_span,
    span_le]
  refine fun r hr =>
    Submonoid.closure_induction (fun c hc => hxy c hc) (subset_span <| mem_insert_self _ _)
      (fun p q _ _ hp hq => hyy <| Submodule.mul_mem_mul hp hq) hr

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
⊢ False

Tactic:
have := degree_lt_degree_mul_X hp0

Goal state after:
R : Type u
inst✝ : Ring R
a✝ : Nontrivial R
hR : IsField R[X]
p : R[X]
hp : X * p = 1
hp0 : p ≠ 0
this : p.degree < (p * X).degree
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp.zero
R : Type u
inst✝ : CommRing R
P : Ideal R
H : (map C P).IsPrime
this : (comap C (map C P)).IsPrime
x : R
h : x ∈ P
⊢ (C x).coeff 0 ∈ P

Tactic:
rwa [coeff_C_zero]

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

Goal state before:
pp: case inl
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
⊢ g.coeff (i, j).2 * f.coeff (i, j).1 ∈ P

Tactic:
apply P.mul_mem_left

Goal state after:
case inl
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := ⋯
n : ℕ := ⋯
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hi : i < m
⊢ f.coeff (i, j).1 ∈ P
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case inr
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := Nat.find hf
n : ℕ := Nat.find hg
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hj : j < n
⊢ f.coeff (i, j).1 * g.coeff (i, j).2 ∈ P

Tactic:
apply P.mul_mem_left

Goal state after:
case inr
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
f g : R[X]
hf : ∃ n, f.coeff n ∉ P
hg : ∃ n, g.coeff n ∉ P
m : ℕ := ⋯
n : ℕ := ⋯
i j : ℕ
hij : (¬i = m ∨ ¬j = n) ∧ i + j = m + n
hj : j < n
⊢ g.coeff (i, j).2 ∈ P