-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem coeff_pow_mul_natDegree (p : R[X]) (n : ℕ) :
    (p ^ n).coeff (n * p.natDegree) = p.leadingCoeff ^ n

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

Tactic:
by_cases hp2 : p ^ i = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : p ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

Proof state:
case zero
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ (p ^ 0).coeff (0 * p.natDegree) = p.leadingCoeff ^ 0

Tactic:
simp

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : p ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

Tactic:
rw [hp2, zero_mul, coeff_zero]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
⊢ (p ^ (i + 1)).coeff ((i + 1) * p.natDegree) = p.leadingCoeff ^ (i + 1)

Tactic:
rw [pow_succ, pow_succ, Nat.succ_mul]

Result:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (p ^ i).natDegree = 0
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
⊢ p ^ i = 0

Tactic:
exact leadingCoeff_eq_zero.mp hi

Result:
no goals

Proof state:
case neg.h
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h1 : (p ^ i).natDegree < i * p.natDegree
⊢ (p ^ i * p).natDegree < i * p.natDegree + p.natDegree

Tactic:
calc
  (p ^ i * p).natDegree ≤ (p ^ i).natDegree + p.natDegree := natDegree_mul_le
  _ < i * p.natDegree + p.natDegree := add_lt_add_right h1 _

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
⊢ (p ^ i).natDegree < i * p.natDegree

Tactic:
refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
⊢ p ^ i = 0

Proof state:
case neg.h
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
⊢ (p ^ i * p).natDegree < i * p.natDegree + p.natDegree

Tactic:
have h1 : (p ^ i).natDegree < i * p.natDegree := by
  refine lt_of_le_of_ne natDegree_pow_le fun h => hp2 ?_
  rw [← h, hp1] at hi
  exact leadingCoeff_eq_zero.mp hi

Result:
case neg.h
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h1 : (p ^ i).natDegree < i * p.natDegree
⊢ (p ^ i * p).natDegree < i * p.natDegree + p.natDegree

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : ¬p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

Tactic:
rw [← natDegree_pow' hp1, ← leadingCoeff_pow' hp1]

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : ¬p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff ((p ^ i).natDegree + p.natDegree) = (p ^ i).leadingCoeff * p.leadingCoeff

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

Tactic:
apply coeff_eq_zero_of_natDegree_lt

Result:
case neg.h
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
⊢ (p ^ i * p).natDegree < i * p.natDegree + p.natDegree

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

Tactic:
rw [hp1, zero_mul]

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = 0

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : ¬p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff ((p ^ i).natDegree + p.natDegree) = (p ^ i).leadingCoeff * p.leadingCoeff

Tactic:
exact coeff_mul_degree_add_degree _ _

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
⊢ p ^ i = 0

Tactic:
rw [← h, hp1] at hi

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (p ^ i).natDegree = 0
hp1 : p.leadingCoeff ^ i = 0
hp2 : ¬p ^ i = 0
h : (p ^ i).natDegree = i * p.natDegree
⊢ p ^ i = 0

Proof state:
case succ
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

Tactic:
by_cases hp1 : p.leadingCoeff ^ i = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hi : (p ^ i).coeff (i * p.natDegree) = p.leadingCoeff ^ i
hp1 : ¬p.leadingCoeff ^ i = 0
⊢ (p ^ i * p).coeff (i * p.natDegree + p.natDegree) = p.leadingCoeff ^ i * p.leadingCoeff