mathlib-initiative/mathlib-tactics huggingface dataset:
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:
rw [← neg_eq_zero, ← Int.cast_neg, ← Int.dvd_neg]
    lift -a to ℕ using Int.neg_nonneg.mpr (le_of_lt h) with b
    rw [Int.cast_natCast, CharP.cast_eq_zero_iff R p, Int.natCast_dvd_natCast]

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

Goal state before:
pp: m n : ℕ
h : n = 1 ∨ m ≤ n.minFac
p : ℕ
pp : Prime p
d : p ∣ n
⊢ n = 1 → m ≤ p

Tactic:
rintro rfl; cases pp.not_dvd_one d

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
n : ℤ
⊢ (↑n).natDegree = 0

Tactic:
rw [← C_eq_intCast, natDegree_C]

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

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
hp : p ≠ 0
h : p.degree < q.degree
⊢ p.natDegree < q.natDegree

Tactic:
have hq : q ≠ 0 := ne_zero_of_degree_gt h
    rwa [degree_eq_natDegree hp, degree_eq_natDegree hq, Nat.cast_lt] at h

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
⊢ (p + C a).natDegree = p.natDegree

Tactic:
by_cases! hpd : p.degree ≤ 0

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : p.degree ≤ 0
⊢ (p + C a).natDegree = p.natDegree

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
a : R
hp : p ≠ 0
hpd : 0 < p.degree
⊢ (p + C a).natDegree = p.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
⊢ p.natDegree = q.natDegree

Tactic:
by_cases h₁ : natDegree p = 0

Goal state after:
case pos
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : p.natDegree = 0
⊢ p.natDegree = q.natDegree

case neg
R : Type u
inst✝ : Semiring R
p q : R[X]
H : (p + q).natDegree = 0
h₁ : ¬p.natDegree = 0
⊢ p.natDegree = q.natDegree
Module: Mathlib.Algebra.Polynomial.Degree.Operations

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

Tactic:
suffices natDegree q < j by
              rw [coeff_eq_zero_of_degree_lt
                  (lt_of_le_of_lt degree_le_natDegree (WithBot.coe_lt_coe.2 this)),
                mul_zero]
            by_contra! H'
            exact
              ne_of_lt (Nat.lt_of_lt_of_le (Nat.add_lt_add_right H j) (Nat.add_le_add_left H' _))
                h₁

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

Goal state before:
pp: R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 2 + (C b * X + C c)).degree = 2

Tactic:
degree_add_eq_left_of_degree_lt <| degree_linear_lt_degree_C_mul_X_sq ha,

Goal state after:
R : Type u
a b c : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X ^ 2).degree = 2
Module: Mathlib.Algebra.MonoidAlgebra.Degree

Goal state before:
pp: case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j✝ : ι
hj✝ : j✝ ∈ s
hne✝ : f j✝ ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
⊢ ∑ i ∈ s, f i ≠ 0

Tactic:
apply ne_zero_of_supDegree_ne_bot (D := D)

Goal state after:
case neg
R : Type u_1
A : Type u_3
B : Type u_5
inst✝³ : Semiring R
inst✝² : LinearOrder B
inst✝¹ : OrderBot B
D : A → B
ι : Type u_7
s : Finset ι
f : ι → R[A]
inst✝ : AddZeroClass A
hd : Set.InjOn (supDegree D ∘ f) ↑s
j✝ : ι
hj✝ : j✝ ∈ s
hne✝ : f j✝ ≠ 0
i : ι
hi : i ∈ s
he : s.sup (supDegree D ∘ f) = (supDegree D ∘ f) i
j : ι
hj : j ∈ s
hne : j ≠ i
⊢ supDegree D (∑ i ∈ s, f i) ≠ ⊥
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

pp: case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : ¬p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

Tactic:
· rw [hp1, zero_mul]
      by_cases hp2 : p ^ i = 0
      · rw [hp2, zero_mul, coeff_zero]
      · apply coeff_eq_zero_of_natDegree_lt
        have h1 : (p ^ i).natDegree < i * p.natDegree := by
          refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
          rw [← h, hp1] at hi
          exact leadingCoeff_eq_zero.mp hi
        calc
          (p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree := natDegree_mul_le
          _ < i * p.natDegree + p.natDegree := by gcongr

Goal state after:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : ¬p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff
Module: Mathlib.Algebra.Polynomial.Degree.Operations

Goal state before:
pp: R : Type u
inst✝ : Ring R
p q : R[X]
h : p.degree < q.degree
⊢ (p - q).leadingCoeff = -q.leadingCoeff

Tactic:
by
  rw [← q.degree_neg] at h
  rw [sub_eq_add_neg, leadingCoeff_add_of_degree_lt h, leadingCoeff_neg]

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

Goal state before:
pp: case neg
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
hn : f.support ⊆ {n}
i : ℕ
hi : ¬i = n
⊢ f.coeff i = ((monomial n) (f.coeff n)).coeff i

Tactic:
· have : f.coeff i = 0 := by
        rw [← notMem_support_iff]
        exact fun hi' => hi (Finset.mem_singleton.1 (hn hi'))
      simp [this, Ne.symm hi, coeff_monomial]

Goal state after:
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 = 0

Tactic:
suffices P.coeff l * Q.leadingCoeff = 0 by
    rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]

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
⊢ P.coeff l * Q.leadingCoeff = 0
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
S : Subalgebra R (MvPolynomial σ R) := Algebra.adjoin R (range X)
p : MvPolynomial σ R
⊢ p ∈ S

Tactic:
induction p using MvPolynomial.induction_on with

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ (eval₂Hom (RingHom.id R) (⇑(eval₂Hom (RingHom.id R) g) ∘ f)) p =
    eval₂ ((eval₂Hom (RingHom.id R) g).comp C) (⇑(eval₂Hom (RingHom.id R) g) ∘ f) p

Tactic:
simp only [coe_eval₂Hom]

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
τ : Type u_2
f : σ → MvPolynomial τ R
g : τ → R
p : MvPolynomial σ R
⊢ eval₂ (RingHom.id R) (eval₂ (RingHom.id R) g ∘ f) p =
    eval₂ ((eval₂Hom (RingHom.id R) g).comp C) (eval₂ (RingHom.id R) g ∘ f) p
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
q : S₁ →+* S₂
g : σ → S₁
p : MvPolynomial σ S₁
⊢ q ((eval g) p) = eval₂ q (⇑q ∘ g) p

Tactic:
← eval₂_id,

Goal state after:
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring S₁
S₂ : Type u_2
inst✝ : CommSemiring S₂
q : S₁ →+* S₂
g : σ → S₁
p : MvPolynomial σ S₁
⊢ q (eval₂ (RingHom.id S₁) g p) = eval₂ q (⇑q ∘ g) p
Module: Mathlib.Algebra.MvPolynomial.Basic

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
d : σ →₀ ℕ
r : R
⊢ constantCoeff ((monomial d) r) = if d = 0 then r else 0

Tactic:
by
  rw [constantCoeff_eq, coeff_monomial]

Goal state after:
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₁
p : MvPolynomial σ R
⊢ ∀ (m : σ →₀ ℕ), coeff m ((map f) p) = f (coeff m p)

Tactic:
classical
  apply MvPolynomial.induction_on p <;> clear p
  · intro r m
    simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]
  · intro p q hp hq m
    simp only [hp, hq, (map f).map_add, coeff_add, f.map_add]
  · intro p i hp m
    simp only [(map f).map_mul, map_X, hp, coeff_mul_X', f.map_zero, apply_ite f]

Goal state after:
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:
rw [mem_degrees]; refine ⟨d, ?_, hj⟩; assumption

Goal state after:
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₁
p : MvPolynomial σ R
x : σ →₀ ℕ
hx : coeff x p = 0
⊢ coeff x ((map f) p) = 0

Tactic:
rw [coeff_map, hx, map_zero]

Goal state after:
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:
rw [mem_degrees]; refine ⟨d, ?_, hj⟩; assumption

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

Goal state before:
pp: σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.coeff.support
h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = (mapDomain.addMonoidHom f) u → coeff u_1 φ = 0
⊢ False

Tactic:
specialize h u rfl

Goal state after:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.coeff.support
h : coeff u φ = 0
⊢ False
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: R : Type u
σ : Type u_1
τ : Type u_2
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
⊢ ((rename f) φ).degrees ⊆ Multiset.map f φ.degrees

Tactic:
intro i
  rw [mem_degrees, Multiset.mem_map]
  rintro ⟨d, hd, hi⟩
  obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
  simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
  rw [sum_apply, Finsupp.sum] at hi
  contrapose! hi
  rw [Finset.sum_eq_zero]
  intro j hj
  simp only [mem_degrees] at hi
  specialize hi j ⟨x, hx, hj⟩
  rw [Finsupp.single_apply, if_neg hi]

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

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

Tactic:
rw [Finset.image_union, Finset.union_subset_iff]

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

Goal state before:
pp: 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
h2 : x ∈ {d'}
⊢ x ∈ {d'}

Tactic:
rwa [Finset.mem_singleton] at h2 ⊢

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

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

Tactic:
degrees_neg

Goal state after:
R : Type u
σ : Type u_1
inst✝ : CommRing R
i : σ
p : MvPolynomial σ R
⊢ Multiset.count i p.degrees = Multiset.count i p.degrees
Module: Mathlib.Algebra.MvPolynomial.CommRing

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommRing R
a b : MvPolynomial σ R
⊢ max a.totalDegree (-b).totalDegree = max a.totalDegree b.totalDegree

Tactic:
by rw [totalDegree_neg]

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
c : R
⊢ degreeOf i (p * C c) ≤ degreeOf i p

Tactic:
unfold degreeOf
  convert! Multiset.count_le_of_le i degrees_mul_le
  simp only [degrees_C, add_zero]

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

Goal state before:
pp: case pos
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : p = 0
⊢ p.totalDegree ≤ (p + q).totalDegree

pp: case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
⊢ p.totalDegree ≤ (p + q).totalDegree

Tactic:
· simp [hp]

Goal state after:
case neg
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p q : MvPolynomial σ R
h : q.totalDegree < p.totalDegree
hp : ¬p = 0
⊢ p.totalDegree ≤ (p + q).totalDegree
Module: Mathlib.Algebra.MvPolynomial.Degrees

Goal state before:
pp: case mp
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p.totalDegree = 0
⊢ p = C (coeff 0 p)

pp: case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p = C (coeff 0 p)
⊢ p.totalDegree = 0

Tactic:
· ext m; classical rw [coeff_C]; split_ifs with hm; · rw [← hm]
    apply coeff_eq_zero_of_totalDegree_lt; rw [h]
    exact Finset.sum_pos (fun i hi ↦ Nat.pos_of_ne_zero <| Finsupp.mem_support_iff.mp hi)
      (Finsupp.support_nonempty_iff.mpr <| Ne.symm hm)

Goal state after:
case mpr
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
h : p = C (coeff 0 p)
⊢ p.totalDegree = 0
Module: Mathlib.Algebra.MvPolynomial.Eval

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
S : Type u_2
T : Type u_3
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra R S
inst✝³ : CommSemiring T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
σ : Type u_4
τ : Type u_5
p : MvPolynomial (σ ⊕ τ) R
f : τ → S
g : σ → T
⊢ (aeval (Sum.elim g (⇑(algebraMap S T) ∘ f))) p = (aeval g) ((aeval (Sum.elim X (⇑C ∘ f))) p)

Tactic:
induction p using MvPolynomial.induction_on with

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

Goal state before:
pp: R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
q : MvPolynomial σ R
s : Set σ
hs : ↑q.vars ⊆ s
inst✝ : (i : σ) → Decidable (i ∈ s)
⊢ (aeval fun i ↦ if i ∈ s then X i else 0) q = q

Tactic:
rw [MvPolynomial.as_sum q, MvPolynomial.aeval_sum]
  refine Finset.sum_congr rfl fun u hu ↦ ?_
  rw [MvPolynomial.aeval_monomial, MvPolynomial.monomial_eq]
  congr 1
  exact Finsupp.prod_congr (fun i hi ↦ by simp [hs ((mem_vars_iff_mem_support _).mpr ⟨u, hu, hi⟩)])

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
⊢ (↑n).toNat = n

Tactic:
ENat.toNat_natCast

Goal state after:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
h : p.trailingDegree = ↑n
⊢ n = n
Module: Mathlib.Algebra.Polynomial.Degree.Lemmas

Goal state before:
pp: R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
⊢ (p + q).natDegree ≤ n ↔ p.natDegree ≤ n

Tactic:
refine ⟨fun h => ?_, fun h => natDegree_add_le_of_degree_le h qn⟩

Goal state after:
R : Type u
inst✝ : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
⊢ p.natDegree ≤ n
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ f.eraseLead.coeff f.natDegree = 0

Tactic:
by simp [eraseLead_coeff]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
⊢ #f.eraseLead.support + 1 = c

Tactic:
cases h₁ : c

Goal state after:
case zero
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
h₁ : c = 0
⊢ #f.eraseLead.support + 1 = 0

case succ
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f ≠ 0
c : ℕ := #f.support
hc : c = #f.support
n✝ : ℕ
h₁ : c = n✝ + 1
⊢ #f.eraseLead.support + 1 = n✝ + 1
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead ≠ 0
h₂ : ¬0 < f.natDegree
⊢ False

Tactic:
eq_C_of_natDegree_eq_zero (Nat.eq_zero_of_not_pos h₂)

Goal state after:
R : Type u_1
inst✝ : Semiring R
f : R[X]
h : (C (f.coeff 0)).eraseLead ≠ 0
h₂ : ¬0 < f.natDegree
⊢ False
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
f : R[X]
h : f.eraseLead ≠ 0
⊢ 0 < f.natDegree

Tactic:
by
  by_contra h₂
  rw [eq_C_of_natDegree_eq_zero (Nat.eq_zero_of_not_pos h₂)] at h
  simp at h

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

Goal state before:
pp: case pos
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
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead

pp: case neg
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
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead

Tactic:
· simp [hp]

Goal state after:
case neg
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
⊢ ((X - C x) * P).eraseLead.eraseLead = (X - C x) * P.eraseLead
Module: Mathlib.Algebra.Polynomial.Reverse

Goal state before:
pp: case succ
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
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g

Tactic:
| succ cf hcf =>

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

Goal state before:
pp: case pos
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp : p = 0
⊢ (p * C p.leadingCoeff⁻¹).degree = p.degree

pp: case neg
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp : ¬p = 0
⊢ (p * C p.leadingCoeff⁻¹).degree = p.degree

Tactic:
· simp [hp]

Goal state after:
case neg
K : Type u_1
inst✝ : DivisionRing K
p : K[X]
hp : ¬p = 0
⊢ (p * C p.leadingCoeff⁻¹).degree = p.degree
Module: Mathlib.Algebra.Polynomial.Reverse

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

Tactic:
reverse_zero,

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

Goal state before:
pp: R : Type u
S₁ : Type v
inst✝ : CommSemiring R
r : R
⊢ (optionEquivRight R S₁) (C r) = C (Polynomial.C r)

Tactic:
simp only [optionEquivRight_apply, aeval_C, algebraMap_apply, Polynomial.algebraMap_eq]

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

Goal state before:
pp: case pos
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
⊢ reverse 0 = f.reverse * reverse 0

Tactic:
reverse_zero,

Goal state after:
case pos
R : Type u_2
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
f g : R[X]
f0 : ¬f = 0
g0 : g = 0
⊢ 0 = f.reverse * 0
Module: Mathlib.Algebra.Polynomial.EraseLead

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ (φ f + φ g).natDegree = fu g.natDegree

Tactic:
natDegree_add_eq_right_of_natDegree_lt,

Goal state after:
case pos
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ (φ g).natDegree = fu g.natDegree

case pos
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
F : Type u_3
inst✝² : Semiring S
inst✝¹ : FunLike F R[X] S[X]
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
k : ℕ
fu : ℕ → ℕ
fu0 : ∀ {n : ℕ}, n ≤ k → fu n = 0
fc : ∀ {n m : ℕ}, k ≤ n → n < m → fu n < fu m
φ_k : ∀ {f : R[X]}, f.natDegree < k → φ f = 0
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → (φ ((monomial n) c)).natDegree = fu n
f g : R[X]
fg : f.natDegree < g.natDegree
a✝ : g.natDegree ≤ p.natDegree
fk : (φ f).natDegree = fu f.natDegree
gk : (φ g).natDegree = fu g.natDegree
FG : k ≤ f.natDegree
⊢ (φ f).natDegree < (φ g).natDegree
Module: Mathlib.Algebra.Polynomial.BigOperators

Goal state before:
pp: case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : (Multiset.map leadingCoeff (a ::ₘ t)).prod ≠ 0
⊢ (a ::ₘ t).prod.leadingCoeff = (Multiset.map leadingCoeff (a ::ₘ t)).prod

Tactic:
simp only [Multiset.map_cons, Multiset.prod_cons] at h ⊢

Goal state after:
case cons
R : Type u
inst✝ : CommSemiring R
t✝ : Multiset R[X]
a : R[X]
t : Multiset R[X]
ih : (Multiset.map leadingCoeff t).prod ≠ 0 → t.prod.leadingCoeff = (Multiset.map leadingCoeff t).prod
h : a.leadingCoeff * (Multiset.map leadingCoeff t).prod ≠ 0
⊢ (a * t.prod).leadingCoeff = a.leadingCoeff * (Multiset.map leadingCoeff t).prod
Module: Mathlib.Algebra.Ring.GeomSum

Goal state before:
pp: case succ
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)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
⊢ (∑ i ∈ range (n + 1), f (n + 1) i) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n

Tactic:
sum_range_succ_comm,

Goal state after:
case succ
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)
n : ℕ
ih : (∑ i ∈ range n, f n i) * x + y ^ n = (x + y) ^ n
f_last : f (n + 1) n = (x + y) ^ n
f_succ : ∀ i ∈ range n, f (n + 1) i = y * f n i
⊢ (f (n + 1) n + ∑ x ∈ range n, f (n + 1) x) * x + y ^ (n + 1) = x * (x + y) ^ n + y * (x + y) ^ n