A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
this : (a : Prop) → Decidable a
⊢ degree (scaleRoots p s) = degree p
A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
⊢ degree (scaleRoots p s) = degree p
haveI := Classical.propDecidable
case pos
A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : p = 0
⊢ degree (scaleRoots p s) = degree p

case neg
A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ degree (scaleRoots p s) = degree p
A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
this : (a : Prop) → Decidable a
⊢ degree (scaleRoots p s) = degree p
by_cases hp : p = 0
case neg
A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ coeff (scaleRoots p s) (natDegree p) ≠ 0
case neg
A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ degree (scaleRoots p s) = degree p
refine' le_antisymm (Finset.sup_mono (support_scaleRoots_le p s)) (degree_le_degree _)
case neg
A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ leadingCoeff p ≠ 0
case neg
A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ coeff (scaleRoots p s) (natDegree p) ≠ 0
rw [coeff_scaleRoots_natDegree]
case neg
A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
h : leadingCoeff p = 0
⊢ False
case neg
A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
⊢ leadingCoeff p ≠ 0
intro h
case neg
A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
this✝ : (a : Prop) → Decidable a
hp : ¬p = 0
h : leadingCoeff p = 0
this : p = 0
⊢ False
case neg
A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : ¬p = 0
h : leadingCoeff p = 0
⊢ False
have := leadingCoeff_eq_zero.mp h
no goals
case neg
A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
this✝ : (a : Prop) → Decidable a
hp : ¬p = 0
h : leadingCoeff p = 0
this : p = 0
⊢ False
contradiction
no goals
case pos
A : Type ?u.34124
K : Type ?u.34127
R : Type u_1
S : Type ?u.34133
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Field K
inst✝¹ : CommRing R
inst✝ : CommRing S
M : Submonoid A
p : R[X]
s : R
this : (a : Prop) → Decidable a
hp : p = 0
⊢ degree (scaleRoots p s) = degree p
rw [hp, zero_scaleRoots]