mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.Finite

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
⊢ finrank R M = 0

Tactic:
finrank,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : Subsingleton M
⊢ toNat (Module.rank R M) = 0
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
⊢ ∃ n b i j, i ≠ j ∧ ↑v = b i ∧ f = b.coord j

Tactic:
have H₁ : LinearIndepOn K _root_.id n := by
    apply LinearIndepOn.id_insert
    · apply LinearIndepOn.image
      · exact b₁.linearIndependent.linearIndepOn_id
      · simp
    · simp [hs, hw]

Goal state after:
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
⊢ ∃ n b i j, i ≠ j ∧ ↑v = b i ∧ f = b.coord j
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
x : V
⊢ x ∈ span K n

Tactic:
simp only [n, mem_span_insert']

Goal state after:
K : Type u_6
V : Type u_7
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : V →ₗ[K] K
hf : f ≠ 0
v : ↥f.ker
hv : ↑v ≠ 0
this : LinearIndepOn K _root_.id {v}
b₁ : Basis (↑(this.extend ⋯)) K ↥f.ker := Basis.extend this
w : V
hw : f w = 1
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
n : Set V := insert w s
H₁ : LinearIndepOn K _root_.id n
x : V
⊢ ∃ a, x + a • w ∈ span K s
Module: Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : finrank F ↥S = 1
inst✝ : Free F ↥S
⊢ Module.rank F ↥S ≤ 1

Tactic:
finrank,

Goal state after:
F : Type u_1
E : Type u_2
inst✝⁴ : CommRing F
inst✝³ : StrongRankCondition F
inst✝² : Ring E
inst✝¹ : Algebra F E
S : Subalgebra F E
h : toNat (Module.rank F ↥S) = 1
inst✝ : Free F ↥S
⊢ Module.rank F ↥S ≤ 1
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
⊢ ∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c

Tactic:
have hdir : DirectedOn (· ≤ ·) (domain '' c) :=
    directedOn_image.2 (hc.mono @(domain_mono.monotone))

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
⊢ ∃ f, { domain := sSup (domain '' c), toFun := f } ∈ upperBounds c
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
a✝ : R
⊢ ((C a✝).comp ψ).comp χ = (C a✝).comp (ψ.comp χ)

Tactic:
simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ, ← mul_assoc]

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ p✝ q✝ : R[X]
a✝¹ : (p✝.comp ψ).comp χ = p✝.comp (ψ.comp χ)
a✝ : (q✝.comp ψ).comp χ = q✝.comp (ψ.comp χ)
⊢ ((p✝ + q✝).comp ψ).comp χ = (p✝ + q✝).comp (ψ.comp χ)

Tactic:
simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ, ← mul_assoc]

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

Goal state before:
pp: case refine_3
R : Type u_1
inst✝ : CommSemiring R
φ ψ χ : R[X]
n✝ : ℕ
a✝¹ : R
a✝ : ((C a✝¹ * X ^ n✝).comp ψ).comp χ = (C a✝¹ * X ^ n✝).comp (ψ.comp χ)
⊢ ((C a✝¹ * X ^ (n✝ + 1)).comp ψ).comp χ = (C a✝¹ * X ^ (n✝ + 1)).comp (ψ.comp χ)

Tactic:
simp_all only [add_comp, mul_comp, C_comp, X_comp, pow_succ, ← mul_assoc]

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

Goal state before:
pp: ⊢ minFac 1 = 1

Tactic:
by
  simp [minFac, minFacAux]

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

Goal state before:
pp: n : ℕ
n1 : n = 1
⊢ n.minFac ∣ n

Tactic:
by simp [n1]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonAssocSemiring R
⊢ ∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x

Tactic:
let : CharP R (ringChar R) := (Classical.choose_spec (CharP.existsUnique R)).1

Goal state after:
R : Type u_1
inst✝ : NonAssocSemiring R
this : CharP R (ringChar R) := (Classical.choose_spec (CharP.existsUnique R)).left
⊢ ∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: R : Type u_1
inst✝ : AddMonoidWithOne R
p q : ℕ
hp : ExpChar R p
hq : ExpChar R q
⊢ p = q

Tactic:
rcases hp with ⟨hp⟩ | ⟨hp'⟩
  · rcases hq with hq | hq'
    exacts [rfl, False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hq'))]
  · rcases hq with hq | hq'
    exacts [False.elim (Nat.not_prime_zero (CharP.eq R ‹_› (CharP.ofCharZero R) ▸ hp')),
      CharP.eq R ‹_› ‹_›]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : Nontrivial R
hq : ExpChar R 1
⊢ CharZero R

Tactic:
by
  cases hq
  · assumption
  · exact False.elim (CharP.char_ne_one R 1 rfl)

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
x : R
n : ℕ
⊢ (C x * X).coeff n = if n = 1 then x else 0

Tactic:
← pow_one X,

Goal state after:
R : Type u
inst✝ : Semiring R
x : R
n : ℕ
⊢ (C x * X ^ 1).coeff n = if n = 1 then x else 0
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
by rw [hp, leadingCoeff_zero, zero_mul]

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p : R[X]
h : IsUnit p
⊢ p.natDegree = 0

Tactic:
nontriviality R
  obtain ⟨q, hq⟩ := h.exists_right_inv
  have := natDegree_mul (left_ne_zero_of_mul_eq_one hq) (right_ne_zero_of_mul_eq_one hq)
  rw [hq, natDegree_one, eq_comm, add_eq_zero] at this
  exact this.1

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

Goal state before:
pp: case inr
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
h✝ : Nontrivial R
⊢ supDegree D (p * q) = supDegree D p + supDegree D q

Tactic:
apply supDegree_mul hD hadd ?_ hp.ne_zero hq

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
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
h✝ : Nontrivial R
⊢ leadingCoeff D p * leadingCoeff D q ≠ 0
Module: Mathlib.Algebra.Polynomial.Eval.Degree

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ eval₂ f x p = ∑ i ∈ range n, f (p.coeff i) * x ^ i

Tactic:
rw [eval₂_eq_sum, p.sum_over_range' _ _ hn]
  intro i
  rw [f.map_zero, zero_mul]

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
M : ↥R[x] → Prop
a : ↥R[x]
f : ∀ (p : R[X]), M ⟨(aeval x) p, ⋯⟩
⊢ M a

Tactic:
obtain ⟨p, hp⟩ := Algebra.adjoin_eq_exists_aeval _ x a
  grind

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
M : ↥R[x] → Prop
a : ↥R[x]
f : ∀ (p : R[X]), M ⟨(aeval x) p, ⋯⟩
⊢ M a

Tactic:
by
  obtain ⟨p, hp⟩ := Algebra.adjoin_eq_exists_aeval _ x a
  grind

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

Goal state before:
pp: case mpr
α : Type u
inst✝ : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ (∃ a_1 b, a_1 + b = n ∧ single a a_1 = x ∧ single a b = y) → x + y = single a n

Tactic:
rintro ⟨a, b, rfl, rfl, rfl⟩

Goal state after:
case mpr
α : Type u
inst✝ : DecidableEq α
a✝ : α
a b : ℕ
⊢ single a✝ a + single a✝ b = single a✝ (a + b)
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝⁴ : AddCommMonoid α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : Sub α
inst✝ : OrderedSub α
f : ι ↪ κ
f1 f2 : ι →₀ α
⊢ embDomain f (f1 - f2) = embDomain f f1 - embDomain f f2

Tactic:
by
  simp_rw [embDomain_eq_mapDomain, mapDomain_tsub f.injective]

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

Goal state before:
pp: S : Type v
inst✝ : CommSemiring S
⊢ aevalTower (AlgHom.id S S) = aeval

Tactic:
by
  ext s
  simp only [eval_X, aevalTower_X, coe_aeval_eq_eval]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
φ : MvPolynomial σ R
d₀ : σ →₀ ℕ
h : ∀ d ∈ φ.support, d = d₀
⊢ φ = (monomial d₀) (coeff d₀ φ)

Tactic:
classical
  ext d
  rcases eq_or_ne d d₀ with rfl | hd
  · rw [coeff_monomial, if_pos rfl]
  · rw [notMem_support_iff.mp fun hmem ↦ hd (h d hmem), coeff_monomial, if_neg fun e ↦ hd e.symm]

Goal state after:
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
⊢ coeff m (p * (monomial s) r) = if s ≤ m then r * coeff (m - s) p else 0

Tactic:
mul_comm r

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
m s : σ →₀ ℕ
r : R
p : MvPolynomial σ R
⊢ coeff m (p * (monomial s) r) = if s ≤ m then coeff (m - s) p * r else 0
Module: Mathlib.Algebra.MvPolynomial.Rename

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
hs : ↑s.support ⊆ range f
⊢ (killCompl hf) ((monomial s) c) = (monomial (Finsupp.comapDomain f s ⋯)) c

Tactic:
nth_rw 1 [← s.mapDomain_comapDomain f hf hs, killCompl_monomial_mapDomain]

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

Goal state before:
pp: σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
p : MvPolynomial σ R
r : R
⊢ C r = (rename Subtype.val) (C r)

Tactic:
by rw [rename_C]

Goal state after:
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
p : MvPolynomial σ S
⊢ p ∈ coeffsIn σ M ↔ ↑p.coeffs ⊆ ↑M

Tactic:
simp only [mem_coeffsIn, coeffs, Finset.coe_image, image_subset_iff]

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
p : MvPolynomial σ S
⊢ (∀ (i : σ →₀ ℕ), coeff i p ∈ M) ↔ ↑p.support ⊆ (fun m ↦ coeff m p) ⁻¹' ↑M
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: case pos
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
h : ↑p.support ⊆ (fun m ↦ coeff m p) ⁻¹' ↑M
i : σ →₀ ℕ
hp : i ∈ p.support
⊢ coeff i p ∈ M

Tactic:
exact h hp

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
⊢ coeffsIn σ M * coeffsIn σ N ≤ coeffsIn σ (M * N)

Tactic:
· rw [Submodule.mul_le]
    intro x hx y hy k
    rw [MvPolynomial.coeff_mul]
    exact sum_mem fun c hc ↦ Submodule.mul_mem_mul (hx _) (hy _)

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
i j : σ
k : ℕ
h : i ≠ j
⊢ degreeOf i (X j ^ k) = 0

Tactic:
by
  induction k with
  | zero => rw [pow_zero, ← C_1, degreeOf_C]
  | succ k hk => rw [pow_add, pow_one, degreeOf_mul_X_of_ne _ h, hk]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : LinearOrder σ
r : R
⊢ supDegree (⇑toLex) (C r) = 0

Tactic:
classical
    exact (supDegree_single _ r).trans (ite_eq_iff'.mpr ⟨fun _ => rfl, fun _ => rfl⟩)

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

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

Tactic:
coeff_comp_degree_mul_degree hq

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
h : p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
hq : ¬q.natDegree = 0
⊢ p.leadingCoeff * q.leadingCoeff ^ p.natDegree ≠ 0
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg.refine_1
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ x ∈ {i | i ∈ insert x s ∧ f i ≠ 0}

pp: case neg.refine_2
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ y ∈ {i | i ∈ insert x s ∧ f i ≠ 0}

pp: case neg.refine_3
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H✝ : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
H : x = y
⊢ x ∈ s

Tactic:
· simp [hx0]

Goal state after:
case neg.refine_2
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ y ∈ {i | i ∈ insert x s ∧ f i ≠ 0}

case neg.refine_3
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H✝ : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
H : x = y
⊢ x ∈ s
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case neg.refine_3
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
hs : s.Nonempty
y : S
H✝ : (f x).degree = (f y).degree
hy : y ∈ s
hy' : (s.sup fun i ↦ (f i).degree) = (f y).degree
hx0 : ¬f x = 0
hy0 : f y ≠ 0
H : x = y
⊢ x ∈ s

Tactic:
· exact H.symm ▸ hy

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

Goal state before:
pp: case insert.inr.inr
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (s.sum f).degree < (f x).degree
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree

Tactic:
degree_add_eq_left_of_degree_lt H

Goal state after:
case insert.inr.inr
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH : (s.sum f).degree = s.sup fun i ↦ (f i).degree
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
H : (s.sum f).degree < (f x).degree
⊢ (f x).degree = (f x).degree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
x : S₁
⊢ (optionEquivLeft R S₁) (X (Option.some x)) = Polynomial.C (X x)

Tactic:
simp [optionEquivLeft_apply, aeval_X]

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
⊢ (optionEquivLeft R S₁) (X none) = Polynomial.X

Tactic:
simp [optionEquivLeft_apply, aeval_X]

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

Goal state before:
pp: case e'_3.e'_6
R : Type u
S₁ : Type v
inst✝ : CommSemiring R
s : S₁ → R
y : R
f : MvPolynomial (Option S₁) R
r : R
⊢ r = (eval s) ((algebraMap R (MvPolynomial S₁ R)) r)

Tactic:
exact (eval_C _).symm

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

Goal state before:
pp: case e'_3.e'_6
R : Type u
inst✝ : CommSemiring R
n : ℕ
s : Fin n → R
y : R
f : MvPolynomial (Fin (n + 1)) R
r : R
⊢ r = (eval s) ((algebraMap R (MvPolynomial (Fin n) R)) r)

Tactic:
exact (eval_C _).symm

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ f p.leadingCoeff ≠ 0

Tactic:
rw [hp.leadingCoeff, f.map_one]

Goal state after:
R : Type u
inst✝² : Semiring R
p : R[X]
S : Type u_1
inst✝¹ : Semiring S
inst✝ : Nontrivial S
f : R →+* S
hp : p.Monic
map_eq : Polynomial.map f p = 1
a✝ : Nontrivial R
⊢ 1 ≠ 0
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case some
ι : Type w
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
s : Finset ι
hf : ∑ k ∈ s, (f k).leadingCoeff ≠ 0
d : ℕ
hd : ∀ k ∈ s, (f k).degree = some d
⊢ (∑ k ∈ s, f k).leadingCoeff = ∑ k ∈ s, (f k).leadingCoeff

Tactic:
replace hd k (hk : k ∈ s) : (f k).natDegree = d := natDegree_eq_of_degree_eq_some <| hd k hk
    suffices (∑ k ∈ s, f k).natDegree = d by simp_all [leadingCoeff]
    apply natDegree_eq_of_le_of_coeff_ne_zero
    · aesop (add safe natDegree_sum_le_of_forall_le)
    · simp_all [leadingCoeff]

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
t : Multiset R[X]
⊢ ∀ (a : List R[X]), (prod ⟦a⟧).degree ≤ (Multiset.map degree ⟦a⟧).sum

Tactic:
simpa using degree_list_prod_le

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ (((finSuccEquiv R n) p).coeff i).support
⊢ (cons i m) j.succ ≤ p.support.sup fun m ↦ m j.succ

Tactic:
exact Finset.le_sup
    (f := fun (g : Fin (Nat.succ n) →₀ ℕ) => g (Fin.succ j))
    (mem_support_coeff_finSuccEquiv.1 hm)

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : ℕ
e : σ ≃ Fin n
φ : MvPolynomial (Option σ) R
⊢ (finSuccEquiv R n) ((rename ⇑(e.optionCongr.trans (_root_.finSuccEquiv n).symm)) φ) =
    Polynomial.map (rename ⇑e).toRingHom ((optionEquivLeft R σ) φ)

Tactic:
by
  suffices (finSuccEquiv R n).toRingEquiv.toRingHom.comp (rename ((Equiv.optionCongr e).trans
        (_root_.finSuccEquiv n).symm)).toRingHom =
      (Polynomial.mapRingHom (rename e).toRingHom).comp (optionEquivLeft R σ) by
    exact DFunLike.congr_fun this φ
  apply ringHom_ext
  · simp [Polynomial.algebraMap_apply, algebraMap_eq, finSuccEquiv_apply, optionEquivLeft_apply]
  · rintro (i | i) <;> simp [finSuccEquiv_apply, optionEquivLeft_apply]

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : k • p = 0
⊢ p = 0

Tactic:
rw [← smul_zero k] at hp

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
S : Type u_1
inst✝ : SMulZeroClass S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : k • p = k • 0
⊢ p = 0
Module: Mathlib.Algebra.Polynomial.EraseLead

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

Tactic:
Fin.sum_univ_castSucc,

Goal state after:
case refine_1
R : Type u_1
inst✝ : Semiring R
k : Fin 2 → ℕ
x : Fin 2 → R
hk : StrictMono k
hx : ∀ (i : Fin 2), x i ≠ 0
h : #(∑ i, C (x i) * X ^ k i).support = 2
⊢ ∑ i, C (x i.castSucc) * X ^ k i.castSucc + C (x (Fin.last 1)) * X ^ k (Fin.last 1) =
    C (x 0) * X ^ k 0 + C (x 1) * X ^ k 1
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:
Fin.sum_univ_castSucc,

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
⊢ ∑ i, C (x i.castSucc) * X ^ k i.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.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.castSucc) * X ^ k i.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

Tactic:
Fin.sum_univ_castSucc,

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
⊢ ∑ i, C (x i.castSucc.castSucc) * X ^ k i.castSucc.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 neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : ¬s.Nonempty
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n

Tactic:
Set.not_nonempty_iff_eq_empty

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
s : Set R[X]
s_fin : s.Finite
s_emp : s = ∅
⊢ ∃ n, Submodule.span R s ≤ degreeLE R ↑n
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case mp
R : Type u
inst✝ : CommSemiring R
I : Ideal R[X]
i : ℕ
p : R[X]
hpI : p ∈ I
left✝ : p.degree ≤ ↑i
⊢ ∃ p_1 ∈ I, p_1.leadingCoeff = p.leadingCoeff

Tactic:
exact ⟨p, hpI, rfl⟩

Goal state after: