-- Module: Mathlib.RingTheory.Henselian
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)
is_henselian :
  ∀
    (ha₂ :
      HSub.hSub (α := ResidueField R) (β := ResidueField R) ((residue R : (a : R) → ResidueField R) a : ResidueField R)
          ((residue R : (a : R) → ResidueField R) a₀ : ResidueField R) =
        0),
    Eq (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
      ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R) (a - a₀) :
        HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
      (0 : HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
is_henselian₁ is_henselian₂ is_henselian₃ is_henselian₄ :
  ∀
    (ha₂ :
      Eq (α := ResidueField R) ((residue R : (a : R) → ResidueField R) (a - a₀) : ResidueField R) (0 : ResidueField R)),
    Eq (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
      ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R) (a - a₀) :
        HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
      (0 : HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
⊢ Eq (α := HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
    ((Ideal.Quotient.mk (maximalIdeal R) : (a : R) → R ⧸ maximalIdeal R) (a - a₀) :
      HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))
    (0 : HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R : Ideal R))

Tactic:
rwa [← sub_eq_zero, ← map_sub] at ha₂

Premises used: map_sub, sub_eq_zero