awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.InfiniteNeg → ¬x.InfinitePos

Tactic:
fun hn hp =>
  (hn 0).not_gt (hp 0)

Premises used: LT.lt.not_gt, OfNat.ofNat, Not
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hp : x.InfinitePos
⊢ ¬x.InfiniteNeg

Tactic:
fun hn ↦
  hn.not_infinitePos hp

Premises used: Not, Hyperreal.InfiniteNeg.not_infinitePos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.InfinitePos → (-x).InfiniteNeg

Tactic:
fun hp r =>
  neg_lt.mp (hp (-r))

Premises used: Hyperreal.InfiniteNeg, Iff.mp, neg_lt, Neg.neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.InfiniteNeg → (-x).InfinitePos

Tactic:
fun hp r =>
  lt_neg.mp (hp (-r))

Premises used: lt_neg, Hyperreal.InfinitePos, Iff.mp, Neg.neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ (-x).InfiniteNeg ↔ x.InfinitePos

Tactic:
⟨fun hin => neg_neg x ▸ hin.neg, InfinitePos.neg⟩

Premises used: Hyperreal.InfiniteNeg.neg, Hyperreal.InfinitePos.neg, Eq.rec, neg_neg, Iff.intro
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ (-x).InfinitePos ↔ x.InfiniteNeg

Tactic:
⟨fun hin => neg_neg x ▸ hin.neg, InfiniteNeg.neg⟩

Premises used: Hyperreal.InfiniteNeg.neg, Hyperreal.InfinitePos.neg, Eq.rec, neg_neg, Iff.intro
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ (-x).Infinite ↔ x.Infinite

Tactic:
or_comm.trans <| infiniteNeg_neg.or infinitePos_neg

Premises used: Hyperreal.infinitePos_neg, Iff.or, Hyperreal.Infinite, Iff.trans, Hyperreal.infiniteNeg_neg, or_comm
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x.Infinitesimal
⊢ ¬x.Infinite

Tactic:
h.not_infinite

Premises used: Hyperreal.IsSt.not_infinite
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x.Infinite
⊢ ¬x.Infinitesimal

Tactic:
fun h' ↦
  h'.not_infinite h

Premises used: Hyperreal.Infinitesimal.not_infinite, Not
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x.InfinitePos
⊢ ¬x.Infinitesimal

Tactic:
Infinite.not_infinitesimal (Or.inl h)

Premises used: Or.inl, Hyperreal.Infinite.not_infinitesimal
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x.InfiniteNeg
⊢ ¬x.Infinitesimal

Tactic:
Infinite.not_infinitesimal (Or.inr h)

Premises used: Hyperreal.Infinite.not_infinitesimal, Or.inr
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.InfinitePos ↔ x.Infinite ∧ 0 < x

Tactic:
⟨fun hip => ⟨Or.inl hip, hip 0⟩, fun ⟨hi, hp⟩ =>
    hi.casesOn id fun hin => False.elim (not_lt_of_gt hp (hin 0))⟩

Premises used: _private.0.Hyperreal.infinitePos_iff_infinite_and_pos.match_1, Hyperreal.InfinitePos, Or.casesOn, And.intro, Iff.intro, Or.inl, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.InfiniteNeg ↔ x.Infinite ∧ x < 0

Tactic:
⟨fun hip => ⟨Or.inr hip, hip 0⟩, fun ⟨hi, hp⟩ =>
    hi.casesOn (fun hin => False.elim (not_lt_of_gt hp (hin 0))) fun hip => hip⟩

Premises used: _private.0.Hyperreal.infiniteNeg_iff_infinite_and_neg.match_1, Or.casesOn, Hyperreal.InfiniteNeg, And.intro, Iff.intro, OfNat.ofNat, Or.inr
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hp : 0 ≤ x
⊢ x.InfinitePos ↔ x.Infinite

Tactic:
.symm <| or_iff_left fun h ↦ h.lt_zero.not_ge hp

Premises used: Hyperreal.InfiniteNeg.lt_zero, or_iff_left, LT.lt.not_ge, Iff.symm
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hp : 0 < x
⊢ x.InfinitePos ↔ x.Infinite

Tactic:
infinitePos_iff_infinite_of_nonneg hp.le

Premises used: LT.lt.le, Hyperreal.infinitePos_iff_infinite_of_nonneg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hn : x < 0
⊢ x.InfiniteNeg ↔ x.Infinite

Tactic:
.symm <| or_iff_right fun h ↦ h.pos.not_gt hn

Premises used: LT.lt.not_gt, or_iff_right, Hyperreal.InfinitePos.pos, Iff.symm
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ |x|.InfinitePos ↔ |x|.Infinite

Tactic:
infinitePos_iff_infinite_of_nonneg (abs_nonneg _)

Premises used: Hyperreal.infinitePos_iff_infinite_of_nonneg, abs_nonneg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
inl : 0 ≤ x → (|x|.Infinite ↔ x.Infinite)
inr : x ≤ 0 → (|x|.Infinite ↔ x.Infinite)
⊢ |x|.Infinite ↔ x.Infinite

Tactic:
cases le_total 0 x

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : 0 ≤ x
⊢ |x|.Infinite ↔ x.Infinite

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos, infinite_neg]

Premises used: Hyperreal.infinite_neg, abs_of_nonpos, abs_of_nonneg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x ≤ 0
⊢ |x|.Infinite ↔ x.Infinite

Tactic:
simp [*, abs_of_nonneg, abs_of_nonpos, infinite_neg]

Premises used: Hyperreal.infinite_neg, abs_of_nonpos, abs_of_nonneg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ |x|.InfinitePos ↔ x.Infinite

Tactic:
infinitePos_abs_iff_infinite_abs.trans infinite_abs_iff

Premises used: Hyperreal.infinite_abs_iff, Hyperreal.infinitePos_abs_iff_infinite_abs, Iff.trans
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.Infinite ↔ ∀ (r : ℝ), |(↑r : ℝ*)| < |x|

Tactic:
infinitePos_abs_iff_infinite.symm.trans ⟨fun hI r => coe_abs r ▸ hI |r|, fun hR r =>
    (le_abs_self _).trans_lt (hR r)⟩

Premises used: le_abs_self, abs, Eq.rec, Hyperreal.ofReal, Iff.intro, Iff.trans, Hyperreal.coe_abs, LE.le.trans_lt, Hyperreal.infinitePos_abs_iff_infinite, Iff.symm
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hip : x.InfinitePos
hnin : ¬y.InfiniteNeg
r : ℝ
obtain : ∀ (r₂ : ℝ) (hr₂ : ¬y < (↑r₂ : ℝ*)), (↑r : ℝ*) < x + y
⊢ (↑r : ℝ*) < x + y

Tactic:
obtain ⟨r₂, hr₂⟩ := not_forall.mp hnin

Premises used: Iff.mp, Classical.not_forall
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hip : x.InfinitePos
hnin : ¬y.InfiniteNeg
r r₂ : ℝ
hr₂ : ¬y < (↑r₂ : ℝ*)
⊢ (↑(r + -r₂) : ℝ*) + (↑r₂ : ℝ*) < x + y

Tactic:
add_lt_add_of_lt_of_le (hip (r + -r₂)) (not_lt.mp hr₂)

Premises used: add_lt_add_of_lt_of_le, not_lt, HAdd.hAdd, Iff.mp, Neg.neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hip : x.InfinitePos
hnin : ¬y.InfiniteNeg
r r₂ : ℝ
hr₂ : ¬y < (↑r₂ : ℝ*)
h : (↑r : ℝ*) = (↑(r + -r₂) : ℝ*) + (↑r₂ : ℝ*)
⊢ (↑r : ℝ*) < x + y

Tactic:
convert! add_lt_add_of_lt_of_le (hip (r + -r₂)) (not_lt.mp hr₂) using 1

Premises used: add_lt_add_of_lt_of_le, not_lt, HAdd.hAdd, Iff.mp, Neg.neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hip : x.InfinitePos
hnin : ¬y.InfiniteNeg
r r₂ : ℝ
hr₂ : ¬y < (↑r₂ : ℝ*)
⊢ (↑r : ℝ*) = (↑(r + -r₂) : ℝ*) + (↑r₂ : ℝ*)

Tactic:
simp
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ ¬x.InfiniteNeg → y.InfinitePos → (x + y).InfinitePos

Tactic:
fun hx hy =>
  add_comm y x ▸ infinitePos_add_not_infiniteNeg hy hx

Premises used: Hyperreal.infinitePos_add_not_infiniteNeg, Eq.rec, add_comm
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
rw : (-x).InfinitePos → ¬(-y).InfiniteNeg → (-x + -y).InfinitePos
⊢ x.InfiniteNeg → ¬y.InfinitePos → (x + y).InfiniteNeg

Tactic:
rw [← infinitePos_neg, ← infinitePos_neg, ← @infiniteNeg_neg y, neg_add]

Premises used: Hyperreal.infinitePos_neg, neg_add, Hyperreal.infiniteNeg_neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ (-x).InfinitePos → ¬(-y).InfiniteNeg → (-x + -y).InfinitePos

Tactic:
infinitePos_add_not_infiniteNeg

Premises used: Hyperreal.infinitePos_add_not_infiniteNeg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ (-x).InfinitePos → ¬(-y).InfiniteNeg → (-x + -y).InfinitePos

Tactic:
exact infinitePos_add_not_infiniteNeg

Premises used: Hyperreal.infinitePos_add_not_infiniteNeg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ ¬x.InfinitePos → y.InfiniteNeg → (x + y).InfiniteNeg

Tactic:
fun hx hy =>
  add_comm y x ▸ infiniteNeg_add_not_infinitePos hy hx

Premises used: Eq.rec, add_comm, Hyperreal.infiniteNeg_add_not_infinitePos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ x.InfinitePos → y.InfinitePos → (x + y).InfinitePos

Tactic:
fun hx hy =>
  infinitePos_add_not_infiniteNeg hx hy.not_infiniteNeg

Premises used: Hyperreal.infinitePos_add_not_infiniteNeg, Hyperreal.InfinitePos.not_infiniteNeg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ x.InfiniteNeg → y.InfiniteNeg → (x + y).InfiniteNeg

Tactic:
fun hx hy =>
  infiniteNeg_add_not_infinitePos hx hy.not_infinitePos

Premises used: Hyperreal.infiniteNeg_add_not_infinitePos, Hyperreal.InfiniteNeg.not_infinitePos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ x.InfinitePos → ¬y.Infinite → (x + y).InfinitePos

Tactic:
fun hx hy =>
  infinitePos_add_not_infiniteNeg hx (not_or.mp hy).2

Premises used: Hyperreal.infinitePos_add_not_infiniteNeg, not_or, And.right, Iff.mp
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
⊢ x.InfiniteNeg → ¬y.Infinite → (x + y).InfiniteNeg

Tactic:
fun hx hy =>
  infiniteNeg_add_not_infinitePos hx (not_or.mp hy).1

Premises used: not_or, And.left, Iff.mp, Hyperreal.infiniteNeg_add_not_infinitePos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f atTop atTop
⊢ Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atTop

Tactic:
replace hf := hf.mono_left Nat.hyperfilter_le_atTop
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atTop
rw : 0 < ofSeq f ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0
⊢ (ofSeq f).InfinitePos

Tactic:
rw [infinitePos_iff]

Premises used: Hyperreal.infinitePos_iff
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atTop
⊢ 0 < ofSeq f ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0

Tactic:
⟨lt_of_tendsto_atTop 0 hf, archimedeanClassMk_neg_of_tendsto_atTop hf⟩

Premises used: Hyperreal.archimedeanClassMk_neg_of_tendsto_atTop, Hyperreal.lt_of_tendsto_atTop, And.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atTop
⊢ 0 < ofSeq f ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0

Tactic:
exact ⟨lt_of_tendsto_atTop 0 hf, archimedeanClassMk_neg_of_tendsto_atTop hf⟩
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f atTop atBot
⊢ Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atBot

Tactic:
replace hf := hf.mono_left Nat.hyperfilter_le_atTop
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atBot
rw : ofSeq f < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0
⊢ (ofSeq f).InfiniteNeg

Tactic:
rw [infiniteNeg_iff]

Premises used: Hyperreal.infiniteNeg_iff
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atBot
⊢ ofSeq f < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0

Tactic:
⟨lt_of_tendsto_atBot 0 hf, archimedeanClassMk_neg_of_tendsto_atBot hf⟩

Premises used: Hyperreal.archimedeanClassMk_neg_of_tendsto_atBot, Hyperreal.lt_of_tendsto_atBot, And.intro, OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atBot
⊢ ofSeq f < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0

Tactic:
exact ⟨lt_of_tendsto_atBot 0 hf, archimedeanClassMk_neg_of_tendsto_atBot hf⟩
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ ¬x.Infinite → ¬(-x).Infinite

Tactic:
mt infinite_neg.mp

Premises used: Hyperreal.infinite_neg, mt, Iff.mp
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hx : ¬x.Infinite
hy : ¬y.Infinite
⊢ ¬(x + y).Infinite

Tactic:
have ⟨r, hr⟩ := exists_st_of_not_infinite hx
  have ⟨s, hs⟩ := exists_st_of_not_infinite hy
  not_infinite_of_exists_st <| ⟨r + s, hr.add hs⟩

Premises used: Hyperreal.not_infinite_of_exists_st, Hyperreal.IsSt.add, HAdd.hAdd, Hyperreal.Infinite, Exists.intro, _private.0.Hyperreal.not_infinite_of_exists_st.match_1, Hyperreal.exists_st_of_not_infinite, Not
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ ¬x.Infinite ↔ ∃ (r : ℝ) (s : ℝ), (↑r : ℝ*) < x ∧ x < (↑s : ℝ*)

Tactic:
⟨fun hni ↦ let ⟨r, hr⟩ := exists_st_of_not_infinite hni; ⟨r - 1, r + 1, hr 1 one_pos⟩,
    fun ⟨r, s, hr, hs⟩ hi ↦ hi.elim (fun hp ↦ (hp s).not_gt hs) (fun hn ↦ (hn r).not_gt hr)⟩

Premises used: False, HSub.hSub, Exists, _private.0.Hyperreal.not_infinite_iff_exist_lt_gt.match_1, And, Hyperreal.ofReal, HAdd.hAdd, LT.lt, Iff.intro, Exists.intro, LT.lt.not_gt, _private.0.Hyperreal.not_infinite_of_exists_st.match_1, Hyperreal.exists_st_of_not_infinite, Or.elim, OfNat.ofNat, one_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
rw : ∃ (r_1 : ℝ) (s : ℝ), (↑r_1 : ℝ*) < (↑r : ℝ*) ∧ (↑r : ℝ*) < (↑s : ℝ*)
⊢ ¬(↑r : ℝ*).Infinite

Tactic:
rw [not_infinite_iff_exist_lt_gt]

Premises used: Hyperreal.not_infinite_iff_exist_lt_gt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
⊢ ∃ (r_1 : ℝ) (s : ℝ), (↑r_1 : ℝ*) < (↑r : ℝ*) ∧ (↑r : ℝ*) < (↑s : ℝ*)

Tactic:
⟨r - 1, r + 1, coe_lt_coe.2 <| sub_one_lt r, coe_lt_coe.2 <| lt_add_one r⟩

Premises used: Iff.mpr, lt_add_one, HSub.hSub, sub_one_lt, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, Hyperreal.coe_lt_coe
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
⊢ ∃ (r_1 : ℝ) (s : ℝ), (↑r_1 : ℝ*) < (↑r : ℝ*) ∧ (↑r : ℝ*) < (↑s : ℝ*)

Tactic:
exact ⟨r - 1, r + 1, coe_lt_coe.2 <| sub_one_lt r, coe_lt_coe.2 <| lt_add_one r⟩
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.Infinite → ∀ (r : ℝ), x ≠ (↑r : ℝ*)

Tactic:
fun hi r hr =>
  not_infinite_real r <| @Eq.subst _ Infinite _ _ hr hi

Premises used: Eq.subst, Hyperreal.not_infinite_real, Not
-- 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_mul.continuousAt

Premises used: continuous_mul, Quotient.map₂, Hyperreal.IsSt.map₂, Filter.Germ.map₂, Continuous.continuousAt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hx : ¬x.Infinite
hy : ¬y.Infinite
⊢ ¬(x * y).Infinite

Tactic:
have ⟨_r, hr⟩ := exists_st_of_not_infinite hx
  have ⟨_s, hs⟩ := exists_st_of_not_infinite hy
  (hr.mul hs).not_infinite

Premises used: HMul.hMul, Hyperreal.IsSt.not_infinite, Hyperreal.IsSt.mul, Hyperreal.Infinite, _private.0.Hyperreal.not_infinite_of_exists_st.match_1, Hyperreal.exists_st_of_not_infinite, Not
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hx : ¬x.Infinite
hy : ¬y.Infinite
⊢ (x + y).st = x.st + y.st

Tactic:
(isSt_st' (not_infinite_add hx hy)).unique ((isSt_st' hx).add (isSt_st' hy))

Premises used: Hyperreal.IsSt.add, Hyperreal.IsSt.unique, Hyperreal.not_infinite_add, Hyperreal.isSt_st'
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
pos : ∀ (h : x.Infinite), (-x).st = -x.st
neg : ∀ (h : ¬x.Infinite), (-x).st = -x.st
⊢ (-x).st = -x.st

Tactic:
by_cases h : Infinite x

Premises used: Hyperreal.Infinite
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x.Infinite
pos : (-x).st = -0
pos₁ : Eq (α := ℝ) 0 (-0)
pos₂ pos₃ : Eq (α := ℝ) 0 0
⊢ (-x).st = -x.st

Tactic:
rw [h.st_eq, (infinite_neg.2 h).st_eq, neg_zero]

Premises used: Iff.mpr, Hyperreal.infinite_neg, Hyperreal.Infinite.st_eq, neg_zero
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : ¬x.Infinite
⊢ (-x).st = -x.st

Tactic:
(isSt_st' (not_infinite_neg h)).unique (isSt_st' h).neg

Premises used: Hyperreal.IsSt.unique, Hyperreal.not_infinite_neg, Hyperreal.isSt_st', Hyperreal.IsSt.neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : ¬x.Infinite
⊢ (-x).st = -x.st

Tactic:
exact (isSt_st' (not_infinite_neg h)).unique (isSt_st' h).neg

Premises used: Hyperreal.IsSt.unique, Hyperreal.not_infinite_neg, Hyperreal.isSt_st', Hyperreal.IsSt.neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
pos : ∀ (h : x.Infinite), (-x).st = -x.st
neg neg₁ : ∀ (h : ¬x.Infinite), (-x).st = -x.st
⊢ (-x).st = -x.st

Tactic:
classical
  by_cases h : Infinite x
  · rw [h.st_eq, (infinite_neg.2 h).st_eq, neg_zero]
  · exact (isSt_st' (not_infinite_neg h)).unique (isSt_st' h).neg

Premises used: Hyperreal.Infinite, neg_zero
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hx : ¬x.Infinite
hy : ¬y.Infinite
⊢ (x * y).st = x.st * y.st

Tactic:
have hx' := isSt_st' hx
  have hy' := isSt_st' hy
  have hxy := isSt_st' (not_infinite_mul hx hy)
  hxy.unique (hx'.mul hy')

Premises used: Hyperreal.IsSt.mul, Hyperreal.IsSt.unique, Hyperreal.not_infinite_mul, Hyperreal.isSt_st'
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.Infinitesimal ↔ ∀ (r : ℝ), 0 < r → -(↑r : ℝ*) < x ∧ x < (↑r : ℝ*)

Tactic:
simp [Infinitesimal, IsSt]

Premises used: Hyperreal.Infinitesimal, Hyperreal.IsSt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.Infinitesimal → ∀ (r : ℝ), 0 < r → x < (↑r : ℝ*)

Tactic:
fun hi r hr => ((infinitesimal_def.mp hi) r hr).2

Premises used: Hyperreal.infinitesimal_def, And.right, Iff.mp
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.Infinitesimal → ∀ (r : ℝ), 0 < r → -(↑r : ℝ*) < x

Tactic:
fun hi r hr => ((infinitesimal_def.mp hi) r hr).1

Premises used: Hyperreal.infinitesimal_def, And.left, Iff.mp
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hi : x.Infinitesimal
r : ℝ
hr : r < 0
⊢ (↑r : ℝ*) < x

Tactic:
neg_neg r ▸ (infinitesimal_def.1 hi (-r) (neg_pos.2 hr)).1

Premises used: Iff.mpr, Hyperreal.infinitesimal_def, neg_pos, Eq.rec, neg_neg, And.left, Iff.mp, Neg.neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.Infinitesimal ↔ ∀ (r : ℝ), r ≠ 0 → |x| < |(↑r : ℝ*)|

Tactic:
⟨fun hi r hr ↦ abs_lt.mpr (coe_abs r ▸ infinitesimal_def.mp hi |r| (abs_pos.2 hr)), fun hR ↦
    infinitesimal_def.mpr fun r hr => abs_lt.mp <| (abs_of_pos <| coe_pos.2 hr) ▸ hR r <| hr.ne'⟩

Premises used: Iff.mpr, Hyperreal.infinitesimal_def, abs, Eq.rec, abs_pos, Iff.intro, Iff.mp, abs_lt, Hyperreal.coe_abs
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ Infinitesimal 0

Tactic:
isSt_refl_real 0

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Hyperreal.Infinitesimal, Hyperreal.isSt_refl_real, Hyperreal.ofReal, Quotient.mk', OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
⊢ (↑r : ℝ*).Infinitesimal → r = 0

Tactic:
eq_of_isSt_real

Premises used: Hyperreal.eq_of_isSt_real, Hyperreal.Infinitesimal
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
⊢ (↑r : ℝ*).Infinitesimal ↔ r = 0

Tactic:
isSt_real_iff_eq

Premises used: Hyperreal.Infinitesimal, Hyperreal.isSt_real_iff_eq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hx : x.Infinitesimal
hy : y.Infinitesimal
⊢ (x + y).Infinitesimal

Tactic:
simpa only [add_zero] using hx.add hy

Premises used: Hyperreal.Infinitesimal.add, add_zero
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hx : x.Infinitesimal
⊢ (-x).Infinitesimal

Tactic:
simpa only [neg_zero] using hx.neg

Premises used: neg_zero, Hyperreal.Infinitesimal.neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ (-x).Infinitesimal ↔ x.Infinitesimal

Tactic:
⟨fun h => neg_neg x ▸ h.neg, Infinitesimal.neg⟩

Premises used: Eq.rec, neg_neg, Iff.intro, Hyperreal.Infinitesimal.neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
hx : x.Infinitesimal
hy : y.Infinitesimal
⊢ (x * y).Infinitesimal

Tactic:
simpa only [mul_zero] using hx.mul hy

Premises used: MulZeroClass.mul_zero, Hyperreal.Infinitesimal.mul
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
h : Tendsto f atTop (𝓝 0)
⊢ (ofSeq f).Infinitesimal

Tactic:
isSt_of_tendsto h

Premises used: Hyperreal.Infinitesimal, Hyperreal.isSt_of_tendsto
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ ε.Infinitesimal

Tactic:
infinitesimal_of_tendsto_zero tendsto_inv_atTop_nhds_zero_nat

Premises used: Hyperreal.infinitesimal_of_tendsto_zero, Hyperreal.epsilon, tendsto_inv_atTop_nhds_zero_nat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.Infinitesimal → x ≠ 0 → ∀ (r : ℝ), x ≠ (↑r : ℝ*)

Tactic:
fun hi hx r hr =>
  hx <| hr.trans <| coe_eq_zero.2 <| IsSt.unique (hr.symm ▸ isSt_refl_real r : IsSt x r) hi

Premises used: Iff.mpr, Eq.rec, Hyperreal.isSt_refl_real, Hyperreal.IsSt.unique, Hyperreal.coe_eq_zero, Eq.symm, Not, Eq.trans
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hxr : x.IsSt r
⊢ (x - (↑r : ℝ*)).Infinitesimal

Tactic:
simpa only [sub_self] using hxr.sub (isSt_refl_real r)

Premises used: sub_self, Hyperreal.isSt_refl_real, Hyperreal.IsSt.sub
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hx : ¬x.Infinite
⊢ (x - (↑x.st : ℝ*)).Infinitesimal

Tactic:
(isSt_st' hx).infinitesimal_sub

Premises used: Hyperreal.isSt_st', Hyperreal.IsSt.infinitesimal_sub
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
rw :
  0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0 ↔
    LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x⁻¹) ∧ 0 < x⁻¹
⊢ x.InfinitePos ↔ x⁻¹.Infinitesimal ∧ 0 < x⁻¹

Tactic:
rw [infinitePos_iff, infinitesimal_iff]

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

Tactic:
aesop
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
rw : (-x).InfinitePos ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
rw₁ : (-x)⁻¹.Infinitesimal ∧ 0 < (-x)⁻¹ ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
rw₂ : (-x⁻¹).Infinitesimal ∧ 0 < -x⁻¹ ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
rw₃ : (-x⁻¹).Infinitesimal ∧ x⁻¹ < 0 ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
rw₄ rw₅ : x⁻¹.Infinitesimal ∧ x⁻¹ < 0 ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0
⊢ x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0

Tactic:
rw [← infinitePos_neg, infinitePos_iff_infinitesimal_inv_pos, inv_neg, neg_pos, infinitesimal_neg]

Premises used: neg_pos, Hyperreal.infinitePos_neg, inv_neg, Hyperreal.infinitePos_iff_infinitesimal_inv_pos, Hyperreal.infinitesimal_neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.Infinite → x⁻¹.Infinitesimal

Tactic:
fun hi =>
  Or.casesOn hi (fun hip => (infinitePos_iff_infinitesimal_inv_pos.mp hip).1) fun hin =>
    (infiniteNeg_iff_infinitesimal_inv_neg.mp hin).1

Premises used: Or.casesOn
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
inl : ∀ (hn : x < 0), x.Infinite
inr : ∀ (hp : 0 < x), x.Infinite
⊢ x.Infinite

Tactic:
rcases lt_or_gt_of_ne h0 with hn | hp

Premises used: lt_or_gt_of_ne
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hn : x < 0
⊢ x.Infinite

Tactic:
Or.inr (infiniteNeg_iff_infinitesimal_inv_neg.mpr ⟨hi, inv_lt_zero.mpr hn⟩)

Premises used: Iff.mpr, Hyperreal.Infinite, And.intro, Hyperreal.infiniteNeg_iff_infinitesimal_inv_neg, inv_lt_zero, Or.inr
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hn : x < 0
⊢ x.Infinite

Tactic:
exact Or.inr (infiniteNeg_iff_infinitesimal_inv_neg.mpr ⟨hi, inv_lt_zero.mpr hn⟩)

Premises used: Iff.mpr, And.intro, Hyperreal.infiniteNeg_iff_infinitesimal_inv_neg, inv_lt_zero, Or.inr
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hp : 0 < x
⊢ x.Infinite

Tactic:
Or.inl (infinitePos_iff_infinitesimal_inv_pos.mpr ⟨hi, inv_pos.mpr hp⟩)

Premises used: Iff.mpr, Hyperreal.infinitePos_iff_infinitesimal_inv_pos, inv_pos, Hyperreal.Infinite, And.intro, Or.inl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h0 : x ≠ 0
hi : x⁻¹.Infinitesimal
hp : 0 < x
⊢ x.Infinite

Tactic:
exact Or.inl (infinitePos_iff_infinitesimal_inv_pos.mpr ⟨hi, inv_pos.mpr hp⟩)

Premises used: Iff.mpr, Hyperreal.infinitePos_iff_infinitesimal_inv_pos, inv_pos, And.intro, Or.inl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h0 : x ≠ 0
⊢ x.Infinite ↔ x⁻¹.Infinitesimal

Tactic:
⟨infinitesimal_inv_of_infinite, infinite_of_infinitesimal_inv h0⟩

Premises used: Hyperreal.infinitesimal_inv_of_infinite, Iff.intro, Hyperreal.infinite_of_infinitesimal_inv
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
rw rw₁ : x.Infinitesimal ∧ 0 < x ↔ x.Infinitesimal ∧ 0 < x
⊢ x⁻¹⁻¹.Infinitesimal ∧ 0 < x⁻¹⁻¹ ↔ x.Infinitesimal ∧ 0 < x

Tactic:
rw [inv_inv]

Premises used: inv_inv
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
rw rw₁ : x.Infinitesimal ∧ x < 0 ↔ x.Infinitesimal ∧ x < 0
⊢ x⁻¹⁻¹.Infinitesimal ∧ x⁻¹⁻¹ < 0 ↔ x.Infinitesimal ∧ x < 0

Tactic:
rw [inv_inv]

Premises used: inv_inv
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x ≠ 0
rw rw₁ : x.Infinitesimal ↔ x.Infinitesimal
⊢ x.Infinitesimal ↔ x⁻¹⁻¹.Infinitesimal

Tactic:
rw [inv_inv]

Premises used: inv_inv