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
hx : Eq (α := ArchimedeanClass K) (mk x) 0
hx' : LE.le (α := ArchimedeanClass K) 0 (mk x⁻¹)
⊢ HMul.hMul (α := ℝ) (β := ℝ)
      ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk x⁻¹ hx') :
        ℝ)
      ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk x ⋯) :
        ℝ) =
    1
have inl : HMul.hMul (α := FiniteElement K) (FiniteElement.mk x⁻¹ hx') (FiniteElement.mk x sorry) = 1
Tactic: suffices FiniteElement.mk x⁻¹ hx' * .mk x hx.ge = 1 by
        rw [← map_mul, this, map_one]
-- 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
hx : Eq (α := ArchimedeanClass K) (mk x) 0
hx' : LE.le (α := ArchimedeanClass K) 0 (mk x⁻¹)
⊢ HMul.hMul (α := FiniteElement K) (FiniteElement.mk x⁻¹ hx') (FiniteElement.mk x ⋯) = 1
have inl : (↑(HMul.hMul (α := FiniteElement K) (FiniteElement.mk x⁻¹ hx') (FiniteElement.mk x sorry)) : K) = (↑1 : K)
Tactic: ext
-- 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
hx : Eq (α := ArchimedeanClass K) (mk x) 0
hx' : LE.le (α := ArchimedeanClass K) 0 (mk x⁻¹)
⊢ (↑(HMul.hMul (α := FiniteElement K) (FiniteElement.mk x⁻¹ hx') (FiniteElement.mk x ⋯)) : K) = (↑1 : K)
have inl : x ≠ 0
Tactic: apply inv_mul_cancel₀
-- 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
hx : Ne (α := ArchimedeanClass K) (mk x) 0
⊢ stdPart x⁻¹ = (stdPart x)⁻¹
have inr : Ne (α := ArchimedeanClass K) (mk x⁻¹) 0
Tactic: rw [stdPart_of_mk_ne_zero hx, stdPart_of_mk_ne_zero, inv_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
hx : Ne (α := ArchimedeanClass K) (mk x) 0
⊢ Ne (α := ArchimedeanClass K) (mk x⁻¹) 0
have inr : Ne (α := ArchimedeanClass K) (-mk x) 0
Tactic: rwa [mk_inv, neg_ne_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 y : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
⊢ (if h : LE.le (α := ArchimedeanClass K) 0 (mk (x + y)) then
      (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (FiniteElement.mk (x + y) h)
    else 0) =
    HAdd.hAdd (α := ℝ)
      (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)
      (if h : LE.le (α := ArchimedeanClass K) 0 (mk y) then
        (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk y h)
      else 0)
have rw : (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
    (FiniteElement.mk (x + y) sorry) =
  HAdd.hAdd (α := ℝ) (β := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (FiniteElement.mk x hx) :
      ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (FiniteElement.mk y hy) :
      ℝ)
Tactic: rw [dif_pos hx, dif_pos hy, dif_pos]
-- 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 y : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
rw :
  (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
      (FiniteElement.mk (x + y) ⋯) =
    HAdd.hAdd (α := ℝ) (β := ℝ)
      ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk x hx) :
        ℝ)
      ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk y hy) :
        ℝ)
⊢ (if h : LE.le (α := ArchimedeanClass K) 0 (mk (x + y)) then
      (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (FiniteElement.mk (x + y) h)
    else 0) =
    HAdd.hAdd (α := ℝ)
      (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)
      (if h : LE.le (α := ArchimedeanClass K) 0 (mk y) then
        (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk y h)
      else 0)
have hc : LE.le (α := ArchimedeanClass K) 0 (mk (x + y))
Tactic: rw [dif_pos hx, dif_pos hy, dif_pos]
-- 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 y : K
hx : LT.lt (α := ArchimedeanClass K) 0 (mk x)
⊢ stdPart (x + y) = stdPart y
have inl : ∀ (hy : LE.le (α := ArchimedeanClass K) 0 (mk y)), stdPart (x + y) = stdPart y
Tactic: obtain hy | hy := le_or_gt 0 (mk y)
-- 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 y : K
hx : LT.lt (α := ArchimedeanClass K) 0 (mk x)
inl : ∀ (hy : LE.le (α := ArchimedeanClass K) 0 (mk y)), stdPart (x + y) = stdPart y
⊢ stdPart (x + y) = stdPart y
have inr : ∀ (hy : LT.lt (α := ArchimedeanClass K) (mk y) 0), stdPart (x + y) = stdPart y
Tactic: obtain hy | hy := le_or_gt 0 (mk y)
-- 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 y : K
hx : LT.lt (α := ArchimedeanClass K) 0 (mk x)
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
⊢ stdPart (x + y) = stdPart y
have inl : stdPart x + stdPart y = stdPart y
Tactic: rw [stdPart_add hx.le hy, stdPart_of_mk_ne_zero hx.ne', zero_add]
-- 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 y : K
hx : LT.lt (α := ArchimedeanClass K) 0 (mk x)
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
inl : stdPart x + stdPart y = stdPart y
⊢ stdPart (x + y) = stdPart y
have inl₁ : 0 + stdPart y = stdPart y
Tactic: rw [stdPart_add hx.le hy, stdPart_of_mk_ne_zero hx.ne', zero_add]
-- 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 y : K
hx : LT.lt (α := ArchimedeanClass K) 0 (mk x)
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
inl : stdPart x + stdPart y = stdPart y
inl₁ : 0 + stdPart y = stdPart y
⊢ stdPart (x + y) = stdPart y
have inl₂ : stdPart y = stdPart y
Tactic: rw [stdPart_add hx.le hy, stdPart_of_mk_ne_zero hx.ne', zero_add]
-- 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 y : K
hx : LT.lt (α := ArchimedeanClass K) 0 (mk x)
hy : LT.lt (α := ArchimedeanClass K) (mk y) 0
⊢ stdPart (x + y) = stdPart y
have inr : Ne (α := ArchimedeanClass K) (mk (x + y)) 0
Tactic: rw [stdPart_of_mk_ne_zero hy.ne, stdPart_of_mk_ne_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 y : K
hx : LT.lt (α := ArchimedeanClass K) 0 (mk x)
hy : LT.lt (α := ArchimedeanClass K) (mk y) 0
⊢ Ne (α := ArchimedeanClass K) (mk (x + y)) 0
have inr : Ne (α := ArchimedeanClass K) (mk y) 0
Tactic: rw [mk_add_eq_mk_right (hy.trans 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 y : K
hy : LT.lt (α := ArchimedeanClass K) 0 (mk y)
⊢ stdPart (x + y) = stdPart x
have rw : stdPart (y + x) = stdPart x
Tactic: rw [add_comm, stdPart_add_eq_right hy]
-- 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 y : K
hy : LT.lt (α := ArchimedeanClass K) 0 (mk y)
rw : stdPart (y + x) = stdPart x
⊢ stdPart (x + y) = stdPart x
have rw₁ : stdPart x = stdPart x
Tactic: rw [add_comm, stdPart_add_eq_right hy]
-- 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 y : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
⊢ stdPart (x - y) = stdPart x - stdPart y
have rw : LE.le (α := ArchimedeanClass K) 0 (mk (-y))
Tactic: rw [sub_eq_add_neg, sub_eq_add_neg, stdPart_add hx, stdPart_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 y : K
hx : LT.lt (α := ArchimedeanClass K) 0 (mk x)
⊢ stdPart (x - y) = -stdPart y
have rw : stdPart (x + -y) = -stdPart y
Tactic: rw [sub_eq_add_neg, stdPart_add_eq_right hx, stdPart_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 y : K
hx : LT.lt (α := ArchimedeanClass K) 0 (mk x)
rw : stdPart (x + -y) = -stdPart y
⊢ stdPart (x - y) = -stdPart y
have rw₁ : stdPart (-y) = -stdPart y
Tactic: rw [sub_eq_add_neg, stdPart_add_eq_right hx, stdPart_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 y : K
hx : LT.lt (α := ArchimedeanClass K) 0 (mk x)
rw : stdPart (x + -y) = -stdPart y
rw₁ : stdPart (-y) = -stdPart y
⊢ stdPart (x - y) = -stdPart y
have rw₂ : -stdPart y = -stdPart y
Tactic: rw [sub_eq_add_neg, stdPart_add_eq_right hx, stdPart_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 y : K
hy : LT.lt (α := ArchimedeanClass K) 0 (mk y)
⊢ stdPart (x - y) = stdPart x
have rw : stdPart (x + -y) = stdPart x
Tactic: rw [sub_eq_add_neg, stdPart_add_eq_left (by simpa)]
-- 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 y : K
hy : LT.lt (α := ArchimedeanClass K) 0 (mk y)
rw : stdPart (x + -y) = stdPart x
⊢ stdPart (x - y) = stdPart x
have rw₁ : stdPart x = stdPart x
Tactic: rw [sub_eq_add_neg, stdPart_add_eq_left (by simpa)]
-- 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 y : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
⊢ (if h : LE.le (α := ArchimedeanClass K) 0 (mk (x * y)) then
      (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (FiniteElement.mk (x * y) h)
    else 0) =
    HMul.hMul (α := ℝ)
      (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)
      (if h : LE.le (α := ArchimedeanClass K) 0 (mk y) then
        (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk y h)
      else 0)
have rw : (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
    (FiniteElement.mk (x * y) sorry) =
  HMul.hMul (α := ℝ) (β := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (FiniteElement.mk x hx) :
      ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (FiniteElement.mk y hy) :
      ℝ)
Tactic: rw [dif_pos hx, dif_pos hy, dif_pos]
-- 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 y : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
rw :
  (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
      (FiniteElement.mk (x * y) ⋯) =
    HMul.hMul (α := ℝ) (β := ℝ)
      ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk x hx) :
        ℝ)
      ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk y hy) :
        ℝ)
⊢ (if h : LE.le (α := ArchimedeanClass K) 0 (mk (x * y)) then
      (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (FiniteElement.mk (x * y) h)
    else 0) =
    HMul.hMul (α := ℝ)
      (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)
      (if h : LE.le (α := ArchimedeanClass K) 0 (mk y) then
        (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk y h)
      else 0)
have hc : LE.le (α := ArchimedeanClass K) 0 (mk (x * y))
Tactic: rw [dif_pos hx, dif_pos hy, dif_pos]
-- 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 y : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
hy : LE.le (α := ArchimedeanClass K) 0 (-mk y)
⊢ stdPart (x / y) = stdPart x / stdPart y
have rw : LE.le (α := ArchimedeanClass K) 0 (mk y⁻¹)
Tactic: rw [div_eq_mul_inv, div_eq_mul_inv, stdPart_mul hx, stdPart_inv]
-- 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
q : ℚ
⊢ stdPart.{u_1} (K := K) (↑q : K) = (↑q : ℝ)
have rw : Eq (α := ℝ)
  ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk (↑q : K) sorry) :
        FiniteResidueField K) :
    ℝ)
  ((↑q : ℝ) : ℝ)
Tactic: rw [stdPart_of_mk_nonneg Classical.ofNonempty (mk_ratCast_nonneg q), FiniteElement.mk_ratCast,
    FiniteResidueField.mk_ratCast, map_ratCast]
-- 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
q : ℚ
rw :
  Eq (α := ℝ)
    ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk (↑q : K) ⋯) :
          FiniteResidueField K) :
      ℝ)
    ((↑q : ℝ) : ℝ)
⊢ stdPart.{u_1} (K := K) (↑q : K) = (↑q : ℝ)
have rw₁ : Eq (α := ℝ)
  ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (↑q : FiniteElement K)) :
    ℝ)
  ((↑q : ℝ) : ℝ)
Tactic: rw [stdPart_of_mk_nonneg Classical.ofNonempty (mk_ratCast_nonneg q), FiniteElement.mk_ratCast,
    FiniteResidueField.mk_ratCast, map_ratCast]
-- 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
q : ℚ
rw :
  Eq (α := ℝ)
    ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk (↑q : K) ⋯) :
          FiniteResidueField K) :
      ℝ)
    ((↑q : ℝ) : ℝ)
rw₁ :
  Eq (α := ℝ)
    ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (↑q : FiniteElement K)) :
      ℝ)
    ((↑q : ℝ) : ℝ)
⊢ stdPart.{u_1} (K := K) (↑q : K) = (↑q : ℝ)
have rw₂ : Eq (α := ℝ) ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ) (↑q : FiniteResidueField K) : ℝ) ((↑q : ℝ) : ℝ)
Tactic: rw [stdPart_of_mk_nonneg Classical.ofNonempty (mk_ratCast_nonneg q), FiniteElement.mk_ratCast,
    FiniteResidueField.mk_ratCast, map_ratCast]
-- 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
q : ℚ
rw :
  Eq (α := ℝ)
    ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk (↑q : K) ⋯) :
          FiniteResidueField K) :
      ℝ)
    ((↑q : ℝ) : ℝ)
rw₁ :
  Eq (α := ℝ)
    ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (↑q : FiniteElement K)) :
      ℝ)
    ((↑q : ℝ) : ℝ)
rw₂ :
  Eq (α := ℝ) ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ) (↑q : FiniteResidueField K) : ℝ) ((↑q : ℝ) : ℝ)
⊢ stdPart.{u_1} (K := K) (↑q : K) = (↑q : ℝ)
have rw₃ : Eq (α := ℝ) (↑q : ℝ) (↑q : ℝ)
Tactic: rw [stdPart_of_mk_nonneg Classical.ofNonempty (mk_ratCast_nonneg q), FiniteElement.mk_ratCast,
    FiniteResidueField.mk_ratCast, map_ratCast]
-- 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
f : ℝ →+*o K
r : ℝ
⊢ stdPart (K := K) ((f : (a : ℝ) → K) r : K) = r
have rw : (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
    (FiniteElement.mk ((f : (a : ℝ) → K) r) sorry : FiniteElement K) =
  r
Tactic: rw [stdPart, dif_pos]
-- 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
f : ℝ →+*o K
r : ℝ
rw :
  (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
      (FiniteElement.mk ((f : (a : ℝ) → K) r) ⋯ : FiniteElement K) =
    r
⊢ stdPart (K := K) ((f : (a : ℝ) → K) r : K) = r
have hc : LE.le (α := ArchimedeanClass K) (0 : ArchimedeanClass K) (mk ((f : (a : ℝ) → K) r) : ArchimedeanClass K)
Tactic: rw [stdPart, dif_pos]
-- 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)
⊢ 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.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)
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)
⊢ 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.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)
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)
⊢ 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)
          (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)
Tactic: rw [stdPart, dif_pos hx, ← OrderRingHom.comp_apply, ← OrderRingHom.comp_assoc,
    OrderRingHom.comp_apply, OrderRingHom.apply_eq_self]