awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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) (mk x) 0
⊢ stdPart x = 0

Tactic:
exact dif_neg h.not_ge

Premises used: dif_neg, LT.lt.not_ge
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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 : ℝ)
inr₄ inr₅ : Eq (α := ℝ) 0 0
⊢ stdPart x = 0

Tactic:
rw [stdPart, dif_pos h.le, OrderRingHom.comp_apply, FiniteResidueField.mk_eq_zero.2 h,
        map_zero]

Premises used: Iff.mpr, ArchimedeanClass.FiniteResidueField.mk_eq_zero, map_zero, dif_pos, LT.lt.le, ArchimedeanClass.stdPart, OrderRingHom.comp_apply
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
mk :
  ∀ (hx : LE.le (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk x)) ⦃b : K⦄,
    Membership.mem (γ := Set K) {x : K | LE.le (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk x)} b →
      x ≤ b → stdPart x ≤ stdPart b
⊢ Membership.mem (γ := Set K) {x : K | LE.le (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk x)} x →
    ∀ ⦃b : K⦄,
      Membership.mem (γ := Set K) {x : K | LE.le (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk x)} b →
        x ≤ b → stdPart x ≤ stdPart b

Tactic:
(hx : 0 ≤ mk x)
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk x)
y : K
mk : ∀ (hy : LE.le (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk y)), x ≤ y → stdPart x ≤ stdPart y
⊢ Membership.mem (γ := Set K) {x : K | LE.le (α := ArchimedeanClass K) 0 (ArchimedeanClass.mk x)} y →
    x ≤ y → stdPart x ≤ stdPart y

Tactic:
(hy : 0 ≤ mk y)
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
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) :
      ℝ)
⊢ 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)

Tactic:
rw [dif_pos hx, dif_pos hy]

Premises used: dif_pos
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
a : LE.le (α := FiniteElement K) (FiniteElement.mk x hx) (FiniteElement.mk y hy)
⊢ 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:
apply OrderRingHom.monotone'

Premises used: OrderRingHom.monotone'
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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 a a₁ a₂ a₃ : x ≤ y
⊢ LE.le (α := FiniteElement K) (FiniteElement.mk x hx) (FiniteElement.mk y hy)

Tactic:
rwa [FiniteElement.mk_le_mk]

Premises used: ArchimedeanClass.FiniteElement.mk_le_mk
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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 : ℝ)
hc : LE.le.{u_1} (α := ArchimedeanClass K) 0 (mk 0)
⊢ stdPart.{u_1} (K := K) 0 = 0

Tactic:
rw [stdPart, dif_pos]

Premises used: dif_pos, ArchimedeanClass.stdPart
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
⊢ Eq (α := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk 0 ⋯) :
      ℝ)
    (0 : ℝ)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
⊢ LE.le.{u_1} (α := ArchimedeanClass K) 0 (mk 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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 : ℝ)
hc : LE.le.{u_1} (α := ArchimedeanClass K) 0 (mk 1)
⊢ stdPart.{u_1} (K := K) 1 = 1

Tactic:
rw [stdPart, dif_pos]

Premises used: dif_pos, ArchimedeanClass.stdPart
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
⊢ Eq (α := ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk 1 ⋯) :
      ℝ)
    (1 : ℝ)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
⊢ LE.le.{u_1} (α := ArchimedeanClass K) 0 (mk 1)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
x : K
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) ⋯)
    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)
⊢ stdPart (-x) = -stdPart x

Tactic:
simp_rw [stdPart, ArchimedeanClass.mk_neg]

Premises used: ArchimedeanClass.stdPart, ArchimedeanClass.mk_neg
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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) :
        ℝ)
neg : ¬LE.le (α := ArchimedeanClass K) 0 (mk x) → Eq (α := ℝ) 0 (-0)
⊢ 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)

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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)
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)
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) :
      ℝ)

Tactic:
rw [← FiniteElement.neg_mk, map_neg]

Premises used: map_neg, ArchimedeanClass.FiniteElement.neg_mk
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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 (α := ℝ) 0 (-0)

Tactic:
simp
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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)⁻¹
inr : ∀ (hx : Ne (α := ArchimedeanClass K) (mk x) 0), stdPart x⁻¹ = (stdPart x)⁻¹
⊢ stdPart x⁻¹ = (stdPart x)⁻¹

Tactic:
obtain hx | hx := eq_or_ne (mk x) 0

Premises used: eq_or_ne, OfNat.ofNat, ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
⊢ LE.le (α := ArchimedeanClass K) 0 (mk x⁻¹)

Tactic:
simp_all
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
⊢ LE.le (α := ArchimedeanClass K) 0 (mk x⁻¹)

Tactic:
have hx' : 0 ≤ mk x⁻¹ := by simp_all
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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⁻¹)
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 ⋯))⁻¹ :
      ℝ)
⊢ 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)⁻¹

Tactic:
rw [dif_pos hx.ge, dif_pos hx']

Premises used: Eq.ge, dif_pos
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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⁻¹)
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 ⋯) :
        ℝ) =
    1
⊢ 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 ⋯))⁻¹ :
      ℝ)

Tactic:
apply eq_inv_of_mul_eq_one_left

Premises used: eq_inv_of_mul_eq_one_left
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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 : ℝ)
rw₂ rw₃ : Eq (α := ℝ) 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

Tactic:
rw [← map_mul, this, map_one]

Premises used: map_mul, map_one
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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⁻¹)
inl : 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

Tactic:
suffices FiniteElement.mk x⁻¹ hx' * .mk x hx.ge = 1 by
        rw [← map_mul, this, map_one]
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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⁻¹)
inl : (↑(HMul.hMul (α := FiniteElement K) (FiniteElement.mk x⁻¹ hx') (FiniteElement.mk x ⋯)) : K) = (↑1 : K)
⊢ HMul.hMul (α := FiniteElement K) (FiniteElement.mk x⁻¹ hx') (FiniteElement.mk x ⋯) = 1

Tactic:
ext
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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⁻¹)
inl : x ≠ 0
⊢ (↑(HMul.hMul (α := FiniteElement K) (FiniteElement.mk x⁻¹ hx') (FiniteElement.mk x ⋯)) : K) = (↑1 : K)

Tactic:
apply inv_mul_cancel₀

Premises used: inv_mul_cancel₀
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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⁻¹)
⊢ x ≠ 0

Tactic:
aesop
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
inr : Ne (α := ArchimedeanClass K) (mk x⁻¹) 0
⊢ stdPart x⁻¹ = (stdPart x)⁻¹

Tactic:
rw [stdPart_of_mk_ne_zero hx, stdPart_of_mk_ne_zero, inv_zero]

Premises used: ArchimedeanClass.stdPart_of_mk_ne_zero, inv_zero
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
inr : Ne (α := ArchimedeanClass K) (-mk x) 0
inr₁ inr₂ inr₃ inr₄ : Ne (α := ArchimedeanClass K) (mk x) 0
⊢ Ne (α := ArchimedeanClass K) (mk x⁻¹) 0

Tactic:
rwa [mk_inv, neg_ne_zero]

Premises used: neg_ne_zero, ArchimedeanClass.mk_inv
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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) :
        ℝ)
hc : LE.le (α := ArchimedeanClass K) 0 (mk (x + 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)

Tactic:
rw [dif_pos hx, dif_pos hy, dif_pos]

Premises used: dif_pos
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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)
⊢ (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) :
        ℝ)

Tactic:
map_add _ (FiniteElement.mk x hx) (.mk y hy)

Premises used: ArchimedeanClass.FiniteElement.mk, map_add
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
inr : ∀ (hy : LT.lt (α := ArchimedeanClass K) (mk y) 0), stdPart (x + y) = stdPart y
⊢ stdPart (x + y) = stdPart y

Tactic:
obtain hy | hy := le_or_gt 0 (mk y)

Premises used: le_or_gt, OfNat.ofNat, ArchimedeanClass.mk
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
inl₂ inl₃ : stdPart y = stdPart y
⊢ stdPart (x + y) = stdPart y

Tactic:
rw [stdPart_add hx.le hy, stdPart_of_mk_ne_zero hx.ne', zero_add]

Premises used: ArchimedeanClass.stdPart_of_mk_ne_zero, ArchimedeanClass.stdPart_add, LT.lt.le, zero_add, LT.lt.ne'
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
inr : Ne (α := ArchimedeanClass K) (mk (x + y)) 0
⊢ stdPart (x + y) = stdPart y

Tactic:
rw [stdPart_of_mk_ne_zero hy.ne, stdPart_of_mk_ne_zero]

Premises used: ArchimedeanClass.stdPart_of_mk_ne_zero, LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
inr : Ne (α := ArchimedeanClass K) (mk y) 0
⊢ Ne (α := ArchimedeanClass K) (mk (x + y)) 0

Tactic:
rw [mk_add_eq_mk_right (hy.trans hx)]

Premises used: ArchimedeanClass.mk_add_eq_mk_right, LT.lt.trans
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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 y) 0

Tactic:
hy.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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 y) 0

Tactic:
exact hy.ne

Premises used: LT.lt.ne
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
rw₁ rw₂ : stdPart x = stdPart x
⊢ stdPart (x + y) = stdPart x

Tactic:
rw [add_comm, stdPart_add_eq_right hy]

Premises used: ArchimedeanClass.stdPart_add_eq_right, add_comm
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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 : LE.le (α := ArchimedeanClass K) 0 (mk (-y))
⊢ stdPart (x - y) = stdPart x - stdPart y

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, stdPart_add hx, stdPart_neg]

Premises used: sub_eq_add_neg, ArchimedeanClass.stdPart_add, ArchimedeanClass.stdPart_neg
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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 rwa rwa₁ rwa₂ rwa₃ : LE.le (α := ArchimedeanClass K) 0 (mk y)
⊢ LE.le (α := ArchimedeanClass K) 0 (mk (-y))

Tactic:
rwa [mk_neg]

Premises used: ArchimedeanClass.mk_neg
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
rw₂ rw₃ : -stdPart y = -stdPart y
⊢ stdPart (x - y) = -stdPart y

Tactic:
rw [sub_eq_add_neg, stdPart_add_eq_right hx, stdPart_neg]

Premises used: sub_eq_add_neg, ArchimedeanClass.stdPart_add_eq_right, ArchimedeanClass.stdPart_neg
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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)
⊢ LT.lt (α := ArchimedeanClass K) 0 (mk (-y))

Tactic:
simpa
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
rw₁ rw₂ : stdPart x = stdPart x
⊢ stdPart (x - y) = stdPart x

Tactic:
rw [sub_eq_add_neg, stdPart_add_eq_left (by simpa)]

Premises used: sub_eq_add_neg, ArchimedeanClass.stdPart_add_eq_left