Theorem: Polynomial.degree_discConv_lt (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
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
⊢ (discConv w P).degree < P.degree
Tactic:
have := coeff_discConv_natDegree w P
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
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = (w.sum fun x => id) • P.leadingCoeff
⊢ (discConv w P).degree < P.degree

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
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = (w.sum fun x => id) • P.leadingCoeff
⊢ (discConv w P).degree < P.degree
Tactic:
rw [hw, zero_smul] at this
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
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ (discConv w P).degree < P.degree

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
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ (discConv w P).degree < P.degree
Tactic:
refine' (degree_sum_le _ _).trans_lt $ (Finset.sup_lt_iff _).2 _
State after:
case refine'_1
ι : 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
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ ⊥ < P.degree

case refine'_2
ι : 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
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ ∀ b ∈ w.support, ((fun r s => s • P.comp (X + C r)) b (w b)).degree < P.degree

State before:
case refine'_1
ι : 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
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ ⊥ < P.degree

case refine'_2
ι : 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
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ ∀ b ∈ w.support, ((fun r s => s • P.comp (X + C r)) b (w b)).degree < P.degree
Tactic:
sorry
State after:
case refine'_2
ι : 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
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ ∀ b ∈ w.support, ((fun r s => s • P.comp (X + C r)) b (w b)).degree < P.degree

State before:
case refine'_2
ι : 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
hw : (w.sum fun x => id) = 0
hP : P ≠ 0
this : (discConv w P).coeff P.natDegree = 0
⊢ ∀ b ∈ w.support, ((fun r s => s • P.comp (X + C r)) b (w b)).degree < P.degree
Tactic:
sorry
State after:
no goals