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

Goal state before:
pp: case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder B
inst✝⁵ : OrderBot B
q : R[A]
D : A → B
inst✝⁴ : AddZeroClass A
inst✝³ : Add B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
⊢ leadingCoeff D (0 * q) = 0 * leadingCoeff D q

Tactic:
zero_mul,

Goal state after:
case inl
R : Type u_1
A : Type u_3
B : Type u_5
inst✝⁷ : Semiring R
inst✝⁶ : LinearOrder B
inst✝⁵ : OrderBot B
q : R[A]
D : A → B
inst✝⁴ : AddZeroClass A
inst✝³ : Add B
inst✝² : AddLeftStrictMono B
inst✝¹ : AddRightStrictMono B
inst✝ : NoZeroDivisors R
hD : Function.Injective D
hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2
⊢ leadingCoeff D 0 = 0
Module: Mathlib.Algebra.Polynomial.Eval.Coeff

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

Tactic:
by
  induction p using Polynomial.induction_on' with
  | add p q hp hq => simp only [hp, hq, Polynomial.map_add, map_add, eval_add]
  | monomial n r => simp only [one_pow, mul_one, eval_monomial, map_monomial]

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

Goal state before:
pp: R : Type u
a b : R
m✝ n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Nontrivial R
m n : ℕ
h : (fun i ↦ (monomial i) 1) m = (fun i ↦ (monomial i) 1) n
⊢ m = n

Tactic:
by simpa [monomial_one_eq_iff] using h

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

Goal state before:
pp: S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ∑ i ∈ range d, ↑d.succ * (↑(d.choose i) * y ^ i) =
    ∑ k ∈ range d, ↑((d + 1).choose (k + 1)) * (↑(k + 1) * y ^ (k + 1 - 1)) + ↑((d + 1).choose 0) * (0 * y ^ (0 - 1))

Tactic:
zero_mul,

Goal state after:
S : Type v
inst✝ : CommRing S
d : ℕ
y : S
cast_succ : ↑d + 1 = ↑d.succ
⊢ ∑ i ∈ range d, ↑d.succ * (↑(d.choose i) * y ^ i) =
    ∑ k ∈ range d, ↑((d + 1).choose (k + 1)) * (↑(k + 1) * y ^ (k + 1 - 1)) + ↑((d + 1).choose 0) * 0
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: case mp
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : Zero α
inst✝¹ : LE α
inst✝ : Std.Refl fun x1 x2 ↦ x1 ≤ x2
f : ι ↪ κ
g₁ g₂ : ι →₀ α
⊢ embDomain f g₁ ≤ embDomain f g₂ → g₁ ≤ g₂

Tactic:
rw [Finsupp.le_def]
    intro h' x
    simpa [Finsupp.embDomain_apply] using h' (f x)

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝¹ : AddCommMonoid α
inst✝ : Preorder α
f : ι → κ
h : Function.Injective f
g₁ g₂ : ι →₀ α
⊢ mapDomain f g₁ < mapDomain f g₂ ↔ g₁ < g₂

Tactic:
simpa [Finsupp.embDomain_eq_mapDomain] using Finsupp.embDomain_lt_embDomain_iff_lt ⟨f, h⟩ g₁ g₂

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

Goal state before:
pp: R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type u_3
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : B →ₐ[R] C
g : A →ₐ[R] B
⊢ (mapAlgHom f).comp (mapAlgHom g) = mapAlgHom (f.comp g)

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u
A : Type z
B : Type u_2
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Semiring B
inst✝³ : Algebra R A
inst✝² : Algebra R B
C : Type u_3
inst✝¹ : Semiring C
inst✝ : Algebra R C
f : A ≃ₐ[R] B
g : B ≃ₐ[R] C
⊢ (mapAlgEquiv f).trans (mapAlgEquiv g) = mapAlgEquiv (f.trans g)

Tactic:
ext
  simp

Goal state after:
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)) = ((mapAlg A C) p).coeff 0

Tactic:
mapAlg_eq_map,

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)) = (map (algebraMap A C) p).coeff 0
Module: Mathlib.Data.Finsupp.Order

Goal state before:
pp: ι : Type u_1
α : Type u_3
inst✝³ : AddCommMonoid α
inst✝² : LinearOrder α
inst✝¹ : IsBotZeroClass α
inst✝ : DecidableEq ι
f g : ι →₀ α
⊢ (f ⊓ g).support = f.support ∩ g.support

Tactic:
ext
  simp

Goal state after:
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
⊢ (f ⊓ g).support = f.support ∩ g.support

Tactic:
ext
  simp

Goal state after:
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:
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
l : ℕ
IH : ∀ m > l, P.coeff m • Q = 0
hl : (P.coeff l • Q).natDegree = Q.natDegree
m : ℕ := Q.natDegree
i j : ℕ
hij : i + j = l + m
H : i = l → ¬j = m
hi : i < l
⊢ m < j

Tactic:
lia

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

Goal state before:
pp: case inr.inl
R : Type u
inst✝ : CommSemiring R
P : R[X]
h : ∀ (r : R), r • P = 0 → r = 0
Q : R[X]
hQ : P * Q = 0
m : ℕ := Q.natDegree
i j : ℕ
IH : ∀ m > i, P.coeff m • Q = 0
hl : (P.coeff i • Q).natDegree = Q.natDegree
hij : i + j = i + m
H : i = i → ¬j = m
⊢ P.coeff i * Q.coeff j = 0

Tactic:
lia

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

Goal state before:
pp: R : Type u
σ : Type u_1
a : R
inst✝ : CommSemiring R
⊢ C a = a • 1

Tactic:
← C_mul',

Goal state after:
R : Type u
σ : Type u_1
a : R
inst✝ : CommSemiring R
⊢ C a = C a * 1
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₁
φ : S₁ →+* S₂
⊢ φ.comp (eval₂Hom f g) = eval₂Hom (φ.comp f) fun i ↦ φ (g i)

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₂
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ eval₂ φ g ((map f) p) = eval₂ (φ.comp f) g p

Tactic:
← eval_map,

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₂
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ (eval g) ((map φ) ((map f) p)) = eval₂ (φ.comp f) g p
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₂
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ (eval g) ((map φ) ((map f) p)) = eval₂ (φ.comp f) g p

Tactic:
← eval_map,

Goal state after:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S₁
inst✝ : CommSemiring S₂
f : R →+* S₁
g : σ → S₂
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ (eval g) ((map φ) ((map f) p)) = (eval g) ((map (φ.comp f)) p)
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
⊢ constantCoeff.comp (map f) = f.comp constantCoeff

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ Multiset.count n f.degrees = f.support.sup fun m ↦ m n

Tactic:
degrees,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f : MvPolynomial σ R
⊢ Multiset.count n (f.support.sup fun s ↦ toMultiset s) = f.support.sup fun m ↦ m n
Module: Mathlib.Algebra.MvPolynomial.CommRing

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

Tactic:
degrees,

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
p : MvPolynomial σ R
⊢ ((-p).support.sup fun s ↦ toMultiset s) = p.degrees
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
j : σ
f : MvPolynomial σ R
⊢ degreeOf j (f * X j) ≤ degreeOf j f + 1

Tactic:
by
  classical
  simp only [degreeOf]
  apply (Multiset.count_le_of_le j degrees_mul_le).trans
  simp only [Multiset.count_add, add_le_add_iff_left]
  convert! Multiset.count_le_of_le j <| degrees_X' j
  rw [Multiset.count_singleton_self]

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

Goal state before:
pp: R : Type u
S₂ : Type w
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₂
f : R →+* S₂
⊢ eval₂Hom f 0 = f.comp constantCoeff

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd : d ∈ f.support
⊢ d i = 0 → d i ≤ f.totalDegree

Tactic:
lia

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
f : MvPolynomial σ R
i : σ
d : σ →₀ ℕ
hd : d ∈ f.support
h : d i ≠ 0
⊢ ∀ i ∈ d.support, 0 ≤ d i

Tactic:
lia

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

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
⊢ f₁ = eval₂Hom (f₁.comp C) (⇑f₁ ∘ X)

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u
S : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : MvPolynomial σ R →+* S
p₁ p₂ : MvPolynomial σ R
hC : f₁.comp C = f₂.comp C
hv : ∀ i ∈ p₁.vars, i ∈ p₂.vars → f₁ (X i) = f₂ (X i)
hp : p₁ = p₂
⊢ eval₂Hom (f₂.comp C) (⇑f₂ ∘ X) = f₂

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.trailingDegree = ↑n
⊢ p.natTrailingDegree = n

Tactic:
by
  simp [natTrailingDegree, h]

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

Goal state before:
pp: R : Type u_2
inst✝ : Ring R
f : R[X]
⊢ f - C f.leadingCoeff * X ^ f.natDegree = f.eraseLead

Tactic:
by
  rw [C_mul_X_pow_eq_monomial, self_sub_monomial_natDegree_leadingCoeff]

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

Goal state before:
pp: case pos
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
H : ∃ x ∈ s, f x ≠ 0
⊢ (s.sum f).natDegree = s.sup fun i ↦ (f i).natDegree

pp: case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
H : ∀ x ∈ s, f x = 0
⊢ (s.sum f).natDegree = s.sup fun i ↦ (f i).natDegree

Tactic:
· obtain ⟨x, hx, hx'⟩ := H
    have hs : s.Nonempty := ⟨x, hx⟩
    refine natDegree_eq_of_degree_eq_some ?_
    rw [degree_sum_eq_of_disjoint]
    · rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs,
        Nat.cast_withBot, Finset.coe_sup' hs, ←
        Finset.sup'_eq_sup hs]
      refine le_antisymm ?_ ?_
      · rw [Finset.sup'_le_iff]
        intro b hb
        by_cases hb' : f b = 0
        · simpa [hb'] using! hs
        rw [degree_eq_natDegree hb', Nat.cast_withBot]
        exact Finset.le_sup' (fun i : S => (natDegree (f i) : WithBot ℕ)) hb
      · rw [Finset.sup'_le_iff]
        intro b hb
        simp only [Finset.le_sup'_iff, Function.comp_apply]
        by_cases hb' : f b = 0
        · refine ⟨x, hx, ?_⟩
          contrapose! hx'
          simpa [← Nat.cast_withBot, hb', degree_eq_bot] using! hx'
        exact ⟨b, hb, (degree_eq_natDegree hb').ge⟩
    · exact h.imp fun x y hxy hxy' => hxy (natDegree_eq_of_degree_eq hxy')

Goal state after:
case neg
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
s : Finset S
h : {i | i ∈ s ∧ f i ≠ 0}.Pairwise (Ne on natDegree ∘ f)
H : ∀ x ∈ s, f x = 0
⊢ (s.sum f).natDegree = s.sup fun i ↦ (f i).natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: case inl
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
h : p.natDegree = 0
⊢ (map f p).natDegree = 0 ↔ True

Tactic:
iff_true,

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

Goal state before:
pp: 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).natDegree = n

Tactic:
lia

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : f = 0
⊢ reflect (N + O) (0 * g) = 0 * reflect O g

Tactic:
zero_mul,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : f = 0
⊢ reflect (N + O) 0 = 0 * reflect O g
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : f = 0
⊢ reflect (N + O) 0 = 0 * reflect O g

Tactic:
zero_mul,

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
cf : ℕ
hcf : ∀ (f : R[X]), #f.support ≤ cf.succ → f.natDegree ≤ N → reflect (N + O) (f * g) = reflect N f * reflect O g
f : R[X]
Cf : #f.support ≤ (cf + 1).succ
Nf : f.natDegree ≤ N
f0 : f = 0
⊢ reflect (N + O) 0 = 0
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u
S₁ : Type v
S₂ : Type w
inst✝ : CommSemiring R
r : R
⊢ (sumRingEquiv R S₁ S₂).symm (C (C r)) = C r

Tactic:
simp [← sumRingEquiv_C]

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

Goal state before:
pp: 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
hn₂ : n = 0
x✝ : P.natDegree = 0
⊢ x = 0

Tactic:
lia

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

Goal state before:
pp: 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
n✝ : ℕ
hn₂ : n = n✝ + 1
⊢ ¬P.natDegree = n✝

Tactic:
lia

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

Goal state before:
pp: 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
n✝ : ℕ
hn₂ : n = n✝ + 1
⊢ ¬P.natDegree = n✝ + 1

Tactic:
lia

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

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.natDegree = 0
⊢ f.coeff ((revAt f.natDegree) 1) = 0

Tactic:
have : coeff f 1 = 0 := coeff_eq_zero_of_natDegree_lt (by simp only [hf, zero_lt_one])

Goal state after:
case pos
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.natDegree = 0
this : f.coeff 1 = 0
⊢ f.coeff ((revAt f.natDegree) 1) = 0
Module: Mathlib.Algebra.Polynomial.Reverse

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

Tactic:
rw [revAt_le]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : ¬f.natDegree = 0
⊢ 1 ≤ f.natDegree
Module: Mathlib.Algebra.MvPolynomial.Equiv

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
i : σ
⊢ toMvPolynomial i = (MvPolynomial.rename fun x ↦ i).comp ↑(MvPolynomial.uniqueAlgEquiv R Unit).symm

Tactic:
ext
  simp

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

Goal state before:
pp: R : Type u_1
σ : Type u_3
inst✝ : CommSemiring R
f : σ → R
i : σ
⊢ (eval f).comp ↑(toMvPolynomial i) = evalRingHom (f i)

Tactic:
ext <;> simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
σ : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : σ → S
i : σ
⊢ (aeval f).comp (toMvPolynomial i) = Polynomial.aeval (f i)

Tactic:
ext
  simp

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

Goal state before:
pp: R : Type u_1
σ : Type u_3
τ : Type u_4
inst✝ : CommSemiring R
f : σ → τ
a : σ
⊢ (rename f).comp (toMvPolynomial a) = toMvPolynomial (f a)

Tactic:
ext
  simp

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

Goal state before:
pp: case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
⊢ 0 * x + y ^ 0 = (x + y) ^ 0

Tactic:
zero_mul,

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
x y : R
h : Commute x y
f : ℕ → ℕ → R := fun m i ↦ (x + y) ^ i * y ^ (m - 1 - i)
⊢ 0 + y ^ 0 = (x + y) ^ 0
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case a.e_a.e_a
R : Type u_1
inst✝⁶ : CommSemiring R
inst✝⁵ : PartialOrder R
inst✝⁴ : AddLeftReflectLE R
inst✝³ : AddLeftMono R
inst✝² : ExistsAddOfLE R
inst✝¹ : Sub R
inst✝ : OrderedSub R
x y : R
hxy : x ≤ y
n x✝ : ℕ
a✝ : x✝ < n
⊢ n - 1 - (n - 1 - x✝) = x✝

Tactic:
lia

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

Goal state before:
pp: case e_a.e_a
R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
m n : ℕ
hmn : m ≤ n
j : ℕ
j_in : j < m
⊢ n - 1 - j = n - m + (m - 1 - j)

Tactic:
lia

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
x : R
⊢ ∀ (i : ℕ), 0 * x ^ i = 0

Tactic:
zero_mul,

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
p : R[X]
hp : p ∈ degreeLT R n
x : R
⊢ ∀ (i : ℕ), True
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
x y : R
h : Commute x y
n i : ℕ
hi : i < n
⊢ n - 1 - i + 1 = n - i

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : CommSemiring C
inst✝⁹ : CommSemiring D
inst✝⁸ : CommSemiring E
inst✝⁷ : CommSemiring F
inst✝⁶ : Algebra C D
inst✝⁵ : Algebra C E
inst✝⁴ : Algebra C F
inst✝³ : Algebra D F
inst✝² : Algebra E F
inst✝¹ : IsScalarTower C D F
inst✝ : IsScalarTower C E F
S : Set D
T : Set E
hS : adjoin C S = ⊤
hT : adjoin C T = ⊤
⊢ Subalgebra.restrictScalars C (adjoin (↥(adjoin C (⇑↑(IsScalarTower.toAlgHom C E F) '' T))) (⇑(algebraMap D F) '' S)) =
    Subalgebra.restrictScalars C (adjoin (↥(adjoin C (⇑↑(IsScalarTower.toAlgHom C D F) '' S))) (⇑(algebraMap E F) '' T))

Tactic:
IsScalarTower.coe_toAlgHom,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : CommSemiring C
inst✝⁹ : CommSemiring D
inst✝⁸ : CommSemiring E
inst✝⁷ : CommSemiring F
inst✝⁶ : Algebra C D
inst✝⁵ : Algebra C E
inst✝⁴ : Algebra C F
inst✝³ : Algebra D F
inst✝² : Algebra E F
inst✝¹ : IsScalarTower C D F
inst✝ : IsScalarTower C E F
S : Set D
T : Set E
hS : adjoin C S = ⊤
hT : adjoin C T = ⊤
⊢ Subalgebra.restrictScalars C (adjoin (↥(adjoin C (⇑(algebraMap E F) '' T))) (⇑(algebraMap D F) '' S)) =
    Subalgebra.restrictScalars C (adjoin (↥(adjoin C (⇑↑(IsScalarTower.toAlgHom C D F) '' S))) (⇑(algebraMap E F) '' T))
Module: Mathlib.RingTheory.Adjoin.Tower

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : CommSemiring C
inst✝⁹ : CommSemiring D
inst✝⁸ : CommSemiring E
inst✝⁷ : CommSemiring F
inst✝⁶ : Algebra C D
inst✝⁵ : Algebra C E
inst✝⁴ : Algebra C F
inst✝³ : Algebra D F
inst✝² : Algebra E F
inst✝¹ : IsScalarTower C D F
inst✝ : IsScalarTower C E F
S : Set D
T : Set E
hS : adjoin C S = ⊤
hT : adjoin C T = ⊤
⊢ Subalgebra.restrictScalars C (adjoin (↥(adjoin C (⇑(algebraMap E F) '' T))) (⇑(algebraMap D F) '' S)) =
    Subalgebra.restrictScalars C (adjoin (↥(adjoin C (⇑↑(IsScalarTower.toAlgHom C D F) '' S))) (⇑(algebraMap E F) '' T))

Tactic:
IsScalarTower.coe_toAlgHom,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
F : Type u_4
inst✝¹⁰ : CommSemiring C
inst✝⁹ : CommSemiring D
inst✝⁸ : CommSemiring E
inst✝⁷ : CommSemiring F
inst✝⁶ : Algebra C D
inst✝⁵ : Algebra C E
inst✝⁴ : Algebra C F
inst✝³ : Algebra D F
inst✝² : Algebra E F
inst✝¹ : IsScalarTower C D F
inst✝ : IsScalarTower C E F
S : Set D
T : Set E
hS : adjoin C S = ⊤
hT : adjoin C T = ⊤
⊢ Subalgebra.restrictScalars C (adjoin (↥(adjoin C (⇑(algebraMap E F) '' T))) (⇑(algebraMap D F) '' S)) =
    Subalgebra.restrictScalars C (adjoin (↥(adjoin C (⇑(algebraMap D F) '' S))) (⇑(algebraMap E F) '' T))
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
n : ℕ
⊢ 1 ≤ m

Tactic:
lia

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

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
⊢ False

Tactic:
rcases span_le_degreeLE_of_finite hs with ⟨n, hn⟩

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s : Set R[X]
hs : s.Finite
contra : Submodule.span R s = ⊤
n : ℕ
hn : Submodule.span R s ≤ degreeLE R ↑n
⊢ False
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
a✝ : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ ((range n).sup fun b ↦ (P ^ b).degree) < (P ^ n).degree

Tactic:
rw [Finset.sup_lt_iff]

Goal state after:
R : Type u
inst✝ : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
a✝ : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ ∀ b ∈ range n, (P ^ b).degree < (P ^ n).degree

R : Type u
inst✝ : Semiring R
P : R[X]
hP : P.Monic
hdeg : 0 < P.natDegree
a✝ : Nontrivial R
n : ℕ
hn : n.succ ≠ 0
⊢ ⊥ < (P ^ n).degree
Module: Mathlib.RingTheory.Polynomial.Basic

Goal state before:
pp: R : Type u
inst✝ : Ring R
p : R[X]
n : ℕ
⊢ ↑(p.restriction.coeff n) = p.coeff n

Tactic:
by
  classical
  simp only [restriction, coeff_monomial, finsetSum_coeff, mem_support_iff, Finset.sum_ite_eq',
    Ne, ite_not]
  split_ifs with h
  · rw [h]
    rfl
  · rfl

Goal state after: