case empty
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h✝ : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
h : Set.Pairwise {i | i ∈ ∅ ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (Finset.sum ∅ f) = sup ∅ fun i => degree (f i)

case insert
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
IH : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f) → degree (Finset.sum s f) = sup s fun i => degree (f i)
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (Finset.sum (insert x s) f) = sup (insert x s) fun i => degree (f i)
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (Finset.sum s f) = sup s fun i => degree (f i)
induction' s using Finset.induction_on with x s hx IH
no goals
case empty
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h✝ : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
h : Set.Pairwise {i | i ∈ ∅ ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (Finset.sum ∅ f) = sup ∅ fun i => degree (f i)
simp
case insert
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
IH : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f) → degree (Finset.sum s f) = sup s fun i => degree (f i)
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
case insert
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
IH : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f) → degree (Finset.sum s f) = sup s fun i => degree (f i)
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (Finset.sum (insert x s) f) = sup (insert x s) fun i => degree (f i)
simp only [hx, Finset.sum_insert, not_false_iff, Finset.sup_insert]
case insert
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
case insert
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
IH : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f) → degree (Finset.sum s f) = sup s fun i => degree (f i)
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
specialize IH (h.mono fun _ => by simp (config := { contextual := true }))
case insert.inl
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) < degree (Finset.sum s f)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)

case insert.inr.inl
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) = degree (Finset.sum s f)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)

case insert.inr.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (Finset.sum s f) < degree (f x)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
case insert
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
rcases lt_trichotomy (degree (f x)) (degree (s.sum f)) with (H | H | H)
no goals
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
IH : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f) → degree (Finset.sum s f) = sup s fun i => degree (f i)
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
x✝ : S
⊢ x✝ ∈ {i | i ∈ s ∧ f i ≠ 0} → x✝ ∈ {i | i ∈ insert x s ∧ f i ≠ 0}
simp (config := { contextual := true })
no goals
case insert.inl
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) < degree (Finset.sum s f)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
rw [← IH, sup_eq_right.mpr H.le, degree_add_eq_right_of_degree_lt H]
case insert.inr.inl.inl
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h✝ : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
hx : ¬x ∈ ∅
h : Set.Pairwise {i | i ∈ insert x ∅ ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum ∅ f) = sup ∅ fun i => degree (f i)
H : degree (f x) = degree (Finset.sum ∅ f)
⊢ degree (f x + Finset.sum ∅ fun x => f x) = degree (f x) ⊔ sup ∅ fun i => degree (f i)

case insert.inr.inl.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) = degree (Finset.sum s f)
hs : Finset.Nonempty s
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
case insert.inr.inl
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) = degree (Finset.sum s f)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
rcases s.eq_empty_or_nonempty with (rfl | hs)
case insert.inr.inl.inr.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) = degree (Finset.sum s f)
hs : Finset.Nonempty s
y : S
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
case insert.inr.inl.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) = degree (Finset.sum s f)
hs : Finset.Nonempty s
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)
case insert.inr.inl.inr.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
case insert.inr.inl.inr.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (f x) = degree (Finset.sum s f)
hs : Finset.Nonempty s
y : S
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
rw [IH, hy'] at H
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : f x = 0
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)

case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
case insert.inr.inl.inr.intro.intro
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
by_cases hx0 : f x = 0
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
have hy0 : f y ≠ 0 := by
  contrapose! H
  simpa [H, degree_eq_bot] using hx0
case neg.refine'_1
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ x ∈ {i | i ∈ insert x s ∧ f i ≠ 0}

case neg.refine'_2
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ y ∈ {i | i ∈ insert x s ∧ f i ≠ 0}

case neg.refine'_3
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H✝ : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
H : x = y
⊢ x ∈ s
case neg
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
refine' absurd H (h _ _ fun H => hx _)
no goals
case insert.inr.inl.inl
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s : Finset S
h✝ : Set.Pairwise {i | i ∈ s ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
hx : ¬x ∈ ∅
h : Set.Pairwise {i | i ∈ insert x ∅ ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum ∅ f) = sup ∅ fun i => degree (f i)
H : degree (f x) = degree (Finset.sum ∅ f)
⊢ degree (f x + Finset.sum ∅ fun x => f x) = degree (f x) ⊔ sup ∅ fun i => degree (f i)
simp
no goals
case pos
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : f x = 0
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
simp [hx0, IH]
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
H : f y = 0
⊢ degree (f x) ≠ degree (f y)
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
⊢ f y ≠ 0
contrapose! H
no goals
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
H : f y = 0
⊢ degree (f x) ≠ degree (f y)
simpa [H, degree_eq_bot] using hx0
no goals
case neg.refine'_1
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ x ∈ {i | i ∈ insert x s ∧ f i ≠ 0}
simp [hx0]
no goals
case neg.refine'_2
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
⊢ y ∈ {i | i ∈ insert x s ∧ f i ≠ 0}
simp [hy, hy0]
no goals
case neg.refine'_3
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
hs : Finset.Nonempty s
y : S
H✝ : degree (f x) = degree (f y)
hy : y ∈ s
hy' : (sup s fun i => degree (f i)) = degree (f y)
hx0 : ¬f x = 0
hy0 : f y ≠ 0
H : x = y
⊢ x ∈ s
exact H.symm ▸ hy
no goals
case insert.inr.inr
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
f : S → R[X]
s✝ : Finset S
h✝ : Set.Pairwise {i | i ∈ s✝ ∧ f i ≠ 0} (Ne on degree ∘ f)
x : S
s : Finset S
hx : ¬x ∈ s
h : Set.Pairwise {i | i ∈ insert x s ∧ f i ≠ 0} (Ne on degree ∘ f)
IH : degree (Finset.sum s f) = sup s fun i => degree (f i)
H : degree (Finset.sum s f) < degree (f x)
⊢ degree (f x + Finset.sum s fun x => f x) = degree (f x) ⊔ sup s fun i => degree (f i)
rw [← IH, sup_eq_left.mpr H.le, degree_add_eq_left_of_degree_lt H]