awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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')
⊢ ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ I
have hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
Tactic: have hfcI : ∀ n, f.eval (c n) ∈ I ^ (n + 1) := by
        intro n
        induction n with
        | zero => simpa only [Nat.rec_zero, zero_add, pow_one] using h₁
        | succ n ih => ?_
        rw [← taylor_eval_sub (c n), hc, sub_eq_add_neg, sub_eq_add_neg,
          add_neg_cancel_comm]
        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 _ _)]
        swap
        · intro i
          rw [zero_mul]
        refine Ideal.add_mem _ ?_ ?_
        · 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]
          exact Ideal.zero_mem _
        · refine Submodule.sum_mem _ ?_
          simp only [Finset.mem_Ico]
          rintro i ⟨h2i, _⟩
          have aux : n + 2 ≤ i * (n + 1) := by trans 2 * (n + 1) <;> nlinarith only [h2i]
          refine Ideal.mul_mem_left _ _ (Ideal.pow_le_pow_right aux ?_)
          rw [pow_mul']
          exact Ideal.pow_mem_pow ((Ideal.neg_mem_iff _).2 <| Ideal.mul_mem_right _ _ ih) _
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m n : ℕ
hmn : m ≤ n
⊢ SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
have rw : SModEq (R := R) (I ^ m) (c m) (c n)
Tactic: rw [← Ideal.one_eq_top, Ideal.smul_eq_mul, mul_one]
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m n : ℕ
hmn : m ≤ n
⊢ SModEq (R := R) (I ^ m) (c m) (c n)
have obtain : ∀ (k : ℕ) (hmn : m ≤ m + k), SModEq (R := R) (I ^ m) (c m) (c (m + k))
Tactic: obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
Cleared hypotheses: n, hmn
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m : ℕ
⊢ SModEq (R := R) (I ^ m) (c m) (c (m + 0))
have zero : SModEq (R := R) (I ^ m) (c m) (c m)
Tactic: rw [add_zero]
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
⊢ SModEq (R := R) (I ^ m) (c m) (c (m + k))
have succ : ∀ (k : ℕ) (ih : SModEq (R := R) (I ^ m) (c m) (c (m + k))), SModEq (R := R) (I ^ m) (c m) (c (m + (k + 1)))
Tactic: induction k with
        | zero => rw [add_zero]
        | succ k ih => ?_
Cleared hypotheses: k
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : SModEq (R := R) (I ^ m) (c m) (c (m + k))
⊢ SModEq (R := R) (I ^ m) (c m) (c (m + (k + 1)))
have succ : SModEq (R := R) (I ^ m) (c m + 0) (c (m + k) + -(Polynomial.eval (c (m + k)) f * (Polynomial.eval (c (m + k)) f')⁻¹ʳ))
Tactic: rw [← add_assoc, hc, ← add_zero (c m), sub_eq_add_neg]
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : SModEq (R := R) (I ^ m) (c m) (c (m + k))
⊢ SModEq (R := R) (I ^ m) (c m + 0) (c (m + k) + -(Polynomial.eval (c (m + k)) f * (Polynomial.eval (c (m + k)) f')⁻¹ʳ))
have succ : SModEq (R := R) (I ^ m) 0 (-(Polynomial.eval (c (m + k)) f * (Polynomial.eval (c (m + k)) f')⁻¹ʳ))
Tactic: refine ih.add ?_
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : SModEq (R := R) (I ^ m) (c m) (c (m + k))
⊢ SModEq (R := R) (I ^ m) 0 (-(Polynomial.eval (c (m + k)) f * (Polynomial.eval (c (m + k)) f')⁻¹ʳ))
have succ : SModEq (R := R) (I ^ m) (-(Polynomial.eval (c (m + k)) f * (Polynomial.eval (c (m + k)) f')⁻¹ʳ)) 0
Tactic: symm
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : SModEq (R := R) (I ^ m) (c m) (c (m + k))
⊢ SModEq (R := R) (I ^ m) (-(Polynomial.eval (c (m + k)) f * (Polynomial.eval (c (m + k)) f')⁻¹ʳ)) 0
have succ : Polynomial.eval (c (m + k)) f * (Polynomial.eval (c (m + k)) f')⁻¹ʳ ∈ I ^ m
Tactic: rw [SModEq.zero, Ideal.neg_mem_iff]
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : SModEq (R := R) (I ^ m) (c m) (c (m + k))
⊢ Polynomial.eval (c (m + k)) f * (Polynomial.eval (c (m + k)) f')⁻¹ʳ ∈ I ^ m
have succ : m ≤ m + k + 1
Tactic: refine Ideal.mul_mem_right _ _ (Ideal.pow_le_pow_right ?_ (hfcI _))
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
m k : ℕ
ih : SModEq (R := R) (I ^ m) (c m) (c (m + k))
⊢ m ≤ m + k + 1
have succ : m ≤ m + (k + 1)
Tactic: rw [add_assoc]
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
⊢ ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ I
have aux : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
Tactic: have aux : ∀ m n, m ≤ n → c m ≡ c n [SMOD (I ^ m • ⊤ : Ideal R)] := by
        intro m n hmn
        rw [← Ideal.one_eq_top, Ideal.smul_eq_mul, mul_one]
        obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
        clear hmn
        induction k with
        | zero => rw [add_zero]
        | succ k ih => ?_
        rw [← add_assoc, hc, ← add_zero (c m), sub_eq_add_neg]
        refine ih.add ?_
        symm
        rw [SModEq.zero, Ideal.neg_mem_iff]
        refine Ideal.mul_mem_right _ _ (Ideal.pow_le_pow_right ?_ (hfcI _))
        rw [add_assoc]
        exact le_self_add
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
⊢ ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ I
have obtain : ∀ (a : R) (ha : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (c n) a),
  ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ I
Tactic: obtain ⟨a, ha⟩ := IsPrecomplete.prec' c (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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
a : R
ha : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (c n) a
⊢ ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ I
have refine_1 : f.IsRoot a
Tactic: refine ⟨a, ?_, ?_⟩
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
a : R
ha : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (c n) a
refine_1 : f.IsRoot a
⊢ ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ I
have refine_2 : a - a₀ ∈ I
Tactic: refine ⟨a, ?_, ?_⟩
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
a : R
ha : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (c n) a
⊢ f.IsRoot a
have refine_1 : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) (Polynomial.eval a f) 0
Tactic: suffices ∀ n, f.eval a ≡ 0 [SMOD (I ^ n • ⊤ : Ideal R)] by exact IsHausdorff.haus' _ this
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
a : R
ha : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (c n) a
n : ℕ
⊢ SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) (Polynomial.eval a f) 0
have ha₁ : SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (c n) a
Tactic: specialize ha n
Cleared hypotheses: ha
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
a : R
n : ℕ
ha : SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (c n) a
⊢ SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) (Polynomial.eval a f) 0
have refine_1 : ∀ (ha : SModEq (R := R) (I ^ n) (c n) a), SModEq (R := R) (I ^ n) (Polynomial.eval a f) 0
Tactic: rw [← Ideal.one_eq_top, Ideal.smul_eq_mul, mul_one] at ha ⊢
Cleared hypotheses: ha
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
a : R
n : ℕ
ha : SModEq (R := R) (I ^ n) (c n) a
⊢ SModEq (R := R) (I ^ n) (Polynomial.eval a f) 0
have refine_1 : SModEq (R := R) (I ^ n) (Polynomial.eval (c n) f) 0
Tactic: refine (ha.symm.eval f).trans ?_
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
a : R
n : ℕ
ha : SModEq (R := R) (I ^ n) (c n) a
⊢ SModEq (R := R) (I ^ n) (Polynomial.eval (c n) f) 0
have refine_1 : Polynomial.eval (c n) f ∈ I ^ n
Tactic: rw [SModEq.zero]
-- 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')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → SModEq (R := R) (HSMul.hSMul (β := Ideal R) (I ^ m) ⊤) (c m) (c n)
a : R
ha : ∀ (n : ℕ), SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ n) ⊤) (c n) a
⊢ a - a₀ ∈ I
have ha₁ : SModEq (R := R) (HSMul.hSMul (β := Submodule R R) (I ^ HAdd.hAdd (α := ℕ) 0 1) ⊤) (c (HAdd.hAdd (α := ℕ) 0 1)) a
Tactic: specialize ha (0 + 1)
Cleared hypotheses: ha