Theorem: Polynomial.derivative_scaleRoots (FltRegular/NumberTheory/AuxLemmas.lean)

State before:
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
⊢ derivative (p.scaleRoots r) = r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r
Tactic:
by_cases hp : natDegree p = 0
State after:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p.natDegree = 0
⊢ derivative (p.scaleRoots r) = r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r

case neg
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
⊢ derivative (p.scaleRoots r) = r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r

State before:
case neg
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
⊢ derivative (p.scaleRoots r) = r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r
Tactic:
ext i
State after:
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ (derivative (p.scaleRoots r)).coeff i =
    (r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r).coeff i

State before:
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ (derivative (p.scaleRoots r)).coeff i =
    (r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r).coeff i
Tactic:
simp only [coeff_smul, coeff_scaleRoots, ge_iff_le, smul_eq_mul, coeff_derivative,
  mul_comm (r ^ (natDegree p - _)), mul_assoc, ← pow_add]
State after:
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ p.coeff (i + 1) * ((↑i + 1) * r ^ (p.natDegree - (i + 1))) =
    p.coeff (i + 1) * ((↑i + 1) * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1))))

State before:
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ p.coeff (i + 1) * ((↑i + 1) * r ^ (p.natDegree - (i + 1))) =
    p.coeff (i + 1) * ((↑i + 1) * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1))))
Tactic:
simp_rw [← mul_assoc, ← coeff_derivative]
State after:
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ (derivative p).coeff i * r ^ (p.natDegree - (i + 1)) =
    (derivative p).coeff i * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1)))

State before:
case neg.a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
⊢ (derivative p).coeff i * r ^ (p.natDegree - (i + 1)) =
    (derivative p).coeff i * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1)))
Tactic:
cases lt_or_le (natDegree (derivative p)) i with
| inl h => simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul]
| inr h =>
  congr
  have h' := natDegree_derivative_lt hp
  zify
  rw [Int.ofNat_sub h', Int.ofNat_sub h, Int.ofNat_sub (h.trans_lt h')]
  simp only [Nat.cast_succ]
  abel
State after:
no goals

State before:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p.natDegree = 0
⊢ derivative (p.scaleRoots r) = r ^ (p.natDegree - ((derivative p).natDegree + 1)) • (derivative p).scaleRoots r
Tactic:
rw [hp, Nat.zero_sub, pow_zero, one_smul]
State after:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p.natDegree = 0
⊢ derivative (p.scaleRoots r) = (derivative p).scaleRoots r

State before:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p.natDegree = 0
⊢ derivative (p.scaleRoots r) = (derivative p).scaleRoots r
Tactic:
rw [natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hp
State after:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p = C (p.coeff 0)
⊢ derivative (p.scaleRoots r) = (derivative p).scaleRoots r

State before:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p = C (p.coeff 0)
⊢ derivative (p.scaleRoots r) = (derivative p).scaleRoots r
Tactic:
rw [hp]
State after:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p = C (p.coeff 0)
⊢ derivative ((C (p.coeff 0)).scaleRoots r) = (derivative (C (p.coeff 0))).scaleRoots r

State before:
case pos
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : p = C (p.coeff 0)
⊢ derivative ((C (p.coeff 0)).scaleRoots r) = (derivative (C (p.coeff 0))).scaleRoots r
Tactic:
simp only [scaleRoots_C, derivative_C, zero_scaleRoots]
State after:
no goals

State before:
case neg.a.inl
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : (derivative p).natDegree < i
⊢ (derivative p).coeff i * r ^ (p.natDegree - (i + 1)) =
    (derivative p).coeff i * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1)))
Tactic:
simp only [coeff_eq_zero_of_natDegree_lt h, zero_mul]
State after:
no goals

State before:
case neg.a.inr
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
⊢ (derivative p).coeff i * r ^ (p.natDegree - (i + 1)) =
    (derivative p).coeff i * r ^ ((derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1)))
Tactic:
congr
State after:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
⊢ p.natDegree - (i + 1) = (derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1))

State before:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
⊢ p.natDegree - (i + 1) = (derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1))
Tactic:
have h' := natDegree_derivative_lt hp
State after:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ p.natDegree - (i + 1) = (derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1))

State before:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ p.natDegree - (i + 1) = (derivative p).natDegree - i + (p.natDegree - ((derivative p).natDegree + 1))
Tactic:
zify
State after:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ ↑(p.natDegree - (i + 1)) = ↑((derivative p).natDegree - i) + ↑(p.natDegree - ((derivative p).natDegree + 1))

State before:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ ↑(p.natDegree - (i + 1)) = ↑((derivative p).natDegree - i) + ↑(p.natDegree - ((derivative p).natDegree + 1))
Tactic:
rw [Int.ofNat_sub h', Int.ofNat_sub h, Int.ofNat_sub (h.trans_lt h')]
State after:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ ↑p.natDegree - ↑i.succ = ↑(derivative p).natDegree - ↑i + (↑p.natDegree - ↑(derivative p).natDegree.succ)

State before:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ ↑p.natDegree - ↑i.succ = ↑(derivative p).natDegree - ↑i + (↑p.natDegree - ↑(derivative p).natDegree.succ)
Tactic:
simp only [Nat.cast_succ]
State after:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ ↑p.natDegree - (↑i + 1) = ↑(derivative p).natDegree - ↑i + (↑p.natDegree - (↑(derivative p).natDegree + 1))

State before:
case neg.a.inr.e_a.e_a
R : Type u_1
inst✝ : CommRing R
p : R[X]
r : R
hp : ¬p.natDegree = 0
i : ℕ
h : i ≤ (derivative p).natDegree
h' : (derivative p).natDegree < p.natDegree
⊢ ↑p.natDegree - (↑i + 1) = ↑(derivative p).natDegree - ↑i + (↑p.natDegree - (↑(derivative p).natDegree + 1))
Tactic:
abel
State after:
no goals