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

case refine'_2
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.39868
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      degrees (∏ i in s, f i) ≤ ∑ i in s, degrees (f i) →
        degrees (∏ i in insert a s, f i) ≤ ∑ i in insert a s, degrees (f i)
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.39868
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degrees (∏ i in s, f i) ≤ ∑ i in s, degrees (f i)
refine' s.induction _ _
no goals
case refine'_1
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.39868
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
s : Finset ι
f : ι → MvPolynomial σ R
⊢ degrees (∏ i in ∅, f i) ≤ ∑ i in ∅, degrees (f i)
simp only [Finset.prod_empty, Finset.sum_empty, degrees_one, le_refl]
case refine'_2
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.39868
r : R
e : ℕ
n m : σ
s✝¹ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
s✝ : Finset ι
f : ι → MvPolynomial σ R
i : ι
s : Finset ι
his : ¬i ∈ s
ih : degrees (∏ i in s, f i) ≤ ∑ i in s, degrees (f i)
⊢ degrees (∏ i in insert i s, f i) ≤ ∑ i in insert i s, degrees (f i)
case refine'_2
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.39868
r : R
e : ℕ
n m : σ
s✝ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
s : Finset ι
f : ι → MvPolynomial σ R
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      degrees (∏ i in s, f i) ≤ ∑ i in s, degrees (f i) →
        degrees (∏ i in insert a s, f i) ≤ ∑ i in insert a s, degrees (f i)
intro i s his ih
case refine'_2
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.39868
r : R
e : ℕ
n m : σ
s✝¹ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
s✝ : Finset ι
f : ι → MvPolynomial σ R
i : ι
s : Finset ι
his : ¬i ∈ s
ih : degrees (∏ i in s, f i) ≤ ∑ i in s, degrees (f i)
⊢ degrees (f i * ∏ x in s, f x) ≤ degrees (f i) + ∑ x in s, degrees (f x)
case refine'_2
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.39868
r : R
e : ℕ
n m : σ
s✝¹ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
s✝ : Finset ι
f : ι → MvPolynomial σ R
i : ι
s : Finset ι
his : ¬i ∈ s
ih : degrees (∏ i in s, f i) ≤ ∑ i in s, degrees (f i)
⊢ degrees (∏ i in insert i s, f i) ≤ ∑ i in insert i s, degrees (f i)
rw [Finset.prod_insert his, Finset.sum_insert his]
no goals
case refine'_2
R : Type u
S : Type v
σ : Type u_2
τ : Type ?u.39868
r : R
e : ℕ
n m : σ
s✝¹ : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
ι : Type u_1
s✝ : Finset ι
f : ι → MvPolynomial σ R
i : ι
s : Finset ι
his : ¬i ∈ s
ih : degrees (∏ i in s, f i) ≤ ∑ i in s, degrees (f i)
⊢ degrees (f i * ∏ x in s, f x) ≤ degrees (f i) + ∑ x in s, degrees (f x)
exact le_trans (degrees_mul _ _) (add_le_add_left ih _)