awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsLocalRing R
tfae_3_to_2 :
  ∀
    (a :
      ∀ {K : Type u} [inst_2 : Field K] (φ : R →+* K),
        Surjective (α := R) (β := K) (⇑φ : (a : R) → K) →
          ∀ (f : R[X]),
            f.Monic →
              ∀ (a₀ : K),
                eval₂ φ a₀ f = 0 →
                  eval₂ φ a₀ ((derivative : (a : R[X]) → R[X]) f) ≠ 0 →
                    ∃ (a : R), f.IsRoot a ∧ (φ : (a : R) → K) a = a₀)
    (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R),
        Eq (α := ResidueField R) ((aeval a₀ : (a : R[X]) → ResidueField R) f : ResidueField R) (0 : ResidueField R) →
          Ne (α := ResidueField R)
              ((aeval a₀ : (a : R[X]) → ResidueField R) ((derivative : (a : R[X]) → R[X]) f) : ResidueField R)
              (0 : ResidueField R) →
            ∃ (a : R), f.IsRoot a ∧ (residue R : (a : R) → ResidueField R) a = a₀
tfae_2_to_1 :
  ∀
    (a :
      ∀ (f : R[X]),
        f.Monic →
          ∀ (a₀ : ResidueField R),
            Eq (α := ResidueField R) ((aeval a₀ : (a : R[X]) → ResidueField R) f : ResidueField R)
                (0 : ResidueField R) →
              Ne (α := ResidueField R)
                  ((aeval a₀ : (a : R[X]) → ResidueField R) ((derivative : (a : R[X]) → R[X]) f) : ResidueField R)
                  (0 : ResidueField R) →
                ∃ (a : R), f.IsRoot a ∧ (residue R : (a : R) → ResidueField R) a = a₀),
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective (α := R) (β := K) (⇑φ : (a : R) → K)
f : R[X]
hf : f.Monic
a₀ : R
H :
  Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ f) : K) (0 : K) →
    IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) →
      ∃ (a : R), f.IsRoot a ∧ Eq (α := K) ((φ : (a : R) → K) (a - a₀) : K) (0 : K)
h₁ : Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ f) : K) (0 : K)
h₂ : Ne (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
⊢ ∃ (a : R), f.IsRoot a ∧ Eq (α := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K)
have obtain : ∀ (a : R) (ha₁ : f.IsRoot a) (ha₂ : Eq (α := K) ((φ : (a : R) → K) (a - a₀) : K) (0 : K)),
  ∃ (a : R), f.IsRoot a ∧ Eq (α := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K)
Tactic: obtain ⟨a, ha₁, ha₂⟩ := H h₁ (by
      contrapose h₂
      rwa [← mem_nonunits_iff, ← mem_maximalIdeal, ← ker_eq_maximalIdeal φ hφ,
        RingHom.mem_ker] at h₂)
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsLocalRing R
tfae_3_to_2 :
  ∀
    (a :
      ∀ {K : Type u} [inst_2 : Field K] (φ : R →+* K),
        Surjective (α := R) (β := K) (⇑φ : (a : R) → K) →
          ∀ (f : R[X]),
            f.Monic →
              ∀ (a₀ : K),
                eval₂ φ a₀ f = 0 →
                  eval₂ φ a₀ ((derivative : (a : R[X]) → R[X]) f) ≠ 0 →
                    ∃ (a : R), f.IsRoot a ∧ (φ : (a : R) → K) a = a₀)
    (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R),
        Eq (α := ResidueField R) ((aeval a₀ : (a : R[X]) → ResidueField R) f : ResidueField R) (0 : ResidueField R) →
          Ne (α := ResidueField R)
              ((aeval a₀ : (a : R[X]) → ResidueField R) ((derivative : (a : R[X]) → R[X]) f) : ResidueField R)
              (0 : ResidueField R) →
            ∃ (a : R), f.IsRoot a ∧ (residue R : (a : R) → ResidueField R) a = a₀
tfae_2_to_1 :
  ∀
    (a :
      ∀ (f : R[X]),
        f.Monic →
          ∀ (a₀ : ResidueField R),
            Eq (α := ResidueField R) ((aeval a₀ : (a : R[X]) → ResidueField R) f : ResidueField R)
                (0 : ResidueField R) →
              Ne (α := ResidueField R)
                  ((aeval a₀ : (a : R[X]) → ResidueField R) ((derivative : (a : R[X]) → R[X]) f) : ResidueField R)
                  (0 : ResidueField R) →
                ∃ (a : R), f.IsRoot a ∧ (residue R : (a : R) → ResidueField R) a = a₀),
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective (α := R) (β := K) (⇑φ : (a : R) → K)
f : R[X]
hf : f.Monic
a₀ : R
H :
  Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ f) : K) (0 : K) →
    IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) →
      ∃ (a : R), f.IsRoot a ∧ Eq (α := K) ((φ : (a : R) → K) (a - a₀) : K) (0 : K)
h₁ : Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ f) : K) (0 : K)
h₂ : Ne (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
a : R
ha₁ : f.IsRoot a
ha₂ : Eq (α := K) ((φ : (a : R) → K) (a - a₀) : K) (0 : K)
⊢ ∃ (a : R), f.IsRoot a ∧ Eq (α := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K)
have refine : Eq (α := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K)
Tactic: refine ⟨a, ha₁, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsLocalRing R
tfae_3_to_2 :
  ∀
    (a :
      ∀ {K : Type u} [inst_2 : Field K] (φ : R →+* K),
        Surjective (α := R) (β := K) (⇑φ : (a : R) → K) →
          ∀ (f : R[X]),
            f.Monic →
              ∀ (a₀ : K),
                eval₂ φ a₀ f = 0 →
                  eval₂ φ a₀ ((derivative : (a : R[X]) → R[X]) f) ≠ 0 →
                    ∃ (a : R), f.IsRoot a ∧ (φ : (a : R) → K) a = a₀)
    (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R),
        Eq (α := ResidueField R) ((aeval a₀ : (a : R[X]) → ResidueField R) f : ResidueField R) (0 : ResidueField R) →
          Ne (α := ResidueField R)
              ((aeval a₀ : (a : R[X]) → ResidueField R) ((derivative : (a : R[X]) → R[X]) f) : ResidueField R)
              (0 : ResidueField R) →
            ∃ (a : R), f.IsRoot a ∧ (residue R : (a : R) → ResidueField R) a = a₀
tfae_2_to_1 :
  ∀
    (a :
      ∀ (f : R[X]),
        f.Monic →
          ∀ (a₀ : ResidueField R),
            Eq (α := ResidueField R) ((aeval a₀ : (a : R[X]) → ResidueField R) f : ResidueField R)
                (0 : ResidueField R) →
              Ne (α := ResidueField R)
                  ((aeval a₀ : (a : R[X]) → ResidueField R) ((derivative : (a : R[X]) → R[X]) f) : ResidueField R)
                  (0 : ResidueField R) →
                ∃ (a : R), f.IsRoot a ∧ (residue R : (a : R) → ResidueField R) a = a₀),
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective (α := R) (β := K) (⇑φ : (a : R) → K)
f : R[X]
hf : f.Monic
a₀ : R
H :
  Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ f) : K) (0 : K) →
    IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) →
      ∃ (a : R), f.IsRoot a ∧ Eq (α := K) ((φ : (a : R) → K) (a - a₀) : K) (0 : K)
h₁ : Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ f) : K) (0 : K)
h₂ : Ne (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
a : R
ha₁ : f.IsRoot a
ha₂ : Eq (α := K) ((φ : (a : R) → K) (a - a₀) : K) (0 : K)
⊢ Eq (α := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K)
have rwa : ∀ (ha₂ : HSub.hSub (α := K) (β := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K) = 0),
  Eq (α := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K)
Tactic: rwa [φ.map_sub, sub_eq_zero] at ha₂
Cleared hypotheses: ha₂
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsLocalRing R
tfae_3_to_2 :
  ∀
    (a :
      ∀ {K : Type u} [inst_2 : Field K] (φ : R →+* K),
        Surjective (α := R) (β := K) (⇑φ : (a : R) → K) →
          ∀ (f : R[X]),
            f.Monic →
              ∀ (a₀ : K),
                eval₂ φ a₀ f = 0 →
                  eval₂ φ a₀ ((derivative : (a : R[X]) → R[X]) f) ≠ 0 →
                    ∃ (a : R), f.IsRoot a ∧ (φ : (a : R) → K) a = a₀)
    (f : R[X]),
    f.Monic →
      ∀ (a₀ : ResidueField R),
        Eq (α := ResidueField R) ((aeval a₀ : (a : R[X]) → ResidueField R) f : ResidueField R) (0 : ResidueField R) →
          Ne (α := ResidueField R)
              ((aeval a₀ : (a : R[X]) → ResidueField R) ((derivative : (a : R[X]) → R[X]) f) : ResidueField R)
              (0 : ResidueField R) →
            ∃ (a : R), f.IsRoot a ∧ (residue R : (a : R) → ResidueField R) a = a₀
tfae_2_to_1 :
  ∀
    (a :
      ∀ (f : R[X]),
        f.Monic →
          ∀ (a₀ : ResidueField R),
            Eq (α := ResidueField R) ((aeval a₀ : (a : R[X]) → ResidueField R) f : ResidueField R)
                (0 : ResidueField R) →
              Ne (α := ResidueField R)
                  ((aeval a₀ : (a : R[X]) → ResidueField R) ((derivative : (a : R[X]) → R[X]) f) : ResidueField R)
                  (0 : ResidueField R) →
                ∃ (a : R), f.IsRoot a ∧ (residue R : (a : R) → ResidueField R) a = a₀),
    HenselianLocalRing R
hR : HenselianLocalRing R
K : Type u
_K : Field K
φ : R →+* K
hφ : Surjective (α := R) (β := K) (⇑φ : (a : R) → K)
f : R[X]
hf : f.Monic
a₀ : R
H :
  Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ f) : K) (0 : K) →
    IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) →
      ∃ (a : R), f.IsRoot a ∧ Eq (α := K) ((φ : (a : R) → K) (a - a₀) : K) (0 : K)
h₁ : Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ f) : K) (0 : K)
h₂ : Ne (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
a : R
ha₁ : f.IsRoot a
ha₂ : Eq (α := K) ((φ : (a : R) → K) (a - a₀) : K) (0 : K)
rwa :
  ∀ (ha₂ : HSub.hSub (α := K) (β := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K) = 0),
    Eq (α := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K)
⊢ Eq (α := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K)
have rwa₁ : ∀ (ha₂ : Eq (α := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K)),
  Eq (α := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K)
Tactic: rwa [φ.map_sub, sub_eq_zero] at ha₂
Cleared hypotheses: ha₂
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : HenselianLocalRing R
⊢ LE.le (α := Ideal R) (maximalIdeal R) (Ideal.jacobson ⊥)
have rw : ∀ (b : Ideal R), Membership.mem (γ := Set (Ideal R)) {J : Ideal R | ⊥ ≤ J ∧ J.IsMaximal} b → maximalIdeal R ≤ b
Tactic: rw [Ideal.jacobson, le_sInf_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : f.Monic
a₀ : R
h₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) (Polynomial.eval a₀ f)
h₂ :
  IsUnit (M := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
    ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R)
        (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
⊢ ∃ (a : R), f.IsRoot a ∧ Membership.mem (γ := Ideal R) (maximalIdeal R) (a - a₀)
have refine : IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))
Tactic: refine HenselianLocalRing.is_henselian f hf a₀ h₁ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : f.Monic
a₀ : R
h₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) (Polynomial.eval a₀ f)
h₂ :
  IsUnit (M := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
    ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R)
        (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
⊢ IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))
have contrapose : ∀ (h₂ : ¬IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))),
  ¬IsUnit (M := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
      ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R)
          (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) :
        HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
Tactic: contrapose h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : f.Monic
a₀ : R
h₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) (Polynomial.eval a₀ f)
h₂ : ¬IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))
⊢ ¬IsUnit (M := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
      ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R)
          (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) :
        HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
have h₃ : Eq (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
  ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R)
      (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) :
    HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
  (0 : HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
Tactic: rw [← mem_nonunits_iff, ← IsLocalRing.mem_maximalIdeal, ← Ideal.Quotient.eq_zero_iff_mem] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : HenselianLocalRing R
f : R[X]
hf : f.Monic
a₀ : R
h₁ : Membership.mem (γ := Ideal R) (maximalIdeal R) (Polynomial.eval a₀ f)
h₂ :
  Eq (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
    ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R)
        (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
    (0 : HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
⊢ ¬IsUnit (M := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
      ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R)
          (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) :
        HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
have rw : ¬IsUnit.{u_1} (M := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R)) 0
Tactic: rw [h₂]
-- 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')⁻¹ʳ
⊢ ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ I
have hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
Tactic: have hc : ∀ n, c (n + 1) = c n - f.eval (c n) * (f'.eval (c n))⁻¹ʳ := by
        intro n
        simp only [c]
-- 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')⁻¹ʳ
n : ℕ
⊢ SModEq (R := R) I (c n) a₀
have succ : ∀ (n : ℕ) (ih : SModEq (R := R) I (c n) a₀), SModEq (R := R) I (c (n + 1)) a₀
Tactic: induction n with
        | zero => rfl
        | 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')⁻¹ʳ
n : ℕ
ih : SModEq (R := R) I (c n) a₀
⊢ SModEq (R := R) I (c (n + 1)) a₀
have succ : SModEq (R := R) I (c n + -(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) (a₀ + 0)
Tactic: rw [hc, sub_eq_add_neg, ← add_zero 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')⁻¹ʳ
n : ℕ
ih : SModEq (R := R) I (c n) a₀
⊢ SModEq (R := R) I (c n + -(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) (a₀ + 0)
have succ : SModEq (R := R) I (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) 0
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')⁻¹ʳ
n : ℕ
ih : SModEq (R := R) I (c n) a₀
⊢ SModEq (R := R) I (-(Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ)) 0
have succ : Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ ∈ I
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')⁻¹ʳ
n : ℕ
ih : SModEq (R := R) I (c n) a₀
⊢ Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ ∈ I
have succ : Polynomial.eval (c n) f ∈ I
Tactic: refine I.mul_mem_right _ ?_
-- 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')⁻¹ʳ
n : ℕ
ih : SModEq (R := R) I (c n) a₀
⊢ Polynomial.eval (c n) f ∈ I
have succ : ∀ (h₁ : SModEq (R := R) I (Polynomial.eval a₀ f) 0)
  (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)),
  let f' : R[X] := (derivative : (a : R[X]) → R[X]) f;
  let 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')⁻¹ʳ) (n : ℕ)
    (ih : SModEq (R := R) I (c n) a₀), SModEq (R := R) I (Polynomial.eval (c n) f) 0
Tactic: rw [← SModEq.zero] at h₁ ⊢
Cleared hypotheses: h₁, h₂, f', c, hc, n, ih
-- 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')⁻¹ʳ
⊢ ∃ (a : R), f.IsRoot a ∧ a - a₀ ∈ I
have hc_mod : ∀ (n : ℕ), SModEq (R := R) I (c n) a₀
Tactic: have hc_mod : ∀ n, c n ≡ a₀ [SMOD I] := by
        intro n
        induction n with
        | zero => rfl
        | succ n ih => ?_
        rw [hc, sub_eq_add_neg, ← add_zero a₀]
        refine ih.add ?_
        rw [SModEq.zero, Ideal.neg_mem_iff]
        refine I.mul_mem_right _ ?_
        rw [← SModEq.zero] at h₁ ⊢
        exact (ih.eval f).trans h₁
-- 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₀
n : ℕ
⊢ IsUnit (Polynomial.eval (c n) f')
have this : IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
Tactic: haveI := isLocalHom_of_le_jacobson_bot I (IsAdicComplete.le_jacobson_bot I)
-- 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 (Polynomial.eval (c n) f')
have h : IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (Polynomial.eval (c n) f') : R ⧸ I)
Tactic: apply IsUnit.of_map (Ideal.Quotient.mk I)