case refine'_1
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ degree (k • p) ≤ degree p

case refine'_2
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ degree p ≤ degree (k • p)
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ degree (k • p) = degree p
refine' le_antisymm _ _
case refine'_1
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ ∀ (m : ℕ), degree p < ↑m → coeff (k • p) m = 0
case refine'_1
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ degree (k • p) ≤ degree p
rw [degree_le_iff_coeff_zero]
case refine'_1
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : degree p < ↑m
⊢ coeff (k • p) m = 0
case refine'_1
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ ∀ (m : ℕ), degree p < ↑m → coeff (k • p) m = 0
intro m hm
case refine'_1
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff p m_1 = 0
⊢ coeff (k • p) m = 0
case refine'_1
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : degree p < ↑m
⊢ coeff (k • p) m = 0
rw [degree_lt_iff_coeff_zero] at hm
no goals
case refine'_1
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff p m_1 = 0
⊢ coeff (k • p) m = 0
simp [hm m le_rfl]
case refine'_2
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ ∀ (m : ℕ), degree (k • p) < ↑m → coeff p m = 0
case refine'_2
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ degree p ≤ degree (k • p)
rw [degree_le_iff_coeff_zero]
case refine'_2
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : degree (k • p) < ↑m
⊢ coeff p m = 0
case refine'_2
R : Type u
S✝ : Type v
a b : R
m n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ ∀ (m : ℕ), degree (k • p) < ↑m → coeff p m = 0
intro m hm
case refine'_2
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff (k • p) m_1 = 0
⊢ coeff p m = 0
case refine'_2
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : degree (k • p) < ↑m
⊢ coeff p m = 0
rw [degree_lt_iff_coeff_zero] at hm
case refine'_2
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff (k • p) m_1 = 0
⊢ (fun x => k • x) (coeff p m) = (fun x => k • x) 0
case refine'_2
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff (k • p) m_1 = 0
⊢ coeff p m = 0
refine' h _
no goals
case refine'_2
R : Type u
S✝ : Type v
a b : R
m✝ n : ℕ
ι : Type y
inst✝² : Semiring R
p✝ : R[X]
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : ∀ (m_1 : ℕ), m ≤ m_1 → coeff (k • p) m_1 = 0
⊢ (fun x => k • x) (coeff p m) = (fun x => k • x) 0
simpa using hm m le_rfl