R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.474475
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ support f
h : ∀ (i : σ), n ≤ ↑d i
⊢ n * Fintype.card σ ≤ totalDegree f
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.474475
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
h : totalDegree f < n * Fintype.card σ
d : σ →₀ ℕ
hd : d ∈ support f
⊢ ∃ i, ↑d i < n
contrapose! h
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.474475
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ support f
h : ∀ (i : σ), n ≤ ↑d i
⊢ n * Fintype.card σ ≤ totalDegree f
calc
  n * Fintype.card σ = ∑ _s : σ, n := by
    rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]
  _ ≤ ∑ s, d s := (Finset.sum_le_sum fun s _ => h s)
  _ ≤ d.sum fun _ e => e := by
    rw [Finsupp.sum_fintype]
    intros
    rfl
  _ ≤ f.totalDegree := le_totalDegree hd
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.474475
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ support f
h : ∀ (i : σ), n ≤ ↑d i
⊢ n * Fintype.card σ = ∑ _s : σ, n
rw [Finset.sum_const, Nat.nsmul_eq_mul, mul_comm, Finset.card_univ]
case h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.474475
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ support f
h : ∀ (i : σ), n ≤ ↑d i
⊢ σ → 0 = 0
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.474475
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ support f
h : ∀ (i : σ), n ≤ ↑d i
⊢ ∑ s : σ, ↑d s ≤ sum d fun x e => e
rw [Finsupp.sum_fintype]
case h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.474475
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ support f
h : ∀ (i : σ), n ≤ ↑d i
i✝ : σ
⊢ 0 = 0
case h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.474475
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ support f
h : ∀ (i : σ), n ≤ ↑d i
⊢ σ → 0 = 0
intros
no goals
case h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.474475
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝¹ : CommSemiring R
p q : MvPolynomial σ R
inst✝ : Fintype σ
f : MvPolynomial σ R
n : ℕ
d : σ →₀ ℕ
hd : d ∈ support f
h : ∀ (i : σ), n ≤ ↑d i
i✝ : σ
⊢ 0 = 0
rfl