case refine'_1
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.34158
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degrees (∑ i in ∅, f i) ≤ Finset.sup ∅ fun i => degrees (f i)

case refine'_2
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.34158
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      (degrees (∑ i in s, f i) ≤ Finset.sup s fun i => degrees (f i)) →
        degrees (∑ i in insert a s, f i) ≤ Finset.sup (insert a s) fun i => degrees (f i)
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.34158
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degrees (∑ i in s, f i) ≤ Finset.sup s fun i => degrees (f i)
refine' s.induction _ _
case refine'_1
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.34158
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ 0 ≤ ⊥
case refine'_1
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.34158
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degrees (∑ i in ∅, f i) ≤ Finset.sup ∅ fun i => degrees (f i)
simp only [Finset.sum_empty, Finset.sup_empty, degrees_zero]
no goals
case refine'_1
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.34158
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ 0 ≤ ⊥
exact le_rfl
case refine'_2
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.34158
r : R
e : ℕ
n m : σ
s✝¹ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
s✝ : Finset ι
f : ι → MvPolynomial σ R
i : ι
s : Finset ι
his : ¬i ∈ s
ih : degrees (∑ i in s, f i) ≤ Finset.sup s fun i => degrees (f i)
⊢ degrees (∑ i in insert i s, f i) ≤ Finset.sup (insert i s) fun i => degrees (f i)
case refine'_2
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.34158
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      (degrees (∑ i in s, f i) ≤ Finset.sup s fun i => degrees (f i)) →
        degrees (∑ i in insert a s, f i) ≤ Finset.sup (insert a s) fun i => degrees (f i)
intro i s his ih
case refine'_2
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.34158
r : R
e : ℕ
n m : σ
s✝¹ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
s✝ : Finset ι
f : ι → MvPolynomial σ R
i : ι
s : Finset ι
his : ¬i ∈ s
ih : degrees (∑ i in s, f i) ≤ Finset.sup s fun i => degrees (f i)
⊢ degrees (f i + ∑ x in s, f x) ≤ degrees (f i) ⊔ Finset.sup s fun i => degrees (f i)
case refine'_2
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.34158
r : R
e : ℕ
n m : σ
s✝¹ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
s✝ : Finset ι
f : ι → MvPolynomial σ R
i : ι
s : Finset ι
his : ¬i ∈ s
ih : degrees (∑ i in s, f i) ≤ Finset.sup s fun i => degrees (f i)
⊢ degrees (∑ i in insert i s, f i) ≤ Finset.sup (insert i s) fun i => degrees (f i)
rw [Finset.sup_insert, Finset.sum_insert his]
no goals
case refine'_2
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.34158
r : R
e : ℕ
n m : σ
s✝¹ : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
inst✝ : DecidableEq σ
s✝ : Finset ι
f : ι → MvPolynomial σ R
i : ι
s : Finset ι
his : ¬i ∈ s
ih : degrees (∑ i in s, f i) ≤ Finset.sup s fun i => degrees (f i)
⊢ degrees (f i + ∑ x in s, f x) ≤ degrees (f i) ⊔ Finset.sup s fun i => degrees (f i)
exact le_trans (degrees_add _ _) (sup_le_sup_left ih _)