-- Mathlib/RingTheory/Polynomial/Basic.lean
lemma aeval_natDegree_le {R : Type*} [CommSemiring R] {m n : ℕ}
    (F : MvPolynomial σ R) (hF : F.totalDegree ≤ m)
    (f : σ → Polynomial R) (hf : ∀ i, (f i).natDegree ≤ n) :
    (MvPolynomial.aeval f F).natDegree ≤ m * n

Proof state:
case a
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
⊢ ∀ b ∈ F.support,
    (natDegree ∘ fun i => (fun s a => (algebraMap R R[X]) a * s.prod fun n e => f n ^ e) i (F i)) b ≤ m * n

Tactic:
intro d hd

Result:
case a
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ (natDegree ∘ fun i => (fun s a => (algebraMap R R[X]) a * s.prod fun n e => f n ^ e) i (F i)) d ≤ m * n

Proof state:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
⊢ (Finsupp.sum F fun s a => (algebraMap R R[X]) a * s.prod fun n e => f n ^ e).natDegree ≤ m * n

Tactic:
apply (Polynomial.natDegree_sum_le _ _).trans

Result:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
⊢ fold max 0 (natDegree ∘ fun i => (fun s a => (algebraMap R R[X]) a * s.prod fun n e => f n ^ e) i (F i)) F.support ≤
    m * n

Proof state:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
this : ∑ i ∈ d.support, d i * n ≤ m * n
⊢ ∀ i ∈ d.support, ((fun n e => f n ^ e) i (d i)).natDegree ≤ d i * n

Tactic:
rintro i -

Result:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
this : ∑ i ∈ d.support, d i * n ≤ m * n
i : σ
⊢ ((fun n e => f n ^ e) i (d i)).natDegree ≤ d i * n

Proof state:
case a
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
this : ∑ i ∈ d.support, d i * n ≤ m * n
⊢ ∑ i ∈ d.support, ((fun n e => f n ^ e) i (d i)).natDegree ≤ m * n

Tactic:
apply (Finset.sum_le_sum _).trans this

Result:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
this : ∑ i ∈ d.support, d i * n ≤ m * n
⊢ ∀ i ∈ d.support, ((fun n e => f n ^ e) i (d i)).natDegree ≤ d i * n

Proof state:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
⊢ fold max 0 (natDegree ∘ fun i => (fun s a => (algebraMap R R[X]) a * s.prod fun n e => f n ^ e) i (F i)) F.support ≤
    m * n

Tactic:
apply Finset.sup_le

Result:
case a
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
⊢ ∀ b ∈ F.support,
    (natDegree ∘ fun i => (fun s a => (algebraMap R R[X]) a * s.prod fun n e => f n ^ e) i (F i)) b ≤ m * n

Proof state:
case a
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ (Polynomial.C (F d) * d.prod fun n e => f n ^ e).natDegree ≤ m * n

Tactic:
apply (Polynomial.natDegree_C_mul_le _ _).trans

Result:
case a
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ (d.prod fun n e => f n ^ e).natDegree ≤ m * n

Proof state:
case a
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ (natDegree ∘ fun i => (fun s a => (algebraMap R R[X]) a * s.prod fun n e => f n ^ e) i (F i)) d ≤ m * n

Tactic:
simp_rw [Function.comp_apply, ← C_eq_algebraMap]

Result:
case a
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ (Polynomial.C (F d) * d.prod fun n e => f n ^ e).natDegree ≤ m * n

Proof state:
case a
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ ∑ i ∈ d.support, ((fun n e => f n ^ e) i (d i)).natDegree ≤ m * n

Tactic:
have : ∑ i ∈ d.support, (d i) * n ≤ m * n := by
  rw [← Finset.sum_mul]
  apply mul_le_mul' (.trans _ hF) le_rfl
  rw [MvPolynomial.totalDegree]
  exact Finset.le_sup_of_le hd le_rfl

Result:
case a
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
this : ∑ i ∈ d.support, d i * n ≤ m * n
⊢ ∑ i ∈ d.support, ((fun n e => f n ^ e) i (d i)).natDegree ≤ m * n

Proof state:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
this : ∑ i ∈ d.support, d i * n ≤ m * n
i : σ
⊢ d i * (f i).natDegree ≤ d i * n

Tactic:
exact mul_le_mul' le_rfl (hf i)

Result:
no goals

Proof state:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ ∑ i ∈ d.support, d i ≤ F.support.sup fun s => s.sum fun x e => e

Tactic:
exact Finset.le_sup_of_le hd le_rfl

Result:
no goals

Proof state:
case a
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ (d.prod fun n e => f n ^ e).natDegree ≤ m * n

Tactic:
apply (Polynomial.natDegree_prod_le _ _).trans

Result:
case a
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ ∑ i ∈ d.support, ((fun n e => f n ^ e) i (d i)).natDegree ≤ m * n

Proof state:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ ∑ i ∈ d.support, d i * n ≤ m * n

Tactic:
rw [← Finset.sum_mul]

Result:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
⊢ (∑ i ∈ d.support, d i) * n ≤ m * n

Proof state:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
this : ∑ i ∈ d.support, d i * n ≤ m * n
i : σ
⊢ ((fun n e => f n ^ e) i (d i)).natDegree ≤ d i * n

Tactic:
apply Polynomial.natDegree_pow_le.trans

Result:
σ : Type v
R : Type u_2
inst✝ : CommSemiring R
m n : ℕ
F : MvPolynomial σ R
hF : F.totalDegree ≤ m
f : σ → R[X]
hf : ∀ (i : σ), (f i).natDegree ≤ n
d : σ →₀ ℕ
hd : d ∈ F.support
this : ∑ i ∈ d.support, d i * n ≤ m * n
i : σ
⊢ d i * (f i).natDegree ≤ d i * n