awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
rw :
  Eq (α := FiniteResidueField K)
    ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K)
        (if h : LE.le (α := ArchimedeanClass K) 0 (mk x) then
          (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
            (FiniteElement.mk x h)
        else 0) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
rw₁ :
  Eq (α := FiniteResidueField K)
    ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K)
        ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
            (FiniteElement.mk x hx) :
          ℝ) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
rw₂ :
  Eq (α := FiniteResidueField K)
    ((OrderRingHom.comp (FiniteResidueField.ofArchimedean f)
            (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk) :
          (a : FiniteElement K) → FiniteResidueField K)
        (FiniteElement.mk x hx) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
⊢ Eq (α := FiniteResidueField K)
    ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) (stdPart x) : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
have rw₃ : Eq (α := FiniteResidueField K)
  ((OrderRingHom.comp (OrderRingHom.comp (FiniteResidueField.ofArchimedean f) Classical.ofNonempty)
          FiniteResidueField.mk :
        (a : FiniteElement K) → FiniteResidueField K)
      (FiniteElement.mk x hx) :
    FiniteResidueField K)
  ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
    FiniteResidueField K)
Tactic: rw [stdPart, dif_pos hx, ← OrderRingHom.comp_apply, ← OrderRingHom.comp_assoc,
    OrderRingHom.comp_apply, OrderRingHom.apply_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
rw :
  Eq (α := FiniteResidueField K)
    ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K)
        (if h : LE.le (α := ArchimedeanClass K) 0 (mk x) then
          (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
            (FiniteElement.mk x h)
        else 0) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
rw₁ :
  Eq (α := FiniteResidueField K)
    ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K)
        ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
            (FiniteElement.mk x hx) :
          ℝ) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
rw₂ :
  Eq (α := FiniteResidueField K)
    ((OrderRingHom.comp (FiniteResidueField.ofArchimedean f)
            (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk) :
          (a : FiniteElement K) → FiniteResidueField K)
        (FiniteElement.mk x hx) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
rw₃ :
  Eq (α := FiniteResidueField K)
    ((OrderRingHom.comp (OrderRingHom.comp (FiniteResidueField.ofArchimedean f) Classical.ofNonempty)
            FiniteResidueField.mk :
          (a : FiniteElement K) → FiniteResidueField K)
        (FiniteElement.mk x hx) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
⊢ Eq (α := FiniteResidueField K)
    ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) (stdPart x) : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
have rw₄ : Eq (α := FiniteResidueField K)
  ((OrderRingHom.comp (FiniteResidueField.ofArchimedean f) Classical.ofNonempty :
        (a : FiniteResidueField K) → FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx)) :
    FiniteResidueField K)
  ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
    FiniteResidueField K)
Tactic: rw [stdPart, dif_pos hx, ← OrderRingHom.comp_apply, ← OrderRingHom.comp_assoc,
    OrderRingHom.comp_apply, OrderRingHom.apply_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
rw :
  Eq (α := FiniteResidueField K)
    ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K)
        (if h : LE.le (α := ArchimedeanClass K) 0 (mk x) then
          (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
            (FiniteElement.mk x h)
        else 0) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
rw₁ :
  Eq (α := FiniteResidueField K)
    ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K)
        ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
            (FiniteElement.mk x hx) :
          ℝ) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
rw₂ :
  Eq (α := FiniteResidueField K)
    ((OrderRingHom.comp (FiniteResidueField.ofArchimedean f)
            (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk) :
          (a : FiniteElement K) → FiniteResidueField K)
        (FiniteElement.mk x hx) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
rw₃ :
  Eq (α := FiniteResidueField K)
    ((OrderRingHom.comp (OrderRingHom.comp (FiniteResidueField.ofArchimedean f) Classical.ofNonempty)
            FiniteResidueField.mk :
          (a : FiniteElement K) → FiniteResidueField K)
        (FiniteElement.mk x hx) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
rw₄ :
  Eq (α := FiniteResidueField K)
    ((OrderRingHom.comp (FiniteResidueField.ofArchimedean f) Classical.ofNonempty :
          (a : FiniteResidueField K) → FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx)) :
      FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
⊢ Eq (α := FiniteResidueField K)
    ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) (stdPart x) : FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
      FiniteResidueField K)
have rw₅ : Eq (α := FiniteResidueField K)
  ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
    FiniteResidueField K)
  ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
    FiniteResidueField K)
Tactic: rw [stdPart, dif_pos hx, ← OrderRingHom.comp_apply, ← OrderRingHom.comp_assoc,
    OrderRingHom.comp_apply, OrderRingHom.apply_eq_self]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
h : 0 ≤ x
⊢ 0 ≤ stdPart x
have inl : ∀ (hx : Eq (α := ArchimedeanClass K) (mk x) 0), 0 ≤ stdPart x
Tactic: obtain hx | hx := eq_or_ne (ArchimedeanClass.mk x) 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
h : 0 ≤ x
inl : ∀ (hx : Eq (α := ArchimedeanClass K) (mk x) 0), 0 ≤ stdPart x
⊢ 0 ≤ stdPart x
have inr : ∀ (hx : Ne (α := ArchimedeanClass K) (mk x) 0), 0 ≤ stdPart x
Tactic: obtain hx | hx := eq_or_ne (ArchimedeanClass.mk x) 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
h : 0 ≤ x
hx : Eq (α := ArchimedeanClass K) (mk x) 0
⊢ 0 ≤ stdPart x
have inl : LE.le (α := ℝ) (0 : ℝ)
  ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk x sorry) :
    ℝ)
Tactic: rw [stdPart, dif_pos hx.ge]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
h : 0 ≤ x
hx : Ne (α := ArchimedeanClass K) (mk x) 0
⊢ 0 ≤ stdPart x
have inr : LE.le (α := ℝ) 0 0
Tactic: rw [stdPart_of_mk_ne_zero hx]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
⊢ LT.lt (α := ArchimedeanClass K) 0 (mk (HSub.hSub (β := K) x ((f : (a : ℝ) → K) r : K))) ↔ stdPart x = r
have refine : Eq (α := FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K)
        (HSub.hSub (α := FiniteElement K) (β := FiniteElement K) (FiniteElement.mk x hx)
          (FiniteElement.mk ((f : (a : ℝ) → K) r) sorry : FiniteElement K)) :
      FiniteResidueField K)
    (0 : FiniteResidueField K) ↔
  stdPart x = r
Tactic: refine (FiniteResidueField.mk_eq_zero
    (x := .mk x hx - .mk _ (mk_map_nonneg_of_archimedean f r))).symm.trans ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
⊢ Eq (α := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K)
          (HSub.hSub (α := FiniteElement K) (β := FiniteElement K) (FiniteElement.mk x hx)
            (FiniteElement.mk ((f : (a : ℝ) → K) r) ⋯ : FiniteElement K)) :
        FiniteResidueField K)
      (0 : FiniteResidueField K) ↔
    stdPart x = r
have rw : HSub.hSub (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
        FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K)
          (FiniteElement.mk ((f : (a : ℝ) → K) r) sorry) :
        FiniteResidueField K) =
    0 ↔
  stdPart x = r
Tactic: rw [map_sub, ← FiniteResidueField.ofArchimedean_apply, ← ofArchimedean_stdPart f hx,
    sub_eq_zero, FiniteResidueField.ofArchimedean_inj f]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
rw :
  HSub.hSub (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
          FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K)
            (FiniteElement.mk ((f : (a : ℝ) → K) r) ⋯) :
          FiniteResidueField K) =
      0 ↔
    stdPart x = r
⊢ Eq (α := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K)
          (HSub.hSub (α := FiniteElement K) (β := FiniteElement K) (FiniteElement.mk x hx)
            (FiniteElement.mk ((f : (a : ℝ) → K) r) ⋯ : FiniteElement K)) :
        FiniteResidueField K)
      (0 : FiniteResidueField K) ↔
    stdPart x = r
have rw₁ : HSub.hSub (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
        FiniteResidueField K)
      ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) r : FiniteResidueField K) =
    0 ↔
  stdPart x = r
Tactic: rw [map_sub, ← FiniteResidueField.ofArchimedean_apply, ← ofArchimedean_stdPart f hx,
    sub_eq_zero, FiniteResidueField.ofArchimedean_inj f]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
rw :
  HSub.hSub (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
          FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K)
            (FiniteElement.mk ((f : (a : ℝ) → K) r) ⋯) :
          FiniteResidueField K) =
      0 ↔
    stdPart x = r
rw₁ :
  HSub.hSub (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
          FiniteResidueField K)
        ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) r : FiniteResidueField K) =
      0 ↔
    stdPart x = r
⊢ Eq (α := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K)
          (HSub.hSub (α := FiniteElement K) (β := FiniteElement K) (FiniteElement.mk x hx)
            (FiniteElement.mk ((f : (a : ℝ) → K) r) ⋯ : FiniteElement K)) :
        FiniteResidueField K)
      (0 : FiniteResidueField K) ↔
    stdPart x = r
have rw₂ : HSub.hSub (α := FiniteResidueField K) (β := FiniteResidueField K)
      ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) (stdPart x) : FiniteResidueField K)
      ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) r : FiniteResidueField K) =
    0 ↔
  stdPart x = r
Tactic: rw [map_sub, ← FiniteResidueField.ofArchimedean_apply, ← ofArchimedean_stdPart f hx,
    sub_eq_zero, FiniteResidueField.ofArchimedean_inj f]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
rw :
  HSub.hSub (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
          FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K)
            (FiniteElement.mk ((f : (a : ℝ) → K) r) ⋯) :
          FiniteResidueField K) =
      0 ↔
    stdPart x = r
rw₁ :
  HSub.hSub (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
          FiniteResidueField K)
        ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) r : FiniteResidueField K) =
      0 ↔
    stdPart x = r
rw₂ :
  HSub.hSub (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) (stdPart x) : FiniteResidueField K)
        ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) r : FiniteResidueField K) =
      0 ↔
    stdPart x = r
⊢ Eq (α := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K)
          (HSub.hSub (α := FiniteElement K) (β := FiniteElement K) (FiniteElement.mk x hx)
            (FiniteElement.mk ((f : (a : ℝ) → K) r) ⋯ : FiniteElement K)) :
        FiniteResidueField K)
      (0 : FiniteResidueField K) ↔
    stdPart x = r
have rw₃ : Eq (α := FiniteResidueField K)
    ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) (stdPart x) : FiniteResidueField K)
    ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) r : FiniteResidueField K) ↔
  stdPart x = r
Tactic: rw [map_sub, ← FiniteResidueField.ofArchimedean_apply, ← ofArchimedean_stdPart f hx,
    sub_eq_zero, FiniteResidueField.ofArchimedean_inj f]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
rw :
  HSub.hSub (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
          FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K)
            (FiniteElement.mk ((f : (a : ℝ) → K) r) ⋯) :
          FiniteResidueField K) =
      0 ↔
    stdPart x = r
rw₁ :
  HSub.hSub (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x hx) :
          FiniteResidueField K)
        ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) r : FiniteResidueField K) =
      0 ↔
    stdPart x = r
rw₂ :
  HSub.hSub (α := FiniteResidueField K) (β := FiniteResidueField K)
        ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) (stdPart x) : FiniteResidueField K)
        ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) r : FiniteResidueField K) =
      0 ↔
    stdPart x = r
rw₃ :
  Eq (α := FiniteResidueField K)
      ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) (stdPart x) : FiniteResidueField K)
      ((FiniteResidueField.ofArchimedean f : (a : ℝ) → FiniteResidueField K) r : FiniteResidueField K) ↔
    stdPart x = r
⊢ Eq (α := FiniteResidueField K)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K)
          (HSub.hSub (α := FiniteElement K) (β := FiniteElement K) (FiniteElement.mk x hx)
            (FiniteElement.mk ((f : (a : ℝ) → K) r) ⋯ : FiniteElement K)) :
        FiniteResidueField K)
      (0 : FiniteResidueField K) ↔
    stdPart x = r
have rw₄ : stdPart x = r ↔ stdPart x = r
Tactic: rw [map_sub, ← FiniteResidueField.ofArchimedean_apply, ← ofArchimedean_stdPart f hx,
    sub_eq_zero, FiniteResidueField.ofArchimedean_inj f]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : r < stdPart x
⊢ (f : (a : ℝ) → K) r < x
have rw : (f : (a : ℝ) → K) (r - stdPart x) < HSub.hSub (β := K) x ((f : (a : ℝ) → K) (stdPart x) : K)
Tactic: rw [← sub_lt_sub_iff_right (c := f (stdPart x)), ← map_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : r < stdPart x
⊢ (f : (a : ℝ) → K) (r - stdPart x) < HSub.hSub (β := K) x ((f : (a : ℝ) → K) (stdPart x) : K)
have h₁ : LT.lt (α := ArchimedeanClass K) (mk ((f : (a : ℝ) → K) (r - stdPart x)) : ArchimedeanClass K)
  (mk (HSub.hSub (β := K) x ((f : (a : ℝ) → K) (stdPart x) : K)) : ArchimedeanClass K)
Tactic: apply lt_of_mk_lt_mk_of_nonpos
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : r < stdPart x
h₁ :
  LT.lt (α := ArchimedeanClass K) (mk ((f : (a : ℝ) → K) (r - stdPart x)) : ArchimedeanClass K)
    (mk (HSub.hSub (β := K) x ((f : (a : ℝ) → K) (stdPart x) : K)) : ArchimedeanClass K)
⊢ (f : (a : ℝ) → K) (r - stdPart x) < HSub.hSub (β := K) x ((f : (a : ℝ) → K) (stdPart x) : K)
have hneg : LE.le (α := K) ((f : (a : ℝ) → K) (r - stdPart x) : K) (0 : K)
Tactic: apply lt_of_mk_lt_mk_of_nonpos
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : r < stdPart x
⊢ LT.lt (α := ArchimedeanClass K) (mk ((f : (a : ℝ) → K) (r - stdPart x)) : ArchimedeanClass K)
    (mk (HSub.hSub (β := K) x ((f : (a : ℝ) → K) (stdPart x) : K)) : ArchimedeanClass K)
have h₁ : r - stdPart x ≠ 0
Tactic: rw [mk_map_of_archimedean', mk_sub_pos_iff f hx]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : r < stdPart x
⊢ r - stdPart x ≠ 0
have h₁ : ¬r = stdPart x
Tactic: rw [ne_eq, sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : stdPart x < r
⊢ x < (f : (a : ℝ) → K) r
have rw : (f : (a : ℝ) → K) (-r) < -x
Tactic: rw [← neg_lt_neg_iff, ← map_neg]
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : stdPart x < r
⊢ (f : (a : ℝ) → K) (-r) < -x
have hx₁ : LE.le (α := ArchimedeanClass K) 0 (mk (-x))
Tactic: apply lt_of_lt_stdPart
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : stdPart x < r
hx₁ : LE.le (α := ArchimedeanClass K) 0 (mk (-x))
⊢ (f : (a : ℝ) → K) (-r) < -x
have h₁ : -r < stdPart (-x)
Tactic: apply lt_of_lt_stdPart
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, (f : (a : ℝ) → K) s ≤ x
hr : ∀ s > r, x ≤ (f : (a : ℝ) → K) s
⊢ LE.le (α := ArchimedeanClass K) 0 (mk x)
have apply : r - 1 < r
Tactic: apply mk_nonneg_of_le_of_le_of_archimedean f (hl (r - 1) _) (hr (r + 1) _)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (goal)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, (f : (a : ℝ) → K) s ≤ x
hr : ∀ s > r, x ≤ (f : (a : ℝ) → K) s
apply : r - 1 < r
⊢ LE.le (α := ArchimedeanClass K) 0 (mk x)
have apply₁ : r + 1 > r
Tactic: apply mk_nonneg_of_le_of_le_of_archimedean f (hl (r - 1) _) (hr (r + 1) _)
-- Lean 4 proof step from Mathlib.Algebra.Order.Ring.StandardPart (hypothesis)
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, (f : (a : ℝ) → K) s ≤ x
hr : ∀ s > r, x ≤ (f : (a : ℝ) → K) s
⊢ stdPart x = r
have hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
Tactic: have hx : 0 ≤ mk x := by
    apply mk_nonneg_of_le_of_le_of_archimedean f (hl (r - 1) _) (hr (r + 1) _) <;> simp