mathlib-initiative/mathlib-tactics huggingface dataset:
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
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
⊢ ↑v ∈ n

Tactic:
by simp [n, hvs]

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.VectorSpace

Goal state before:
pp: case refine_2.inl
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
s : Set V := ⇑f.ker.subtype '' Set.range ⇑b₁
hs : span K s = f.ker
hvs : ↑v ∈ s
x : V
hw : f x = 1
n : Set V := insert x s
H₁ : LinearIndepOn K _root_.id n
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
⊢ f ((Basis.mk H₁ ⋯) ⟨x, ⋯⟩) = (Finsupp.single ⟨x, ⋯⟩ 1) ⟨x, ⋯⟩

pp: case refine_2.inr
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
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
x : ↥f.ker
hx : x ∈ Set.range ⇑b₁
⊢ f ((Basis.mk H₁ ⋯) ⟨f.ker.subtype x, ⋯⟩) = (Finsupp.single ⟨f.ker.subtype x, ⋯⟩ 1) ⟨w, ⋯⟩

Tactic:
· simp [hw]

Goal state after:
case refine_2.inr
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
H₂ : ⊤ ≤ span K n
b : Basis (↑n) K V := Basis.mk H₁ ⋯
x : ↥f.ker
hx : x ∈ Set.range ⇑b₁
⊢ f ((Basis.mk H₁ ⋯) ⟨f.ker.subtype x, ⋯⟩) = (Finsupp.single ⟨f.ker.subtype x, ⋯⟩ 1) ⟨w, ⋯⟩
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f g : E →ₛₗ.[σ] F
c : R
x : E
x✝ : x ∈ {x | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩}
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx : ↑f ⟨x, hfx⟩ = ↑g ⟨x, hgx⟩
this : ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain), ⟨c • x, ⋯⟩ = c • ⟨x, hfx⟩
⊢ ↑f ⟨c • x, ⋯⟩ = ↑g ⟨c • x, ⋯⟩

Tactic:
this hfx,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring S
inst✝⁶ : Ring T
σ : R →+* S
τ : S →+* T
E : Type u_4
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_5
inst✝³ : AddCommGroup F
inst✝² : Module S F
G : Type u_6
inst✝¹ : AddCommGroup G
inst✝ : Module T G
f g : E →ₛₗ.[σ] F
c : R
x : E
x✝ : x ∈ {x | ∃ (hf : x ∈ f.domain) (hg : x ∈ g.domain), ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩}
hfx : x ∈ f.domain
hgx : x ∈ g.domain
hx : ↑f ⟨x, hfx⟩ = ↑g ⟨x, hgx⟩
this : ∀ {f : E →ₛₗ.[σ] F} (hfx : x ∈ f.domain), ⟨c • x, ⋯⟩ = c • ⟨x, hfx⟩
⊢ ↑f (c • ⟨x, hfx⟩) = ↑g ⟨c • x, ⋯⟩
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 : Module.rank F ↥S ≤ 1
inst✝ : Free F ↥S
a✝ : Nontrivial E
⊢ S = ⊥

Tactic:
obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := F) (M := S)

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 : Module.rank F ↥S ≤ 1
inst✝ : Free F ↥S
a✝ : Nontrivial E
κ : Type u_2
b : Basis κ F ↥S
⊢ 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 : Module.rank F ↥S ≤ 1
inst✝ : Free F ↥S
⊢ S = ⊥

Tactic:
nontriviality E
  obtain ⟨κ, b⟩ := Module.Free.exists_basis (R := F) (M := S)
  by_cases h1 : Module.rank F S = 1
  · refine bot_unique fun x hx ↦ Algebra.mem_bot.2 ?_
    rw [← b.mk_eq_rank'', eq_one_iff_unique, ← unique_iff_subsingleton_and_nonempty] at h1
    obtain ⟨h1⟩ := h1
    obtain ⟨y, hy⟩ := (bijective_algebraMap_of_linearEquiv (b.repr ≪≫ₗ
      Finsupp.uniqueLinearEquiv _ _ default).symm).surjective ⟨x, hx⟩
    exact ⟨y, congr(Subtype.val $(hy))⟩
  have := mk_eq_zero_iff.1 (b.mk_eq_rank''.symm ▸ Cardinal.lt_one_iff.1 (h.lt_of_ne h1))
  have := b.repr.toEquiv.subsingleton
  exact False.elim <| one_ne_zero congr(S.val $(Subsingleton.elim 1 0))

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

Goal state before:
pp: case succ
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
ih : eval₂ f x ↑n = ↑n
⊢ eval₂ f x ↑(n + 1) = ↑(n + 1)

Tactic:
n.cast_succ,

Goal state after:
case succ
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
ih : eval₂ f x ↑n = ↑n
⊢ eval₂ f x (↑n + 1) = ↑(n + 1)
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p q : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
hf : ∀ (k : ℕ), Commute (f (q.coeff k)) x
⊢ eval₂ f x (p * q) = eval₂ f x p * eval₂ f x q

Tactic:
rcases p with ⟨p⟩; rcases q with ⟨q⟩
  simp only [coeff] at hf
  simp only [← ofFinsupp_mul, eval₂_ofFinsupp]
  exact liftNC_mul _ _ p q fun {k n} _hn => (hf k).pow_right n

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : Semiring R
p : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x (X * p) = eval₂ f x p * x

Tactic:
by rw [X_mul, eval₂_mul_X]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case add
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
x y : FreeAlgebra R X
hx : x ∈ S
hy : y ∈ S
⊢ x + y ∈ S

Tactic:
exact S.add_mem hx hy

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

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : DecidableEq G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x : G
lx : IsLeftRegular x
y : G
yf : y ∈ f.coeff.support
hy : x * y ∈ image (fun x_1 ↦ x * x_1) f.coeff.support
⊢ x * y ∈ (single x r * f).coeff.support

Tactic:
simp [coeff_mul, mem_support_iff.mp yf, hr, lx.eq_iff]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_2
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)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
⊢ ∀ (m : R) (x : ↥(sSup (domain '' c))), f (m • x) = σ m • f x

Tactic:
intro c x

Goal state after:
case w.refine_2
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✝)
P : (x : ↥(sSup (domain '' c✝))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c✝)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c✝) (x : ↥(sSup (domain '' c✝))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
c : R
x : ↥(sSup (domain '' c✝))
⊢ f (c • x) = σ c • f x
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
⊢ -↑a = 0 ↔ ↑p ∣ a

Tactic:
← Int.cast_neg,

Goal state after:
case inl
R : Type u_1
inst✝¹ : AddGroupWithOne R
p : ℕ
inst✝ : CharP R p
a : ℤ
h : a < 0
⊢ ↑(-a) = 0 ↔ ↑p ∣ a
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (List.map (fun f ↦ f.coeff.support.sup degb) (List.replicate n f)).sum =
    (List.replicate n (f.coeff.support.sup degb)).sum

Tactic:
List.map_replicate

Goal state after:
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁶ : SemilatticeSup B
inst✝⁵ : OrderBot B
inst✝⁴ : Semiring R
inst✝³ : AddMonoid A
inst✝² : AddMonoid B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
degb : A → B
degb0 : degb 0 ≤ 0
degbm : ∀ (a b : A), degb (a + b) ≤ degb a + degb b
n : ℕ
f : R[A]
⊢ (List.replicate n (f.coeff.support.sup degb)).sum = (List.replicate n (f.coeff.support.sup degb)).sum
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case refine_2
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s✝ : Finset ι
f : ι → R[A]
i : ι
s : Finset ι
⊢ i ∉ s →
    supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i) →
      supDegree D (∏ i ∈ insert i s, f i) ≤ ∑ i ∈ insert i s, supDegree D (f i)

Tactic:
his

Goal state after:
case refine_2
R : Type u_7
A : Type u_8
B : Type u_9
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A
inst✝⁴ : AddCommMonoid B
inst✝³ : SemilatticeSup B
inst✝² : OrderBot B
inst✝¹ : AddLeftMono B
inst✝ : AddRightMono B
D : A → B
hzero : D 0 = 0
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
ι : Type u_10
s✝ : Finset ι
f : ι → R[A]
i : ι
s : Finset ι
his : i ∉ s
⊢ supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i) →
    supDegree D (∏ i ∈ insert i s, f i) ≤ ∑ i ∈ insert i s, supDegree D (f i)
Module: Mathlib.Algebra.Polynomial.Degree.Defs

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

Tactic:
rw [C_mul_X_pow_eq_monomial, leadingCoeff_monomial]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.degree + q.degree ≤ ↑p.natDegree + ↑q.natDegree

Tactic:
apply add_le_add

Goal state after:
case h₁
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ p.degree ≤ ↑p.natDegree

case h₂
R : Type u
inst✝ : Semiring R
p q : R[X]
⊢ q.degree ≤ ↑q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Domain

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.natDegree ≤ p.natDegree + q.natDegree

Tactic:
exact Nat.le_add_right _ _

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

Goal state before:
pp: case pos
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ ∑ n ∈ f.support, (RingHom.id S) (f.coeff n) * z ^ n
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
⊢ p ∣ f.coeff i * z ^ i

Tactic:
← Finset.insert_erase hi,

Goal state after:
case pos
S : Type v
inst✝ : CommRing S
z p : S
f : S[X]
i : ℕ
dvd_eval : p ∣ ∑ n ∈ insert i (f.support.erase i), (RingHom.id S) (f.coeff n) * z ^ n
dvd_terms : ∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * z ^ j
hi : i ∈ f.support
⊢ p ∣ f.coeff i * z ^ i
Module: Mathlib.Data.DFinsupp.Order

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (α i)
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), IsBotZeroClass (α i)
inst✝ : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ Disjoint f g ↔ Disjoint f.support g.support

Tactic:
by
  simp [disjoint_iff, bot_eq_zero, ← DFinsupp.support_eq_empty]

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

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

Tactic:
← leadingCoeff_eq_zero

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
g : α → R
⊢ (∏ x ∈ s, C (g x)) * ∏ i ∈ s, (monomial (f i)) 1 = ∏ i ∈ s, (monomial (f i)) (g i)

Tactic:
← Finset.prod_mul_distrib,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
α : Type u_2
s : Finset α
f : α → σ →₀ ℕ
g : α → R
⊢ ∏ x ∈ s, C (g x) * (monomial (f x)) 1 = ∏ i ∈ s, (monomial (f i)) (g i)
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ toMultiset d ≤ (p + q).degrees

Tactic:
rw [Multiset.disjoint_iff_ne] at h

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
⊢ toMultiset d ≤ (p + q).degrees
Module: Mathlib.Algebra.MvPolynomial.Variables

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ (p + q).degrees
⊢ x ∈ p.degrees ∨ x ∈ q.degrees

Tactic:
simpa using Multiset.mem_of_le degrees_add_le hx

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

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝¹ : CommRing R
p : MvPolynomial σ R
inst✝ : DecidableEq σ
d d' : σ →₀ ℕ
c : R
hdd' : d ≠ d'
hc : coeff d p = c
x : σ →₀ ℕ
hx : x ∈ (p - ((monomial d) c - (monomial d') c)).support
hd_not : d ∉ (p - ((monomial d) c - (monomial d') c)).support
hdelta : x ∈ ((monomial d) c - (monomial d') c).support
h✝ : c = 0
h1 : x ∈ ∅
⊢ x ∈ p.support.erase d ∪ {d'}

Tactic:
exact absurd h1 (Finset.notMem_empty _)

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : MvPolynomial σ R
n : ℕ
⊢ (a ^ n).totalDegree ≤ n * a.totalDegree

Tactic:
rw [Finset.pow_eq_prod_const, ← Nat.nsmul_eq_mul, Finset.nsmul_eq_sum_const]
  refine supDegree_prod_le rfl (fun _ _ => ?_)
  exact Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)

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

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

pp: case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : ¬f = 0
⊢ #f.support ≤ 1

Tactic:
case pos => simp [hpz]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead = 0
hpz : ¬f = 0
⊢ #f.support ≤ 1
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : f.natDegree < 2
⊢ f.eraseLead = 0

Tactic:
Nat.lt_succ_iff,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
hnext : f.nextCoeff = 0
hlead : f.natDegree ≤ 1
⊢ f.eraseLead = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: σ : Type u_1
R : Type u_2
S : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Unique σ
f : R[X]
φ : R →+* S
a : σ → S
⊢ eval₂ φ a ((uniqueAlgEquiv R σ).symm f) = Polynomial.eval₂ φ (a default) f

Tactic:
rw [(eval₂_uniqueAlgEquiv (R := R) (σ := σ) (f := (MvPolynomial.uniqueAlgEquiv R σ).symm f)
    (φ := φ) (a := a)).symm]
  rw [AlgEquiv.apply_symm_apply]

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

Goal state before:
pp: case neg.inl
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
⊢ ((X - C x) * P).eraseLead.coeff n - 0 = ((X - C x) * P.eraseLead).coeff n

Tactic:
rw [← self_sub_monomial_natDegree_leadingCoeff, coeff_sub, coeff_monomial, if_neg (by lia)]

Goal state after:
case neg.inl
R : Type u_2
inst✝² : Ring R
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
x : R
P : R[X]
hx : x ≠ 0
h : P.nextCoeff = 0
hp : ¬P = 0
he : ¬P.eraseLead = 0
h₁ : ((X - C x) * P).natDegree = P.natDegree + 1
dP : ℕ
hdP : P.natDegree = dP + 2
h₂ : ((X - C x) * P).nextCoeff ≠ 0
n : ℕ
hn : n < P.natDegree
hd₁ : n < ((X - C x) * P).eraseLead.natDegree
⊢ ((X - C x) * P).coeff n - 0 - 0 = ((X - C x) * P.eraseLead).coeff n
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
i : S₂
⊢ (commAlgEquiv R S₁ S₂) (C (X i)) = X i

Tactic:
by simp [map, X, monomial]

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

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

Tactic:
by
  by_cases q0 : q.natDegree = 0
  · rw [degree_le_zero_iff.mp (natDegree_eq_zero_iff_degree_le_zero.mp q0), comp_C, natDegree_C,
      natDegree_C, mul_zero]
  · by_cases p0 : p = 0
    · simp only [p0, zero_comp, natDegree_zero, zero_mul]
    · simp only [Ne, mul_eq_zero, leadingCoeff_eq_zero, p0, natDegree_comp_eq_of_mul_ne_zero,
        ne_zero_of_natDegree_gt (Nat.pos_of_ne_zero q0), not_false_eq_true, pow_ne_zero, or_self]

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

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

Tactic:
← mul_eq_zero,

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h : p.comp q = 0
⊢ p.natDegree * q.natDegree = 0
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p.Monic
hq : q.Monic
h : q.natDegree ≠ 0
a✝ : Nontrivial R
this : (p.comp q).natDegree = p.natDegree * q.natDegree
⊢ (p.comp q).Monic

Tactic:
rw [Monic.def, Polynomial.leadingCoeff, this, coeff_comp_degree_mul_degree h, hp.leadingCoeff,
    hq.leadingCoeff, one_pow, mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ f.reverse.coeff n = f.coeff ((revAt f.natDegree) n)

Tactic:
reverse,

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ (reflect f.natDegree f).coeff n = f.coeff ((revAt f.natDegree) n)
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ f.reverse.coeff (f.natDegree - f.natTrailingDegree) ≠ 0

Tactic:
reverse,

Goal state after:
case neg.a
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f = 0
⊢ (reflect f.natDegree f).coeff (f.natDegree - f.natTrailingDegree) ≠ 0
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
⊢ (-f).reverse = -f.reverse

Tactic:
reverse,

Goal state after:
R : Type u_1
inst✝ : Ring R
f : R[X]
⊢ reflect (-f).natDegree (-f) = -f.reverse
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
f : R[X]
⊢ reflect (-f).natDegree (-f) = -f.reverse

Tactic:
reverse,

Goal state after:
R : Type u_1
inst✝ : Ring R
f : R[X]
⊢ reflect (-f).natDegree (-f) = -reflect f.natDegree f
Module: Mathlib.Algebra.Polynomial.Monic

Goal state before:
pp: R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
a✝ : Nontrivial R
⊢ (↑p).coeff n = 1

Tactic:
p.2.1

Goal state after:
R : Type u
n : ℕ
inst✝ : Semiring R
p : MonicDegreeEq R n
a✝ : Nontrivial R
⊢ 1 = 1
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: case p
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
x✝ : Fin n →₀ ℕ
| coeff x✝ (((finSuccEquiv R n) f).coeff i) ≠ 0 ∧ cons i x✝ = m

Tactic:
finSuccEquiv_coeff_coeff,

Goal state after:
case p
R : Type u
inst✝ : CommSemiring R
n : ℕ
f : MvPolynomial (Fin (n + 1)) R
i : ℕ
m : Fin (n + 1) →₀ ℕ
x✝ : Fin n →₀ ℕ
| coeff (cons i x✝) f ≠ 0 ∧ cons i x✝ = m
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⟧).natDegree ≤ (Multiset.map natDegree ⟦a⟧).sum

Tactic:
by simpa using natDegree_list_prod_le

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

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

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

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

Goal state before:
pp: case mp.h
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * (p * C ↑h.unit⁻¹) = 0
⊢ (p * C ↑h.unit⁻¹).Monic

Tactic:
refine monic_mul_C_of_leadingCoeff_mul_eq_one ?_

Goal state after:
case mp.h
R : Type u
inst✝ : Semiring R
p : R[X]
h : IsUnit p.leadingCoeff
q : R[X]
hp : q * (p * C ↑h.unit⁻¹) = 0
⊢ p.leadingCoeff * ↑h.unit⁻¹ = 1
Module: Mathlib.RingTheory.Adjoin.FG

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ y ∈ Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)

Tactic:
rw [← hq']

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s t : Set A
h1 : (Subalgebra.toSubmodule (adjoin R s)).FG
h2 : (Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)).FG
p : Set A
hp : p.Finite
hp' : span R p = Subalgebra.toSubmodule (adjoin R s)
q : Set A
hq : q.Finite
hq' : span (↥(adjoin R s)) q = Subalgebra.toSubmodule (adjoin (↥(adjoin R s)) t)
x : A
hx : x ∈ p
y : A
hy : y ∈ q
⊢ y ∈ span (↥(adjoin R s)) q
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x : R
m n : ℕ
hmn : m ≤ n
⊢ x ^ n - 1 - (x ^ m - 1) = x ^ n - x ^ m

Tactic:
sub_sub_sub_cancel_right

Goal state after:
R : Type u_1
inst✝ : Ring R
x : R
m n : ℕ
hmn : m ≤ n
⊢ x ^ n - x ^ m = x ^ n - x ^ m
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
a✝ : Nontrivial R
⊢ (∑ i ∈ range n, X ^ i).Monic

Tactic:
apply monic_X.geom_sum _ hn

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
a✝ : Nontrivial R
⊢ 0 < X.natDegree
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: case h
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ 1 ∉ P

Tactic:
← eq_top_iff_one

Goal state after:
case h
R : Type u
inst✝ : CommRing R
P : Ideal R
h : P.IsPrime
⊢ ¬P = ⊤
Module: Mathlib.RingTheory.FiniteType

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ (algebraMap A B).FiniteType ↔ Algebra.FiniteType A B

Tactic:
FiniteType,

Goal state after:
A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ Algebra.FiniteType A B ↔ Algebra.FiniteType A B