awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Newton (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
n : ℕ
ih :
  HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 n) ∣
    (aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P
d : S
hd :
  (aeval
          (P.newtonMap^[n] x +
            HMul.hMul (α := S) (β := S)
              (-Ring.inverse
                    ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
                S)
              ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) :
        (a : R[X]) → S)
      P =
    HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
        (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
          HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) +
      d *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
          2
⊢ HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 (n + 1)) ∣
    (aeval (P.newtonMap^[n + 1] x) : (a : R[X]) → S) P
have succ : HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 (n + 1)) ∣
  HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
      (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
        HMul.hMul (α := S) (β := S)
          (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
          ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) +
    d *
      HPow.hPow (β := ℕ)
        (HMul.hMul (α := S) (β := S)
          (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
          ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
        2
Tactic: rw [iterate_succ', comp_apply, newtonMap_apply, sub_eq_add_neg, neg_mul_eq_neg_mul, hd]
-- Lean 4 proof step from Mathlib.Dynamics.Newton (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
n : ℕ
ih :
  HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 n) ∣
    (aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P
d : S
hd :
  (aeval
          (P.newtonMap^[n] x +
            HMul.hMul (α := S) (β := S)
              (-Ring.inverse
                    ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
                S)
              ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) :
        (a : R[X]) → S)
      P =
    HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
        (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
          HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) +
      d *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
          2
⊢ HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 (n + 1)) ∣
    HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
        (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
          HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) +
      d *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
          2
have succ : HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 (n + 1)) ∣
  HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
    (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
      HMul.hMul (α := S) (β := S)
        (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
        ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
Tactic: refine dvd_add ?_ (dvd_mul_of_dvd_right ?_ _)
-- Lean 4 proof step from Mathlib.Dynamics.Newton (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
n : ℕ
ih :
  HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 n) ∣
    (aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P
d : S
hd :
  (aeval
          (P.newtonMap^[n] x +
            HMul.hMul (α := S) (β := S)
              (-Ring.inverse
                    ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
                S)
              ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) :
        (a : R[X]) → S)
      P =
    HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
        (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
          HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) +
      d *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
          2
⊢ HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 (n + 1)) ∣
    HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
      (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
        HMul.hMul (α := S) (β := S)
          (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
          ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
have h₁ : HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
    (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
      HMul.hMul (α := S) (β := S)
        (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
        ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) =
  0
Tactic: convert! dvd_zero _
-- Lean 4 proof step from Mathlib.Dynamics.Newton (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
n : ℕ
ih :
  HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 n) ∣
    (aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P
d : S
hd :
  (aeval
          (P.newtonMap^[n] x +
            HMul.hMul (α := S) (β := S)
              (-Ring.inverse
                    ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
                S)
              ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) :
        (a : R[X]) → S)
      P =
    HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
        (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
          HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) +
      d *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
          2
⊢ HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
      (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
        HMul.hMul (α := S) (β := S)
          (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
          ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) =
    0
have this : IsUnit.{u_2} (M := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
Tactic: have : IsUnit (aeval (P.newtonMap^[n] x) <| derivative P) :=
        isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub h' <|
        isNilpotent_iterate_newtonMap_sub_of_isNilpotent h n
-- Lean 4 proof step from Mathlib.Dynamics.Newton (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
n : ℕ
ih :
  HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 n) ∣
    (aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P
d : S
hd :
  (aeval
          (P.newtonMap^[n] x +
            HMul.hMul (α := S) (β := S)
              (-Ring.inverse
                    ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
                S)
              ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) :
        (a : R[X]) → S)
      P =
    HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
        (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
          HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) +
      d *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
          2
this :
  IsUnit.{u_2} (M := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
⊢ HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
      (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
        HMul.hMul (α := S) (β := S)
          (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
          ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) =
    0
have h₁ : HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
    (eval (P.newtonMap^[n] x) (map (algebraMap R S) ((derivative : (a : R[X]) → R[X]) P)) *
      HMul.hMul (α := S) (β := S)
        (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
        ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) =
  0
Tactic: rw [derivative_map, eval_map_algebraMap, ← mul_assoc, mul_neg, Ring.mul_inverse_cancel _ this,
        neg_mul, one_mul, add_neg_cancel]
-- Lean 4 proof step from Mathlib.Dynamics.Newton (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
n : ℕ
ih :
  HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 n) ∣
    (aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P
d : S
hd :
  (aeval
          (P.newtonMap^[n] x +
            HMul.hMul (α := S) (β := S)
              (-Ring.inverse
                    ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
                S)
              ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) :
        (a : R[X]) → S)
      P =
    HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
        (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
          HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) +
      d *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
          2
this :
  IsUnit.{u_2} (M := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
h₁ :
  HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
      (eval (P.newtonMap^[n] x) (map (algebraMap R S) ((derivative : (a : R[X]) → R[X]) P)) *
        HMul.hMul (α := S) (β := S)
          (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
          ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) =
    0
⊢ HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
      (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
        HMul.hMul (α := S) (β := S)
          (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
          ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) =
    0
have h₂ : HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
    (HMul.hMul (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
      (HMul.hMul (α := S) (β := S)
        (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
        ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))) =
  0
Tactic: rw [derivative_map, eval_map_algebraMap, ← mul_assoc, mul_neg, Ring.mul_inverse_cancel _ this,
        neg_mul, one_mul, add_neg_cancel]
-- Lean 4 proof step from Mathlib.Dynamics.Newton (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
n : ℕ
ih :
  HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 n) ∣
    (aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P
d : S
hd :
  (aeval
          (P.newtonMap^[n] x +
            HMul.hMul (α := S) (β := S)
              (-Ring.inverse
                    ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
                S)
              ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) :
        (a : R[X]) → S)
      P =
    HAdd.hAdd (α := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
        (eval (P.newtonMap^[n] x) ((derivative : (a : S[X]) → S[X]) (map (algebraMap R S) P)) *
          HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)) +
      d *
        HPow.hPow (β := ℕ)
          (HMul.hMul (α := S) (β := S)
            (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) :
              S)
            ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
          2
⊢ HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 (n + 1)) ∣
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := S) (β := S)
        (-Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
        ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S))
      2
have succ : HPow.hPow (β := ℕ) (HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 n)) 2 ∣
  HPow.hPow (α := S) (β := ℕ)
      (Ring.inverse ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S) 2 *
    HPow.hPow (α := S) (β := ℕ) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S) 2
Tactic: rw [neg_mul, even_two.neg_pow, mul_pow, pow_succ, pow_mul]
-- Lean 4 proof step from Mathlib.Dynamics.Newton (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
n : ℕ
⊢ HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 n) ∣
    (aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P
have zero : HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) (β := ℕ) 2 0) ∣
  (aeval (P.newtonMap^[0] x) : (a : R[X]) → S) P
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    have ⟨d, hd⟩ := binomExpansion (P.map (algebraMap R S)) (P.newtonMap^[n] x)
      (-Ring.inverse (aeval (P.newtonMap^[n] x) <| derivative P) * aeval (P.newtonMap^[n] x) P)
    rw [eval_map_algebraMap, eval_map_algebraMap] at hd
    rw [iterate_succ', comp_apply, newtonMap_apply, sub_eq_add_neg, neg_mul_eq_neg_mul, hd]
    refine dvd_add ?_ (dvd_mul_of_dvd_right ?_ _)
    · convert! dvd_zero _
      have : IsUnit (aeval (P.newtonMap^[n] x) <| derivative P) :=
        isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub h' <|
        isNilpotent_iterate_newtonMap_sub_of_isNilpotent h n
      rw [derivative_map, eval_map_algebraMap, ← mul_assoc, mul_neg, Ring.mul_inverse_cancel _ this,
        neg_mul, one_mul, add_neg_cancel]
    · rw [neg_mul, even_two.neg_pow, mul_pow, pow_succ, pow_mul]
      exact dvd_mul_of_dvd_right (pow_dvd_pow_of_dvd ih 2) _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Dynamics.Newton (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
n : ℕ
zero :
  HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) (β := ℕ) 2 0) ∣
    (aeval (P.newtonMap^[0] x) : (a : R[X]) → S) P
⊢ HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 n) ∣
    (aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P
have succ : ∀ (n : ℕ)
  (ih :
    HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 n) ∣
      (aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P),
  HPow.hPow (α := S) ((aeval x : (a : R[X]) → S) P : S) (HPow.hPow (α := ℕ) 2 (n + 1)) ∣
    (aeval (P.newtonMap^[n + 1] x) : (a : R[X]) → S) P
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    have ⟨d, hd⟩ := binomExpansion (P.map (algebraMap R S)) (P.newtonMap^[n] x)
      (-Ring.inverse (aeval (P.newtonMap^[n] x) <| derivative P) * aeval (P.newtonMap^[n] x) P)
    rw [eval_map_algebraMap, eval_map_algebraMap] at hd
    rw [iterate_succ', comp_apply, newtonMap_apply, sub_eq_add_neg, neg_mul_eq_neg_mul, hd]
    refine dvd_add ?_ (dvd_mul_of_dvd_right ?_ _)
    · convert! dvd_zero _
      have : IsUnit (aeval (P.newtonMap^[n] x) <| derivative P) :=
        isUnit_aeval_of_isUnit_aeval_of_isNilpotent_sub h' <|
        isNilpotent_iterate_newtonMap_sub_of_isNilpotent h n
      rw [derivative_map, eval_map_algebraMap, ← mul_assoc, mul_neg, Ring.mul_inverse_cancel _ this,
        neg_mul, one_mul, add_neg_cancel]
    · rw [neg_mul, even_two.neg_pow, mul_pow, pow_succ, pow_mul]
      exact dvd_mul_of_dvd_right (pow_dvd_pow_of_dvd ih 2) _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Dynamics.Newton (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
⊢ ∃! r : S, IsNilpotent (x - r) ∧ Eq.{u_2 + 1} (α := S) ((aeval r : (a : R[X]) → S) P : S) (0 : S)
have simp_rw : ∃! r : S, IsNilpotent (r - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r : (a : R[X]) → S) P : S) (0 : S)
Tactic: simp_rw [(neg_sub _ x).symm, isNilpotent_neg_iff]
-- Lean 4 proof step from Mathlib.Dynamics.Newton (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
⊢ ∃! r : S, IsNilpotent (r - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r : (a : R[X]) → S) P : S) (0 : S)
have refine_1 : ∃ (x_1 : S), IsNilpotent (x_1 - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval x_1 : (a : R[X]) → S) P : S) (0 : S)
Tactic: refine existsUnique_of_exists_of_unique ?_ fun r₁ r₂ ⟨hr₁, hr₁'⟩ ⟨hr₂, hr₂'⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Dynamics.Newton (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
P : R[X]
x : S
h : IsNilpotent.{u_2} (R := S) ((aeval x : (a : R[X]) → S) P : S)
h' : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
refine_1 : ∃ (x_1 : S), IsNilpotent (x_1 - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval x_1 : (a : R[X]) → S) P : S) (0 : S)
⊢ ∃! r : S, IsNilpotent (r - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r : (a : R[X]) → S) P : S) (0 : S)
have refine_2 : ∀ (r₁ r₂ : S),
  IsNilpotent (r₁ - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r₁ : (a : R[X]) → S) P : S) (0 : S) →
    IsNilpotent (r₂ - x) ∧ Eq.{u_2 + 1} (α := S) ((aeval r₂ : (a : R[X]) → S) P : S) (0 : S) →
      ∀ (hr₁ : IsNilpotent (r₁ - x)) (hr₁' : Eq.{u_2 + 1} (α := S) ((aeval r₁ : (a : R[X]) → S) P : S) (0 : S))
        (hr₂ : IsNilpotent (r₂ - x)) (hr₂' : Eq.{u_2 + 1} (α := S) ((aeval r₂ : (a : R[X]) → S) P : S) (0 : S)), r₁ = r₂
Tactic: refine existsUnique_of_exists_of_unique ?_ fun r₁ r₂ ⟨hr₁, hr₁'⟩ ⟨hr₂, hr₂'⟩ ↦ ?_