awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
refine_1 : ∀ (h : x.InfinitePos), 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
refine_2 :
  0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0 →
    ∀ (r : ℝ) (hx : 0 < x) (hx' : LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0), (↑r : ℝ*) < x
⊢ x.InfinitePos ↔ 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨hx, hx'⟩ r ↦ ?_⟩
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x.InfinitePos
⊢ 0 < x

Tactic:
have hx : 0 < x := h 0
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x.InfinitePos
hx : 0 < x
⊢ 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0

Tactic:
⟨h 0, fun n ↦ ?_⟩

Premises used: And.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x.InfinitePos
hx : 0 < x
refine_1 :
  ∀ (n : ℕ),
    HSMul.hSMul (β := ℝ*) n
        (|(ArchimedeanOrder.val : (a : ArchimedeanOrder ℝ*) → ℝ*)
              ((ArchimedeanOrder.of : (a : ℝ*) → ArchimedeanOrder ℝ*) 1)| :
          ℝ*) <
      |(ArchimedeanOrder.val : (a : ArchimedeanOrder ℝ*) → ℝ*)
          ((ArchimedeanOrder.of : (a : ℝ*) → ArchimedeanOrder ℝ*) x)|
⊢ 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0

Tactic:
refine ⟨h 0, fun n ↦ ?_⟩
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x.InfinitePos
hx : 0 < x
n : ℕ
⊢ HSMul.hSMul (β := ℝ*) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder ℝ*) → ℝ*)
            ((ArchimedeanOrder.of : (a : ℝ*) → ArchimedeanOrder ℝ*) 1)| :
        ℝ*) <
    |(ArchimedeanOrder.val : (a : ArchimedeanOrder ℝ*) → ℝ*) ((ArchimedeanOrder.of : (a : ℝ*) → ArchimedeanOrder ℝ*) x)|

Tactic:
simpa [abs_of_pos hx] using h n

Premises used: Nat.cast, abs_of_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
r : ℝ
hx : 0 < x
hx' : LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
⊢ (↑r : ℝ*) < x

Tactic:
lt_of_mk_lt_mk_of_nonneg (hx'.trans_le <| mk_map_nonneg_of_archimedean coeRingHom _) hx.le

Premises used: ArchimedeanClass.mk_map_nonneg_of_archimedean, LT.lt.le, LT.lt.trans_le, ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg, Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
r : ℝ
hx : 0 < x
hx' : LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
⊢ (↑r : ℝ*) < x

Tactic:
exact lt_of_mk_lt_mk_of_nonneg (hx'.trans_le <| mk_map_nonneg_of_archimedean coeRingHom _) hx.le

Premises used: ArchimedeanClass.mk_map_nonneg_of_archimedean, LT.lt.le, LT.lt.trans_le, ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg, Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.InfiniteNeg ↔ x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0

Tactic:
⟨fun h ↦ ?_, fun ⟨hx, hx'⟩ r ↦ ?_⟩

Premises used: Hyperreal.ofReal, _private.0.Hyperreal.infiniteNeg_iff.match_1, LT.lt, Iff.intro
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
refine_1 : ∀ (h : x.InfiniteNeg), x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
refine_2 :
  x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0 →
    ∀ (r : ℝ) (hx : x < 0) (hx' : LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0), x < (↑r : ℝ*)
⊢ x.InfiniteNeg ↔ x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨hx, hx'⟩ r ↦ ?_⟩
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x.InfiniteNeg
⊢ x < 0

Tactic:
have hx : x < 0 := h 0
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x.InfiniteNeg
hx : x < 0
⊢ x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0

Tactic:
⟨h 0, fun n ↦ ?_⟩

Premises used: And.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x.InfiniteNeg
hx : x < 0
refine_1 :
  ∀ (n : ℕ),
    HSMul.hSMul (β := ℝ*) n
        (|(ArchimedeanOrder.val : (a : ArchimedeanOrder ℝ*) → ℝ*)
              ((ArchimedeanOrder.of : (a : ℝ*) → ArchimedeanOrder ℝ*) 1)| :
          ℝ*) <
      |(ArchimedeanOrder.val : (a : ArchimedeanOrder ℝ*) → ℝ*)
          ((ArchimedeanOrder.of : (a : ℝ*) → ArchimedeanOrder ℝ*) x)|
⊢ x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0

Tactic:
refine ⟨h 0, fun n ↦ ?_⟩
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x.InfiniteNeg
hx : x < 0
n : ℕ
⊢ HSMul.hSMul (β := ℝ*) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder ℝ*) → ℝ*)
            ((ArchimedeanOrder.of : (a : ℝ*) → ArchimedeanOrder ℝ*) 1)| :
        ℝ*) <
    |(ArchimedeanOrder.val : (a : ArchimedeanOrder ℝ*) → ℝ*) ((ArchimedeanOrder.of : (a : ℝ*) → ArchimedeanOrder ℝ*) x)|

Tactic:
simpa [abs_of_neg hx, lt_neg] using h (-n)

Premises used: lt_neg, abs_of_neg, Nat.cast, Neg.neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
r : ℝ
hx : x < 0
hx' : LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
⊢ x < (↑r : ℝ*)

Tactic:
lt_of_mk_lt_mk_of_nonpos (hx'.trans_le <| mk_map_nonneg_of_archimedean coeRingHom _) hx.le

Premises used: ArchimedeanClass.mk_map_nonneg_of_archimedean, LT.lt.le, LT.lt.trans_le, ArchimedeanClass.lt_of_mk_lt_mk_of_nonpos, Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
r : ℝ
hx : x < 0
hx' : LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
⊢ x < (↑r : ℝ*)

Tactic:
exact lt_of_mk_lt_mk_of_nonpos (hx'.trans_le <| mk_map_nonneg_of_archimedean coeRingHom _) hx.le

Premises used: ArchimedeanClass.mk_map_nonneg_of_archimedean, LT.lt.le, LT.lt.trans_le, ArchimedeanClass.lt_of_mk_lt_mk_of_nonpos, Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
rw :
  0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0 ∨
      x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0 ↔
    LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
⊢ x.Infinite ↔ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0

Tactic:
rw [Infinite, infinitePos_iff, infiniteNeg_iff]

Premises used: Hyperreal.infinitePos_iff, Hyperreal.Infinite, Hyperreal.infiniteNeg_iff
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0 ∨
      x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0 ↔
    LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
r : ℝ
⊢ (ofSeq f).IsSt r ↔ Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 r)

Tactic:
Iff.trans (forall₂_congr fun _ _ ↦ (ofSeq_lt_ofSeq.and ofSeq_lt_ofSeq).trans eventually_and.symm)
    (nhds_basis_Ioo_pos _).tendsto_right_iff.symm

Premises used: Filter.eventually_and, nhds_basis_Ioo_pos, forall₂_congr, Iff.and, Iff.trans, Filter.HasBasis.tendsto_right_iff, Iff.symm, Hyperreal.ofSeq_lt_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
rcases : ∀ (f : ℕ → ℝ), (ofSeq f).IsSt r ↔ Germ.Tendsto (ofSeq f) (𝓝 r)
⊢ x.IsSt r ↔ Germ.Tendsto x (𝓝 r)

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩

Premises used: Hyperreal.ofSeq_surjective, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
⊢ (ofSeq f).IsSt r ↔ Germ.Tendsto (ofSeq f) (𝓝 r)

Tactic:
isSt_ofSeq_iff_tendsto

Premises used: Quotient.liftOn', Filter.Germ.Tendsto, Filter.Tendsto, Filter.Germ.liftOn, Hyperreal.isSt_ofSeq_iff_tendsto
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
⊢ (ofSeq f).IsSt r ↔ Germ.Tendsto (ofSeq f) (𝓝 r)

Tactic:
exact isSt_ofSeq_iff_tendsto

Premises used: Hyperreal.isSt_ofSeq_iff_tendsto
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
r : ℝ
hf : Tendsto f atTop (𝓝 r)
⊢ (ofSeq f).IsSt r

Tactic:
isSt_ofSeq_iff_tendsto.2 <| hf.mono_left Nat.hyperfilter_le_atTop

Premises used: Iff.mpr, Nat.hyperfilter_le_atTop, Filter.Tendsto.mono_left, Hyperreal.isSt_ofSeq_iff_tendsto
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
r s : ℝ
hxr : x.IsSt r
hys : y.IsSt s
hrs : r < s
rcases : ∀ (f : ℕ → ℝ) (hxr : (ofSeq f).IsSt r), ofSeq f < y
⊢ x < y

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩

Premises used: Hyperreal.ofSeq_surjective, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
y : ℝ*
r s : ℝ
hys : y.IsSt s
hrs : r < s
f : ℕ → ℝ
hxr : (ofSeq f).IsSt r
rcases : ∀ (g : ℕ → ℝ) (hys : (ofSeq g).IsSt s), ofSeq f < ofSeq g
⊢ ofSeq f < y

Tactic:
rcases ofSeq_surjective y with ⟨g, rfl⟩

Premises used: Hyperreal.ofSeq_surjective, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : (ofSeq f).IsSt r
g : ℕ → ℝ
hys : (ofSeq g).IsSt s
rw :
  ∀ (hxr : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 r)) (g : ℕ → ℝ)
    (hys : Tendsto g (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 s)), ofSeq f < ofSeq g
⊢ ofSeq f < ofSeq g

Tactic:
rw [isSt_ofSeq_iff_tendsto] at hxr hys

Premises used: Hyperreal.isSt_ofSeq_iff_tendsto
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 r)
g : ℕ → ℝ
hys : Tendsto g (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 s)
⊢ ofSeq f < ofSeq g

Tactic:
ofSeq_lt_ofSeq.2 <| hxr.eventually_lt hys hrs

Premises used: Iff.mpr, Filter.Tendsto.eventually_lt, Hyperreal.ofSeq_lt_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 r)
g : ℕ → ℝ
hys : Tendsto g (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 s)
⊢ ofSeq f < ofSeq g

Tactic:
exact ofSeq_lt_ofSeq.2 <| hxr.eventually_lt hys hrs

Premises used: Iff.mpr, Filter.Tendsto.eventually_lt, Hyperreal.ofSeq_lt_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r s : ℝ
hr : x.IsSt r
hs : x.IsSt s
rcases : ∀ (f : ℕ → ℝ) (hr : (ofSeq f).IsSt r) (hs : (ofSeq f).IsSt s), r = s
⊢ r = s

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩

Premises used: Hyperreal.ofSeq_surjective, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s : ℝ
f : ℕ → ℝ
hr : (ofSeq f).IsSt r
hs : (ofSeq f).IsSt s
⊢ Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 r)

Tactic:
rw [isSt_ofSeq_iff_tendsto] at hr hs

Premises used: Hyperreal.isSt_ofSeq_iff_tendsto
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s : ℝ
f : ℕ → ℝ
hr : (ofSeq f).IsSt r
hs : (ofSeq f).IsSt s
hr₁ : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 r)
⊢ Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 s)

Tactic:
rw [isSt_ofSeq_iff_tendsto] at hr hs

Premises used: Hyperreal.isSt_ofSeq_iff_tendsto
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s : ℝ
f : ℕ → ℝ
hr : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 r)
hs : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 s)
⊢ r = s

Tactic:
tendsto_nhds_unique hr hs

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s : ℝ
f : ℕ → ℝ
hr : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 r)
hs : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 s)
⊢ r = s

Tactic:
exact tendsto_nhds_unique hr hs

Premises used: tendsto_nhds_unique
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hxr : x.IsSt r
⊢ ∃ (r : ℝ), x.IsSt r

Tactic:
have h : ∃ r, IsSt x r := ⟨r, hxr⟩
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hxr : x.IsSt r
h : ∃ (r : ℝ), x.IsSt r
rw : Classical.choose (p := x.IsSt) h = r
⊢ x.st = r

Tactic:
rw [st, dif_pos h]

Premises used: dif_pos, Hyperreal.st
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hxr : x.IsSt r
h : ∃ (r : ℝ), x.IsSt r
⊢ Classical.choose (p := x.IsSt) h = r

Tactic:
(Classical.choose_spec h).unique hxr

Premises used: Hyperreal.IsSt.unique, Classical.choose_spec
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hxr : x.IsSt r
h : ∃ (r : ℝ), x.IsSt r
⊢ Classical.choose (p := x.IsSt) h = r

Tactic:
exact (Classical.choose_spec h).unique hxr

Premises used: Hyperreal.IsSt.unique, Classical.choose_spec
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
h : x.IsSt r
⊢ ¬x.Infinite

Tactic:
fun hi ↦
  hi.elim (fun hp ↦ lt_asymm (h 1 one_pos).2 (hp (r + 1))) fun hn ↦
    lt_asymm (h 1 one_pos).1 (hn (r - 1))

Premises used: HSub.hSub, lt_asymm, And.right, And.left, HAdd.hAdd, Or.elim, OfNat.ofNat, one_pos, Not
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ (∃ (r : ℝ), x.IsSt r) → ¬x.Infinite

Tactic:
fun ⟨_r, hr⟩ =>
  hr.not_infinite

Premises used: Hyperreal.IsSt.not_infinite, Hyperreal.Infinite, _private.0.Hyperreal.not_infinite_of_exists_st.match_1, Not
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hi : x.Infinite
⊢ x.st = 0

Tactic:
dif_neg fun ⟨_r, hr⟩ ↦ hr.not_infinite hi

Premises used: dif_neg, Hyperreal.st
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hni : ¬x.Infinite
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)

Tactic:
rw [infinite_iff, not_lt] at hni

Premises used: Hyperreal.infinite_iff, not_lt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hni : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
rw : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = sSup {y : ℝ | (↑y : ℝ*) < x}
⊢ x.IsSt (sSup {y : ℝ | (↑y : ℝ*) < x})

Tactic:
rw [isSt_iff]

Premises used: Hyperreal.isSt_iff
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hni : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = sSup {y : ℝ | (↑y : ℝ*) < x}

Tactic:
⟨hni, stdPart_eq_sSup coeRingHom x⟩

Premises used: And.intro, Hyperreal.coeRingHom, ArchimedeanClass.stdPart_eq_sSup
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hni : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = sSup {y : ℝ | (↑y : ℝ*) < x}

Tactic:
exact ⟨hni, stdPart_eq_sSup coeRingHom x⟩
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hni : ¬x.Infinite
⊢ ∃ (r : ℝ), x.IsSt r

Tactic:
⟨sSup { y : ℝ | (y : ℝ*) < x }, isSt_sSup hni⟩

Premises used: setOf, Hyperreal.isSt_sSup, Hyperreal.ofReal, LT.lt, Exists.intro, SupSet.sSup
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
rw : stdPart x = sSup {y : ℝ | (↑y : ℝ*) < x}
⊢ x.st = sSup {y : ℝ | (↑y : ℝ*) < x}

Tactic:
rw [st_eq]

Premises used: Hyperreal.st_eq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ stdPart x = sSup {y : ℝ | (↑y : ℝ*) < x}

Tactic:
stdPart_eq_sSup coeRingHom x

Premises used: Filter.Germ.ofFun, setOf, Filter.Germ.const, Hyperreal.ofReal, Quotient.mk', Hyperreal.coeRingHom, ArchimedeanClass.stdPart_eq_sSup
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ stdPart x = sSup {y : ℝ | (↑y : ℝ*) < x}

Tactic:
exact stdPart_eq_sSup coeRingHom x

Premises used: Hyperreal.coeRingHom, ArchimedeanClass.stdPart_eq_sSup
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ (∃ (r : ℝ), x.IsSt r) ↔ ¬x.Infinite

Tactic:
⟨not_infinite_of_exists_st, exists_st_of_not_infinite⟩

Premises used: Hyperreal.not_infinite_of_exists_st, Iff.intro, Hyperreal.exists_st_of_not_infinite
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.Infinite ↔ ¬∃ (r : ℝ), x.IsSt r

Tactic:
iff_not_comm.mp exists_st_iff_not_infinite

Premises used: iff_not_comm, Hyperreal.exists_st_iff_not_infinite, Iff.mp
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hxr rwa rwa₁ rwa₂ rwa₃ : x.IsSt r
⊢ x.IsSt x.st

Tactic:
rwa [hxr.st_eq]

Premises used: Hyperreal.IsSt.st_eq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hx : ∃ (r : ℝ), x.IsSt r
⊢ x.IsSt x.st

Tactic:
let ⟨_r, hr⟩ := hx; hr.isSt_st

Premises used: Hyperreal.IsSt.isSt_st, _private.0.Hyperreal.not_infinite_of_exists_st.match_1, Hyperreal.IsSt, Hyperreal.st
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hx : ¬x.Infinite
⊢ x.IsSt x.st

Tactic:
(isSt_sSup hx).isSt_st

Premises used: Hyperreal.isSt_sSup, Hyperreal.IsSt.isSt_st
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hx : x.st ≠ 0
⊢ x.IsSt x.st

Tactic:
isSt_st' <| mt Infinite.st_eq hx

Premises used: mt, Hyperreal.Infinite.st_eq, Hyperreal.isSt_st'
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
⊢ (↑r : ℝ*).IsSt r

Tactic:
isSt_ofSeq_iff_tendsto.2 tendsto_const_nhds

Premises used: Iff.mpr, tendsto_const_nhds, Filter.Germ.const, Hyperreal.ofReal, Hyperreal.isSt_ofSeq_iff_tendsto
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
⊢ (↑r : ℝ*).st = r

Tactic:
(isSt_refl_real r).st_eq

Premises used: Hyperreal.IsSt.st_eq, Hyperreal.isSt_refl_real
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s : ℝ
⊢ (↑r : ℝ*).IsSt s → r = s

Tactic:
(isSt_refl_real r).unique

Premises used: Hyperreal.isSt_refl_real, Hyperreal.IsSt.unique
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s : ℝ
⊢ (↑r : ℝ*).IsSt s ↔ r = s

Tactic:
⟨eq_of_isSt_real, fun hrs => hrs ▸ isSt_refl_real r⟩

Premises used: Hyperreal.eq_of_isSt_real, Eq.rec, Hyperreal.isSt_refl_real, Iff.intro
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s : ℝ
rw : r = s ↔ (↑s : ℝ*).IsSt r
rw₁ : r = s ↔ s = r
rw₂ rw₃ : s = r ↔ s = r
⊢ (↑r : ℝ*).IsSt s ↔ (↑s : ℝ*).IsSt r

Tactic:
rw [isSt_real_iff_eq, isSt_real_iff_eq, eq_comm]

Premises used: eq_comm, Hyperreal.isSt_real_iff_eq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s t : ℝ
rw : r = s → s = t → r = t
⊢ (↑r : ℝ*).IsSt s → (↑s : ℝ*).IsSt t → (↑r : ℝ*).IsSt t

Tactic:
rw [isSt_real_iff_eq, isSt_real_iff_eq, isSt_real_iff_eq]

Premises used: Hyperreal.isSt_real_iff_eq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s t : ℝ
⊢ r = s → s = t → r = t

Tactic:
Eq.trans

Premises used: Eq.trans
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s t : ℝ
⊢ r = s → s = t → r = t

Tactic:
exact Eq.trans

Premises used: Eq.trans
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r₁ r₂ s : ℝ
h1 : (↑r₁ : ℝ*).IsSt s
h2 : (↑r₂ : ℝ*).IsSt s
⊢ r₁ = r₂

Tactic:
Eq.trans (eq_of_isSt_real h1) (eq_of_isSt_real h2).symm

Premises used: Hyperreal.eq_of_isSt_real, Eq.symm, Eq.trans
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
⊢ x.IsSt r ↔ ∀ (δ : ℝ), 0 < δ → |x - (↑r : ℝ*)| < (↑δ : ℝ*)

Tactic:
simp only [abs_sub_lt_iff, sub_lt_iff_lt_add, IsSt, and_comm, add_comm]

Premises used: abs_sub_lt_iff, and_comm, add_comm, sub_lt_iff_lt_add, Hyperreal.IsSt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hxr : x.IsSt r
f : ℝ → ℝ
hf : ContinuousAt f r
rcases : ∀ (g : ℕ → ℝ) (hxr : (ofSeq g).IsSt r), IsSt (Germ.map f (ofSeq g)) (f r)
⊢ IsSt (Germ.map f x) (f r)

Tactic:
rcases ofSeq_surjective x with ⟨g, rfl⟩

Premises used: Hyperreal.ofSeq_surjective, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
g : ℕ → ℝ
hxr : (ofSeq g).IsSt r
⊢ IsSt (Germ.map f (ofSeq g)) (f r)

Tactic:
isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (isSt_ofSeq_iff_tendsto.1 hxr)

Premises used: Iff.mpr, Filter.Germ.map', ContinuousAt.tendsto, Quot.map, Iff.mp, Quotient.map', Filter.Germ.map, Filter.Tendsto.comp, Hyperreal.ofSeq, Hyperreal.isSt_ofSeq_iff_tendsto
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
g : ℕ → ℝ
hxr : (ofSeq g).IsSt r
⊢ IsSt (Germ.map f (ofSeq g)) (f r)

Tactic:
exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (isSt_ofSeq_iff_tendsto.1 hxr)

Premises used: Iff.mpr, ContinuousAt.tendsto, Iff.mp, Filter.Tendsto.comp, Hyperreal.isSt_ofSeq_iff_tendsto
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
r s : ℝ
hxr : x.IsSt r
hys : y.IsSt s
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
rcases : ∀ (x : ℕ → ℝ) (hxr : (ofSeq x).IsSt r), IsSt (Germ.map₂ f (ofSeq x) y) (f r s)
⊢ IsSt (Germ.map₂ f x y) (f r s)

Tactic:
rcases ofSeq_surjective x with ⟨x, rfl⟩

Premises used: Hyperreal.ofSeq_surjective, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
y : ℝ*
r s : ℝ
hys : y.IsSt s
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : (ofSeq x).IsSt r
rcases : ∀ (y : ℕ → ℝ) (hys : (ofSeq y).IsSt s), IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
⊢ IsSt (Germ.map₂ f (ofSeq x) y) (f r s)

Tactic:
rcases ofSeq_surjective y with ⟨y, rfl⟩

Premises used: Hyperreal.ofSeq_surjective, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : (ofSeq x).IsSt r
y : ℕ → ℝ
hys : (ofSeq y).IsSt s
rw :
  ∀ (hxr : Tendsto x (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 r)) (y : ℕ → ℝ)
    (hys : Tendsto y (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 s)), IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)

Tactic:
rw [isSt_ofSeq_iff_tendsto] at hxr hys

Premises used: Hyperreal.isSt_ofSeq_iff_tendsto
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Tendsto x (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 r)
y : ℕ → ℝ
hys : Tendsto y (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 s)
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)

Tactic:
isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (hxr.prodMk_nhds hys)

Premises used: Iff.mpr, Quotient.map₂, Filter.Germ.map₂, ContinuousAt.tendsto, Filter.Tendsto.comp, Hyperreal.ofSeq, Filter.Tendsto.prodMk_nhds, Hyperreal.isSt_ofSeq_iff_tendsto
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Tendsto x (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 r)
y : ℕ → ℝ
hys : Tendsto y (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 s)
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)

Tactic:
exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (hxr.prodMk_nhds hys)

Premises used: Iff.mpr, ContinuousAt.tendsto, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds, Hyperreal.isSt_ofSeq_iff_tendsto
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
r s : ℝ
hxr : x.IsSt r
hys : y.IsSt s
⊢ (x + y).IsSt (r + s)

Tactic:
hxr.map₂ hys continuous_add.continuousAt

Premises used: Quotient.map₂, Hyperreal.IsSt.map₂, Filter.Germ.map₂, Continuous.continuousAt, continuous_add
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hxr : x.IsSt r
⊢ (-x).IsSt (-r)

Tactic:
hxr.map continuous_neg.continuousAt

Premises used: Hyperreal.IsSt.map, ContinuousNeg.continuous_neg, Filter.Germ.map', Continuous.continuousAt, Quot.map, Quotient.map', Filter.Germ.map
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
r s : ℝ
hxr : x.IsSt r
hys : y.IsSt s
⊢ (x - y).IsSt (r - s)

Tactic:
hxr.map₂ hys continuous_sub.continuousAt

Premises used: Quotient.map₂, Hyperreal.IsSt.map₂, Filter.Germ.map₂, Continuous.continuousAt, ContinuousSub.continuous_sub
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
r s : ℝ
hrx : x.IsSt r
hsy : y.IsSt s
hxy : x ≤ y
⊢ r ≤ s

Tactic:
not_lt.1 fun h ↦ hxy.not_gt <| hsy.lt hrx h

Premises used: not_lt, LE.le.not_gt, Iff.mp, Hyperreal.IsSt.lt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hix : ¬x.Infinite
hiy : ¬y.Infinite
⊢ x ≤ y → x.st ≤ y.st

Tactic:
(isSt_st' hix).le (isSt_st' hiy)

Premises used: Hyperreal.IsSt.le, Hyperreal.isSt_st'
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hix : ¬x.Infinite
hiy : ¬y.Infinite
⊢ x.st < y.st → x < y

Tactic:
(isSt_st' hix).lt (isSt_st' hiy)

Premises used: Hyperreal.IsSt.lt, Hyperreal.isSt_st'
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.InfinitePos ↔ ∀ (r : ℝ), (↑r : ℝ*) < x

Tactic:
Iff.rfl

Premises used: Iff.rfl, Hyperreal.InfinitePos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.InfiniteNeg ↔ ∀ (r : ℝ), x < (↑r : ℝ*)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Hyperreal.InfiniteNeg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hip : x.InfinitePos
⊢ 0 < x

Tactic:
hip 0

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Hyperreal.ofReal, Quotient.mk', OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.InfiniteNeg → x < 0

Tactic:
fun hin => hin 0

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Hyperreal.ofReal, Quotient.mk', OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hI : x.Infinite
⊢ x ≠ 0

Tactic:
hI.elim (fun hip => hip.pos.ne') fun hin => hin.lt_zero.ne

Premises used: Hyperreal.InfiniteNeg.lt_zero, LT.lt.ne', Hyperreal.InfinitePos.pos, Or.elim, LT.lt.ne
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ ¬Infinite 0

Tactic:
fun hI => hI.ne_zero rfl

Premises used: Hyperreal.Infinite.ne_zero, Not, rfl