awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Dynamics.Flow (goal)
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
f₁ : τ → α → α
cont' : Continuous (uncurry f₁)
map_add' : ∀ (t₁ t₂ : τ) (x : α), f₁ (t₁ + t₂) x = f₁ t₁ (f₁ t₂ x)
map_zero' : ∀ (x : α), f₁ 0 x = x
f₂ : τ → α → α
cont'_1 : Continuous (uncurry f₂)
map_add'_1 : ∀ (t₁ t₂ : τ) (x : α), f₂ (t₁ + t₂) x = f₂ t₁ (f₂ t₂ x)
map_zero'_1 : ∀ (x : α), f₂ 0 x = x
h :
  ∀ (t : τ) (x : α),
    toFun { toFun := f₁, cont' := cont', map_add' := map_add', map_zero' := map_zero' : Flow τ α } t x =
      toFun { toFun := f₂, cont' := cont'_1, map_add' := map_add'_1, map_zero' := map_zero'_1 } t x
⊢ Eq (α := Flow τ α) { toFun := f₁, cont' := cont', map_add' := map_add', map_zero' := map_zero' }
    { toFun := f₂, cont' := cont'_1, map_add' := map_add'_1, map_zero' := map_zero'_1 }
have e_toFun : f₁ = f₂
Tactic: congr
-- Lean 4 proof step from Mathlib.Dynamics.Flow (goal)
Goal:
τ : Type u_1
inst : AddMonoid τ
inst_1 : TopologicalSpace τ
inst_2 : ContinuousAdd τ
α : Type u_2
inst_3 : TopologicalSpace α
f₁ : τ → α → α
cont' : Continuous (uncurry f₁)
map_add' : ∀ (t₁ t₂ : τ) (x : α), f₁ (t₁ + t₂) x = f₁ t₁ (f₁ t₂ x)
map_zero' : ∀ (x : α), f₁ 0 x = x
f₂ : τ → α → α
cont'_1 : Continuous (uncurry f₂)
map_add'_1 : ∀ (t₁ t₂ : τ) (x : α), f₂ (t₁ + t₂) x = f₂ t₁ (f₂ t₂ x)
map_zero'_1 : ∀ (x : α), f₂ 0 x = x
h :
  ∀ (t : τ) (x : α),
    toFun { toFun := f₁, cont' := cont', map_add' := map_add', map_zero' := map_zero' : Flow τ α } t x =
      toFun { toFun := f₂, cont' := cont'_1, map_add' := map_add'_1, map_zero' := map_zero'_1 } t x
⊢ f₁ = f₂
have e_toFun : ∀ (x : τ) (x_1 : α), f₁ x x_1 = f₂ x x_1
Tactic: funext
-- Lean 4 proof step from Mathlib.Dynamics.Flow (goal)
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
s : Set α
h : ∀ (t : τ), ϕ.toFun t '' s = s
t : τ
⊢ ϕ.toFun t '' s ⊆ s
have rw : s ⊆ s
Tactic: rw [h t]
-- Lean 4 proof step from Mathlib.Dynamics.Flow (goal)
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
x x_1 : τ
x_2 : α
⊢ ϕ.toFun (-(x + x_1)) x_2 = ϕ.toFun (-x) (ϕ.toFun (-x_1) x_2)
have rw : ϕ.toFun (-x + -x_1) x_2 = ϕ.toFun (-x) (ϕ.toFun (-x_1) x_2)
Tactic: rw [neg_add, map_add]
-- Lean 4 proof step from Mathlib.Dynamics.Flow (goal)
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
x x_1 : τ
x_2 : α
rw : ϕ.toFun (-x + -x_1) x_2 = ϕ.toFun (-x) (ϕ.toFun (-x_1) x_2)
⊢ ϕ.toFun (-(x + x_1)) x_2 = ϕ.toFun (-x) (ϕ.toFun (-x_1) x_2)
have rw₁ : ϕ.toFun (-x) (ϕ.toFun (-x_1) x_2) = ϕ.toFun (-x) (ϕ.toFun (-x_1) x_2)
Tactic: rw [neg_add, map_add]
-- Lean 4 proof step from Mathlib.Dynamics.Flow (goal)
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
x : α
⊢ ϕ.toFun (-0) x = x
have rw : ϕ.toFun 0 x = x
Tactic: rw [neg_zero, map_zero_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Flow (goal)
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
x : α
rw : ϕ.toFun 0 x = x
⊢ ϕ.toFun (-0) x = x
have rw₁ : x = x
Tactic: rw [neg_zero, map_zero_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Flow (goal)
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
t : τ
x : α
⊢ ϕ.toFun (-t) (ϕ.toFun t x) = x
have rw : ϕ.toFun (-t + t) x = x
Tactic: rw [← map_add, neg_add_cancel, map_zero_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Flow (goal)
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
t : τ
x : α
rw : ϕ.toFun (-t + t) x = x
⊢ ϕ.toFun (-t) (ϕ.toFun t x) = x
have rw₁ : ϕ.toFun 0 x = x
Tactic: rw [← map_add, neg_add_cancel, map_zero_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Flow (goal)
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
t : τ
x : α
rw : ϕ.toFun (-t + t) x = x
rw₁ : ϕ.toFun 0 x = x
⊢ ϕ.toFun (-t) (ϕ.toFun t x) = x
have rw₂ : x = x
Tactic: rw [← map_add, neg_add_cancel, map_zero_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Flow (goal)
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
t : τ
x : α
⊢ ϕ.toFun t (ϕ.toFun (-t) x) = x
have rw : ϕ.toFun (t + -t) x = x
Tactic: rw [← map_add, add_neg_cancel, map_zero_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Flow (goal)
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
t : τ
x : α
rw : ϕ.toFun (t + -t) x = x
⊢ ϕ.toFun t (ϕ.toFun (-t) x) = x
have rw₁ : ϕ.toFun 0 x = x
Tactic: rw [← map_add, add_neg_cancel, map_zero_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Flow (goal)
Goal:
τ : Type u_1
inst : AddCommGroup τ
inst_1 : TopologicalSpace τ
inst_2 : IsTopologicalAddGroup τ
α : Type u_2
inst_3 : TopologicalSpace α
ϕ : Flow τ α
t : τ
x : α
rw : ϕ.toFun (t + -t) x = x
rw₁ : ϕ.toFun 0 x = x
⊢ ϕ.toFun t (ϕ.toFun (-t) x) = x
have rw₂ : x = x
Tactic: rw [← map_add, add_neg_cancel, map_zero_apply]
-- Lean 4 proof step from Mathlib.Dynamics.Minimal (goal)
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
⊢ IsMinimal M α ↔ ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ
have mp : IsMinimal M α → ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Dynamics.Minimal (goal)
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
mp : IsMinimal M α → ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ
⊢ IsMinimal M α ↔ ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ
have mpr : (∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ) → IsMinimal M α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Dynamics.Minimal (goal)
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
⊢ (∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ) → IsMinimal M α
have mpr : ∀ (H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ) (x : α), IsClosed (closure (orbit M x))
Tactic: refine fun H ↦ ⟨fun _ ↦ dense_iff_closure_eq.2 <| (H _ ?_ ?_).resolve_left ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Minimal (goal)
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
mpr :
  ∀ (H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ) (x : α), IsClosed (closure (orbit M x))
⊢ (∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ) → IsMinimal M α
have mpr₁ : ∀ (H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ) (x : α) (c : M),
  c • closure (orbit M x) ⊆ closure (orbit M x)
Tactic: refine fun H ↦ ⟨fun _ ↦ dense_iff_closure_eq.2 <| (H _ ?_ ?_).resolve_left ?_⟩
-- Lean 4 proof step from Mathlib.Dynamics.Minimal (goal)
Goal:
M : Type u_1
α : Type u_3
inst : Monoid M
inst_1 : TopologicalSpace α
inst_2 : MulAction M α
inst_3 : ContinuousConstSMul M α
mpr :
  ∀ (H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ) (x : α), IsClosed (closure (orbit M x))
mpr₁ :
  ∀ (H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ) (x : α) (c : M),
    c • closure (orbit M x) ⊆ closure (orbit M x)
⊢ (∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ) → IsMinimal M α
have mpr₂ : ∀ (H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ) (x : α), ¬closure (orbit M x) = ∅
Tactic: refine fun H ↦ ⟨fun _ ↦ dense_iff_closure_eq.2 <| (H _ ?_ ?_).resolve_left ?_⟩
-- 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)
n : ℕ
ih : IsNilpotent (P.newtonMap^[n] x - x)
⊢ IsNilpotent (P.newtonMap^[n + 1] x - x)
have succ : IsNilpotent
  (P.newtonMap^[n] x - 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))
Tactic: rw [iterate_succ', comp_apply, newtonMap_apply, sub_right_comm]
-- 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)
n : ℕ
ih : IsNilpotent (P.newtonMap^[n] x - x)
⊢ IsNilpotent
    (P.newtonMap^[n] x - 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))
have succ : IsNilpotent.{u_2} (R := S) ((aeval (P.newtonMap^[n] x) : (a : R[X]) → S) P : S)
Tactic: refine (Commute.all _ _).isNilpotent_sub ih <| (Commute.all _ _).isNilpotent_mul_left ?_
-- 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)
n : ℕ
⊢ IsNilpotent (P.newtonMap^[n] x - x)
have zero : IsNilpotent (P.newtonMap^[0] x - x)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [iterate_succ', comp_apply, newtonMap_apply, sub_right_comm]
    refine (Commute.all _ _).isNilpotent_sub ih <| (Commute.all _ _).isNilpotent_mul_left ?_
    simpa using Commute.isNilpotent_add (Commute.all _ _)
      (isNilpotent_aeval_sub_of_isNilpotent_sub P ih) h
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)
n : ℕ
zero : IsNilpotent (P.newtonMap^[0] x - x)
⊢ IsNilpotent (P.newtonMap^[n] x - x)
have succ : ∀ (n : ℕ) (ih : IsNilpotent (P.newtonMap^[n] x - x)), IsNilpotent (P.newtonMap^[n + 1] x - x)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [iterate_succ', comp_apply, newtonMap_apply, sub_right_comm]
    refine (Commute.all _ _).isNilpotent_sub ih <| (Commute.all _ _).isNilpotent_mul_left ?_
    simpa using Commute.isNilpotent_add (Commute.all _ _)
      (isNilpotent_aeval_sub_of_isNilpotent_sub P ih) h
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 : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
⊢ IsFixedPt P.newtonMap x
have rw : P.newtonMap x = x
Tactic: rw [IsFixedPt, newtonMap_apply, h, mul_zero, sub_zero]
-- 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 : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
rw : P.newtonMap x = x
⊢ IsFixedPt P.newtonMap x
have rw₁ : x -
    HMul.hMul (α := S) (β := S)
      (Ring.inverse ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
      ((aeval x : (a : R[X]) → S) P : S) =
  x
Tactic: rw [IsFixedPt, newtonMap_apply, h, mul_zero, sub_zero]
-- 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 : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
rw : P.newtonMap x = x
rw₁ :
  x -
      HMul.hMul (α := S) (β := S)
        (Ring.inverse ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
        ((aeval x : (a : R[X]) → S) P : S) =
    x
⊢ IsFixedPt P.newtonMap x
have rw₂ : x -
    HMul.hMul (α := S) (β := S)
      (Ring.inverse ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S) (0 : S) =
  x
Tactic: rw [IsFixedPt, newtonMap_apply, h, mul_zero, sub_zero]
-- 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 : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
rw : P.newtonMap x = x
rw₁ :
  x -
      HMul.hMul (α := S) (β := S)
        (Ring.inverse ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
        ((aeval x : (a : R[X]) → S) P : S) =
    x
rw₂ :
  x -
      HMul.hMul (α := S) (β := S)
        (Ring.inverse ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S) (0 : S) =
    x
⊢ IsFixedPt P.newtonMap x
have rw₃ : x - 0 = x
Tactic: rw [IsFixedPt, newtonMap_apply, h, mul_zero, sub_zero]
-- 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 : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
rw : P.newtonMap x = x
rw₁ :
  x -
      HMul.hMul (α := S) (β := S)
        (Ring.inverse ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
        ((aeval x : (a : R[X]) → S) P : S) =
    x
rw₂ :
  x -
      HMul.hMul (α := S) (β := S)
        (Ring.inverse ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S) (0 : S) =
    x
rw₃ : x - 0 = x
⊢ IsFixedPt P.newtonMap x
have rw₄ : x = x
Tactic: rw [IsFixedPt, newtonMap_apply, h, mul_zero, sub_zero]
-- 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 : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
⊢ IsFixedPt P.newtonMap x ↔ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
have rw : P.newtonMap x = x ↔ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
Tactic: rw [IsFixedPt, newtonMap_apply, sub_eq_self, Ring.inverse_mul_eq_iff_eq_mul _ _ _ h, mul_zero]
-- 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 : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
rw : P.newtonMap x = x ↔ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
⊢ IsFixedPt P.newtonMap x ↔ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
have rw₁ : x -
      HMul.hMul (α := S) (β := S)
        (Ring.inverse ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
        ((aeval x : (a : R[X]) → S) P : S) =
    x ↔
  Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
Tactic: rw [IsFixedPt, newtonMap_apply, sub_eq_self, Ring.inverse_mul_eq_iff_eq_mul _ _ _ h, mul_zero]
-- 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 : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
rw : P.newtonMap x = x ↔ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
rw₁ :
  x -
        HMul.hMul (α := S) (β := S)
          (Ring.inverse ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
          ((aeval x : (a : R[X]) → S) P : S) =
      x ↔
    Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
⊢ IsFixedPt P.newtonMap x ↔ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
have rw₂ : HMul.hMul (α := S) (β := S) (Ring.inverse ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
      ((aeval x : (a : R[X]) → S) P : S) =
    0 ↔
  Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
Tactic: rw [IsFixedPt, newtonMap_apply, sub_eq_self, Ring.inverse_mul_eq_iff_eq_mul _ _ _ h, mul_zero]
-- 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 : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
rw : P.newtonMap x = x ↔ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
rw₁ :
  x -
        HMul.hMul (α := S) (β := S)
          (Ring.inverse ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
          ((aeval x : (a : R[X]) → S) P : S) =
      x ↔
    Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
rw₂ :
  HMul.hMul (α := S) (β := S)
        (Ring.inverse ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
        ((aeval x : (a : R[X]) → S) P : S) =
      0 ↔
    Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
⊢ IsFixedPt P.newtonMap x ↔ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
have rw₃ : (aeval x : (a : R[X]) → S) P =
    HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S) (0 : S) ↔
  Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
Tactic: rw [IsFixedPt, newtonMap_apply, sub_eq_self, Ring.inverse_mul_eq_iff_eq_mul _ _ _ h, mul_zero]
-- 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 : IsUnit.{u_2} (M := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S)
rw : P.newtonMap x = x ↔ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
rw₁ :
  x -
        HMul.hMul (α := S) (β := S)
          (Ring.inverse ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
          ((aeval x : (a : R[X]) → S) P : S) =
      x ↔
    Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
rw₂ :
  HMul.hMul (α := S) (β := S)
        (Ring.inverse ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X])) : S)
        ((aeval x : (a : R[X]) → S) P : S) =
      0 ↔
    Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
rw₃ :
  (aeval x : (a : R[X]) → S) P =
      HMul.hMul (α := S) (β := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) P : R[X]) : S) (0 : S) ↔
    Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
⊢ IsFixedPt P.newtonMap x ↔ Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
have rw₄ : Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S) ↔
  Eq.{u_2 + 1} (α := S) ((aeval x : (a : R[X]) → S) P : S) (0 : S)
Tactic: rw [IsFixedPt, newtonMap_apply, sub_eq_self, Ring.inverse_mul_eq_iff_eq_mul _ _ _ h, mul_zero]
-- 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
⊢ 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 : ∀ (d : S)
  (hd :
    eval
        (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))
        (map (algebraMap R S) P) =
      eval (P.newtonMap^[n] x) (map (algebraMap R S) P) +
          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
Tactic: 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)
-- 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 :
  eval
      (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))
      (map (algebraMap R S) P) =
    eval (P.newtonMap^[n] x) (map (algebraMap R S) P) +
        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 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
Tactic: rw [eval_map_algebraMap, eval_map_algebraMap] at hd
Cleared hypotheses: hd