awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a : R
b : R ⧸ I
hb : HMul.hMul (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I) b = 1
obtain :
  ∀ (b : R)
    (hb :
      HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
          ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) b : R ⧸ I) =
        1),
    ∃ (b : HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)),
      HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
          ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
          b =
        1
⊢ ∃ (b : HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)),
    HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
        ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
          HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
        b =
      1

Tactic:
obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective b

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a b : R
hb :
  HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
      ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) b : R ⧸ I) =
    1
h₁ :
  HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) (β :=
      HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
      ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
      ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) b :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) =
    1
⊢ ∃ (b : HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)),
    HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
        ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
          HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
        b =
      1

Tactic:
use Ideal.Quotient.mk _ b

Premises used: Ideal.Quotient.mk, DFunLike.coe
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a b : R
hb :
  HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
      ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) b : R ⧸ I) =
    1
h₁ : ∀ (hb : a * b - 1 ∈ I), Membership.mem (γ := Ideal R) (Ideal.jacobson ⊥) (a * b - 1)
⊢ HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) (β :=
      HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
      ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
      ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) b :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) =
    1

Tactic:
rw [← (Ideal.Quotient.mk _).map_one, ← (Ideal.Quotient.mk _).map_mul, Ideal.Quotient.eq] at hb ⊢

Premises used: Ideal.Quotient.mk, RingHom.map_one, Ideal.Quotient.eq, RingHom.map_mul
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a b : R
hb : a * b - 1 ∈ I
⊢ Membership.mem (γ := Ideal R) (Ideal.jacobson ⊥) (a * b - 1)

Tactic:
h hb

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
a b : R
hb : a * b - 1 ∈ I
⊢ Membership.mem (γ := Ideal R) (Ideal.jacobson ⊥) (a * b - 1)

Tactic:
exact h hb
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h_1 : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
⊢ IsUnit (M := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
    ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
      HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))

Tactic:
have : IsUnit (Ideal.Quotient.mk (Ideal.jacobson ⊥) a) := by
    rw [isUnit_iff_exists_inv] at *
    obtain ⟨b, hb⟩ := h
    obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective b
    use Ideal.Quotient.mk _ b
    rw [← (Ideal.Quotient.mk _).map_one, ← (Ideal.Quotient.mk _).map_mul, Ideal.Quotient.eq] at hb ⊢
    exact h hb
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h_1 : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
this :
  IsUnit (M := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
    ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
      HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
map_nonunit :
  ∀ (y : HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
    (h1 :
      HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
          ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
          y =
        1)
    (h2 :
      HMul.hMul (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) y
          ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) =
        1),
    IsUnit a
⊢ IsUnit a

Tactic:
obtain ⟨⟨x, y, h1, h2⟩, rfl : x = _⟩ := this

Premises used: rfl
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h_1 : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
y : HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)
h1 :
  HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
      ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
      y =
    1
h2 :
  HMul.hMul (β := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) y
      ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) =
    1
map_nonunit :
  ∀ (y : R)
    (h1 :
      HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) (β :=
          HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
          ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
          ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) y :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) =
        1)
    (h2 :
      HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) (β :=
          HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
          ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) y :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
          ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
            HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) =
        1),
    IsUnit a
⊢ IsUnit a

Tactic:
obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h_1 : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
y : R
h1 :
  HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) (β :=
      HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
      ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
      ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) y :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) =
    1
h2 :
  HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) (β :=
      HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
      ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) y :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
      ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) =
    1
⊢ ∀ (y_1 : R), IsUnit ((a * y - 1) * y_1 + 1)

Tactic:
rw [← (Ideal.Quotient.mk _).map_mul, ← (Ideal.Quotient.mk _).map_one, Ideal.Quotient.eq,
    Ideal.mem_jacobson_bot] at h1 h2

Premises used: Ideal.Quotient.mk, RingHom.map_one, Ideal.Quotient.eq, RingHom.map_mul, Ideal.mem_jacobson_bot
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h_1 : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
y : R
h1 :
  HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) (β :=
      HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
      ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
      ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) y :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) =
    1
h2 :
  HMul.hMul (α := HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) (β :=
      HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
      ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) y :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥))
      ((Ideal.Quotient.mk (Ideal.jacobson ⊥) : (a : R) → R ⧸ ⊥.jacobson) a :
        HasQuotient.Quotient R (B := Ideal R) (Ideal.jacobson ⊥)) =
    1
h1₁ : ∀ (y_1 : R), IsUnit ((a * y - 1) * y_1 + 1)
⊢ ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)

Tactic:
rw [← (Ideal.Quotient.mk _).map_mul, ← (Ideal.Quotient.mk _).map_one, Ideal.Quotient.eq,
    Ideal.mem_jacobson_bot] at h1 h2

Premises used: Ideal.Quotient.mk, RingHom.map_one, Ideal.Quotient.eq, RingHom.map_mul, Ideal.mem_jacobson_bot
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h_1 : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
y : R
h1 : ∀ (y_1 : R), IsUnit ((a * y - 1) * y_1 + 1)
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
⊢ IsUnit ((a * y - 1) * 1 + 1)

Tactic:
specialize h1 1

Premises used: OfNat.ofNat
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h_1 : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit ((a * y - 1) * 1 + 1)
⊢ IsUnit a ∧ IsUnit y

Tactic:
simpa using h1
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h_1 : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit ((a * y - 1) * 1 + 1)
⊢ IsUnit a ∧ IsUnit y

Tactic:
have h1 : IsUnit a ∧ IsUnit y := by simpa using h1
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h_1 : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1_1 : IsUnit ((a * y - 1) * 1 + 1)
h1 : IsUnit a ∧ IsUnit y
⊢ IsUnit a

Tactic:
h1.1

Premises used: And.left
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h_1 : I ≤ Ideal.jacobson ⊥
a : R
h : IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I)
y : R
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1_1 : IsUnit ((a * y - 1) * 1 + 1)
h1 : IsUnit a ∧ IsUnit y
⊢ IsUnit a

Tactic:
exact h1.1

Premises used: And.left
-- Module: Mathlib.RingTheory.Henselian
Goal:
K : Type u_1
inst : Field K
f : K[X]
h : f.Monic
a₀ : K
h₁ : Membership.mem (γ := Ideal K) (maximalIdeal K) (Polynomial.eval a₀ f)
h_1 : IsUnit (Polynomial.eval a₀ ((derivative : (a : K[X]) → K[X]) f))
simp : ∀ (h₁ : Polynomial.eval a₀ f = 0), ∃ (a : K), f.IsRoot a ∧ a - a₀ = 0
⊢ ∃ (a : K), f.IsRoot a ∧ Membership.mem (γ := Ideal K) (maximalIdeal K) (a - a₀)

Tactic:
simp only [(maximalIdeal K).eq_bot_of_prime, Ideal.mem_bot] at h₁ ⊢

Premises used: Ideal.mem_bot, IsLocalRing.maximalIdeal, Ideal.eq_bot_of_prime
-- Module: Mathlib.RingTheory.Henselian
Goal:
K : Type u_1
inst : Field K
f : K[X]
h : f.Monic
a₀ : K
h_1 : IsUnit (Polynomial.eval a₀ ((derivative : (a : K[X]) → K[X]) f))
h₁ : Polynomial.eval a₀ f = 0
⊢ ∃ (a : K), f.IsRoot a ∧ a - a₀ = 0

Tactic:
⟨a₀, h₁, sub_self _⟩

Premises used: sub_self, And.intro, Exists.intro
-- Module: Mathlib.RingTheory.Henselian
Goal:
K : Type u_1
inst : Field K
f : K[X]
h : f.Monic
a₀ : K
h_1 : IsUnit (Polynomial.eval a₀ ((derivative : (a : K[X]) → K[X]) f))
h₁ : Polynomial.eval a₀ f = 0
⊢ ∃ (a : K), f.IsRoot a ∧ a - a₀ = 0

Tactic:
exact ⟨a₀, h₁, sub_self _⟩
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u
inst : CommRing R
inst_1 : IsLocalRing R
⊢ ∀ {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₀

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u
inst : CommRing R
inst_1 : IsLocalRing 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₀

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u
inst : CommRing R
inst_1 : IsLocalRing R
⊢ ∀
    (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:
3 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.RingTheory.Henselian
Goal:
R : Type u
inst : CommRing R
inst_1 : IsLocalRing R
⊢ ∀
    (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
-- 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₀
⊢ ∀ (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:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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₀
⊢ HenselianLocalRing R

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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₀
⊢ ∀
    (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:
2 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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₀
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
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₀)
⊢ HenselianLocalRing R

Tactic:
constructor