-- Mathlib/Algebra/Polynomial/Monic.lean
theorem degree_smul_of_smul_regular {S : Type*} [Monoid S] [DistribMulAction S R] {k : S}
    (p : R[X]) (h : IsSMulRegular R k) : (k • p).degree = p.degree

Proof state:
case refine_1
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).degree ≤ p.degree

Tactic:
rw [degree_le_iff_coeff_zero]

Result:
case refine_1
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ ∀ (m : ℕ), p.degree < ↑m → (k • p).coeff m = 0

Proof state:
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).degree = p.degree

Tactic:
refine le_antisymm ?_ ?_

Result:
case refine_1
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).degree ≤ p.degree

case refine_2
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ p.degree ≤ (k • p).degree

Proof state:
case refine_2
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ ∀ (m : ℕ), (k • p).degree < ↑m → p.coeff m = 0

Tactic:
intro m hm

Result:
case refine_2
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : (k • p).degree < ↑m
⊢ p.coeff m = 0

Proof state:
case refine_2
R : Type u
inst✝² : Semiring R
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 → (k • p).coeff m_1 = 0
⊢ (fun x => k • x) (p.coeff m) = (fun x => k • x) 0

Tactic:
simpa using hm m le_rfl

Result:
no goals

Proof state:
case refine_2
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : (k • p).degree < ↑m
⊢ p.coeff m = 0

Tactic:
rw [degree_lt_iff_coeff_zero] at hm

Result:
case refine_2
R : Type u
inst✝² : Semiring R
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 → (k • p).coeff m_1 = 0
⊢ p.coeff m = 0

Proof state:
case refine_1
R : Type u
inst✝² : Semiring R
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 → p.coeff m_1 = 0
⊢ (k • p).coeff m = 0

Tactic:
simp [hm m le_rfl]

Result:
no goals

Proof state:
case refine_1
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ ∀ (m : ℕ), p.degree < ↑m → (k • p).coeff m = 0

Tactic:
intro m hm

Result:
case refine_1
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : p.degree < ↑m
⊢ (k • p).coeff m = 0

Proof state:
case refine_1
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
m : ℕ
hm : p.degree < ↑m
⊢ (k • p).coeff m = 0

Tactic:
rw [degree_lt_iff_coeff_zero] at hm

Result:
case refine_1
R : Type u
inst✝² : Semiring R
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 → p.coeff m_1 = 0
⊢ (k • p).coeff m = 0

Proof state:
case refine_2
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ p.degree ≤ (k • p).degree

Tactic:
rw [degree_le_iff_coeff_zero]

Result:
case refine_2
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ ∀ (m : ℕ), (k • p).degree < ↑m → p.coeff m = 0

Proof state:
case refine_2
R : Type u
inst✝² : Semiring R
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 → (k • p).coeff m_1 = 0
⊢ p.coeff m = 0

Tactic:
refine h ?_

Result:
case refine_2
R : Type u
inst✝² : Semiring R
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 → (k • p).coeff m_1 = 0
⊢ (fun x => k • x) (p.coeff m) = (fun x => k • x) 0