-- Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
theorem integralNormalization_coeff_mul_leadingCoeff_pow (i : ℕ) (hp : 1 ≤ natDegree p) :
    (integralNormalization p).coeff i * p.leadingCoeff ^ i =
      p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
⊢ p.integralNormalization.coeff i * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
rw [integralNormalization_coeff]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
⊢ (if p.degree = ↑i then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) * p.leadingCoeff ^ i =
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : p.degree = ↑i
⊢ 1 * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
simp [natDegree_eq_of_degree_eq_some h, leadingCoeff,
  ← pow_succ', tsub_add_cancel_of_le (natDegree_eq_of_degree_eq_some h ▸ hp)]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
⊢ (if p.degree = ↑i then 1 else p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)) * p.leadingCoeff ^ i =
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
split_ifs with h

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : p.degree = ↑i
⊢ 1 * p.leadingCoeff ^ i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff ^ i =
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ i < p.natDegree

Tactic:
exact coe_lt_degree.mp h'

Result:
no goals

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
rw [tsub_add_cancel_of_le]

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ i ≤ p.natDegree - 1

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff ^ i =
    p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
simp only [mul_assoc, ← pow_add]

Result:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
h' : ¬↑i < p.degree
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
simp [coeff_eq_zero_of_degree_lt (lt_of_le_of_ne (le_of_not_gt h') h)]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Tactic:
by_cases h' : i < p.degree

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
h' : ¬↑i < p.degree
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i + i) = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1)

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ i ≤ p.natDegree - 1

Tactic:
rw [le_tsub_iff_right hp, Nat.succ_le_iff]

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
hp : 1 ≤ p.natDegree
h : ¬p.degree = ↑i
h' : ↑i < p.degree
⊢ i < p.natDegree