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
⊢ [HenselianLocalRing R,
      ∀ (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₀,
      ∀ {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₀].TFAE
have 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₀
Tactic: tfae_have 3 → 2
  | H => H (residue R) Ideal.Quotient.mk_surjective
-- 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₀
h :
  ∀ (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₀
H : ∀ (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₀ :=
  h
⊢ HenselianLocalRing R
have is_henselian : ∀ (f : R[X]),
  f.Monic →
    ∀ (a₀ : R),
      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: constructor
-- 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₀
h :
  ∀ (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₀
H : ∀ (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₀ :=
  h
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))
⊢ ∃ (a : R), f.IsRoot a ∧ Membership.mem (γ := Ideal R) (maximalIdeal R) (a - a₀)
have H₁ : Eq (α := ResidueField R)
    (((aeval ((residue R : (a : R) → ResidueField R) a₀) : R[X] →ₐ[R] ResidueField R) : (a : R[X]) → ResidueField R) f :
      ResidueField R)
    (0 : ResidueField R) →
  Ne (α := ResidueField R)
      (((aeval ((residue R : (a : R) → ResidueField R) a₀) : R[X] →ₐ[R] ResidueField R) : (a : R[X]) → ResidueField R)
          ((derivative : (a : R[X]) → R[X]) f) :
        ResidueField R)
      (0 : ResidueField R) →
    ∃ (a : R),
      f.IsRoot a ∧
        Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) a : ResidueField R)
          ((residue R : (a : R) → ResidueField R) a₀ : ResidueField R)
Tactic: specialize H f hf (residue R a₀)
Cleared hypotheses: 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₀
h :
  ∀ (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₀
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))
H :
  Eq (α := ResidueField R)
      (((aeval ((residue R : (a : R) → ResidueField R) a₀) : R[X] →ₐ[R] ResidueField R) : (a : R[X]) → ResidueField R)
          f :
        ResidueField R)
      (0 : ResidueField R) →
    Ne (α := ResidueField R)
        (((aeval ((residue R : (a : R) → ResidueField R) a₀) : R[X] →ₐ[R] ResidueField R) : (a : R[X]) → ResidueField R)
            ((derivative : (a : R[X]) → R[X]) f) :
          ResidueField R)
        (0 : ResidueField R) →
      ∃ (a : R),
        f.IsRoot a ∧
          Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) a : ResidueField R)
            ((residue R : (a : R) → ResidueField R) a₀ : ResidueField R)
⊢ ∃ (a : R), f.IsRoot a ∧ Membership.mem (γ := Ideal R) (maximalIdeal R) (a - a₀)
have aux : Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f) ∈ nonunits R → False
Tactic: have aux := flip mem_nonunits_iff.mp 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₀
h :
  ∀ (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₀
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))
H :
  Eq (α := ResidueField R)
      (((aeval ((residue R : (a : R) → ResidueField R) a₀) : R[X] →ₐ[R] ResidueField R) : (a : R[X]) → ResidueField R)
          f :
        ResidueField R)
      (0 : ResidueField R) →
    Ne (α := ResidueField R)
        (((aeval ((residue R : (a : R) → ResidueField R) a₀) : R[X] →ₐ[R] ResidueField R) : (a : R[X]) → ResidueField R)
            ((derivative : (a : R[X]) → R[X]) f) :
          ResidueField R)
        (0 : ResidueField R) →
      ∃ (a : R),
        f.IsRoot a ∧
          Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) a : ResidueField R)
            ((residue R : (a : R) → ResidueField R) a₀ : ResidueField R)
aux : Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f) ∈ nonunits R → False
⊢ ∃ (a : R), f.IsRoot a ∧ Membership.mem (γ := Ideal R) (maximalIdeal R) (a - a₀)
have H₁ : Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) (Polynomial.eval a₀ f) : ResidueField R)
    (0 : ResidueField R) →
  Ne (α := ResidueField R)
      ((residue R : (a : R) → ResidueField R) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) :
        ResidueField R)
      (0 : ResidueField R) →
    ∃ (a : R),
      f.IsRoot a ∧
        Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) a : ResidueField R)
          ((residue R : (a : R) → ResidueField R) a₀ : ResidueField R)
Tactic: simp only [aeval_def, ResidueField.algebraMap_eq, eval₂_at_apply, ←
      Ideal.Quotient.eq_zero_iff_mem, ← IsLocalRing.mem_maximalIdeal] at H h₁ aux
Cleared hypotheses: h₁, H, aux
-- 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₀
h :
  ∀ (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₀
f : R[X]
hf : f.Monic
a₀ : R
h₂ : IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))
H :
  Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) (Polynomial.eval a₀ f) : ResidueField R)
      (0 : ResidueField R) →
    Ne (α := ResidueField R)
        ((residue R : (a : R) → ResidueField R) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) :
          ResidueField R)
        (0 : ResidueField R) →
      ∃ (a : R),
        f.IsRoot a ∧
          Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) a : ResidueField R)
            ((residue R : (a : R) → ResidueField R) a₀ : ResidueField R)
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₀ f) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
    (0 : HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
aux :
  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)) →
    False
⊢ ∃ (a : R), f.IsRoot a ∧ Membership.mem (γ := Ideal R) (maximalIdeal R) (a - a₀)
have is_henselian : ∀ (a : R) (ha₁ : f.IsRoot a)
  (ha₂ :
    Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) a : ResidueField R)
      ((residue R : (a : R) → ResidueField R) a₀ : ResidueField R)),
  ∃ (a : R), f.IsRoot a ∧ Membership.mem (γ := Ideal R) (maximalIdeal R) (a - a₀)
Tactic: obtain ⟨a, ha₁, ha₂⟩ := H h₁ aux
-- 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₀
h :
  ∀ (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₀
f : R[X]
hf : f.Monic
a₀ : R
h₂ : IsUnit (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f))
H :
  Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) (Polynomial.eval a₀ f) : ResidueField R)
      (0 : ResidueField R) →
    Ne (α := ResidueField R)
        ((residue R : (a : R) → ResidueField R) (Polynomial.eval a₀ ((derivative : (a : R[X]) → R[X]) f)) :
          ResidueField R)
        (0 : ResidueField R) →
      ∃ (a : R),
        f.IsRoot a ∧
          Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) a : ResidueField R)
            ((residue R : (a : R) → ResidueField R) a₀ : ResidueField R)
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₀ f) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
    (0 : HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
aux :
  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)) →
    False
a : R
ha₁ : f.IsRoot a
ha₂ :
  Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) a : ResidueField R)
    ((residue R : (a : R) → ResidueField R) a₀ : ResidueField R)
⊢ ∃ (a : R), f.IsRoot a ∧ Membership.mem (γ := Ideal R) (maximalIdeal R) (a - a₀)
have is_henselian : Membership.mem (γ := Ideal R) (maximalIdeal R) (a - a₀)
Tactic: refine ⟨a, ha₁, ?_⟩
-- 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₀
⊢ [HenselianLocalRing R,
      ∀ (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₀,
      ∀ {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₀].TFAE
have 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
Tactic: tfae_have 2 → 1
  | H => by
    constructor
    intro f hf a₀ h₁ h₂
    specialize H f hf (residue R a₀)
    have aux := flip mem_nonunits_iff.mp h₂
    simp only [aeval_def, ResidueField.algebraMap_eq, eval₂_at_apply, ←
      Ideal.Quotient.eq_zero_iff_mem, ← IsLocalRing.mem_maximalIdeal] at H h₁ aux
    obtain ⟨a, ha₁, ha₂⟩ := H h₁ aux
    refine ⟨a, ha₁, ?_⟩
    rw [← Ideal.Quotient.eq_zero_iff_mem]
    rwa [← sub_eq_zero, ← map_sub] at 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₀ : K
h₁ : eval₂ φ a₀ f = 0
h₂ : eval₂ φ a₀ ((derivative : (a : R[X]) → R[X]) f) ≠ 0
⊢ ∃ (a : R), f.IsRoot a ∧ (φ : (a : R) → K) a = a₀
have obtain : ∀ (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)
Tactic: obtain ⟨a₀, rfl⟩ := hφ a₀
Cleared hypotheses: a₀, h₁, h₂