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 : FiniteResidueField K →+*o ℝ
h : LE.le (α := ArchimedeanClass K) 0 (mk x)
⊢ Eq (α := ℝ)
    ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x h) :
          FiniteResidueField K) :
      ℝ)
    ((f : (a : FiniteResidueField K) → ℝ)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x h) :
          FiniteResidueField K) :
      ℝ)
have e_a : Classical.ofNonempty = f
Tactic: congr
-- 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
⊢ stdPart x = 0 → Ne (α := ArchimedeanClass K) (mk x) 0
have contrapose! : Eq (α := ArchimedeanClass K) (mk x) 0 → stdPart x ≠ 0
Tactic: contrapose!
-- 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 : Eq (α := ArchimedeanClass K) (mk x) 0
⊢ stdPart x ≠ 0
have rwa : Ne (α := ℝ)
  ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x sorry) :
        FiniteResidueField K) :
    ℝ)
  (0 : ℝ)
Tactic: rwa [stdPart_of_mk_nonneg Classical.ofNonempty h.ge, map_ne_zero, FiniteResidueField.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 : K
h : Eq (α := ArchimedeanClass K) (mk x) 0
rwa :
  Ne (α := ℝ)
    ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x ⋯) :
          FiniteResidueField K) :
      ℝ)
    (0 : ℝ)
⊢ stdPart x ≠ 0
have rwa₁ : Ne (α := FiniteResidueField K)
  ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x sorry) : FiniteResidueField K)
  (0 : FiniteResidueField K)
Tactic: rwa [stdPart_of_mk_nonneg Classical.ofNonempty h.ge, map_ne_zero, FiniteResidueField.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 : K
h : Eq (α := ArchimedeanClass K) (mk x) 0
rwa :
  Ne (α := ℝ)
    ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x ⋯) :
          FiniteResidueField K) :
      ℝ)
    (0 : ℝ)
rwa₁ :
  Ne (α := FiniteResidueField K)
    ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x ⋯) :
      FiniteResidueField K)
    (0 : FiniteResidueField K)
⊢ stdPart x ≠ 0
have rwa₂ : Eq (α := ArchimedeanClass K) (mk (↑(FiniteElement.mk x sorry) : K)) 0
Tactic: rwa [stdPart_of_mk_nonneg Classical.ofNonempty h.ge, map_ne_zero, FiniteResidueField.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 : K
h : Ne (α := ArchimedeanClass K) (mk x) 0
⊢ stdPart x = 0
have inl : ∀ (h : LT.lt (α := ArchimedeanClass K) (mk x) 0), stdPart x = 0
Tactic: obtain h | h := h.lt_or_gt
-- 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 : Ne (α := ArchimedeanClass K) (mk x) 0
inl : ∀ (h : LT.lt (α := ArchimedeanClass K) (mk x) 0), stdPart x = 0
⊢ stdPart x = 0
have inr : ∀ (h : LT.lt (α := ArchimedeanClass K) 0 (mk x)), stdPart x = 0
Tactic: obtain h | h := h.lt_or_gt
-- 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_1 : Ne (α := ArchimedeanClass K) (mk x) 0
h : LT.lt (α := ArchimedeanClass K) 0 (mk x)
⊢ stdPart x = 0
have inr : Eq (α := ℝ)
  (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)
  0
Tactic: rw [stdPart, dif_pos h.le, OrderRingHom.comp_apply, FiniteResidueField.mk_eq_zero.2 h,
        map_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
h_1 : Ne (α := ArchimedeanClass K) (mk x) 0
h : LT.lt (α := ArchimedeanClass K) 0 (mk x)
inr :
  Eq (α := ℝ)
    (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)
    0
⊢ stdPart x = 0
have inr₁ : Eq (α := ℝ)
  ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk x sorry) :
    ℝ)
  (0 : ℝ)
Tactic: rw [stdPart, dif_pos h.le, OrderRingHom.comp_apply, FiniteResidueField.mk_eq_zero.2 h,
        map_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
h_1 : Ne (α := ArchimedeanClass K) (mk x) 0
h : LT.lt (α := ArchimedeanClass K) 0 (mk x)
inr :
  Eq (α := ℝ)
    (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)
    0
inr₁ :
  Eq (α := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk x ⋯) :
      ℝ)
    (0 : ℝ)
⊢ stdPart x = 0
have inr₂ : Eq (α := ℝ)
  ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
      ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x sorry) :
        FiniteResidueField K) :
    ℝ)
  (0 : ℝ)
Tactic: rw [stdPart, dif_pos h.le, OrderRingHom.comp_apply, FiniteResidueField.mk_eq_zero.2 h,
        map_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
h_1 : Ne (α := ArchimedeanClass K) (mk x) 0
h : LT.lt (α := ArchimedeanClass K) 0 (mk x)
inr :
  Eq (α := ℝ)
    (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)
    0
inr₁ :
  Eq (α := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk x ⋯) :
      ℝ)
    (0 : ℝ)
inr₂ :
  Eq (α := ℝ)
    ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x ⋯) :
          FiniteResidueField K) :
      ℝ)
    (0 : ℝ)
⊢ stdPart x = 0
have inr₃ : Eq (α := ℝ) ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ) 0 : ℝ) (0 : ℝ)
Tactic: rw [stdPart, dif_pos h.le, OrderRingHom.comp_apply, FiniteResidueField.mk_eq_zero.2 h,
        map_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
h_1 : Ne (α := ArchimedeanClass K) (mk x) 0
h : LT.lt (α := ArchimedeanClass K) 0 (mk x)
inr :
  Eq (α := ℝ)
    (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)
    0
inr₁ :
  Eq (α := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk x ⋯) :
      ℝ)
    (0 : ℝ)
inr₂ :
  Eq (α := ℝ)
    ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ)
        ((FiniteResidueField.mk : (a : FiniteElement K) → FiniteResidueField K) (FiniteElement.mk x ⋯) :
          FiniteResidueField K) :
      ℝ)
    (0 : ℝ)
inr₃ : Eq (α := ℝ) ((Classical.ofNonempty : (a : FiniteResidueField K) → ℝ) 0 : ℝ) (0 : ℝ)
⊢ stdPart x = 0
have inr₄ : Eq (α := ℝ) 0 0
Tactic: rw [stdPart, dif_pos h.le, OrderRingHom.comp_apply, FiniteResidueField.mk_eq_zero.2 h,
        map_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
⊢ Membership.mem (γ := Set K) {x : K | LE.le (α := ArchimedeanClass K) 0 (mk x)} x →
    ∀ ⦃b : K⦄,
      Membership.mem (γ := Set K) {x : K | LE.le (α := ArchimedeanClass K) 0 (mk x)} b → x ≤ b → stdPart x ≤ stdPart b
have mk : ∀ (hx : LE.le (α := ArchimedeanClass K) 0 (mk x)) ⦃b : K⦄,
  Membership.mem (γ := Set K) {x : K | LE.le (α := ArchimedeanClass K) 0 (mk x)} b → x ≤ b → stdPart x ≤ stdPart b
Tactic: (hx : 0 ≤ mk x)
-- 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 : LE.le (α := ArchimedeanClass K) 0 (mk x)
y : K
⊢ Membership.mem (γ := Set K) {x : K | LE.le (α := ArchimedeanClass K) 0 (mk x)} y → x ≤ y → stdPart x ≤ stdPart y
have mk : ∀ (hy : LE.le (α := ArchimedeanClass K) 0 (mk y)), x ≤ y → stdPart x ≤ stdPart y
Tactic: (hy : 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 : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
y : K
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
h : x ≤ y
⊢ LE.le (α := ℝ)
    (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 : LE.le (α := ℝ)
  ((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]
-- 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 : LE.le (α := ArchimedeanClass K) 0 (mk x)
y : K
hy : LE.le (α := ArchimedeanClass K) 0 (mk y)
h : x ≤ y
⊢ LE.le (α := ℝ)
    ((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) :
      ℝ)
have a : LE.le (α := FiniteElement K) (FiniteElement.mk x hx) (FiniteElement.mk y hy)
Tactic: apply OrderRingHom.monotone'
-- 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
⊢ stdPart.{u_1} (K := K) 0 = 0
have rw : Eq (α := ℝ)
  ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk 0 sorry) :
    ℝ)
  (0 : ℝ)
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
rw :
  Eq (α := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk 0 ⋯) :
      ℝ)
    (0 : ℝ)
⊢ stdPart.{u_1} (K := K) 0 = 0
have hc : LE.le.{u_1} (α := ArchimedeanClass K) 0 (mk 0)
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
⊢ stdPart.{u_1} (K := K) 1 = 1
have rw : Eq (α := ℝ)
  ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk 1 sorry) :
    ℝ)
  (1 : ℝ)
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
rw :
  Eq (α := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk 1 ⋯) :
      ℝ)
    (1 : ℝ)
⊢ stdPart.{u_1} (K := K) 1 = 1
have hc : LE.le.{u_1} (α := ArchimedeanClass K) 0 (mk 1)
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
⊢ stdPart (-x) = -stdPart x
have simp_rw : Eq (α := ℝ)
  (if h : LE.le (α := ArchimedeanClass K) 0 (mk x) then
    (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk (-x) sorry)
  else 0)
  (-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)
Tactic: simp_rw [stdPart, ArchimedeanClass.mk_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
⊢ Eq (α := ℝ)
    (if h : LE.le (α := ArchimedeanClass K) 0 (mk x) then
      (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (FiniteElement.mk (-x) ⋯)
    else 0)
    (-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)
have pos : ∀ (h : LE.le (α := ArchimedeanClass K) 0 (mk x)),
  Eq (α := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (FiniteElement.mk (-x) sorry) :
      ℝ)
    (-(OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk x h) :
      ℝ)
Tactic: split_ifs
-- 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
pos :
  ∀ (h : LE.le (α := ArchimedeanClass K) 0 (mk x)),
    Eq (α := ℝ)
      ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk (-x) ⋯) :
        ℝ)
      (-(OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
            (FiniteElement.mk x h) :
        ℝ)
⊢ Eq (α := ℝ)
    (if h : LE.le (α := ArchimedeanClass K) 0 (mk x) then
      (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (FiniteElement.mk (-x) ⋯)
    else 0)
    (-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)
have neg : ¬LE.le (α := ArchimedeanClass K) 0 (mk x) → Eq (α := ℝ) 0 (-0)
Tactic: split_ifs
-- 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 : LE.le (α := ArchimedeanClass K) 0 (mk x)
⊢ Eq (α := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (FiniteElement.mk (-x) ⋯) :
      ℝ)
    (-(OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk x h) :
      ℝ)
have pos : Eq (α := ℝ)
  ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (-FiniteElement.mk x h) :
    ℝ)
  (-(OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk x h) :
    ℝ)
Tactic: rw [← FiniteElement.neg_mk, 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
h : LE.le (α := ArchimedeanClass K) 0 (mk x)
pos :
  Eq (α := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (-FiniteElement.mk x h) :
      ℝ)
    (-(OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk x h) :
      ℝ)
pos₁ : LE.le (α := ArchimedeanClass K) 0 (mk x)
⊢ Eq (α := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (FiniteElement.mk (-x) ⋯) :
      ℝ)
    (-(OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk x h) :
      ℝ)
have pos₂ : Eq (α := ℝ)
  (-(OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk x h) :
    ℝ)
  (-(OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk x h) :
    ℝ)
Tactic: rw [← FiniteElement.neg_mk, 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
⊢ stdPart x⁻¹ = (stdPart x)⁻¹
have inl : ∀ (hx : Eq (α := ArchimedeanClass K) (mk x) 0), stdPart x⁻¹ = (stdPart x)⁻¹
Tactic: obtain hx | hx := eq_or_ne (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
inl : ∀ (hx : Eq (α := ArchimedeanClass K) (mk x) 0), stdPart x⁻¹ = (stdPart x)⁻¹
⊢ stdPart x⁻¹ = (stdPart x)⁻¹
have inr : ∀ (hx : Ne (α := ArchimedeanClass K) (mk x) 0), stdPart x⁻¹ = (stdPart x)⁻¹
Tactic: obtain hx | hx := eq_or_ne (mk x) 0
-- 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
hx : Eq (α := ArchimedeanClass K) (mk x) 0
⊢ Eq (α := ℝ)
    (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 x) then
        (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk x h)
      else 0)⁻¹
have hx' : LE.le (α := ArchimedeanClass K) 0 (mk x⁻¹)
Tactic: have hx' : 0 ≤ mk x⁻¹ := by simp_all
-- 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⁻¹)
⊢ Eq (α := ℝ)
    (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 x) then
        (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
          (FiniteElement.mk x h)
      else 0)⁻¹
have inl : Eq (α := ℝ)
  ((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 sorry))⁻¹ :
    ℝ)
Tactic: rw [dif_pos hx.ge, dif_pos 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
hx : Eq (α := ArchimedeanClass K) (mk x) 0
hx' : LE.le (α := ArchimedeanClass K) 0 (mk x⁻¹)
⊢ Eq (α := ℝ)
    ((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 ⋯))⁻¹ :
      ℝ)
have inl : 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 sorry) :
      ℝ) =
  1
Tactic: apply eq_inv_of_mul_eq_one_left
-- 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⁻¹)
this : HMul.hMul (α := FiniteElement K) (FiniteElement.mk x⁻¹ hx') (FiniteElement.mk x ⋯) = 1
⊢ 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 rw : Eq (α := ℝ)
  ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
      (HMul.hMul (α := FiniteElement K) (FiniteElement.mk x⁻¹ hx') (FiniteElement.mk x sorry)) :
    ℝ)
  (1 : ℝ)
Tactic: 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⁻¹)
this : HMul.hMul (α := FiniteElement K) (FiniteElement.mk x⁻¹ hx') (FiniteElement.mk x ⋯) = 1
rw :
  Eq (α := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (HMul.hMul (α := FiniteElement K) (FiniteElement.mk x⁻¹ hx') (FiniteElement.mk x ⋯)) :
      ℝ)
    (1 : ℝ)
⊢ 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 rw₁ : Eq (α := ℝ) ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) 1 : ℝ) (1 : ℝ)
Tactic: 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⁻¹)
this : HMul.hMul (α := FiniteElement K) (FiniteElement.mk x⁻¹ hx') (FiniteElement.mk x ⋯) = 1
rw :
  Eq (α := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
        (HMul.hMul (α := FiniteElement K) (FiniteElement.mk x⁻¹ hx') (FiniteElement.mk x ⋯)) :
      ℝ)
    (1 : ℝ)
rw₁ :
  Eq (α := ℝ) ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) 1 : ℝ) (1 : ℝ)
⊢ 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 rw₂ : Eq (α := ℝ) 1 1
Tactic: rw [← map_mul, this, map_one]