awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
have pos : ∀ (hx0 : f x = 0), (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
Tactic: by_cases hx0 : f x = 0
-- 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
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
pos : ∀ (hx0 : f x = 0), (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 neg : ∀ (hx0 : ¬f x = 0), (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
Tactic: by_cases hx0 : f x = 0
-- 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
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
hx0 : ¬f x = 0
⊢ f y ≠ 0
have contrapose! : ∀ (H : f y = 0), (f x).degree ≠ (f y).degree
Tactic: contrapose! H
Cleared hypotheses: H
-- 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
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
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
hx0 : ¬f x = 0
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have hy0 : f y ≠ 0
Tactic: have hy0 : f y ≠ 0 := by
        contrapose! H
        simpa [H, degree_eq_bot] using hx0
-- 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
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
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have neg : Membership.mem (γ := Set S) {i : S | i ∈ insert x s ∧ f i ≠ 0} x
Tactic: refine absurd H (h ?_ ?_ fun H => hx ?_)
-- 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
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
hx0 : ¬f x = 0
hy0 : f y ≠ 0
neg : Membership.mem (γ := Set S) {i : S | i ∈ insert x s ∧ f i ≠ 0} x
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have neg₁ : Membership.mem (γ := Set S) {i : S | i ∈ insert x s ∧ f i ≠ 0} y
Tactic: refine absurd H (h ?_ ?_ fun H => hx ?_)
-- 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
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
hx0 : ¬f x = 0
hy0 : f y ≠ 0
neg : Membership.mem (γ := Set S) {i : S | i ∈ insert x s ∧ f i ≠ 0} x
neg₁ : Membership.mem (γ := Set S) {i : S | i ∈ insert x s ∧ f i ≠ 0} y
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have neg₂ : ∀ (H : x = y), x ∈ s
Tactic: refine absurd H (h ?_ ?_ fun H => hx ?_)
-- 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 : (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)
have insert : (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sum f).degree
Tactic: rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_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 : (s.sum f).degree < (f x).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 = (f x).degree
Tactic: rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_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 : (s.sum f).degree < (f x).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 = (f x).degree
⊢ (f x + ∑ x ∈ s, f x).degree = max (f x).degree (s.sup fun (i : S) ↦ (f i).degree)
have insert₂ : (f x).degree = (f x).degree
Tactic: rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_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]
s : Finset S
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
have empty : ∀ (h : Set.Pairwise {i : S | Membership.mem (γ := Finset S) ∅ i ∧ f i ≠ 0} (Ne on degree ∘ f)),
  (Finset.sum ∅ f).degree = sup ∅ fun (i : S) ↦ (f i).degree
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert x s hx IH =>
    simp only [hx, Finset.sum_insert, not_false_iff, Finset.sup_insert]
    specialize IH (h.mono fun _ => by simp +contextual)
    rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
    · rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
    · rcases s.eq_empty_or_nonempty with (rfl | hs)
      · simp
      obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
      rw [IH, hy'] at H
      by_cases hx0 : f x = 0
      · simp [hx0, IH]
      have hy0 : f y ≠ 0 := by
        contrapose! H
        simpa [H, degree_eq_bot] using hx0
      refine absurd H (h ?_ ?_ fun H => hx ?_)
      · simp [hx0]
      · simp [hy, hy0]
      · exact H.symm ▸ hy
    · rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_of_degree_lt H]
Cleared hypotheses: s, 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
empty :
  ∀ (h : Set.Pairwise {i : S | Membership.mem (γ := Finset S) ∅ i ∧ f i ≠ 0} (Ne on degree ∘ f)),
    (Finset.sum ∅ f).degree = sup ∅ fun (i : S) ↦ (f i).degree
⊢ (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
have insert : ∀ (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
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert x s hx IH =>
    simp only [hx, Finset.sum_insert, not_false_iff, Finset.sup_insert]
    specialize IH (h.mono fun _ => by simp +contextual)
    rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
    · rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
    · rcases s.eq_empty_or_nonempty with (rfl | hs)
      · simp
      obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
      rw [IH, hy'] at H
      by_cases hx0 : f x = 0
      · simp [hx0, IH]
      have hy0 : f y ≠ 0 := by
        contrapose! H
        simpa [H, degree_eq_bot] using hx0
      refine absurd H (h ?_ ?_ fun H => hx ?_)
      · simp [hx0]
      · simp [hy, hy0]
      · exact H.symm ▸ hy
    · rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_of_degree_lt H]
Cleared hypotheses: s, 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]
s : Finset S
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
have empty : ∀ (h : Set.Pairwise {i : S | Membership.mem (γ := Finset S) ∅ i ∧ f i ≠ 0} (Ne on degree ∘ f)),
  (Finset.sum ∅ f).degree = sup ∅ fun (i : S) ↦ (f i).degree
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert x s hx IH =>
    simp only [hx, Finset.sum_insert, not_false_iff, Finset.sup_insert]
    specialize IH (h.mono fun _ => by simp +contextual)
    rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
    · rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
    · rcases s.eq_empty_or_nonempty with (rfl | hs)
      · simp
      obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
      rw [IH, hy'] at H
      by_cases hx0 : f x = 0
      · simp [hx0, IH]
      have hy0 : f y ≠ 0 := by
        contrapose! H
        simpa [H, degree_eq_bot] using hx0
      refine absurd H (h ?_ ?_ fun H => hx ?_)
      · simp [hx0]
      · simp [hy, hy0]
      · exact H.symm ▸ hy
    · rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_of_degree_lt H]
Cleared hypotheses: s, 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
empty :
  ∀ (h : Set.Pairwise {i : S | Membership.mem (γ := Finset S) ∅ i ∧ f i ≠ 0} (Ne on degree ∘ f)),
    (Finset.sum ∅ f).degree = sup ∅ fun (i : S) ↦ (f i).degree
⊢ (s.sum f).degree = s.sup fun (i : S) ↦ (f i).degree
have insert : ∀ (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
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert x s hx IH =>
    simp only [hx, Finset.sum_insert, not_false_iff, Finset.sup_insert]
    specialize IH (h.mono fun _ => by simp +contextual)
    rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
    · rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
    · rcases s.eq_empty_or_nonempty with (rfl | hs)
      · simp
      obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
      rw [IH, hy'] at H
      by_cases hx0 : f x = 0
      · simp [hx0, IH]
      have hy0 : f y ≠ 0 := by
        contrapose! H
        simpa [H, degree_eq_bot] using hx0
      refine absurd H (h ?_ ?_ fun H => hx ?_)
      · simp [hx0]
      · simp [hy, hy0]
      · exact H.symm ▸ hy
    · rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_of_degree_lt H]
Cleared hypotheses: s, 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
⊢ (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree
have pos : ∀ (H : ∃ x ∈ s, f x ≠ 0), (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree
Tactic: by_cases! H : ∃ x ∈ s, f x ≠ 0
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
pos : ∀ (H : ∃ x ∈ s, f x ≠ 0), (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree
⊢ (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree
have neg : ∀ (H : ∀ (x : S) (_ : x ∈ s), f x = 0), (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree
Tactic: by_cases! H : ∃ x ∈ s, f x ≠ 0
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ∃ x ∈ s, f x ≠ 0
⊢ (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree
have pos : ∀ (x : S) (hx : x ∈ s) (hx' : f x ≠ 0), (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree
Tactic: obtain ⟨x, hx, hx'⟩ := H
Cleared hypotheses: H
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
⊢ (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree
have hs : s.Nonempty
Tactic: have hs : s.Nonempty := ⟨x, hx⟩
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree
have pos : (s.sum f).degree = (↑(s.sup fun (i : S) ↦ (f i).natDegree) : WithBot ℕ)
Tactic: refine natDegree_eq_of_degree_eq_some ?_
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ (s.sum f).degree = (↑(s.sup fun (i : S) ↦ (f i).natDegree) : WithBot ℕ)
have pos : Eq (α := WithBot ℕ) (s.sup fun (i : S) ↦ (f i).degree) (↑(s.sup fun (i : S) ↦ (f i).natDegree) : WithBot ℕ)
Tactic: rw [degree_sum_eq_of_disjoint]
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
pos : Eq (α := WithBot ℕ) (s.sup fun (i : S) ↦ (f i).degree) (↑(s.sup fun (i : S) ↦ (f i).natDegree) : WithBot ℕ)
⊢ (s.sum f).degree = (↑(s.sup fun (i : S) ↦ (f i).natDegree) : WithBot ℕ)
have pos₁ : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
Tactic: rw [degree_sum_eq_of_disjoint]
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ Eq (α := WithBot ℕ) (s.sup fun (i : S) ↦ (f i).degree) (↑(s.sup fun (i : S) ↦ (f i).natDegree) : WithBot ℕ)
have pos : Eq (α := WithBot ℕ) (s.sup' hs fun (i : S) ↦ (f i).degree) (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree))
Tactic: rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs,
        Nat.cast_withBot, Finset.coe_sup' hs, ←
        Finset.sup'_eq_sup 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ Eq (α := WithBot ℕ) (s.sup' hs fun (i : S) ↦ (f i).degree) (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree))
have pos : LE.le (α := WithBot ℕ) (s.sup' hs fun (i : S) ↦ (f i).degree) (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree))
Tactic: refine le_antisymm ?_ ?_
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
pos :
  LE.le (α := WithBot ℕ) (s.sup' hs fun (i : S) ↦ (f i).degree)
    (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree))
⊢ Eq (α := WithBot ℕ) (s.sup' hs fun (i : S) ↦ (f i).degree) (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree))
have pos₁ : LE.le (α := WithBot ℕ) (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)) (s.sup' hs fun (i : S) ↦ (f i).degree)
Tactic: refine le_antisymm ?_ ?_
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ LE.le (α := WithBot ℕ) (s.sup' hs fun (i : S) ↦ (f i).degree)
    (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree))
have pos : ∀ b ∈ s, (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)
Tactic: rw [Finset.sup'_le_iff]
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
⊢ (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)
have pos : ∀ (hb' : f b = 0), (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)
Tactic: by_cases hb' : f b = 0
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
pos : ∀ (hb' : f b = 0), (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)
⊢ (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)
have neg : ∀ (hb' : ¬f b = 0), (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)
Tactic: by_cases hb' : f b = 0
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : ¬f b = 0
⊢ (f b).degree ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)
have neg : (↑(f b).natDegree : WithBot ℕ) ≤ s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree)
Tactic: rw [degree_eq_natDegree hb', Nat.cast_withBot]
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
⊢ LE.le (α := WithBot ℕ) (s.sup' hs (WithBot.some ∘ fun (i : S) ↦ (f i).natDegree))
    (s.sup' hs fun (i : S) ↦ (f i).degree)
have pos : ∀ b ∈ s,
  LE.le (α := WithBot ℕ) ((WithBot.some ∘ fun (i : S) ↦ (f i).natDegree) b) (s.sup' hs fun (i : S) ↦ (f i).degree)
Tactic: rw [Finset.sup'_le_iff]
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
⊢ LE.le (α := WithBot ℕ) ((WithBot.some ∘ fun (i : S) ↦ (f i).natDegree) b) (s.sup' hs fun (i : S) ↦ (f i).degree)
have pos : ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree
Tactic: simp only [Finset.le_sup'_iff, Function.comp_apply]
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
⊢ ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree
have pos : ∀ (hb' : f b = 0), ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree
Tactic: by_cases hb' : f b = 0
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
pos : ∀ (hb' : f b = 0), ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree
⊢ ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree
have neg : ∀ (hb' : ¬f b = 0), ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree
Tactic: by_cases hb' : f b = 0
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : f b = 0
⊢ ∃ b_1 ∈ s, (↑(f b).natDegree : WithBot ℕ) ≤ (f b_1).degree
have pos : (↑(f b).natDegree : WithBot ℕ) ≤ (f x).degree
Tactic: refine ⟨x, hx, ?_⟩
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
x : S
hx : x ∈ s
hx' : f x ≠ 0
hs : s.Nonempty
b : S
hb : b ∈ s
hb' : f b = 0
⊢ (↑(f b).natDegree : WithBot ℕ) ≤ (f x).degree
have pos : ∀ (hx' : (f x).degree < (↑(f b).natDegree : WithBot ℕ)), f x = 0
Tactic: contrapose! hx'
Cleared hypotheses: hx'
-- 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]
s : Finset S
h : Set.Pairwise {i : S | i ∈ s ∧ f i ≠ 0} (Ne on natDegree ∘ f)
H : ∀ (x : S) (_ : x ∈ s), f x = 0
⊢ (s.sum f).natDegree = s.sup fun (i : S) ↦ (f i).natDegree
have neg : ∀ s_1 ∈ s, (f s_1).natDegree = ⊥
Tactic: rw [Finset.sum_eq_zero H, natDegree_zero, eq_comm, show 0 = ⊥ from rfl, Finset.sup_eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
hlt : p.natDegree ≤ 0
⊢ False
have A : p = (C : (a : R) → R[X]) (p.coeff 0)
Tactic: have A : p = C (p.coeff 0) := eq_C_of_natDegree_le_zero hlt
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Degree.Lemmas (hypothesis)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
p : R[X]
hp : p ≠ 0
f : R →+* S
z : S
hz : eval₂ f z p = 0
inj : ∀ (x : R), Eq.{v + 1} (α := S) ((f : (a : R) → S) x : S) (0 : S) → x = 0
hlt : p.natDegree ≤ 0
A : p = (C : (a : R) → R[X]) (p.coeff 0)
⊢ False
have hz₁ : Eq.{v + 1} (α := S) ((f : (a : R) → S) (p.coeff 0) : S) (0 : S)
Tactic: rw [A, eval₂_C] at hz
Cleared hypotheses: hz, inj, hlt, A