awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
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₁ : eval₂ φ ((φ : (a : R) → K) a₀) f = 0
h₂ : eval₂ φ ((φ : (a : R) → K) a₀) ((derivative : (a : R[X]) → R[X]) f) ≠ 0
⊢ ∃ (a : R), f.IsRoot a ∧ Eq (α := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K)
have H : Membership.mem (γ := Ideal R) (maximalIdeal R) (Polynomial.eval a₀ f) →
  IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) →
    ∃ (a : R), f.IsRoot a ∧ Membership.mem (γ := Ideal R) (maximalIdeal R) (a - a₀)
Tactic: have H := HenselianLocalRing.is_henselian f hf a₀
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
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₁ : eval₂ φ ((φ : (a : R) → K) a₀) f = 0
h₂ : eval₂ φ ((φ : (a : R) → K) a₀) ((derivative : (a : R[X]) → R[X]) f) ≠ 0
H :
  Membership.mem (γ := Ideal R) (maximalIdeal R) (Polynomial.eval a₀ f) →
    IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) →
      ∃ (a : R), f.IsRoot a ∧ Membership.mem (γ := Ideal R) (maximalIdeal R) (a - a₀)
⊢ ∃ (a : R), f.IsRoot a ∧ Eq (α := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K)
have 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)
Tactic: simp only [← ker_eq_maximalIdeal φ hφ, eval₂_at_apply, RingHom.mem_ker] at H h₁ h₂
Cleared hypotheses: h₁, h₂, H
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
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₁ : eval₂ φ ((φ : (a : R) → K) a₀) f = 0
h₂ : eval₂ φ ((φ : (a : R) → K) a₀) ((derivative : (a : R[X]) → R[X]) f) ≠ 0
H :
  Membership.mem (γ := Ideal R) (maximalIdeal R) (Polynomial.eval a₀ f) →
    IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) →
      ∃ (a : R), f.IsRoot a ∧ Membership.mem (γ := Ideal R) (maximalIdeal R) (a - a₀)
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)
⊢ ∃ (a : R), f.IsRoot a ∧ Eq (α := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K)
have h₃ : Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ f) : K) (0 : K)
Tactic: simp only [← ker_eq_maximalIdeal φ hφ, eval₂_at_apply, RingHom.mem_ker] at H h₁ h₂
Cleared hypotheses: h₁, h₂, H
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
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₁ : eval₂ φ ((φ : (a : R) → K) a₀) f = 0
h₂ : eval₂ φ ((φ : (a : R) → K) a₀) ((derivative : (a : R[X]) → R[X]) f) ≠ 0
H :
  Membership.mem (γ := Ideal R) (maximalIdeal R) (Polynomial.eval a₀ f) →
    IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) →
      ∃ (a : R), f.IsRoot a ∧ Membership.mem (γ := Ideal R) (maximalIdeal R) (a - a₀)
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)
⊢ ∃ (a : R), f.IsRoot a ∧ Eq (α := K) ((φ : (a : R) → K) a : K) ((φ : (a : R) → K) a₀ : K)
have h₄ : Ne (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
Tactic: simp only [← ker_eq_maximalIdeal φ hφ, eval₂_at_apply, RingHom.mem_ker] at H h₁ h₂
Cleared hypotheses: h₁, h₂, 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)
⊢ 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))),
  Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
Tactic: contrapose h₂
Cleared hypotheses: 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₂ : ¬IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))
⊢ Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
have rwa : ∀ (h₂ : Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f) ∈ nonunits R),
  Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
Tactic: rwa [← mem_nonunits_iff, ← mem_maximalIdeal, ← ker_eq_maximalIdeal φ hφ,
        RingHom.mem_ker] at h₂
Cleared hypotheses: 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₂ : ¬IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))
rwa :
  ∀ (h₂ : Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f) ∈ nonunits R),
    Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
⊢ Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
have rwa₁ : ∀ (h₂ : Membership.mem (γ := Ideal R) (maximalIdeal R) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))),
  Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
Tactic: rwa [← mem_nonunits_iff, ← mem_maximalIdeal, ← ker_eq_maximalIdeal φ hφ,
        RingHom.mem_ker] at h₂
Cleared hypotheses: 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₂ : ¬IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))
rwa :
  ∀ (h₂ : Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f) ∈ nonunits R),
    Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
rwa₁ :
  ∀ (h₂ : Membership.mem (γ := Ideal R) (maximalIdeal R) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))),
    Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
⊢ Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
have rwa₂ : ∀ (h₂ : Membership.mem (γ := Ideal R) (RingHom.ker φ) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))),
  Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
Tactic: rwa [← mem_nonunits_iff, ← mem_maximalIdeal, ← ker_eq_maximalIdeal φ hφ,
        RingHom.mem_ker] at h₂
Cleared hypotheses: 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₂ : ¬IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))
rwa :
  ∀ (h₂ : Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f) ∈ nonunits R),
    Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
rwa₁ :
  ∀ (h₂ : Membership.mem (γ := Ideal R) (maximalIdeal R) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))),
    Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
rwa₂ :
  ∀ (h₂ : Membership.mem (γ := Ideal R) (RingHom.ker φ) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))),
    Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
⊢ Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
have rwa₃ : ∀ (h₂ : Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)),
  Eq (α := K) ((φ : (a : R) → K) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) : K) (0 : K)
Tactic: rwa [← mem_nonunits_iff, ← mem_maximalIdeal, ← ker_eq_maximalIdeal φ hφ,
        RingHom.mem_ker] at h₂
Cleared hypotheses: h₂