-- Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
theorem integralNormalization_mul_C_leadingCoeff (p : R[X]) :
    integralNormalization p * C p.leadingCoeff = scaleRoots p p.leadingCoeff

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

Tactic:
rw [le_tsub_iff_left (coe_lt_degree.mp h').le, Nat.succ_le_iff]

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

Proof state:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
⊢ (p.integralNormalization * C p.leadingCoeff).coeff i = (p.scaleRoots p.leadingCoeff).coeff i

Tactic:
rw [coeff_mul_C, integralNormalization_coeff]

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

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

Tactic:
simp [natDegree_eq_of_degree_eq_some h, leadingCoeff]

Result:
no goals

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

Tactic:
by_cases h' : i < p.degree

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

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

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

Tactic:
split_ifs with h

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

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

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

Tactic:
rw [mul_assoc, ← pow_succ, tsub_right_comm, tsub_add_cancel_of_le]

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

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

Tactic:
exact coe_lt_degree.mp h'

Result:
no goals

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

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 : ℕ
h : ¬p.degree = ↑i
⊢ p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i) * p.leadingCoeff = (p.scaleRoots p.leadingCoeff).coeff i

Tactic:
simp only [ge_iff_le, tsub_le_iff_right, smul_eq_mul, coeff_scaleRoots]

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

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.integralNormalization * C p.leadingCoeff = p.scaleRoots p.leadingCoeff

Tactic:
ext i

Result:
case a
R : Type u
inst✝ : Semiring R
p : R[X]
i : ℕ
⊢ (p.integralNormalization * C p.leadingCoeff).coeff i = (p.scaleRoots p.leadingCoeff).coeff i