Theorem: Polynomial.natDegree_discConv_le (LeanCamCombi/DiscreteDeriv.lean)

State before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ (discConv w P).natDegree ≤ P.natDegree
Tactic:
refine' (natDegree_sum_le _ _).trans $ Finset.sup_le fun r _ ↦ _
State after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ (natDegree ∘ fun a => (fun r s => s • P.comp (X + C r)) a (w a)) r ≤ P.natDegree

State before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ (natDegree ∘ fun a => (fun r s => s • P.comp (X + C r)) a (w a)) r ≤ P.natDegree
Tactic:
dsimp
State after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ (w r • P.comp (X + C r)).natDegree ≤ P.natDegree

State before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ (w r • P.comp (X + C r)).natDegree ≤ P.natDegree
Tactic:
simp_rw [algebra_compatible_smul R (w r)]
State after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ ((algebraMap S R) (w r) • P.comp (X + C r)).natDegree ≤ P.natDegree

State before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ ((algebraMap S R) (w r) • P.comp (X + C r)).natDegree ≤ P.natDegree
Tactic:
refine (natDegree_smul_le _ _).trans ?_
State after:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ (P.comp (X + C r)).natDegree ≤ P.natDegree

State before:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra S R
w : R →₀ S
P : R[X]
inst✝² : Nontrivial S
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
r : R
x✝ : r ∈ w.support
⊢ (P.comp (X + C r)).natDegree ≤ P.natDegree
Tactic:
simp [natDegree_comp]
State after:
no goals