awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
⊢ (p + q).natDegree ≤ n ↔ p.natDegree ≤ n
have refine : ∀ (h : (p + q).natDegree ≤ n), p.natDegree ≤ n
Tactic: refine ⟨fun h => ?_, fun h => natDegree_add_le_of_degree_le h qn⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
⊢ p.natDegree ≤ n
have refine : ∀ (m : ℕ) (hm : n < m), p.coeff m = 0
Tactic: refine natDegree_le_iff_coeff_eq_zero.mpr fun m hm => ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
⊢ p.coeff m = 0
have h₁ : p.coeff m = (p + q).coeff m
Tactic: convert! natDegree_le_iff_coeff_eq_zero.mp h m hm using 1
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
⊢ p.coeff m = (p + q).coeff m
have h₁ : p.coeff m = p.coeff m + q.coeff m
Tactic: rw [coeff_add, natDegree_le_iff_coeff_eq_zero.mp qn _ hm, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
h₁ : p.coeff m = p.coeff m + q.coeff m
⊢ p.coeff m = (p + q).coeff m
have h₂ : p.coeff m = p.coeff m + 0
Tactic: rw [coeff_add, natDegree_le_iff_coeff_eq_zero.mp qn _ hm, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
qn : q.natDegree ≤ n
h : (p + q).natDegree ≤ n
m : ℕ
hm : n < m
h₁ : p.coeff m = p.coeff m + q.coeff m
h₂ : p.coeff m = p.coeff m + 0
⊢ p.coeff m = (p + q).coeff m
have h₃ : p.coeff m = p.coeff m
Tactic: rw [coeff_add, natDegree_le_iff_coeff_eq_zero.mp qn _ hm, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
inst : Semiring R
n : ℕ
p q : R[X]
pn : p.natDegree ≤ n
⊢ (p + q).natDegree ≤ n ↔ q.natDegree ≤ n
have rw : (q + p).natDegree ≤ n ↔ q.natDegree ≤ n
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ai : R
au : ai * a = 1
⊢ p.natDegree = (1 * p).natDegree
have nth_rw : (1 * p).natDegree = (1 * p).natDegree
Tactic: nth_rw 1 [← one_mul p]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ai : R
au : ai * a = 1
⊢ (1 * p).natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
have rw : ((C : (a : R) → R[X]) 1 * p).natDegree =
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
Tactic: rw [← C_1, ← au, map_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ai : R
au : ai * a = 1
rw :
  ((C : (a : R) → R[X]) 1 * p).natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
⊢ (1 * p).natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
have rw₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (ai * a) : R[X]) p).natDegree =
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
Tactic: rw [← C_1, ← au, map_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ai : R
au : ai * a = 1
rw :
  ((C : (a : R) → R[X]) 1 * p).natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (ai * a) : R[X]) p).natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
⊢ (1 * p).natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
have rw₂ : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) ai : R[X]) ((C : (a : R) → R[X]) a : R[X]) * p).natDegree =
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
Tactic: rw [← C_1, ← au, map_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ai : R
au : ai * a = 1
rw :
  ((C : (a : R) → R[X]) 1 * p).natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
rw₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (ai * a) : R[X]) p).natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
rw₂ :
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) ai : R[X]) ((C : (a : R) → R[X]) a : R[X]) * p).natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
⊢ (1 * p).natDegree =
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) ai : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p)).natDegree
have rw₃ : (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) ai : R[X]) ((C : (a : R) → R[X]) a : R[X]) * p).natDegree =
  (HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) ai : R[X]) ((C : (a : R) → R[X]) a : R[X]) * p).natDegree
Tactic: rw [← C_1, ← au, map_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ p.natDegree = (p * 1).natDegree
have nth_rw : (p * 1).natDegree = (p * 1).natDegree
Tactic: nth_rw 1 [← mul_one p]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ai : R
au : a * ai = 1
⊢ (p * 1).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree
have rw : (p * (C : (a : R) → R[X]) 1).natDegree =
  (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
      ((C : (a : R) → R[X]) ai : R[X])).natDegree
Tactic: rw [← C_1, ← au, map_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ai : R
au : a * ai = 1
rw :
  (p * (C : (a : R) → R[X]) 1).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree
⊢ (p * 1).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree
have rw₁ : (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (a * ai) : R[X])).natDegree =
  (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
      ((C : (a : R) → R[X]) ai : R[X])).natDegree
Tactic: rw [← C_1, ← au, map_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ai : R
au : a * ai = 1
rw :
  (p * (C : (a : R) → R[X]) 1).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree
rw₁ :
  (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (a * ai) : R[X])).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree
⊢ (p * 1).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree
have rw₂ : (p * HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) ai : R[X])).natDegree =
  (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
      ((C : (a : R) → R[X]) ai : R[X])).natDegree
Tactic: rw [← C_1, ← au, map_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
ai : R
au : a * ai = 1
rw :
  (p * (C : (a : R) → R[X]) 1).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree
rw₁ :
  (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) (a * ai) : R[X])).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree
rw₂ :
  (p * HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) a : R[X]) ((C : (a : R) → R[X]) ai : R[X])).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree
⊢ (p * 1).natDegree =
    (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
        ((C : (a : R) → R[X]) ai : R[X])).natDegree
have rw₃ : (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
      ((C : (a : R) → R[X]) ai : R[X])).natDegree =
  (HMul.hMul (β := R[X]) (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X]))
      ((C : (a : R) → R[X]) ai : R[X])).natDegree
Tactic: rw [← C_1, ← au, map_mul, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).natDegree = p.natDegree
have refine : p.natDegree ∈ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).support
Tactic: refine eq_natDegree_of_le_mem_support (natDegree_mul_C_le p a) ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
⊢ p.natDegree ∈ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).support
have refine : (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff p.natDegree ≠ 0
Tactic: refine mem_support_iff.mpr ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : p.leadingCoeff * a ≠ 0
⊢ (HMul.hMul (β := R[X]) p ((C : (a : R) → R[X]) a : R[X])).coeff p.natDegree ≠ 0
have rwa : p.coeff p.natDegree * a ≠ 0
Tactic: rwa [coeff_mul_C]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).natDegree = p.natDegree
have refine : p.natDegree ∈ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).support
Tactic: refine eq_natDegree_of_le_mem_support (natDegree_C_mul_le a p) ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ p.natDegree ∈ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).support
have refine : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).coeff p.natDegree ≠ 0
Tactic: refine mem_support_iff.mpr ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).coeff p.natDegree ≠ 0
have rwa : a * p.coeff p.natDegree ≠ 0
Tactic: rwa [coeff_C_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
a : R
inst : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) p).degree = p.degree
have rw : degree.{u} (R := R) ((C : (a : R) → R[X]) a) + p.degree = p.degree
Tactic: rw [degree_mul' (by simpa)]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
m_1 n : ℕ
inst : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ (m + 1)).coeff ((m + 1) * n) = p.coeff n ^ (m + 1)
have rw : (p ^ m).natDegree ≤ m * n
Tactic: rw [pow_succ, pow_succ, ← hm, Nat.succ_mul, coeff_mul_add_eq_of_natDegree_le _ pn]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
m_1 n : ℕ
inst : Semiring R
p : R[X]
pn : p.natDegree ≤ n
m : ℕ
hm : (p ^ m).coeff (m * n) = p.coeff n ^ m
⊢ (p ^ m).natDegree ≤ m * n
have refine : m * p.natDegree ≤ m * n
Tactic: refine natDegree_pow_le.trans (le_trans ?_ (le_refl _))
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
m n : ℕ
inst : Semiring R
p : R[X]
pn : p.natDegree ≤ n
⊢ (p ^ m).coeff (m * n) = p.coeff n ^ m
have zero : (HPow.hPow (β := ℕ) p 0).coeff (0 * n) = HPow.hPow (β := ℕ) (p.coeff n) 0
Tactic: induction m with
  | zero => simp
  | succ m hm =>
    rw [pow_succ, pow_succ, ← hm, Nat.succ_mul, coeff_mul_add_eq_of_natDegree_le _ pn]
    refine natDegree_pow_le.trans (le_trans ?_ (le_refl _))
    gcongr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
m n : ℕ
inst : Semiring R
p : R[X]
pn : p.natDegree ≤ n
zero : (HPow.hPow (β := ℕ) p 0).coeff (0 * n) = HPow.hPow (β := ℕ) (p.coeff n) 0
⊢ (p ^ m).coeff (m * n) = p.coeff n ^ m
have succ : ∀ (m : ℕ) (hm : (p ^ m).coeff (m * n) = p.coeff n ^ m), (p ^ (m + 1)).coeff ((m + 1) * n) = p.coeff n ^ (m + 1)
Tactic: induction m with
  | zero => simp
  | succ m hm =>
    rw [pow_succ, pow_succ, ← hm, Nat.succ_mul, coeff_mul_add_eq_of_natDegree_le _ pn]
    refine natDegree_pow_le.trans (le_trans ?_ (le_refl _))
    gcongr
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
m n : ℕ
inst : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
have inl : ∀ (mno : m * n ≤ m * n), (p ^ m).coeff (m * n) = if m * n = m * n then p.coeff n ^ m else 0
Tactic: rcases eq_or_ne o (m * n) with rfl | h
Cleared hypotheses: o, mno
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
m n : ℕ
inst : Semiring R
p : R[X]
o : ℕ
pn : p.natDegree ≤ n
mno : m * n ≤ o
inl : ∀ (mno : m * n ≤ m * n), (p ^ m).coeff (m * n) = if m * n = m * n then p.coeff n ^ m else 0
⊢ (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
have inr : ∀ (h : o ≠ m * n), (p ^ m).coeff o = if o = m * n then p.coeff n ^ m else 0
Tactic: rcases eq_or_ne o (m * n) with rfl | h
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
n : ℕ
inst : Semiring R
p q : R[X]
pn : p.natDegree < n
⊢ (p + q).coeff n = q.coeff n
have rw : (q + p).coeff n = q.coeff n
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH :
  ∀ (h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)), (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ ((insert x s).sum f).degree = (insert x s).sup fun (i : S) ↦ (f i).degree
have insert : (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
Tactic: simp only [hx, Finset.sum_insert, not_false_iff, Finset.sup_insert]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
IH :
  ∀ (h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)), (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have IH₁ : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
Tactic: specialize IH (h.mono fun _ => by simp +contextual)
Cleared hypotheses: IH
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have insert : ∀ (H : (f x).degree < (s.sum f).degree),
  (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
Tactic: rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ Insert.insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
insert :
  ∀ (H : (f x).degree < (s.sum f).degree),
    (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have insert₁ : ∀ (H : (f x).degree = (s.sum f).degree),
  (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
Tactic: rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ Insert.insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
insert :
  ∀ (H : (f x).degree < (s.sum f).degree),
    (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
insert₁ :
  ∀ (H : (f x).degree = (s.sum f).degree),
    (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have insert₂ : ∀ (H : (s.sum f).degree < (f x).degree),
  (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
Tactic: rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
H : (f x).degree < (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have insert : (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sum f).degree
Tactic: rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ Insert.insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
H : (f x).degree < (s.sum f).degree
insert : (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have insert₁ : (f x + ∑ x ∈ s, f x).degree = (s.sum f).degree
Tactic: rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ Insert.insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
H : (f x).degree < (s.sum f).degree
insert : (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sum f).degree
insert₁ : (f x + ∑ x ∈ s, f x).degree = (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have insert₂ : (s.sum f).degree = (s.sum f).degree
Tactic: rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
H : (f x).degree = (s.sum f).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have insert : ∀ (hx : x ∉ ∅) (h : Set.Pairwise {i : S | Membership.mem (γ := Finset S) (insert x ∅) i ∧ f i ≠ 0} (Ne on degree ∘ f))
  (IH : (Finset.sum ∅ f).degree = sup ∅ fun (i : S) ↦ (f i).degree) (H : (f x).degree = (Finset.sum ∅ f).degree),
  (f x + ∑ x ∈ ∅, f x).degree = max (f x).degree (sup ∅ fun (i : S) ↦ (f i).degree)
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs)
Cleared hypotheses: s, hx, h, IH, H
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ Insert.insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
H : (f x).degree = (s.sum f).degree
insert :
  ∀ (hx : x ∉ ∅)
    (h : Set.Pairwise {i : S | Membership.mem (γ := Finset S) (Insert.insert x ∅) i ∧ f i ≠ 0} (Ne on degree ∘ f))
    (IH : (Finset.sum ∅ f).degree = sup ∅ fun (i : S) ↦ (f i).degree) (H : (f x).degree = (Finset.sum ∅ f).degree),
    (f x + ∑ x ∈ ∅, f x).degree = max (f x).degree (sup ∅ fun (i : S) ↦ (f i).degree)
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have insert₁ : ∀ (hs : s.Nonempty), (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
Tactic: rcases s.eq_empty_or_nonempty with (rfl | hs)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
H : (f x).degree = (s.sum f).degree
hs : s.Nonempty
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have insert : ∀ (y : S) (hy : y ∈ s) (hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree),
  (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
Tactic: obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : Set.Pairwise {i : S | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
H : (f x).degree = (s.sum f).degree
hs : s.Nonempty
y : S
hy : y ∈ s
hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have insert : ∀ (hs : s.Nonempty) (y : S) (H : (f x).degree = (f y).degree) (hy : y ∈ s)
  (hy' : (s.sup fun (i : S) ↦ (f i).degree) = (f y).degree),
  (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
Tactic: rw [IH, hy'] at H
Cleared hypotheses: H, hs, y, hy, hy'