[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r✝ : ℝ
hr : 0 < r✝
hg : Tendsto (fun x => -f x) atTop (𝓝 (-0))
⊢ -ofSeq f < ↑r✝
[PROOFSTEP]
rw [neg_zero] at hg 
[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r✝ : ℝ
hr : 0 < r✝
hg : Tendsto (fun x => -f x) atTop (𝓝 0)
⊢ -ofSeq f < ↑r✝
[PROOFSTEP]
exact lt_of_tendsto_zero_of_pos hg hr
[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : r < 0
⊢ ↑r < ofSeq f
[PROOFSTEP]
rw [← neg_neg r, coe_neg]
[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : r < 0
⊢ -↑(-r) < ofSeq f
[PROOFSTEP]
exact neg_lt_of_tendsto_zero_of_pos hf (neg_pos.mpr hr)
[GOAL]
x : ℝ*
r : ℝ
⊢ IsSt x r ↔ Germ.Tendsto x (𝓝 r)
[PROOFSTEP]
rcases ofSeq_surjective x with ⟨f, rfl⟩
[GOAL]
case intro
r : ℝ
f : ℕ → ℝ
⊢ IsSt (ofSeq f) r ↔ Germ.Tendsto (ofSeq f) (𝓝 r)
[PROOFSTEP]
exact isSt_ofSeq_iff_tendsto
[GOAL]
x y : ℝ*
r s : ℝ
hxr : IsSt x r
hys : IsSt y s
hrs : r < s
⊢ x < y
[PROOFSTEP]
rcases ofSeq_surjective x with ⟨f, rfl⟩
[GOAL]
case intro
y : ℝ*
r s : ℝ
hys : IsSt y s
hrs : r < s
f : ℕ → ℝ
hxr : IsSt (ofSeq f) r
⊢ ofSeq f < y
[PROOFSTEP]
rcases ofSeq_surjective y with ⟨g, rfl⟩
[GOAL]
case intro.intro
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : IsSt (ofSeq f) r
g : ℕ → ℝ
hys : IsSt (ofSeq g) s
⊢ ofSeq f < ofSeq g
[PROOFSTEP]
rw [isSt_ofSeq_iff_tendsto] at hxr hys 
[GOAL]
case intro.intro
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
g : ℕ → ℝ
hys : Tendsto g (↑(hyperfilter ℕ)) (𝓝 s)
⊢ ofSeq f < ofSeq g
[PROOFSTEP]
exact ofSeq_lt_ofSeq.2 <| hxr.eventually_lt hys hrs
[GOAL]
x : ℝ*
r s : ℝ
hr : IsSt x r
hs : IsSt x s
⊢ r = s
[PROOFSTEP]
rcases ofSeq_surjective x with ⟨f, rfl⟩
[GOAL]
case intro
r s : ℝ
f : ℕ → ℝ
hr : IsSt (ofSeq f) r
hs : IsSt (ofSeq f) s
⊢ r = s
[PROOFSTEP]
rw [isSt_ofSeq_iff_tendsto] at hr hs 
[GOAL]
case intro
r s : ℝ
f : ℕ → ℝ
hr : Tendsto f (↑(hyperfilter ℕ)) (𝓝 r)
hs : Tendsto f (↑(hyperfilter ℕ)) (𝓝 s)
⊢ r = s
[PROOFSTEP]
exact tendsto_nhds_unique hr hs
[GOAL]
x : ℝ*
r : ℝ
hxr : IsSt x r
⊢ st x = r
[PROOFSTEP]
have h : ∃ r, IsSt x r := ⟨r, hxr⟩
[GOAL]
x : ℝ*
r : ℝ
hxr : IsSt x r
h : ∃ r, IsSt x r
⊢ st x = r
[PROOFSTEP]
rw [st, dif_pos h]
[GOAL]
x : ℝ*
r : ℝ
hxr : IsSt x r
h : ∃ r, IsSt x r
⊢ choose h = r
[PROOFSTEP]
exact (Classical.choose_spec h).unique hxr
[GOAL]
x : ℝ*
⊢ st x = sSup {y | ↑y < x}
[PROOFSTEP]
rcases _root_.em (Infinite x) with (hx | hx)
[GOAL]
case inl
x : ℝ*
hx : Infinite x
⊢ st x = sSup {y | ↑y < x}
[PROOFSTEP]
rw [hx.st_eq]
[GOAL]
case inl
x : ℝ*
hx : Infinite x
⊢ 0 = sSup {y | ↑y < x}
[PROOFSTEP]
cases hx with
| inl hx =>
  convert Real.sSup_univ.symm
  exact Set.eq_univ_of_forall hx
| inr hx =>
  convert Real.sSup_empty.symm
  exact Set.eq_empty_of_forall_not_mem fun y hy ↦ hy.out.not_lt (hx _)
[GOAL]
case inl
x : ℝ*
hx : Infinite x
⊢ 0 = sSup {y | ↑y < x}
[PROOFSTEP]
cases hx with
| inl hx =>
  convert Real.sSup_univ.symm
  exact Set.eq_univ_of_forall hx
| inr hx =>
  convert Real.sSup_empty.symm
  exact Set.eq_empty_of_forall_not_mem fun y hy ↦ hy.out.not_lt (hx _)
[GOAL]
case inl.inl
x : ℝ*
hx : InfinitePos x
⊢ 0 = sSup {y | ↑y < x}
[PROOFSTEP]

| inl hx =>
  convert Real.sSup_univ.symm
  exact Set.eq_univ_of_forall hx
[GOAL]
case inl.inl
x : ℝ*
hx : InfinitePos x
⊢ 0 = sSup {y | ↑y < x}
[PROOFSTEP]
convert Real.sSup_univ.symm
[GOAL]
case h.e'_3.h.e'_3
x : ℝ*
hx : InfinitePos x
⊢ {y | ↑y < x} = Set.univ
[PROOFSTEP]
exact Set.eq_univ_of_forall hx
[GOAL]
case inl.inr
x : ℝ*
hx : InfiniteNeg x
⊢ 0 = sSup {y | ↑y < x}
[PROOFSTEP]

| inr hx =>
  convert Real.sSup_empty.symm
  exact Set.eq_empty_of_forall_not_mem fun y hy ↦ hy.out.not_lt (hx _)
[GOAL]
case inl.inr
x : ℝ*
hx : InfiniteNeg x
⊢ 0 = sSup {y | ↑y < x}
[PROOFSTEP]
convert Real.sSup_empty.symm
[GOAL]
case h.e'_3.h.e'_3
x : ℝ*
hx : InfiniteNeg x
⊢ {y | ↑y < x} = ∅
[PROOFSTEP]
exact Set.eq_empty_of_forall_not_mem fun y hy ↦ hy.out.not_lt (hx _)
[GOAL]
case inr
x : ℝ*
hx : ¬Infinite x
⊢ st x = sSup {y | ↑y < x}
[PROOFSTEP]
exact (isSt_sSup hx).st_eq
[GOAL]
x : ℝ*
r : ℝ
hxr : IsSt x r
⊢ IsSt x (st x)
[PROOFSTEP]
rwa [hxr.st_eq]
[GOAL]
r s : ℝ
⊢ IsSt (↑r) s ↔ IsSt (↑s) r
[PROOFSTEP]
rw [isSt_real_iff_eq, isSt_real_iff_eq, eq_comm]
[GOAL]
r s t : ℝ
⊢ IsSt (↑r) s → IsSt (↑s) t → IsSt (↑r) t
[PROOFSTEP]
rw [isSt_real_iff_eq, isSt_real_iff_eq, isSt_real_iff_eq]
[GOAL]
r s t : ℝ
⊢ r = s → s = t → r = t
[PROOFSTEP]
exact Eq.trans
[GOAL]
x : ℝ*
r : ℝ
⊢ IsSt x r ↔ ∀ (δ : ℝ), 0 < δ → |x - ↑r| < ↑δ
[PROOFSTEP]
simp only [abs_sub_lt_iff, sub_lt_iff_lt_add, IsSt, and_comm, add_comm]
[GOAL]
x : ℝ*
r : ℝ
hxr : IsSt x r
f : ℝ → ℝ
hf : ContinuousAt f r
⊢ IsSt (Germ.map f x) (f r)
[PROOFSTEP]
rcases ofSeq_surjective x with ⟨g, rfl⟩
[GOAL]
case intro
r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
g : ℕ → ℝ
hxr : IsSt (ofSeq g) r
⊢ IsSt (Germ.map f (ofSeq g)) (f r)
[PROOFSTEP]
exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (isSt_ofSeq_iff_tendsto.1 hxr)
[GOAL]
x y : ℝ*
r s : ℝ
hxr : IsSt x r
hys : IsSt y s
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
⊢ IsSt (Germ.map₂ f x y) (f r s)
[PROOFSTEP]
rcases ofSeq_surjective x with ⟨x, rfl⟩
[GOAL]
case intro
y : ℝ*
r s : ℝ
hys : IsSt y s
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : IsSt (ofSeq x) r
⊢ IsSt (Germ.map₂ f (ofSeq x) y) (f r s)
[PROOFSTEP]
rcases ofSeq_surjective y with ⟨y, rfl⟩
[GOAL]
case intro.intro
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : IsSt (ofSeq x) r
y : ℕ → ℝ
hys : IsSt (ofSeq y) s
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
[PROOFSTEP]
rw [isSt_ofSeq_iff_tendsto] at hxr hys 
[GOAL]
case intro.intro
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Tendsto x (↑(hyperfilter ℕ)) (𝓝 r)
y : ℕ → ℝ
hys : Tendsto y (↑(hyperfilter ℕ)) (𝓝 s)
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
[PROOFSTEP]
exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (hxr.prod_mk_nhds hys)
[GOAL]
x : ℝ*
⊢ Infinite |x| ↔ Infinite x
[PROOFSTEP]
cases le_total 0 x
[GOAL]
case inl
x : ℝ*
h✝ : 0 ≤ x
⊢ Infinite |x| ↔ Infinite x
[PROOFSTEP]
simp [*, abs_of_nonneg, abs_of_nonpos, infinite_neg]
[GOAL]
case inr
x : ℝ*
h✝ : x ≤ 0
⊢ Infinite |x| ↔ Infinite x
[PROOFSTEP]
simp [*, abs_of_nonneg, abs_of_nonpos, infinite_neg]
[GOAL]
x y : ℝ*
⊢ InfinitePos x → ¬InfiniteNeg y → InfinitePos (x + y)
[PROOFSTEP]
intro hip hnin r
[GOAL]
x y : ℝ*
hip : InfinitePos x
hnin : ¬InfiniteNeg y
r : ℝ
⊢ ↑r < x + y
[PROOFSTEP]
cases' not_forall.mp hnin with r₂ hr₂
[GOAL]
case intro
x y : ℝ*
hip : InfinitePos x
hnin : ¬InfiniteNeg y
r r₂ : ℝ
hr₂ : ¬y < ↑r₂
⊢ ↑r < x + y
[PROOFSTEP]
convert add_lt_add_of_lt_of_le (hip (r + -r₂)) (not_lt.mp hr₂) using 1
[GOAL]
case h.e'_3
x y : ℝ*
hip : InfinitePos x
hnin : ¬InfiniteNeg y
r r₂ : ℝ
hr₂ : ¬y < ↑r₂
⊢ ↑r = ↑(r + -r₂) + ↑r₂
[PROOFSTEP]
simp
[GOAL]
x y : ℝ*
⊢ InfiniteNeg x → ¬InfinitePos y → InfiniteNeg (x + y)
[PROOFSTEP]
rw [← infinitePos_neg, ← infinitePos_neg, ← @infiniteNeg_neg y, neg_add]
[GOAL]
x y : ℝ*
⊢ InfinitePos (-x) → ¬InfiniteNeg (-y) → InfinitePos (-x + -y)
[PROOFSTEP]
exact infinitePos_add_not_infiniteNeg
[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop atTop
r : ℝ
hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ f a
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → r + 1 ≤ f a
hi' : ∀ (a : ℕ), f a < r + 1 → a < i
⊢ {a | r < f a}ᶜ ⊆ {a | a ≤ i}
[PROOFSTEP]
simp only [Set.compl_setOf, not_lt]
[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop atTop
r : ℝ
hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ f a
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → r + 1 ≤ f a
hi' : ∀ (a : ℕ), f a < r + 1 → a < i
⊢ {a | f a ≤ r} ⊆ {a | a ≤ i}
[PROOFSTEP]
exact fun a har => le_of_lt (hi' a (lt_of_le_of_lt har (lt_add_one _)))
[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop atBot
r : ℝ
hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → f a ≤ b
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → f a ≤ r - 1
hi' : ∀ (a : ℕ), r - 1 < f a → a < i
⊢ {a | f a < r}ᶜ ⊆ {a | a ≤ i}
[PROOFSTEP]
simp only [Set.compl_setOf, not_lt]
[GOAL]
f : ℕ → ℝ
hf : Tendsto f atTop atBot
r : ℝ
hf' : ∀ (b : ℝ), ∃ i, ∀ (a : ℕ), i ≤ a → f a ≤ b
i : ℕ
hi : ∀ (a : ℕ), i ≤ a → f a ≤ r - 1
hi' : ∀ (a : ℕ), r - 1 < f a → a < i
⊢ {a | r ≤ f a} ⊆ {a | a ≤ i}
[PROOFSTEP]
exact fun a har => le_of_lt (hi' a (lt_of_lt_of_le (sub_one_lt _) har))
[GOAL]
r : ℝ
⊢ ¬Infinite ↑r
[PROOFSTEP]
rw [not_infinite_iff_exist_lt_gt]
[GOAL]
r : ℝ
⊢ ∃ r_1 s, ↑r_1 < ↑r ∧ ↑r < ↑s
[PROOFSTEP]
exact ⟨r - 1, r + 1, coe_lt_coe.2 <| sub_one_lt r, coe_lt_coe.2 <| lt_add_one r⟩
[GOAL]
x : ℝ*
h : Infinite x
⊢ st (-x) = -st x
[PROOFSTEP]
rw [h.st_eq, (infinite_neg.2 h).st_eq, neg_zero]
[GOAL]
x : ℝ*
⊢ Infinitesimal x ↔ ∀ (r : ℝ), 0 < r → -↑r < x ∧ x < ↑r
[PROOFSTEP]
simp [Infinitesimal, IsSt]
[GOAL]
x y : ℝ*
hx : Infinitesimal x
hy : Infinitesimal y
⊢ Infinitesimal (x + y)
[PROOFSTEP]
simpa only [add_zero] using hx.add hy
[GOAL]
x : ℝ*
hx : Infinitesimal x
⊢ Infinitesimal (-x)
[PROOFSTEP]
simpa only [neg_zero] using hx.neg
[GOAL]
x y : ℝ*
hx : Infinitesimal x
hy : Infinitesimal y
⊢ Infinitesimal (x * y)
[PROOFSTEP]
simpa only [mul_zero] using hx.mul hy
[GOAL]
x : ℝ*
r : ℝ
hxr : IsSt x r
⊢ Infinitesimal (x - ↑r)
[PROOFSTEP]
simpa only [sub_self] using hxr.sub (isSt_refl_real r)
[GOAL]
x : ℝ*
hip : InfinitePos x
r : ℝ
hr : 0 < r
⊢ (↑r)⁻¹ < x
[PROOFSTEP]
convert hip r⁻¹
[GOAL]
x : ℝ*
⊢ InfiniteNeg x ↔ Infinitesimal x⁻¹ ∧ x⁻¹ < 0
[PROOFSTEP]
rw [← infinitePos_neg, infinitePos_iff_infinitesimal_inv_pos, inv_neg, neg_pos, infinitesimal_neg]
[GOAL]
x : ℝ*
h0 : x ≠ 0
hi : Infinitesimal x⁻¹
⊢ Infinite x
[PROOFSTEP]
cases' lt_or_gt_of_ne h0 with hn hp
[GOAL]
case inl
x : ℝ*
h0 : x ≠ 0
hi : Infinitesimal x⁻¹
hn : x < 0
⊢ Infinite x
[PROOFSTEP]
exact Or.inr (infiniteNeg_iff_infinitesimal_inv_neg.mpr ⟨hi, inv_lt_zero.mpr hn⟩)
[GOAL]
case inr
x : ℝ*
h0 : x ≠ 0
hi : Infinitesimal x⁻¹
hp : x > 0
⊢ Infinite x
[PROOFSTEP]
exact Or.inl (infinitePos_iff_infinitesimal_inv_pos.mpr ⟨hi, inv_pos.mpr hp⟩)
[GOAL]
x : ℝ*
⊢ Infinitesimal x⁻¹⁻¹ ∧ 0 < x⁻¹⁻¹ ↔ Infinitesimal x ∧ 0 < x
[PROOFSTEP]
rw [inv_inv]
[GOAL]
x : ℝ*
⊢ Infinitesimal x⁻¹⁻¹ ∧ x⁻¹⁻¹ < 0 ↔ Infinitesimal x ∧ x < 0
[PROOFSTEP]
rw [inv_inv]
[GOAL]
x : ℝ*
h : x ≠ 0
⊢ Infinitesimal x ↔ Infinitesimal x⁻¹⁻¹
[PROOFSTEP]
rw [inv_inv]
[GOAL]
x : ℝ*
r : ℝ
hi : ¬Infinitesimal x
hr : IsSt x r
⊢ r ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
x : ℝ*
hi : ¬Infinitesimal x
hr : IsSt x 0
⊢ False
[PROOFSTEP]
exact hi hr
[GOAL]
x : ℝ*
⊢ st x⁻¹ = (st x)⁻¹
[PROOFSTEP]
by_cases h0 : x = 0
[GOAL]
case pos
x : ℝ*
h0 : x = 0
⊢ st x⁻¹ = (st x)⁻¹
case neg x : ℝ* h0 : ¬x = 0 ⊢ st x⁻¹ = (st x)⁻¹
[PROOFSTEP]
rw [h0, inv_zero, ← coe_zero, st_id_real, inv_zero]
[GOAL]
case neg
x : ℝ*
h0 : ¬x = 0
⊢ st x⁻¹ = (st x)⁻¹
[PROOFSTEP]
by_cases h1 : Infinitesimal x
[GOAL]
case pos
x : ℝ*
h0 : ¬x = 0
h1 : Infinitesimal x
⊢ st x⁻¹ = (st x)⁻¹
case neg x : ℝ* h0 : ¬x = 0 h1 : ¬Infinitesimal x ⊢ st x⁻¹ = (st x)⁻¹
[PROOFSTEP]
rw [((infinitesimal_iff_infinite_inv h0).mp h1).st_eq, h1.st_eq, inv_zero]
[GOAL]
case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
⊢ st x⁻¹ = (st x)⁻¹
[PROOFSTEP]
by_cases h2 : Infinite x
[GOAL]
case pos
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
h2 : Infinite x
⊢ st x⁻¹ = (st x)⁻¹
case neg x : ℝ* h0 : ¬x = 0 h1 : ¬Infinitesimal x h2 : ¬Infinite x ⊢ st x⁻¹ = (st x)⁻¹
[PROOFSTEP]
rw [(infinitesimal_inv_of_infinite h2).st_eq, h2.st_eq, inv_zero]
[GOAL]
case neg
x : ℝ*
h0 : ¬x = 0
h1 : ¬Infinitesimal x
h2 : ¬Infinite x
⊢ st x⁻¹ = (st x)⁻¹
[PROOFSTEP]
exact ((isSt_st' h2).inv h1).st_eq
[GOAL]
x y : ℝ*
hx : InfinitePos x
hy₁ : ¬Infinitesimal y
hy₂ : 0 < y
r : ℝ
⊢ ↑r < x * y
[PROOFSTEP]
have hy₁' := not_forall.mp (mt infinitesimal_def.2 hy₁)
[GOAL]
x y : ℝ*
hx : InfinitePos x
hy₁ : ¬Infinitesimal y
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
⊢ ↑r < x * y
[PROOFSTEP]
let ⟨r₁, hy₁''⟩ := hy₁'
[GOAL]
x y : ℝ*
hx : InfinitePos x
hy₁ : ¬Infinitesimal y
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
⊢ ↑r < x * y
[PROOFSTEP]
have hyr : 0 < r₁ ∧ ↑r₁ ≤ y := by rwa [not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁'' 
[GOAL]
x y : ℝ*
hx : InfinitePos x
hy₁ : ¬Infinitesimal y
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
⊢ 0 < r₁ ∧ ↑r₁ ≤ y
[PROOFSTEP]
rwa [not_imp, ← abs_lt, not_lt, abs_of_pos hy₂] at hy₁'' 
[GOAL]
x y : ℝ*
hx : InfinitePos x
hy₁ : ¬Infinitesimal y
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
hyr : 0 < r₁ ∧ ↑r₁ ≤ y
⊢ ↑r < x * y
[PROOFSTEP]
rw [← div_mul_cancel r (ne_of_gt hyr.1), coe_mul]
[GOAL]
x y : ℝ*
hx : InfinitePos x
hy₁ : ¬Infinitesimal y
hy₂ : 0 < y
r : ℝ
hy₁' : ∃ x, ¬(0 < x → -↑x < y ∧ y < ↑x)
r₁ : ℝ
hy₁'' : ¬(0 < r₁ → -↑r₁ < y ∧ y < ↑r₁)
hyr : 0 < r₁ ∧ ↑r₁ ≤ y
⊢ ↑(r / r₁) * ↑r₁ < x * y
[PROOFSTEP]
exact mul_lt_mul (hx (r / r₁)) hyr.2 (coe_lt_coe.2 hyr.1) (le_of_lt (hx 0))
[GOAL]
x y : ℝ*
⊢ InfiniteNeg x → ¬Infinitesimal y → y < 0 → InfinitePos (x * y)
[PROOFSTEP]
rw [← infinitePos_neg, ← neg_pos, ← neg_mul_neg, ← infinitesimal_neg]
[GOAL]
x y : ℝ*
⊢ InfinitePos (-x) → ¬Infinitesimal (-y) → 0 < -y → InfinitePos (-x * -y)
[PROOFSTEP]
exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos
[GOAL]
x y : ℝ*
⊢ InfinitePos x → ¬Infinitesimal y → y < 0 → InfiniteNeg (x * y)
[PROOFSTEP]
rw [← infinitePos_neg, ← neg_pos, neg_mul_eq_mul_neg, ← infinitesimal_neg]
[GOAL]
x y : ℝ*
⊢ InfinitePos x → ¬Infinitesimal (-y) → 0 < -y → InfinitePos (x * -y)
[PROOFSTEP]
exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos
[GOAL]
x y : ℝ*
⊢ InfiniteNeg x → ¬Infinitesimal y → 0 < y → InfiniteNeg (x * y)
[PROOFSTEP]
rw [← infinitePos_neg, ← infinitePos_neg, neg_mul_eq_neg_mul]
[GOAL]
x y : ℝ*
⊢ InfinitePos (-x) → ¬Infinitesimal y → 0 < y → InfinitePos (-x * y)
[PROOFSTEP]
exact infinitePos_mul_of_infinitePos_not_infinitesimal_pos
[GOAL]
x y : ℝ*
hx : ¬Infinitesimal x
hp : 0 < x
hy : InfiniteNeg y
⊢ InfiniteNeg (x * y)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
x y : ℝ*
hx : ¬Infinitesimal x
hp : 0 < x
hy : InfiniteNeg y
⊢ InfiniteNeg (y * x)
[PROOFSTEP]
exact infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos hy hx hp
[GOAL]
x y : ℝ*
hx : ¬Infinitesimal x
hy : Infinite y
⊢ Infinite (x * y)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
x y : ℝ*
hx : ¬Infinitesimal x
hy : Infinite y
⊢ Infinite (y * x)
[PROOFSTEP]
exact infinite_mul_of_infinite_not_infinitesimal hy hx
