awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
x : R⟦Γ⟧
x0 : x ≠ 0
h :
  HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x *
      (SummableFamily.powers
          (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1
rw :
  x *
      HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧)
        (SummableFamily.powers
            (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1
⊢ x * x⁻¹ = 1
have rw₁ : HMul.hMul (β := R⟦Γ⟧) x ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) *
    (SummableFamily.powers
        (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
  1
Tactic: rw [inv_def, ← mul_assoc, mul_comm x, h]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
x : R⟦Γ⟧
x0 : x ≠ 0
h :
  HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x *
      (SummableFamily.powers
          (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1
rw :
  x *
      HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧)
        (SummableFamily.powers
            (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1
rw₁ :
  HMul.hMul (β := R⟦Γ⟧) x ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) *
      (SummableFamily.powers
          (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1
rw₂ :
  HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x *
      (SummableFamily.powers
          (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x)).hsum =
    1
⊢ x * x⁻¹ = 1
have rw₃ : Eq (α := R⟦Γ⟧) 1 1
Tactic: rw [inv_def, ← mul_assoc, mul_comm x, h]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
q : ℚ≥0
x : R⟦Γ⟧
⊢ q • x = (↑q : R⟦Γ⟧) * x
have coeff : ∀ (x_1 : Γ), (q • x).coeff x_1 = ((↑q : R⟦Γ⟧) * x).coeff x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommGroup Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
q : ℚ
x : R⟦Γ⟧
⊢ q • x = (↑q : R⟦Γ⟧) * x
have coeff : ∀ (x_1 : Γ), (q • x).coeff x_1 = ((↑q : R⟦Γ⟧) * x).coeff x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Valuation (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have pos : ∀ (hx : x = 0), (x * y).orderTop = x.orderTop + y.orderTop
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Valuation (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
pos : ∀ (hx : x = 0), (x * y).orderTop = x.orderTop + y.orderTop
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have neg : ∀ (hx : ¬x = 0), (x * y).orderTop = x.orderTop + y.orderTop
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Valuation (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have pos : ∀ (hy : y = 0), (x * y).orderTop = x.orderTop + y.orderTop
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Valuation (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
pos : ∀ (hy : y = 0), (x * y).orderTop = x.orderTop + y.orderTop
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have neg : ∀ (hy : ¬y = 0), (x * y).orderTop = x.orderTop + y.orderTop
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Valuation (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have neg : (x * y).orderTop = (↑x.order : WithTop Γ) + y.orderTop
Tactic: rw [← order_eq_orderTop_of_ne_zero hx, ← order_eq_orderTop_of_ne_zero hy,
      ← order_eq_orderTop_of_ne_zero (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
      order_mul hx hy]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Valuation (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
neg : (x * y).orderTop = (↑x.order : WithTop Γ) + y.orderTop
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have neg₁ : (x * y).orderTop = (↑x.order : WithTop Γ) + (↑y.order : WithTop Γ)
Tactic: rw [← order_eq_orderTop_of_ne_zero hx, ← order_eq_orderTop_of_ne_zero hy,
      ← order_eq_orderTop_of_ne_zero (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
      order_mul hx hy]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Valuation (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
neg : (x * y).orderTop = (↑x.order : WithTop Γ) + y.orderTop
neg₁ : (x * y).orderTop = (↑x.order : WithTop Γ) + (↑y.order : WithTop Γ)
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have neg₂ : (↑(x * y).order : WithTop Γ) = (↑x.order : WithTop Γ) + (↑y.order : WithTop Γ)
Tactic: rw [← order_eq_orderTop_of_ne_zero hx, ← order_eq_orderTop_of_ne_zero hy,
      ← order_eq_orderTop_of_ne_zero (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
      order_mul hx hy]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Valuation (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
neg : (x * y).orderTop = (↑x.order : WithTop Γ) + y.orderTop
neg₁ : (x * y).orderTop = (↑x.order : WithTop Γ) + (↑y.order : WithTop Γ)
neg₂ : (↑(x * y).order : WithTop Γ) = (↑x.order : WithTop Γ) + (↑y.order : WithTop Γ)
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have neg₃ : (↑(x * y).order : WithTop Γ) = (↑(x.order + y.order) : WithTop Γ)
Tactic: rw [← order_eq_orderTop_of_ne_zero hx, ← order_eq_orderTop_of_ne_zero hy,
      ← order_eq_orderTop_of_ne_zero (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
      order_mul hx hy]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Valuation (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
neg : (x * y).orderTop = (↑x.order : WithTop Γ) + y.orderTop
neg₁ : (x * y).orderTop = (↑x.order : WithTop Γ) + (↑y.order : WithTop Γ)
neg₂ : (↑(x * y).order : WithTop Γ) = (↑x.order : WithTop Γ) + (↑y.order : WithTop Γ)
neg₃ : (↑(x * y).order : WithTop Γ) = (↑(x.order + y.order) : WithTop Γ)
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have neg₄ : (x * y).order = x.order + y.order
Tactic: rw [← order_eq_orderTop_of_ne_zero hx, ← order_eq_orderTop_of_ne_zero hy,
      ← order_eq_orderTop_of_ne_zero (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
      order_mul hx hy]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Valuation (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : AddCancelCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
inst_4 : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
neg : (x * y).orderTop = (↑x.order : WithTop Γ) + y.orderTop
neg₁ : (x * y).orderTop = (↑x.order : WithTop Γ) + (↑y.order : WithTop Γ)
neg₂ : (↑(x * y).order : WithTop Γ) = (↑x.order : WithTop Γ) + (↑y.order : WithTop Γ)
neg₃ : (↑(x * y).order : WithTop Γ) = (↑(x.order + y.order) : WithTop Γ)
neg₄ : (x * y).order = x.order + y.order
⊢ (x * y).orderTop = x.orderTop + y.orderTop
have neg₅ : x.order + y.order = x.order + y.order
Tactic: rw [← order_eq_orderTop_of_ne_zero hx, ← order_eq_orderTop_of_ne_zero hy,
      ← order_eq_orderTop_of_ne_zero (mul_ne_zero hx hy), ← WithTop.coe_add, WithTop.coe_eq_coe,
      order_mul hx hy]
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h : I ≤ Ideal.jacobson ⊥
⊢ IsLocalHom (R := R) (S := R ⧸ I) (F := R →+* R ⧸ I) (Ideal.Quotient.mk I)
have map_nonunit : ∀ (a : R), IsUnit (M := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I) → IsUnit a
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
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 ⊥))
have rw : ∀ (h : ∃ (b : R ⧸ I), HMul.hMul (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I) 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: rw [isUnit_iff_exists_inv] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
h_1 : I ≤ Ideal.jacobson ⊥
a : R
h : ∃ (b : R ⧸ I), HMul.hMul (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I) 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
have obtain : ∀ (b : R ⧸ I) (hb : HMul.hMul (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) a : R ⧸ I) 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, hb⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
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
⊢ ∃ (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
have 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
Tactic: obtain ⟨b, rfl⟩ := Ideal.Quotient.mk_surjective b
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
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
⊢ ∃ (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
have 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
Tactic: use Ideal.Quotient.mk _ b
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
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
⊢ 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
have h₁ : ∀ (hb : a * b - 1 ∈ I), Membership.mem (γ := Ideal R) (Ideal.jacobson ⊥) (a * b - 1)
Tactic: rw [← (Ideal.Quotient.mk _).map_one, ← (Ideal.Quotient.mk _).map_mul, Ideal.Quotient.eq] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
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 a
have 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 ⊥))
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
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
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 ⊥))
⊢ IsUnit a
have 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
Tactic: obtain ⟨⟨x, y, h1, h2⟩, rfl : x = _⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
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
⊢ IsUnit a
have 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
Tactic: obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective y
Cleared hypotheses: y, h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
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
⊢ IsUnit a
have h1₁ : ∀ (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
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
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)
⊢ IsUnit a
have h2₁ : ∀ (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
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
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
have h1₁ : IsUnit ((a * y - 1) * 1 + 1)
Tactic: specialize h1 1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (hypothesis)
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
have h1₁ : IsUnit a ∧ IsUnit y
Tactic: have h1 : IsUnit a ∧ IsUnit y := by simpa using h1
-- Lean 4 proof step from Mathlib.RingTheory.Henselian (goal)
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))
⊢ ∃ (a : K), f.IsRoot a ∧ Membership.mem (γ := Ideal K) (maximalIdeal K) (a - a₀)
have simp : ∀ (h₁ : Polynomial.eval a₀ f = 0), ∃ (a : K), f.IsRoot a ∧ a - a₀ = 0
Tactic: simp only [(maximalIdeal K).eq_bot_of_prime, Ideal.mem_bot] at h₁ ⊢
Cleared hypotheses: h₁