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 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) :
        ℝ)
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) =
    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)

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) ⋯) =
    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:
map_mul _ (FiniteElement.mk x hx) (.mk y hy)

Premises used: ArchimedeanClass.FiniteElement.mk, map_mul
-- 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 [div_eq_mul_inv, div_eq_mul_inv, stdPart_mul hx, stdPart_inv]

Premises used: div_eq_mul_inv, ArchimedeanClass.stdPart_mul, ArchimedeanClass.stdPart_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 rwa rwa₁ rwa₂ rwa₃ : LE.le (α := ArchimedeanClass K) 0 (-mk y)
⊢ LE.le (α := ArchimedeanClass K) 0 (mk y⁻¹)

Tactic:
rwa [mk_inv]

Premises used: 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
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 : ℝ) : ℝ)
rw₃ rw₄ : Eq (α := ℝ) (↑q : ℝ) (↑q : ℝ)
⊢ stdPart.{u_1} (K := K) (↑q : K) = (↑q : ℝ)

Tactic:
rw [stdPart_of_mk_nonneg Classical.ofNonempty (mk_ratCast_nonneg q), FiniteElement.mk_ratCast,
    FiniteResidueField.mk_ratCast, map_ratCast]

Premises used: ArchimedeanClass.FiniteResidueField.mk_ratCast, Classical.ofNonempty, map_ratCast, ArchimedeanClass.FiniteElement.mk_ratCast, ArchimedeanClass.mk_ratCast_nonneg, ArchimedeanClass.stdPart_of_mk_nonneg
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
n : ℕ
inst_3 : n.AtLeastTwo
⊢ stdPart.{u_1} (K := K) (OfNat.ofNat n) = (↑n : ℝ)

Tactic:
stdPart_natCast n

Premises used: ArchimedeanClass.stdPart_natCast
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
hc : LE.le (α := ArchimedeanClass K) (0 : ArchimedeanClass K) (mk ((f : (a : ℝ) → K) r) : ArchimedeanClass K)
⊢ stdPart (K := K) ((f : (a : ℝ) → K) r : K) = r

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
f : ℝ →+*o K
r : ℝ
⊢ (OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ)
      (FiniteElement.mk ((f : (a : ℝ) → K) r) ⋯ : FiniteElement K) =
    r

Tactic:
r.ringHom_apply <| OrderRingHom.comp _ (FiniteResidueField.ofArchimedean f)

Premises used: Real.ringHom_apply, Submodule.Quotient.mk, ArchimedeanClass.FiniteResidueField.ofArchimedean, OrderRingHom.comp
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
r : ℝ
⊢ stdPart r = r

Tactic:
stdPart_map_real (.id ℝ) r

Premises used: Real, ArchimedeanClass.stdPart_map_real, OrderRingHom.id
-- 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 : 0 ≤ x
inl : ∀ (hx : Eq (α := ArchimedeanClass K) (mk x) 0), 0 ≤ stdPart x
inr : ∀ (hx : Ne (α := ArchimedeanClass K) (mk x) 0), 0 ≤ stdPart x
⊢ 0 ≤ stdPart x

Tactic:
obtain hx | hx := eq_or_ne (ArchimedeanClass.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
h : 0 ≤ x
hx : Eq (α := ArchimedeanClass K) (mk x) 0
inl :
  LE.le (α := ℝ) (0 : ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk x ⋯) :
      ℝ)
⊢ 0 ≤ stdPart x

Tactic:
rw [stdPart, dif_pos hx.ge]

Premises used: Eq.ge, 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
x : K
h : 0 ≤ x
hx : Eq (α := ArchimedeanClass K) (mk x) 0
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk x ⋯) :
      ℝ)

Tactic:
map_nonneg _ h

Premises used: map_nonneg
-- 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 : 0 ≤ x
hx : Eq (α := ArchimedeanClass K) (mk x) 0
⊢ LE.le (α := ℝ) (0 : ℝ)
    ((OrderRingHom.comp Classical.ofNonempty FiniteResidueField.mk : (a : FiniteElement K) → ℝ) (FiniteElement.mk x ⋯) :
      ℝ)

Tactic:
exact map_nonneg _ h

Premises used: map_nonneg
-- 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 : 0 ≤ x
hx : Ne (α := ArchimedeanClass K) (mk x) 0
inr inr₁ : LE.le (α := ℝ) 0 0
⊢ 0 ≤ stdPart x

Tactic:
rw [stdPart_of_mk_ne_zero hx]

Premises used: ArchimedeanClass.stdPart_of_mk_ne_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
h : x ≤ 0
⊢ stdPart x ≤ 0

Tactic:
simpa using stdPart_nonneg (neg_nonneg.2 h)

Premises used: Iff.mpr, neg_nonneg, ArchimedeanClass.stdPart_nonneg
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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

Tactic:
(FiniteResidueField.mk_eq_zero
    (x := .mk x hx - .mk _ (mk_map_nonneg_of_archimedean f r))).symm.trans ?_

Premises used: ArchimedeanClass.FiniteResidueField.mk_eq_zero, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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)
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) ⋯ : FiniteElement K)) :
        FiniteResidueField K)
      (0 : FiniteResidueField K) ↔
    stdPart x = r
⊢ LT.lt (α := ArchimedeanClass K) 0 (mk (HSub.hSub (β := K) x ((f : (a : ℝ) → K) r : K))) ↔ stdPart x = r

Tactic:
refine (FiniteResidueField.mk_eq_zero
    (x := .mk x hx - .mk _ (mk_map_nonneg_of_archimedean f r))).symm.trans ?_

Premises used: ArchimedeanClass.FiniteResidueField.mk_eq_zero, Iff.trans, Iff.symm
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
rw₄ rw₅ : stdPart x = r ↔ 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

Tactic:
rw [map_sub, ← FiniteResidueField.ofArchimedean_apply, ← ofArchimedean_stdPart f hx,
    sub_eq_zero, FiniteResidueField.ofArchimedean_inj f]

Premises used: ArchimedeanClass.FiniteResidueField.ofArchimedean_apply, map_sub, sub_eq_zero, ArchimedeanClass.FiniteResidueField.ofArchimedean_inj, ArchimedeanClass.ofArchimedean_stdPart
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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)
⊢ LT.lt (α := ArchimedeanClass K) 0 (mk (HSub.hSub (β := K) x ((f : (a : ℝ) → K) (stdPart x) : K)))

Tactic:
(mk_sub_pos_iff f hx).2 rfl

Premises used: Iff.mpr, ArchimedeanClass.mk_sub_pos_iff, rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
rw : (f : (a : ℝ) → K) (r - stdPart x) < HSub.hSub (β := K) x ((f : (a : ℝ) → K) (stdPart x) : K)
⊢ (f : (a : ℝ) → K) r < x

Tactic:
rw [← sub_lt_sub_iff_right (c := f (stdPart x)), ← map_sub]

Premises used: map_sub, sub_lt_sub_iff_right, ArchimedeanClass.stdPart, DFunLike.coe
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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)
hneg : LE.le (α := K) ((f : (a : ℝ) → K) (r - stdPart x) : K) (0 : K)
⊢ (f : (a : ℝ) → K) (r - stdPart x) < HSub.hSub (β := K) x ((f : (a : ℝ) → K) (stdPart x) : K)

Tactic:
apply lt_of_mk_lt_mk_of_nonpos

Premises used: ArchimedeanClass.lt_of_mk_lt_mk_of_nonpos
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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₁ : r - stdPart x ≠ 0
⊢ 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:
rw [mk_map_of_archimedean', mk_sub_pos_iff f hx]

Premises used: ArchimedeanClass.mk_sub_pos_iff, ArchimedeanClass.mk_map_of_archimedean'
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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₁ : ¬r = stdPart x
⊢ r - stdPart x ≠ 0

Tactic:
rw [ne_eq, sub_eq_zero]

Premises used: sub_eq_zero, ne_eq
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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

Tactic:
h.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 : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : r < stdPart x
⊢ ¬r = stdPart x

Tactic:
exact h.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 : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : r < stdPart x
⊢ LE.le (α := K) ((f : (a : ℝ) → K) (r - stdPart x) : K) (0 : K)

Tactic:
simpa using f.monotone' h.le

Premises used: LT.lt.le, 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
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : stdPart x < r
rw : (f : (a : ℝ) → K) (-r) < -x
⊢ x < (f : (a : ℝ) → K) r

Tactic:
rw [← neg_lt_neg_iff, ← map_neg]

Premises used: neg_lt_neg_iff, map_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
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : stdPart x < r
hx₁ : LE.le (α := ArchimedeanClass K) 0 (mk (-x))
h₁ : -r < stdPart (-x)
⊢ (f : (a : ℝ) → K) (-r) < -x

Tactic:
apply lt_of_lt_stdPart

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

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 : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : stdPart x < r
⊢ -r < stdPart (-x)

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 : K
f : ℝ →+*o K
r : ℝ
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : x ≤ (f : (a : ℝ) → K) r
⊢ stdPart x ≤ r

Tactic:
le_imp_le_iff_lt_imp_lt.2 (lt_of_lt_stdPart f hx) h

Premises used: Iff.mpr, ArchimedeanClass.lt_of_lt_stdPart, le_imp_le_iff_lt_imp_lt
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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 : (f : (a : ℝ) → K) r ≤ x
⊢ r ≤ stdPart x

Tactic:
le_imp_le_iff_lt_imp_lt.2 (lt_of_stdPart_lt f hx) h

Premises used: Iff.mpr, ArchimedeanClass.lt_of_stdPart_lt, le_imp_le_iff_lt_imp_lt
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
apply₁ : r + 1 > r
⊢ LE.le (α := ArchimedeanClass K) 0 (mk x)

Tactic:
apply mk_nonneg_of_le_of_le_of_archimedean f (hl (r - 1) _) (hr (r + 1) _)

Premises used: HSub.hSub, HAdd.hAdd, ArchimedeanClass.mk_nonneg_of_le_of_le_of_archimedean, OfNat.ofNat
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
⊢ r - 1 < r

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
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, (f : (a : ℝ) → K) s ≤ x
hr : ∀ s > r, x ≤ (f : (a : ℝ) → K) s
⊢ r + 1 > r

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
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)

Tactic:
have hx : 0 ≤ mk x := by
    apply mk_nonneg_of_le_of_le_of_archimedean f (hl (r - 1) _) (hr (r + 1) _) <;> 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
f : ℝ →+*o K
r : ℝ
hl : ∀ s < r, (f : (a : ℝ) → K) s ≤ x
hr : ∀ s > r, x ≤ (f : (a : ℝ) → K) s
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
inl : ∀ (h : stdPart x < r), stdPart x = r
inr :
  ∀ (hl : ∀ s < stdPart x, (f : (a : ℝ) → K) s ≤ x) (hr : ∀ s > stdPart x, x ≤ (f : (a : ℝ) → K) s),
    stdPart x = stdPart x
inr₁ : ∀ (h : r < stdPart x), stdPart x = r
⊢ stdPart x = r

Tactic:
obtain h | rfl | h := lt_trichotomy (stdPart x) r

Premises used: ArchimedeanClass.stdPart, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : stdPart x < r
inl : ∀ (s : ℝ) (hs : stdPart x < s) (hs' : s < r), stdPart x = r
⊢ stdPart x = r

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_between h

Premises used: exists_between
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : stdPart x < r
s : ℝ
hs : stdPart x < s
hs' : s < r
⊢ stdPart x = r

Tactic:
cases (le_stdPart_of_le f hx (hl _ hs')).not_gt hs

Premises used: LE.le.not_gt, ArchimedeanClass.le_stdPart_of_le
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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)
hl : ∀ s < stdPart x, (f : (a : ℝ) → K) s ≤ x
hr : ∀ s > stdPart x, x ≤ (f : (a : ℝ) → K) s
⊢ stdPart x = stdPart x

Tactic:
rfl
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : r < stdPart x
inr : ∀ (s : ℝ) (hs : r < s) (hs' : s < stdPart x), stdPart x = r
⊢ stdPart x = r

Tactic:
obtain ⟨s, hs, hs'⟩ := exists_between h

Premises used: exists_between
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
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
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
h : r < stdPart x
s : ℝ
hs : r < s
hs' : s < stdPart x
⊢ stdPart x = r

Tactic:
cases (stdPart_le_of_le f hx (hr _ hs)).not_gt hs'

Premises used: LE.le.not_gt, ArchimedeanClass.stdPart_le_of_le
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
inl : ∀ (hx : LE.le (α := ArchimedeanClass K) 0 (mk x)), stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
inr : ∀ (hx : LT.lt (α := ArchimedeanClass K) (mk x) 0), stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
⊢ stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}

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

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
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
inl : ∀ (a : ℤ) (ha : (↑a : K) < x), stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
⊢ stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}

Tactic:
obtain ⟨a, ha⟩ := exists_int_lt_of_mk_nonneg hx

Premises used: ArchimedeanClass.exists_int_lt_of_mk_nonneg
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
a : ℤ
ha : (↑a : K) < x
inl : ∀ (b : ℤ) (hb : x < (↑b : K)), stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}
⊢ stdPart x = sInf {r : ℝ | x < (f : (a : ℝ) → K) r}

Tactic:
obtain ⟨b, hb⟩ := exists_int_gt_of_mk_nonneg hx

Premises used: ArchimedeanClass.exists_int_gt_of_mk_nonneg
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
a : ℤ
ha : (↑a : K) < x
b : ℤ
hb : x < (↑b : K)
⊢ Membership.mem (γ := Set ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r} (↑b : ℝ)

Tactic:
simpa using hb
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
a : ℤ
ha : (↑a : K) < x
b : ℤ
hb : x < (↑b : K)
⊢ Set.Nonempty (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}

Tactic:
have hn : {r | x < f r}.Nonempty := ⟨b, by simpa using hb⟩
-- Module: Mathlib.Algebra.Order.Ring.StandardPart
Goal:
K : Type u_1
inst : LinearOrder K
inst_1 : Field K
inst_2 : IsOrderedRing K
f : ℝ →+*o K
x : K
hx : LE.le (α := ArchimedeanClass K) 0 (mk x)
a : ℤ
ha : (↑a : K) < x
b : ℤ
hb : x < (↑b : K)
hn : Set.Nonempty (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}
⊢ BddBelow (α := ℝ) {r : ℝ | x < (f : (a : ℝ) → K) r}

Tactic:
⟨a, fun r hr ↦ ?_⟩

Premises used: Int.cast, Set.Nonempty, BddBelow, Exists.intro