case inl
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
t : R
hpt : IsRoot 0 t
⊢ rootMultiplicity t (↑derivative 0) = rootMultiplicity t 0 - 1

case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
⊢ rootMultiplicity t (↑derivative p) = rootMultiplicity t p - 1
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
⊢ rootMultiplicity t (↑derivative p) = rootMultiplicity t p - 1
rcases eq_or_ne p 0 with (rfl | hp)
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
⊢ rootMultiplicity t (↑derivative (p /ₘ (X - ↑C t) ^ rootMultiplicity t p * (X - ↑C t) ^ rootMultiplicity t p)) =
    rootMultiplicity t p - 1
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
⊢ rootMultiplicity t (↑derivative p) = rootMultiplicity t p - 1
nth_rw 1 [← p.divByMonic_mul_pow_rootMultiplicity_eq t]
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
⊢ rootMultiplicity t
      (↑derivative (p /ₘ (X - ↑C t) ^ rootMultiplicity t p) * (X - ↑C t) ^ rootMultiplicity t p +
        p /ₘ (X - ↑C t) ^ rootMultiplicity t p *
          (↑C ↑(rootMultiplicity t p) * (X - ↑C t) ^ (rootMultiplicity t p - 1))) =
    rootMultiplicity t p - 1
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
⊢ rootMultiplicity t (↑derivative (p /ₘ (X - ↑C t) ^ rootMultiplicity t p * (X - ↑C t) ^ rootMultiplicity t p)) =
    rootMultiplicity t p - 1
simp only [derivative_pow, derivative_mul, derivative_sub, derivative_X, derivative_C, sub_zero,
  mul_one]
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
⊢ rootMultiplicity t
      (↑derivative (p /ₘ (X - ↑C t) ^ rootMultiplicity t p) * (X - ↑C t) ^ rootMultiplicity t p +
        p /ₘ (X - ↑C t) ^ rootMultiplicity t p * (↑C ↑(rootMultiplicity t p) * (X - ↑C t) ^ n)) =
    n
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
⊢ rootMultiplicity t
      (↑derivative (p /ₘ (X - ↑C t) ^ rootMultiplicity t p) * (X - ↑C t) ^ rootMultiplicity t p +
        p /ₘ (X - ↑C t) ^ rootMultiplicity t p *
          (↑C ↑(rootMultiplicity t p) * (X - ↑C t) ^ (rootMultiplicity t p - 1))) =
    rootMultiplicity t p - 1
set n := p.rootMultiplicity t - 1
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
⊢ rootMultiplicity t
      (↑derivative (p /ₘ (X - ↑C t) ^ rootMultiplicity t p) * (X - ↑C t) ^ rootMultiplicity t p +
        p /ₘ (X - ↑C t) ^ rootMultiplicity t p * (↑C ↑(rootMultiplicity t p) * (X - ↑C t) ^ n)) =
    n
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
⊢ rootMultiplicity t
      (↑derivative (p /ₘ (X - ↑C t) ^ rootMultiplicity t p) * (X - ↑C t) ^ rootMultiplicity t p +
        p /ₘ (X - ↑C t) ^ rootMultiplicity t p * (↑C ↑(rootMultiplicity t p) * (X - ↑C t) ^ n)) =
    n
have hn : n + 1 = _ := tsub_add_cancel_of_le ((rootMultiplicity_pos hp).mpr hpt)
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
⊢ rootMultiplicity t
      (↑derivative (p /ₘ (X - ↑C t) ^ (n + 1)) * (X - ↑C t) ^ (n + 1) +
        p /ₘ (X - ↑C t) ^ (n + 1) * (↑C ↑(n + 1) * (X - ↑C t) ^ n)) =
    n
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
⊢ rootMultiplicity t
      (↑derivative (p /ₘ (X - ↑C t) ^ rootMultiplicity t p) * (X - ↑C t) ^ rootMultiplicity t p +
        p /ₘ (X - ↑C t) ^ rootMultiplicity t p * (↑C ↑(rootMultiplicity t p) * (X - ↑C t) ^ n)) =
    n
rw [← hn]
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ rootMultiplicity t (↑derivative q * (X - ↑C t) ^ (n + 1) + q * (↑C ↑(n + 1) * (X - ↑C t) ^ n)) = n
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
⊢ rootMultiplicity t
      (↑derivative (p /ₘ (X - ↑C t) ^ (n + 1)) * (X - ↑C t) ^ (n + 1) +
        p /ₘ (X - ↑C t) ^ (n + 1) * (↑C ↑(n + 1) * (X - ↑C t) ^ n)) =
    n
set q := p /ₘ (X - C t) ^ (n + 1) with _hq
case h.e'_2
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ rootMultiplicity t (↑derivative q * (X - ↑C t) ^ (n + 1) + q * (↑C ↑(n + 1) * (X - ↑C t) ^ n)) =
    rootMultiplicity t ((X - ↑C t) ^ n * (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1)))

case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ rootMultiplicity t ((X - ↑C t) ^ n * (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1))) = n
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ rootMultiplicity t (↑derivative q * (X - ↑C t) ^ (n + 1) + q * (↑C ↑(n + 1) * (X - ↑C t) ^ n)) = n
convert_to rootMultiplicity t ((X - C t) ^ n * (derivative q * (X - C t) + q * C ↑(n + 1))) = n
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
h : eval t (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1)) ≠ 0
⊢ rootMultiplicity t ((X - ↑C t) ^ n * (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1))) = n
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ rootMultiplicity t ((X - ↑C t) ^ n * (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1))) = n
have h : eval t (derivative q * (X - C t) + q * C (R := R) ↑(n + 1)) ≠ 0 := by
  suffices eval t q * ↑(n + 1) ≠ 0 by simpa
  refine' mul_ne_zero _ (Nat.cast_ne_zero.mpr n.succ_ne_zero)
  convert eval_divByMonic_pow_rootMultiplicity_ne_zero t hp
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
h : eval t (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1)) ≠ 0
⊢ (X - ↑C t) ^ n * (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1)) ≠ 0
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
h : eval t (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1)) ≠ 0
⊢ rootMultiplicity t ((X - ↑C t) ^ n * (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1))) = n
rw [rootMultiplicity_mul, rootMultiplicity_X_sub_C_pow, rootMultiplicity_eq_zero h, add_zero]
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
h : eval t (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1)) ≠ 0
⊢ ↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1) ≠ 0
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
h : eval t (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1)) ≠ 0
⊢ (X - ↑C t) ^ n * (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1)) ≠ 0
refine' mul_ne_zero (pow_ne_zero n <| X_sub_C_ne_zero t) _
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
h :
  ↑derivative (p /ₘ (X - ↑C t) ^ (n + 1)) * (X - ↑C t) +
      p /ₘ (X - ↑C t) ^ (n + 1) * ↑C ↑(rootMultiplicity t p - 1 + 1) =
    0
⊢ eval t
      (↑derivative (p /ₘ (X - ↑C t) ^ (n + 1)) * (X - ↑C t) +
        p /ₘ (X - ↑C t) ^ (n + 1) * ↑C ↑(rootMultiplicity t p - 1 + 1)) =
    0
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
h : eval t (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1)) ≠ 0
⊢ ↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1) ≠ 0
contrapose! h
no goals
case inr
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
h :
  ↑derivative (p /ₘ (X - ↑C t) ^ (n + 1)) * (X - ↑C t) +
      p /ₘ (X - ↑C t) ^ (n + 1) * ↑C ↑(rootMultiplicity t p - 1 + 1) =
    0
⊢ eval t
      (↑derivative (p /ₘ (X - ↑C t) ^ (n + 1)) * (X - ↑C t) +
        p /ₘ (X - ↑C t) ^ (n + 1) * ↑C ↑(rootMultiplicity t p - 1 + 1)) =
    0
rw [h, eval_zero]
no goals
case inl
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
t : R
hpt : IsRoot 0 t
⊢ rootMultiplicity t (↑derivative 0) = rootMultiplicity t 0 - 1
simp
case h.e'_2.e_p
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ ↑derivative q * (X - ↑C t) ^ (n + 1) + q * (↑C ↑(n + 1) * (X - ↑C t) ^ n) =
    (X - ↑C t) ^ n * (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1))
case h.e'_2
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ rootMultiplicity t (↑derivative q * (X - ↑C t) ^ (n + 1) + q * (↑C ↑(n + 1) * (X - ↑C t) ^ n)) =
    rootMultiplicity t ((X - ↑C t) ^ n * (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1)))
congr
case h.e'_2.e_p
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ ↑derivative q * (X - ↑C t) ^ (n + 1) + q * (↑C ↑(n + 1) * (X - ↑C t) ^ n) =
    ↑derivative q * (X - ↑C t) ^ (n + 1) + (X - ↑C t) ^ n * (q * ↑C ↑(n + 1))
case h.e'_2.e_p
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ ↑derivative q * (X - ↑C t) ^ (n + 1) + q * (↑C ↑(n + 1) * (X - ↑C t) ^ n) =
    (X - ↑C t) ^ n * (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1))
rw [mul_add, mul_left_comm <| (X - C t) ^ n, ← pow_succ']
case h.e'_2.e_p.e_a
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ q * (↑C ↑(n + 1) * (X - ↑C t) ^ n) = (X - ↑C t) ^ n * (q * ↑C ↑(n + 1))
case h.e'_2.e_p
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ ↑derivative q * (X - ↑C t) ^ (n + 1) + q * (↑C ↑(n + 1) * (X - ↑C t) ^ n) =
    ↑derivative q * (X - ↑C t) ^ (n + 1) + (X - ↑C t) ^ n * (q * ↑C ↑(n + 1))
congr 1
no goals
case h.e'_2.e_p.e_a
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ q * (↑C ↑(n + 1) * (X - ↑C t) ^ n) = (X - ↑C t) ^ n * (q * ↑C ↑(n + 1))
rw [mul_left_comm <| (X - C t) ^ n, mul_comm <| (X - C t) ^ n]
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ eval t q * ↑(n + 1) ≠ 0
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ eval t (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1)) ≠ 0
suffices eval t q * ↑(n + 1) ≠ 0 by simpa
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ eval t q ≠ 0
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ eval t q * ↑(n + 1) ≠ 0
refine' mul_ne_zero _ (Nat.cast_ne_zero.mpr n.succ_ne_zero)
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
⊢ eval t q ≠ 0
convert eval_divByMonic_pow_rootMultiplicity_ne_zero t hp
no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : CharZero R
p : R[X]
t : R
hpt : IsRoot p t
hp : p ≠ 0
n : ℕ := rootMultiplicity t p - 1
hn : n + 1 = rootMultiplicity t p
q : R[X] := p /ₘ (X - ↑C t) ^ (n + 1)
_hq : q = p /ₘ (X - ↑C t) ^ (n + 1)
this : eval t q * ↑(n + 1) ≠ 0
⊢ eval t (↑derivative q * (X - ↑C t) + q * ↑C ↑(n + 1)) ≠ 0
simpa