awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
x : ℝ × ℝ
s t : ℝ
h : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
refine_3 : ∀ (u : ℝ) (hu : (s, t).1 < u) (hu' : u < r), (ofSeq fun (n : ℕ) ↦ (s, t).1) < ofSeq f
⊢ (ofSeq fun (n : ℕ) ↦ (s, t).1) < ofSeq f

Tactic:
obtain ⟨u, hu, hu'⟩ := exists_between hs

Premises used: exists_between
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
x : ℝ × ℝ
s t : ℝ
h : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
u : ℝ
hu : (s, t).1 < u
hu' : u < r
⊢ (ofSeq fun (n : ℕ) ↦ (s, t).1) < ofSeq f

Tactic:
(coe_lt_coe.2 hu).trans_le (H.1 _ hu')

Premises used: Iff.mpr, Filter.Germ.const, And.left, LT.lt.trans_le, Hyperreal.coe_lt_coe, Hyperreal.ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
x : ℝ × ℝ
s t : ℝ
h : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
u : ℝ
hu : (s, t).1 < u
hu' : u < r
⊢ (ofSeq fun (n : ℕ) ↦ (s, t).1) < ofSeq f

Tactic:
exact (coe_lt_coe.2 hu).trans_le (H.1 _ hu')

Premises used: Iff.mpr, And.left, LT.lt.trans_le, Hyperreal.coe_lt_coe
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
x : ℝ × ℝ
s t : ℝ
h : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
refine_4 : ∀ (u : ℝ) (hu : r < u) (hu' : u < (s, t).2), ofSeq f < ofSeq fun (n : ℕ) ↦ (s, t).2
⊢ ofSeq f < ofSeq fun (n : ℕ) ↦ (s, t).2

Tactic:
obtain ⟨u, hu, hu'⟩ := exists_between ht

Premises used: exists_between
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
x : ℝ × ℝ
s t : ℝ
h : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
u : ℝ
hu : r < u
hu' : u < (s, t).2
⊢ ofSeq f < ofSeq fun (n : ℕ) ↦ (s, t).2

Tactic:
(H.2 _ hu).trans_lt (coe_lt_coe.2 hu')

Premises used: Iff.mpr, And.right, Hyperreal.coe_lt_coe, LE.le.trans_lt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
H : (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
x : ℝ × ℝ
s t : ℝ
h : (s, t).1 < r ∧ r < (s, t).2
hs : (s, t).1 < r
ht : r < (s, t).2
u : ℝ
hu : r < u
hu' : u < (s, t).2
⊢ ofSeq f < ofSeq fun (n : ℕ) ↦ (s, t).2

Tactic:
exact (H.2 _ hu).trans_lt (coe_lt_coe.2 hu')

Premises used: Iff.mpr, And.right, Hyperreal.coe_lt_coe, LE.le.trans_lt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hx : Germ.Tendsto x (𝓝 r)
⊢ (∀ s < r, (↑s : ℝ*) ≤ x) ∧ ∀ s > r, x ≤ (↑s : ℝ*)

Tactic:
rw [tendsto_iff_forall] at hx

Premises used: Hyperreal.tendsto_iff_forall
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hx : (∀ s < r, (↑s : ℝ*) ≤ x) ∧ ∀ s > r, x ≤ (↑s : ℝ*)
obtain : ∀ (s : ℝ) (hs : s < r), LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)

Tactic:
obtain ⟨s, hs⟩ := exists_lt r

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hx : (∀ s < r, (↑s : ℝ*) ≤ x) ∧ ∀ s > r, x ≤ (↑s : ℝ*)
s : ℝ
hs : s < r
obtain : ∀ (t : ℝ) (ht : r < t), LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)

Tactic:
obtain ⟨t, ht⟩ := exists_gt r

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hx : (∀ s < r, (↑s : ℝ*) ≤ x) ∧ ∀ s > r, x ≤ (↑s : ℝ*)
s : ℝ
hs : s < r
t : ℝ
ht : r < t
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)

Tactic:
mk_nonneg_of_le_of_le_of_archimedean coeRingHom (hx.1 s hs) (hx.2 t ht)

Premises used: And.right, And.left, ArchimedeanClass.mk_nonneg_of_le_of_le_of_archimedean, Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hx : (∀ s < r, (↑s : ℝ*) ≤ x) ∧ ∀ s > r, x ≤ (↑s : ℝ*)
s : ℝ
hs : s < r
t : ℝ
ht : r < t
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)

Tactic:
exact mk_nonneg_of_le_of_le_of_archimedean coeRingHom (hx.1 s hs) (hx.2 t ht)

Premises used: And.right, And.left, ArchimedeanClass.mk_nonneg_of_le_of_le_of_archimedean, Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hx : (∀ s < r, (↑s : ℝ*) ≤ x) ∧ ∀ s > r, x ≤ (↑s : ℝ*)
⊢ stdPart x = r

Tactic:
stdPart_eq coeRingHom hx.1 hx.2

Premises used: ArchimedeanClass.stdPart_eq, And.right, And.left, Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hx : (∀ s < r, (↑s : ℝ*) ≤ x) ∧ ∀ s > r, x ≤ (↑s : ℝ*)
⊢ stdPart x = r

Tactic:
exact stdPart_eq coeRingHom hx.1 hx.2

Premises used: ArchimedeanClass.stdPart_eq, And.right, And.left, Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hx : Germ.Tendsto x (𝓝 0)
apply : Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
⊢ LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)

Tactic:
apply (archimedeanClassMk_nonneg_of_tendsto hx).lt_of_ne'

Premises used: Hyperreal.archimedeanClassMk_nonneg_of_tendsto, LE.le.lt_of_ne'
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hx : Germ.Tendsto x (𝓝 0)
rw : stdPart x = 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0

Tactic:
rw [← stdPart_eq_zero, stdPart_of_tendsto hx]

Premises used: ArchimedeanClass.stdPart_eq_zero, Hyperreal.stdPart_of_tendsto
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ stdPart ε = 0

Tactic:
stdPart_eq_zero.2 <| archimedeanClassMk_epsilon_pos.ne'

Premises used: Iff.mpr, LT.lt.ne', ArchimedeanClass.stdPart_eq_zero, Hyperreal.archimedeanClassMk_epsilon_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
⊢ 0 < r → ε < (↑r : ℝ*)

Tactic:
lt_of_pos_of_archimedean coeRingHom archimedeanClassMk_epsilon_pos

Premises used: Filter.Germ.ofFun, Filter.Germ.const, ArchimedeanClass.lt_of_pos_of_archimedean, Hyperreal.ofReal, Quotient.mk', Hyperreal.coeRingHom, Hyperreal.archimedeanClassMk_epsilon_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
⊢ r < 0 → (↑r : ℝ*) < ε

Tactic:
lt_of_neg_of_archimedean coeRingHom archimedeanClassMk_epsilon_pos

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Hyperreal.ofReal, Quotient.mk', ArchimedeanClass.lt_of_neg_of_archimedean, Hyperreal.coeRingHom, Hyperreal.archimedeanClassMk_epsilon_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
⊢ 0 < r → ofSeq f < (↑r : ℝ*)

Tactic:
fun hr ↦
  ofSeq_lt_ofSeq.2 <| (hf.eventually <| gt_mem_nhds hr).filter_mono Nat.hyperfilter_le_atTop

Premises used: Iff.mpr, gt_mem_nhds, Filter.Eventually.filter_mono, Filter.Germ.const, Hyperreal.ofReal, Nat.hyperfilter_le_atTop, Filter.Tendsto.eventually, Hyperreal.ofSeq_lt_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : 0 < r
hg : Tendsto (β := ℝ) (fun (x : ℕ) ↦ -f x) atTop (𝓝 (-0))
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ -f x) atTop (𝓝 0)

Tactic:
rw [neg_zero] at hg

Premises used: neg_zero
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : 0 < r
hg : Tendsto (β := ℝ) (fun (x : ℕ) ↦ -f x) atTop (𝓝 0)
⊢ -ofSeq f < (↑r : ℝ*)

Tactic:
lt_of_tendsto_zero_of_pos hg hr

Premises used: Filter.Germ.ofFun, Filter.Germ.map', Quotient.mk', Quot.map, Hyperreal.lt_of_tendsto_zero_of_pos, Quotient.map', Filter.Germ.map, Hyperreal.ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : 0 < r
hg : Tendsto (β := ℝ) (fun (x : ℕ) ↦ -f x) atTop (𝓝 0)
⊢ -ofSeq f < (↑r : ℝ*)

Tactic:
exact lt_of_tendsto_zero_of_pos hg hr

Premises used: Hyperreal.lt_of_tendsto_zero_of_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : r < 0
rw : -(↑(-r) : ℝ*) < ofSeq f
⊢ (↑r : ℝ*) < ofSeq f

Tactic:
rw [← neg_neg r, coe_neg]

Premises used: neg_neg, Hyperreal.coe_neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : r < 0
⊢ -(↑(-r) : ℝ*) < ofSeq f

Tactic:
neg_lt_of_tendsto_zero_of_pos hf (neg_pos.mpr hr)

Premises used: Iff.mpr, Hyperreal.neg_lt_of_tendsto_zero_of_pos, neg_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : r < 0
⊢ -(↑(-r) : ℝ*) < ofSeq f

Tactic:
exact neg_lt_of_tendsto_zero_of_pos hf (neg_pos.mpr hr)

Premises used: Iff.mpr, Hyperreal.neg_lt_of_tendsto_zero_of_pos, neg_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hx : Germ.Tendsto x atTop
rcases : ∀ (f : ℕ → ℝ) (hx : Germ.Tendsto (ofSeq f) atTop), (↑r : ℝ*) < ofSeq f
⊢ (↑r : ℝ*) < x

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩

Premises used: Hyperreal.ofSeq_surjective, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
hx : Germ.Tendsto (ofSeq f) atTop
⊢ Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atTop

Tactic:
rw [tendsto_ofSeq] at hx

Premises used: Hyperreal.tendsto_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
hx : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atTop
⊢ (↑r : ℝ*) < ofSeq f

Tactic:
ofSeq_lt_ofSeq.2 <| hx.eventually_mem (Ioi_mem_atTop r)

Premises used: Iff.mpr, Filter.Germ.const, Filter.Tendsto.eventually_mem, Filter.Ioi_mem_atTop, Hyperreal.ofReal, Hyperreal.ofSeq_lt_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
hx : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atTop
⊢ (↑r : ℝ*) < ofSeq f

Tactic:
exact ofSeq_lt_ofSeq.2 <| hx.eventually_mem (Ioi_mem_atTop r)

Premises used: Iff.mpr, Filter.Tendsto.eventually_mem, Filter.Ioi_mem_atTop, Hyperreal.ofSeq_lt_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
hx : Germ.Tendsto x atBot
rcases : ∀ (f : ℕ → ℝ) (hx : Germ.Tendsto (ofSeq f) atBot), ofSeq f < (↑r : ℝ*)
⊢ x < (↑r : ℝ*)

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩

Premises used: Hyperreal.ofSeq_surjective, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
hx : Germ.Tendsto (ofSeq f) atBot
⊢ Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atBot

Tactic:
rw [tendsto_ofSeq] at hx

Premises used: Hyperreal.tendsto_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
hx : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atBot
⊢ ofSeq f < (↑r : ℝ*)

Tactic:
ofSeq_lt_ofSeq.2 <| hx.eventually_mem (Iio_mem_atBot r)

Premises used: Iff.mpr, Filter.Germ.const, Filter.Tendsto.eventually_mem, Hyperreal.ofReal, Filter.Iio_mem_atBot, Hyperreal.ofSeq_lt_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
hx : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atBot
⊢ ofSeq f < (↑r : ℝ*)

Tactic:
exact ofSeq_lt_ofSeq.2 <| hx.eventually_mem (Iio_mem_atBot r)

Premises used: Iff.mpr, Filter.Tendsto.eventually_mem, Filter.Iio_mem_atBot, Hyperreal.ofSeq_lt_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hx : Germ.Tendsto x atTop
⊢ 0 < x

Tactic:
have : 0 < x := lt_of_tendsto_atTop 0 hx
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hx : Germ.Tendsto x atTop
this : 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 this] using lt_of_tendsto_atTop n hx

Premises used: Hyperreal.lt_of_tendsto_atTop, Nat.cast, abs_of_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hx : Germ.Tendsto x atBot
⊢ x < 0

Tactic:
have : x < 0 := lt_of_tendsto_atBot 0 hx
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
hx : Germ.Tendsto x atBot
this : 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 this, lt_neg] using lt_of_tendsto_atBot (-n) hx

Premises used: lt_neg, abs_of_neg, Nat.cast, Hyperreal.lt_of_tendsto_atBot, Neg.neg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
rcases :
  ∀ (f : ℕ → ℝ) (h : 0 < ofSeq f ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0),
    Germ.Tendsto (ofSeq f) atTop
⊢ Germ.Tendsto x atTop

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩

Premises used: Hyperreal.ofSeq_surjective, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
h : 0 < ofSeq f ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0
rw : ∀ (b : ℝ), ∀ᶠ (a : ℕ) in (↑(hyperfilter ℕ) : Filter ℕ), b ≤ f a
⊢ Germ.Tendsto (ofSeq f) atTop

Tactic:
rw [tendsto_ofSeq, tendsto_atTop]

Premises used: Filter.tendsto_atTop, Hyperreal.tendsto_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
h : 0 < ofSeq f ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0
⊢ ∀ (b : ℝ), ∀ᶠ (a : ℕ) in (↑(hyperfilter ℕ) : Filter ℕ), b ≤ f a

Tactic:
fun r ↦ ofSeq_le_ofSeq.1 <|
      (lt_of_mk_lt_mk_of_nonneg (h.2.trans_le <| archimedeanClassMk_coe_nonneg r) h.1.le).le

Premises used: LT.lt.le, And.right, And.left, LT.lt.trans_le, Hyperreal.ofSeq_le_ofSeq, Hyperreal.archimedeanClassMk_coe_nonneg, Iff.mp, ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
h : 0 < ofSeq f ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0
⊢ ∀ (b : ℝ), ∀ᶠ (a : ℕ) in (↑(hyperfilter ℕ) : Filter ℕ), b ≤ f a

Tactic:
exact fun r ↦ ofSeq_le_ofSeq.1 <|
      (lt_of_mk_lt_mk_of_nonneg (h.2.trans_le <| archimedeanClassMk_coe_nonneg r) h.1.le).le

Premises used: LT.lt.le, And.right, And.left, LT.lt.trans_le, Hyperreal.ofSeq_le_ofSeq, Hyperreal.archimedeanClassMk_coe_nonneg, Iff.mp, ArchimedeanClass.lt_of_mk_lt_mk_of_nonneg
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
rcases :
  ∀ (f : ℕ → ℝ) (h : ofSeq f < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0),
    Germ.Tendsto (ofSeq f) atBot
⊢ Germ.Tendsto x atBot

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩

Premises used: Hyperreal.ofSeq_surjective, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
h : ofSeq f < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0
rw : ∀ (b : ℝ), ∀ᶠ (a : ℕ) in (↑(hyperfilter ℕ) : Filter ℕ), f a ≤ b
⊢ Germ.Tendsto (ofSeq f) atBot

Tactic:
rw [tendsto_ofSeq, tendsto_atBot]

Premises used: Filter.tendsto_atBot, Hyperreal.tendsto_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
h : ofSeq f < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0
⊢ ∀ (b : ℝ), ∀ᶠ (a : ℕ) in (↑(hyperfilter ℕ) : Filter ℕ), f a ≤ b

Tactic:
fun r ↦ ofSeq_le_ofSeq.1 <|
      (lt_of_mk_lt_mk_of_nonpos (h.2.trans_le <| archimedeanClassMk_coe_nonneg r) h.1.le).le

Premises used: LT.lt.le, And.right, And.left, LT.lt.trans_le, Hyperreal.ofSeq_le_ofSeq, Hyperreal.archimedeanClassMk_coe_nonneg, Iff.mp, ArchimedeanClass.lt_of_mk_lt_mk_of_nonpos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
h : ofSeq f < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0
⊢ ∀ (b : ℝ), ∀ᶠ (a : ℕ) in (↑(hyperfilter ℕ) : Filter ℕ), f a ≤ b

Tactic:
exact fun r ↦ ofSeq_le_ofSeq.1 <|
      (lt_of_mk_lt_mk_of_nonpos (h.2.trans_le <| archimedeanClassMk_coe_nonneg r) h.1.le).le

Premises used: LT.lt.le, And.right, And.left, LT.lt.trans_le, Hyperreal.ofSeq_le_ofSeq, Hyperreal.archimedeanClassMk_coe_nonneg, Iff.mp, ArchimedeanClass.lt_of_mk_lt_mk_of_nonpos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
h : x.IsSt r
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = r

Tactic:
⟨?_, stdPart_eq coeRingHom (fun s hs ↦ ?_) (fun s hs ↦ ?_)⟩

Premises used: ArchimedeanClass.stdPart_eq, And.intro, Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
h : x.IsSt r
refine_1 : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
refine_2 : ∀ (s : ℝ) (hs : s < r), (coeRingHom : (a : ℝ) → ℝ*) s ≤ x
refine_3 : ∀ (s : ℝ) (hs : s > r), x ≤ (coeRingHom : (a : ℝ) → ℝ*) s
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = r

Tactic:
refine ⟨?_, stdPart_eq coeRingHom (fun s hs ↦ ?_) (fun s hs ↦ ?_)⟩
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
h : x.IsSt r
⊢ (↑r : ℝ*) - (↑1 : ℝ*) < x ∧ x < (↑r : ℝ*) + (↑1 : ℝ*)

Tactic:
have h := h 1 zero_lt_one
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
h_1 : x.IsSt r
h : (↑r : ℝ*) - (↑1 : ℝ*) < x ∧ x < (↑r : ℝ*) + (↑1 : ℝ*)
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)

Tactic:
mk_nonneg_of_le_of_le_of_archimedean coeRingHom h.1.le h.2.le

Premises used: LT.lt.le, And.right, And.left, ArchimedeanClass.mk_nonneg_of_le_of_le_of_archimedean, Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
h_1 : x.IsSt r
h : (↑r : ℝ*) - (↑1 : ℝ*) < x ∧ x < (↑r : ℝ*) + (↑1 : ℝ*)
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)

Tactic:
exact mk_nonneg_of_le_of_le_of_archimedean coeRingHom h.1.le h.2.le

Premises used: LT.lt.le, And.right, And.left, ArchimedeanClass.mk_nonneg_of_le_of_le_of_archimedean, Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s < r
⊢ (coeRingHom : (a : ℝ) → ℝ*) s ≤ x

Tactic:
simpa using (h _ (sub_pos_of_lt hs)).1.le

Premises used: LT.lt.le, And.left, sub_pos_of_lt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
h : x.IsSt r
s : ℝ
hs : s > r
⊢ x ≤ (coeRingHom : (a : ℝ) → ℝ*) s

Tactic:
simpa using (h _ (sub_pos_of_lt hs)).2.le

Premises used: LT.lt.le, And.right, sub_pos_of_lt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
h : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = r
obtain : ∀ (h : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)), x.IsSt (stdPart x)
⊢ x.IsSt r

Tactic:
obtain ⟨h, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
⊢ x.IsSt (stdPart x)

Tactic:
fun y hy ↦ ⟨?_, ?_⟩

Premises used: And.intro, Hyperreal.IsSt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
refine_1 : ∀ (y : ℝ) (hy : 0 < y), (↑(stdPart x) : ℝ*) - (↑y : ℝ*) < x
refine_2 : ∀ (y : ℝ) (hy : 0 < y), x < (↑(stdPart x) : ℝ*) + (↑y : ℝ*)
⊢ x.IsSt (stdPart x)

Tactic:
refine fun y hy ↦ ⟨?_, ?_⟩
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
y : ℝ
hy : 0 < y
refine_1 : (fun (x1 x2 : ℝ) ↦ x1 - x2) (stdPart x) y < stdPart x
⊢ (↑(stdPart x) : ℝ*) - (↑y : ℝ*) < x

Tactic:
apply lt_of_lt_stdPart coeRingHom h

Premises used: ArchimedeanClass.lt_of_lt_stdPart, Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
y : ℝ
hy : 0 < y
⊢ (fun (x1 x2 : ℝ) ↦ x1 - x2) (stdPart x) y < stdPart x

Tactic:
simpa
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
y : ℝ
hy : 0 < y
refine_2 : stdPart x < (fun (x1 x2 : ℝ) ↦ x1 + x2) (stdPart x) y
⊢ x < (↑(stdPart x) : ℝ*) + (↑y : ℝ*)

Tactic:
apply lt_of_stdPart_lt coeRingHom h

Premises used: ArchimedeanClass.lt_of_stdPart_lt, Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
y : ℝ
hy : 0 < y
⊢ stdPart x < (fun (x1 x2 : ℝ) ↦ x1 + x2) (stdPart x) y

Tactic:
simpa
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
pos : ∀ (h : ∃ (r : ℝ), x.IsSt r), Classical.choose (p := x.IsSt) h = stdPart x
neg : ∀ (h : ¬∃ (r : ℝ), x.IsSt r), 0 = stdPart x
⊢ (if h : ∃ (r : ℝ), x.IsSt r then Classical.choose (p := x.IsSt) h else 0) = stdPart x

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : ∃ (r : ℝ), x.IsSt r
⊢ Classical.choose (p := x.IsSt) h = stdPart x

Tactic:
(isSt_iff.1 (Classical.choose_spec h)).2.symm

Premises used: Classical.choose_spec, And.right, Hyperreal.isSt_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : ∃ (r : ℝ), x.IsSt r
⊢ Classical.choose (p := x.IsSt) h = stdPart x

Tactic:
exact (isSt_iff.1 (Classical.choose_spec h)).2.symm

Premises used: Classical.choose_spec, And.right, Hyperreal.isSt_iff, Iff.mp, Eq.symm
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : ¬∃ (r : ℝ), x.IsSt r
⊢ ¬∃ (r : ℝ), LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = r

Tactic:
simp_rw [isSt_iff] at h

Premises used: Hyperreal.isSt_iff
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : ¬∃ (r : ℝ), LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = r
⊢ ∀ (r : ℝ) (_ : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)), stdPart x ≠ r

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : ∀ (r : ℝ) (_ : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)), stdPart x ≠ r
neg : Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
⊢ 0 = stdPart x

Tactic:
rw [eq_comm, stdPart_eq_zero]

Premises used: eq_comm, ArchimedeanClass.stdPart_eq_zero
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : ∀ (r : ℝ) (_ : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)), stdPart x ≠ r
neg : LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
⊢ Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0

Tactic:
apply ne_of_lt

Premises used: ne_of_lt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : ∀ (r : ℝ) (_ : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)), stdPart x ≠ r
neg : ∀ (hx : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)), False
⊢ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0

Tactic:
by_contra! hx
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : ∀ (r : ℝ) (_ : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)), stdPart x ≠ r
hx : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
⊢ False

Tactic:
h _ hx rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
h : ∀ (r : ℝ) (_ : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)), stdPart x ≠ r
hx : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
⊢ False

Tactic:
exact h _ hx rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
rw : x.IsSt 0 ↔ LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
rw₁ :
  LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = 0 ↔
    LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
rw₂ :
  LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0 ↔
    LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
rw₃ rw₄ :
  LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0 ↔
    LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
⊢ x.Infinitesimal ↔ LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)

Tactic:
rw [Infinitesimal, isSt_iff, stdPart_eq_zero, lt_iff_le_and_ne']

Premises used: lt_iff_le_and_ne', Hyperreal.Infinitesimal, Hyperreal.isSt_iff, ArchimedeanClass.stdPart_eq_zero
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
⊢ x.InfinitePos ↔ 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0

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

Premises used: Hyperreal.ofReal, LT.lt, Iff.intro, _private.0.Hyperreal.infinitePos_iff.match_1