awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
n : ℕ
this : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
⊢ IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval (c n) f') : R ⧸ I)
have h : Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval (c n) f') : R ⧸ I)
  ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
Tactic: convert! h₂ using 1
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
⊢ ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ I
have hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
Tactic: have hf'c : ∀ n, IsUnit (f'.eval (c n)) := by
        intro n
        haveI := isLocalHom_of_le_jacobson_bot I (IsAdicComplete.le_jacobson_bot I)
        apply IsUnit.of_map (Ideal.Quotient.mk I)
        convert! h₂ using 1
        exact SModEq.def.mp ((hc_mod n).eval _)
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
⊢ Polynomial.eval (c n) f ∈ I ^ (n + 1)
have succ : ∀ (n : ℕ) (ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)), Polynomial.eval (c (n + 1)) f ∈ I ^ (n + 1 + 1)
Tactic: induction n with
        | zero => simpa only [Nat.rec_zero, zero_add, pow_one] using h₁
        | succ n ih => ?_
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ Polynomial.eval (c (n + 1)) f ∈ I ^ (n + 1 + 1)
have succ : Polynomial.eval (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ((taylor (c n) : (a : R[X]) → R[X]) f) ∈
  I ^ (n + 1 + 1)
Tactic: rw [← taylor_eval_sub (c n), hc, sub_eq_add_neg, sub_eq_add_neg,
          add_neg_cancel_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ Polynomial.eval (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ((taylor (c n) : (a : R[X]) → R[X]) f) ∈
    I ^ (n + 1 + 1)
have succ : HAdd.hAdd (α := R)
    (∑ k ∈ Finset.range 2,
      coeff ((taylor (c n) : (a : R[X]) → R[X]) f) k * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k)
    (∑ k ∈ Finset.Ico 2 (natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2),
      coeff ((taylor (c n) : (a : R[X]) → R[X]) f) k *
        (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k) ∈
  I ^ (n + 1 + 1)
Tactic: rw [eval_eq_sum, sum_over_range' _ _ _ (lt_add_of_pos_right _ zero_lt_two), ←
          Finset.sum_range_add_sum_Ico _ (Nat.le_add_left _ _)]
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
succ :
  HAdd.hAdd (α := R)
      (∑ k ∈ Finset.range 2,
        coeff ((taylor (c n) : (a : R[X]) → R[X]) f) k *
          (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k)
      (∑ k ∈ Finset.Ico 2 (natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2),
        coeff ((taylor (c n) : (a : R[X]) → R[X]) f) k *
          (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k) ∈
    I ^ (n + 1 + 1)
⊢ Polynomial.eval (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ((taylor (c n) : (a : R[X]) → R[X]) f) ∈
    I ^ (n + 1 + 1)
have rw : ∀ (n_1 : ℕ), 0 * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ n_1 = 0
Tactic: rw [eval_eq_sum, sum_over_range' _ _ _ (lt_add_of_pos_right _ zero_lt_two), ←
          Finset.sum_range_add_sum_Ico _ (Nat.le_add_left _ _)]
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
⊢ 0 * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ i = 0
have rw : Eq.{u_1 + 1} (α := R) 0 0
Tactic: rw [zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ HAdd.hAdd (α := R)
      (∑ k ∈ Finset.range 2,
        coeff ((taylor (c n) : (a : R[X]) → R[X]) f) k *
          (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k)
      (∑ k ∈ Finset.Ico 2 (natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2),
        coeff ((taylor (c n) : (a : R[X]) → R[X]) f) k *
          (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k) ∈
    I ^ (n + 1 + 1)
have succ : ∑ k ∈ Finset.range 2,
    coeff ((taylor (c n) : (a : R[X]) → R[X]) f) k * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k ∈
  I ^ (n + 1 + 1)
Tactic: refine Ideal.add_mem _ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
succ :
  ∑ k ∈ Finset.range 2,
      coeff ((taylor (c n) : (a : R[X]) → R[X]) f) k *
        (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k ∈
    I ^ (n + 1 + 1)
⊢ HAdd.hAdd (α := R)
      (∑ k ∈ Finset.range 2,
        coeff ((taylor (c n) : (a : R[X]) → R[X]) f) k *
          (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k)
      (∑ k ∈ Finset.Ico 2 (natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2),
        coeff ((taylor (c n) : (a : R[X]) → R[X]) f) k *
          (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k) ∈
    I ^ (n + 1 + 1)
have succ₁ : ∑ k ∈ Finset.Ico 2 (natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2),
    coeff ((taylor (c n) : (a : R[X]) → R[X]) f) k * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k ∈
  I ^ (n + 1 + 1)
Tactic: refine Ideal.add_mem _ ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∑ k ∈ Finset.range 2,
      coeff ((taylor (c n) : (a : R[X]) → R[X]) f) k *
        (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k ∈
    I ^ (n + 1 + 1)
have succ : 0 ∈ I ^ (n + 1 + 1)
Tactic: rw [← one_add_one_eq_two, Finset.sum_range_succ, Finset.range_one, Finset.sum_singleton,
            taylor_coeff_zero, taylor_coeff_one, pow_zero, pow_one, mul_one, mul_neg,
            mul_left_comm, Ring.mul_inverse_cancel _ (hf'c n), mul_one, add_neg_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∑ k ∈ Finset.Ico 2 (natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2),
      coeff ((taylor (c n) : (a : R[X]) → R[X]) f) k *
        (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ k ∈
    I ^ (n + 1 + 1)
have succ : ∀ c_1 ∈ Finset.Ico 2 (natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2),
  coeff ((taylor (c n) : (a : R[X]) → R[X]) f) c_1 *
      (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ c_1 ∈
    I ^ (n + 1 + 1)
Tactic: refine Submodule.sum_mem _ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∀ c_1 ∈ Finset.Ico 2 (natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2),
    coeff ((taylor (c n) : (a : R[X]) → R[X]) f) c_1 *
        (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ c_1 ∈
      I ^ (n + 1 + 1)
have succ : ∀ (c_1 : ℕ),
  2 ≤ c_1 ∧ c_1 < natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2 →
    coeff ((taylor (c n) : (a : R[X]) → R[X]) f) c_1 *
        (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ c_1 ∈
      I ^ (n + 1 + 1)
Tactic: simp only [Finset.mem_Ico]
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right : i < natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2
⊢ n + 2 ≤ i * (n + 1)
have trans : n + 2 ≤ 2 * (n + 1)
Tactic: trans 2 * (n + 1)
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right : i < natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2
trans : n + 2 ≤ 2 * (n + 1)
⊢ n + 2 ≤ i * (n + 1)
have trans₁ : 2 * (n + 1) ≤ i * (n + 1)
Tactic: trans 2 * (n + 1)
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right : i < natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2
⊢ n + 2 ≤ 2 * (n + 1)
have nlinarith : 2 * (n + 1) < n + 2 →
  -1 + HSub.hSub (α := ℤ) 0 (↑n : ℤ) + (2 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 - HAdd.hAdd (α := ℤ) (↑n : ℤ) 2) = 0
Tactic: nlinarith only [h2i]
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right : i < natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2
⊢ 2 * (n + 1) ≤ i * (n + 1)
have nlinarith : i * (n + 1) < 2 * (n + 1) →
  -1 + ((↑i : ℤ) * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + 1 - 2 * HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) +
        HSub.hSub (α := ℤ) 2 (↑i : ℤ) +
      (0 - HSub.hSub (α := ℤ) 0 (↑n : ℤ) * HSub.hSub (α := ℤ) 2 (↑i : ℤ)) =
    0
Tactic: nlinarith only [h2i]
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right : i < natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2
⊢ coeff ((taylor (c n) : (a : R[X]) → R[X]) f) i * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ i ∈
    I ^ (n + 1 + 1)
have aux : n + 2 ≤ i * (n + 1)
Tactic: have aux : n + 2 ≤ i * (n + 1) := by trans 2 * (n + 1) <;> nlinarith only [h2i]
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right : i < natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2
aux : n + 2 ≤ i * (n + 1)
⊢ coeff ((taylor (c n) : (a : R[X]) → R[X]) f) i * (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ i ∈
    I ^ (n + 1 + 1)
have succ : (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ i ∈ I ^ (i * (n + 1))
Tactic: refine Ideal.mul_mem_left _ _ (Ideal.pow_le_pow_right aux ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsAdicComplete I R
f : R[X]
h : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ :
  IsUnit (M := R ⧸ I)
    ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : R ⧸ I)
f' : R[X] := (derivative : (a : R[X]) → R[X]) f
c : ℕ → R :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ R) n a₀ fun (x : ℕ) (b : R) ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
n : ℕ
ih : Polynomial.eval (c n) f ∈ I ^ (n + 1)
i : ℕ
h2i : 2 ≤ i
right : i < natDegree.{u_1} (R := R) ((taylor (c n) : (a : R[X]) → R[X]) f) + 2
aux : n + 2 ≤ i * (n + 1)
⊢ (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ i ∈ I ^ (i * (n + 1))
have succ : (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) ^ i ∈ (I ^ (n + 1)) ^ i
Tactic: rw [pow_mul']