awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
x : ℝ*
r : ℝ
hx : Germ.Tendsto x (𝓝 r)
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
have hx₁ : (∀ s < r, (↑s : ℝ*) ≤ x) ∧ ∀ s > r, x ≤ (↑s : ℝ*)
Tactic: rw [tendsto_iff_forall] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
r : ℝ
hx : (∀ s < r, (↑s : ℝ*) ≤ x) ∧ ∀ s > r, x ≤ (↑s : ℝ*)
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
have obtain : ∀ (s : ℝ) (hs : s < r), LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
Tactic: obtain ⟨s, hs⟩ := exists_lt r
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
r : ℝ
hx : (∀ s < r, (↑s : ℝ*) ≤ x) ∧ ∀ s > r, x ≤ (↑s : ℝ*)
s : ℝ
hs : s < r
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
have obtain : ∀ (t : ℝ) (ht : r < t), LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
Tactic: obtain ⟨t, ht⟩ := exists_gt r
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
x : ℝ*
r : ℝ
hx : Germ.Tendsto x (𝓝 r)
⊢ stdPart x = r
have hx₁ : (∀ s < r, (↑s : ℝ*) ≤ x) ∧ ∀ s > r, x ≤ (↑s : ℝ*)
Tactic: rw [tendsto_iff_forall] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
hx : Germ.Tendsto x (𝓝 0)
⊢ LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
have apply : Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
Tactic: apply (archimedeanClassMk_nonneg_of_tendsto hx).lt_of_ne'
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
hx : Germ.Tendsto x (𝓝 0)
⊢ Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have rw : stdPart x = 0
Tactic: rw [← stdPart_eq_zero, stdPart_of_tendsto hx]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
hx : Germ.Tendsto x (𝓝 0)
rw : stdPart x = 0
⊢ Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [← stdPart_eq_zero, stdPart_of_tendsto hx]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : 0 < r
hg : Tendsto (β := ℝ) (fun (x : ℕ) ↦ -f x) atTop (𝓝 (-0))
⊢ -ofSeq f < (↑r : ℝ*)
have hg₁ : Tendsto (β := ℝ) (fun (x : ℕ) ↦ -f x) atTop (𝓝 0)
Tactic: rw [neg_zero] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
f : ℕ → ℝ
hf : Tendsto f atTop (𝓝 0)
r : ℝ
hr : r < 0
⊢ (↑r : ℝ*) < ofSeq f
have rw : -(↑(-r) : ℝ*) < ofSeq f
Tactic: rw [← neg_neg r, coe_neg]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
r : ℝ
hx : Germ.Tendsto x atTop
⊢ (↑r : ℝ*) < x
have rcases : ∀ (f : ℕ → ℝ) (hx : Germ.Tendsto (ofSeq f) atTop), (↑r : ℝ*) < ofSeq f
Tactic: rcases ofSeq_surjective x with ⟨f, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
r : ℝ
f : ℕ → ℝ
hx : Germ.Tendsto (ofSeq f) atTop
⊢ (↑r : ℝ*) < ofSeq f
have hx₁ : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atTop
Tactic: rw [tendsto_ofSeq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
r : ℝ
hx : Germ.Tendsto x atBot
⊢ x < (↑r : ℝ*)
have rcases : ∀ (f : ℕ → ℝ) (hx : Germ.Tendsto (ofSeq f) atBot), ofSeq f < (↑r : ℝ*)
Tactic: rcases ofSeq_surjective x with ⟨f, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
r : ℝ
f : ℕ → ℝ
hx : Germ.Tendsto (ofSeq f) atBot
⊢ ofSeq f < (↑r : ℝ*)
have hx₁ : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atBot
Tactic: rw [tendsto_ofSeq] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
x : ℝ*
hx : Germ.Tendsto x atTop
⊢ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have this : 0 < x
Tactic: have : 0 < x := lt_of_tendsto_atTop 0 hx
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
x : ℝ*
hx : Germ.Tendsto x atBot
⊢ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have this : x < 0
Tactic: have : x < 0 := lt_of_tendsto_atBot 0 hx
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
⊢ Germ.Tendsto x atTop
have rcases : ∀ (f : ℕ → ℝ) (h : 0 < ofSeq f ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0),
  Germ.Tendsto (ofSeq f) atTop
Tactic: rcases ofSeq_surjective x with ⟨f, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
f : ℕ → ℝ
h : 0 < ofSeq f ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0
⊢ Germ.Tendsto (ofSeq f) atTop
have rw : ∀ (b : ℝ), ∀ᶠ (a : ℕ) in (↑(hyperfilter ℕ) : Filter ℕ), b ≤ f a
Tactic: rw [tendsto_ofSeq, tendsto_atTop]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
⊢ Germ.Tendsto x atBot
have rcases : ∀ (f : ℕ → ℝ) (h : ofSeq f < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0),
  Germ.Tendsto (ofSeq f) atBot
Tactic: rcases ofSeq_surjective x with ⟨f, rfl⟩
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
f : ℕ → ℝ
h : ofSeq f < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0
⊢ Germ.Tendsto (ofSeq f) atBot
have rw : ∀ (b : ℝ), ∀ᶠ (a : ℕ) in (↑(hyperfilter ℕ) : Filter ℕ), f a ≤ b
Tactic: rw [tendsto_ofSeq, tendsto_atBot]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
r : ℝ
h : x.IsSt r
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = r
have refine_1 : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
Tactic: refine ⟨?_, stdPart_eq coeRingHom (fun s hs ↦ ?_) (fun s hs ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
r : ℝ
h : x.IsSt r
refine_1 : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = r
have refine_2 : ∀ (s : ℝ) (hs : s < r), (coeRingHom : (a : ℝ) → ℝ*) s ≤ x
Tactic: refine ⟨?_, stdPart_eq coeRingHom (fun s hs ↦ ?_) (fun s hs ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
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
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = r
have refine_3 : ∀ (s : ℝ) (hs : s > r), x ≤ (coeRingHom : (a : ℝ) → ℝ*) s
Tactic: refine ⟨?_, stdPart_eq coeRingHom (fun s hs ↦ ?_) (fun s hs ↦ ?_)⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
x : ℝ*
r : ℝ
h : x.IsSt r
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
have h₁ : (↑r : ℝ*) - (↑1 : ℝ*) < x ∧ x < (↑r : ℝ*) + (↑1 : ℝ*)
Tactic: have h := h 1 zero_lt_one
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
r : ℝ
h : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = r
⊢ x.IsSt r
have obtain : ∀ (h : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)), x.IsSt (stdPart x)
Tactic: obtain ⟨h, rfl⟩ := h
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
⊢ x.IsSt (stdPart x)
have refine_1 : ∀ (y : ℝ) (hy : 0 < y), (↑(stdPart x) : ℝ*) - (↑y : ℝ*) < x
Tactic: refine fun y hy ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
refine_1 : ∀ (y : ℝ) (hy : 0 < y), (↑(stdPart x) : ℝ*) - (↑y : ℝ*) < x
⊢ x.IsSt (stdPart x)
have refine_2 : ∀ (y : ℝ) (hy : 0 < y), x < (↑(stdPart x) : ℝ*) + (↑y : ℝ*)
Tactic: refine fun y hy ↦ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
y : ℝ
hy : 0 < y
⊢ (↑(stdPart x) : ℝ*) - (↑y : ℝ*) < x
have refine_1 : (fun (x1 x2 : ℝ) ↦ x1 - x2) (stdPart x) y < stdPart x
Tactic: apply lt_of_lt_stdPart coeRingHom h
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
y : ℝ
hy : 0 < y
⊢ x < (↑(stdPart x) : ℝ*) + (↑y : ℝ*)
have refine_2 : stdPart x < (fun (x1 x2 : ℝ) ↦ x1 + x2) (stdPart x) y
Tactic: apply lt_of_stdPart_lt coeRingHom h
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
⊢ (if h : ∃ (r : ℝ), x.IsSt r then Classical.choose (p := x.IsSt) h else 0) = stdPart x
have pos : ∀ (h : ∃ (r : ℝ), x.IsSt r), Classical.choose (p := x.IsSt) h = stdPart x
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
pos : ∀ (h : ∃ (r : ℝ), x.IsSt r), Classical.choose (p := x.IsSt) h = stdPart x
⊢ (if h : ∃ (r : ℝ), x.IsSt r then Classical.choose (p := x.IsSt) h else 0) = stdPart x
have neg : ∀ (h : ¬∃ (r : ℝ), x.IsSt r), 0 = stdPart x
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
x : ℝ*
h : ¬∃ (r : ℝ), x.IsSt r
⊢ 0 = stdPart x
have h₁ : ¬∃ (r : ℝ), LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = r
Tactic: simp_rw [isSt_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
x : ℝ*
h : ¬∃ (r : ℝ), LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = r
⊢ 0 = stdPart x
have h₁ : ∀ (r : ℝ) (_ : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)), stdPart x ≠ r
Tactic: push Not at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : ∀ (r : ℝ) (_ : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)), stdPart x ≠ r
⊢ 0 = stdPart x
have neg : Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
Tactic: rw [eq_comm, stdPart_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : ∀ (r : ℝ) (_ : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)), stdPart x ≠ r
⊢ Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have neg : LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
Tactic: apply ne_of_lt
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : ∀ (r : ℝ) (_ : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)), stdPart x ≠ r
⊢ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have neg : ∀ (hx : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)), False
Tactic: by_contra! hx
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
⊢ x.Infinitesimal ↔ LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
have rw : x.IsSt 0 ↔ LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
Tactic: rw [Infinitesimal, isSt_iff, stdPart_eq_zero, lt_iff_le_and_ne']
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
rw : x.IsSt 0 ↔ LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
⊢ x.Infinitesimal ↔ LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
have rw₁ : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = 0 ↔
  LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
Tactic: rw [Infinitesimal, isSt_iff, stdPart_eq_zero, lt_iff_le_and_ne']
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
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)
⊢ x.Infinitesimal ↔ LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
have rw₂ : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0 ↔
  LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
Tactic: rw [Infinitesimal, isSt_iff, stdPart_eq_zero, lt_iff_le_and_ne']
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
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)
⊢ x.Infinitesimal ↔ LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
have 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
Tactic: rw [Infinitesimal, isSt_iff, stdPart_eq_zero, lt_iff_le_and_ne']
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
⊢ x.InfinitePos ↔ 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have refine_1 : ∀ (h : x.InfinitePos), 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
Tactic: refine ⟨fun h ↦ ?_, fun ⟨hx, hx'⟩ r ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
refine_1 : ∀ (h : x.InfinitePos), 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
⊢ x.InfinitePos ↔ 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have 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
Tactic: refine ⟨fun h ↦ ?_, fun ⟨hx, hx'⟩ r ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
x : ℝ*
h : x.InfinitePos
⊢ 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have hx : 0 < x
Tactic: have hx : 0 < x := h 0
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : x.InfinitePos
hx : 0 < x
⊢ 0 < x ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have refine_1 : ∀ (n : ℕ),
  HSMul.hSMul (β := ℝ*) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder ℝ*) → ℝ*)
            ((ArchimedeanOrder.of : (a : ℝ*) → ArchimedeanOrder ℝ*) 1)| :
        ℝ*) <
    |(ArchimedeanOrder.val : (a : ArchimedeanOrder ℝ*) → ℝ*) ((ArchimedeanOrder.of : (a : ℝ*) → ArchimedeanOrder ℝ*) x)|
Tactic: refine ⟨h 0, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
⊢ x.InfiniteNeg ↔ x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have refine_1 : ∀ (h : x.InfiniteNeg), x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
Tactic: refine ⟨fun h ↦ ?_, fun ⟨hx, hx'⟩ r ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
refine_1 : ∀ (h : x.InfiniteNeg), x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
⊢ x.InfiniteNeg ↔ x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have 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 : ℝ*)
Tactic: refine ⟨fun h ↦ ?_, fun ⟨hx, hx'⟩ r ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
x : ℝ*
h : x.InfiniteNeg
⊢ x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have hx : x < 0
Tactic: have hx : x < 0 := h 0
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
h : x.InfiniteNeg
hx : x < 0
⊢ x < 0 ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have refine_1 : ∀ (n : ℕ),
  HSMul.hSMul (β := ℝ*) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder ℝ*) → ℝ*)
            ((ArchimedeanOrder.of : (a : ℝ*) → ArchimedeanOrder ℝ*) 1)| :
        ℝ*) <
    |(ArchimedeanOrder.val : (a : ArchimedeanOrder ℝ*) → ℝ*) ((ArchimedeanOrder.of : (a : ℝ*) → ArchimedeanOrder ℝ*) x)|
Tactic: refine ⟨h 0, fun n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
⊢ x.Infinite ↔ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk x) 0
have 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
Tactic: rw [Infinite, infinitePos_iff, infiniteNeg_iff]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
r : ℝ
⊢ x.IsSt r ↔ Germ.Tendsto x (𝓝 r)
have rcases : ∀ (f : ℕ → ℝ), (ofSeq f).IsSt r ↔ Germ.Tendsto (ofSeq f) (𝓝 r)
Tactic: rcases ofSeq_surjective x with ⟨f, rfl⟩
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
r s : ℝ
hxr : x.IsSt r
hys : y.IsSt s
hrs : r < s
⊢ x < y
have rcases : ∀ (f : ℕ → ℝ) (hxr : (ofSeq f).IsSt r), ofSeq f < y
Tactic: rcases ofSeq_surjective x with ⟨f, rfl⟩
Cleared hypotheses: x, hxr
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
y : ℝ*
r s : ℝ
hys : y.IsSt s
hrs : r < s
f : ℕ → ℝ
hxr : (ofSeq f).IsSt r
⊢ ofSeq f < y
have rcases : ∀ (g : ℕ → ℝ) (hys : (ofSeq g).IsSt s), ofSeq f < ofSeq g
Tactic: rcases ofSeq_surjective y with ⟨g, rfl⟩
Cleared hypotheses: y, hys
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r s : ℝ
hrs : r < s
f : ℕ → ℝ
hxr : (ofSeq f).IsSt r
g : ℕ → ℝ
hys : (ofSeq g).IsSt s
⊢ ofSeq f < ofSeq g
have rw : ∀ (hxr : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 r)) (g : ℕ → ℝ)
  (hys : Tendsto g (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 s)), ofSeq f < ofSeq g
Tactic: rw [isSt_ofSeq_iff_tendsto] at hxr hys
Cleared hypotheses: hxr, g, hys
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
r s : ℝ
hr : x.IsSt r
hs : x.IsSt s
⊢ r = s
have rcases : ∀ (f : ℕ → ℝ) (hr : (ofSeq f).IsSt r) (hs : (ofSeq f).IsSt s), r = s
Tactic: rcases ofSeq_surjective x with ⟨f, rfl⟩
Cleared hypotheses: x, hr, hs
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
r s : ℝ
f : ℕ → ℝ
hr : (ofSeq f).IsSt r
hs : (ofSeq f).IsSt s
⊢ r = s
have hr₁ : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 r)
Tactic: rw [isSt_ofSeq_iff_tendsto] at hr hs
Cleared hypotheses: hr, hs
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
r s : ℝ
f : ℕ → ℝ
hr : (ofSeq f).IsSt r
hs : (ofSeq f).IsSt s
hr₁ : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 r)
⊢ r = s
have hs₁ : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) (𝓝 s)
Tactic: rw [isSt_ofSeq_iff_tendsto] at hr hs
Cleared hypotheses: hr, hs
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
x : ℝ*
r : ℝ
hxr : x.IsSt r
⊢ x.st = r
have h : ∃ (r : ℝ), x.IsSt r
Tactic: have h : ∃ r, IsSt x r := ⟨r, hxr⟩
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
r : ℝ
hxr : x.IsSt r
h : ∃ (r : ℝ), x.IsSt r
⊢ x.st = r
have rw : Classical.choose (p := x.IsSt) h = r
Tactic: rw [st, dif_pos h]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
x : ℝ*
hni : ¬x.Infinite
⊢ x.IsSt (sSup {y : ℝ | (↑y : ℝ*) < x})
have hni₁ : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
Tactic: rw [infinite_iff, not_lt] at hni
Cleared hypotheses: hni
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
hni : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x)
⊢ x.IsSt (sSup {y : ℝ | (↑y : ℝ*) < x})
have rw : LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk x) ∧ stdPart x = sSup {y : ℝ | (↑y : ℝ*) < x}
Tactic: rw [isSt_iff]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
⊢ x.st = sSup {y : ℝ | (↑y : ℝ*) < x}
have rw : stdPart x = sSup {y : ℝ | (↑y : ℝ*) < x}
Tactic: rw [st_eq]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r s : ℝ
⊢ (↑r : ℝ*).IsSt s ↔ (↑s : ℝ*).IsSt r
have rw : r = s ↔ (↑s : ℝ*).IsSt r
Tactic: rw [isSt_real_iff_eq, isSt_real_iff_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r s : ℝ
rw : r = s ↔ (↑s : ℝ*).IsSt r
⊢ (↑r : ℝ*).IsSt s ↔ (↑s : ℝ*).IsSt r
have rw₁ : r = s ↔ s = r
Tactic: rw [isSt_real_iff_eq, isSt_real_iff_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r s : ℝ
rw : r = s ↔ (↑s : ℝ*).IsSt r
rw₁ : r = s ↔ s = r
⊢ (↑r : ℝ*).IsSt s ↔ (↑s : ℝ*).IsSt r
have rw₂ : s = r ↔ s = r
Tactic: rw [isSt_real_iff_eq, isSt_real_iff_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r s t : ℝ
⊢ (↑r : ℝ*).IsSt s → (↑s : ℝ*).IsSt t → (↑r : ℝ*).IsSt t
have rw : r = s → s = t → r = t
Tactic: rw [isSt_real_iff_eq, isSt_real_iff_eq, isSt_real_iff_eq]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
r : ℝ
hxr : x.IsSt r
f : ℝ → ℝ
hf : ContinuousAt f r
⊢ IsSt (Germ.map f x) (f r)
have rcases : ∀ (g : ℕ → ℝ) (hxr : (ofSeq g).IsSt r), IsSt (Germ.map f (ofSeq g)) (f r)
Tactic: rcases ofSeq_surjective x with ⟨g, rfl⟩
Cleared hypotheses: x, hxr
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
r s : ℝ
hxr : x.IsSt r
hys : y.IsSt s
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
⊢ IsSt (Germ.map₂ f x y) (f r s)
have rcases : ∀ (x : ℕ → ℝ) (hxr : (ofSeq x).IsSt r), IsSt (Germ.map₂ f (ofSeq x) y) (f r s)
Tactic: rcases ofSeq_surjective x with ⟨x, rfl⟩
Cleared hypotheses: x, hxr
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
y : ℝ*
r s : ℝ
hys : y.IsSt s
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : (ofSeq x).IsSt r
⊢ IsSt (Germ.map₂ f (ofSeq x) y) (f r s)
have rcases : ∀ (y : ℕ → ℝ) (hys : (ofSeq y).IsSt s), IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
Tactic: rcases ofSeq_surjective y with ⟨y, rfl⟩
Cleared hypotheses: y, hys
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
r s : ℝ
f : ℝ → ℝ → ℝ
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : (ofSeq x).IsSt r
y : ℕ → ℝ
hys : (ofSeq y).IsSt s
⊢ IsSt (Germ.map₂ f (ofSeq x) (ofSeq y)) (f r s)
have 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)
Tactic: rw [isSt_ofSeq_iff_tendsto] at hxr hys
Cleared hypotheses: hxr, y, hys
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
⊢ |x|.Infinite ↔ x.Infinite
have inl : 0 ≤ x → (|x|.Infinite ↔ x.Infinite)
Tactic: cases le_total 0 x
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x : ℝ*
inl : 0 ≤ x → (|x|.Infinite ↔ x.Infinite)
⊢ |x|.Infinite ↔ x.Infinite
have inr : x ≤ 0 → (|x|.Infinite ↔ x.Infinite)
Tactic: cases le_total 0 x
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
hip : x.InfinitePos
hnin : ¬y.InfiniteNeg
r : ℝ
⊢ (↑r : ℝ*) < x + y
have obtain : ∀ (r₂ : ℝ) (hr₂ : ¬y < (↑r₂ : ℝ*)), (↑r : ℝ*) < x + y
Tactic: obtain ⟨r₂, hr₂⟩ := not_forall.mp hnin
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
hip : x.InfinitePos
hnin : ¬y.InfiniteNeg
r r₂ : ℝ
hr₂ : ¬y < (↑r₂ : ℝ*)
⊢ (↑r : ℝ*) < x + y
have h : (↑r : ℝ*) = (↑(r + -r₂) : ℝ*) + (↑r₂ : ℝ*)
Tactic: convert! add_lt_add_of_lt_of_le (hip (r + -r₂)) (not_lt.mp hr₂) using 1
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
x y : ℝ*
⊢ x.InfiniteNeg → ¬y.InfinitePos → (x + y).InfiniteNeg
have rw : (-x).InfinitePos → ¬(-y).InfiniteNeg → (-x + -y).InfinitePos
Tactic: rw [← infinitePos_neg, ← infinitePos_neg, ← @infiniteNeg_neg y, neg_add]
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (hypothesis)
Goal:
f : ℕ → ℝ
hf : Tendsto f atTop atTop
⊢ (ofSeq f).InfinitePos
have hf₁ : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atTop
Tactic: replace hf := hf.mono_left Nat.hyperfilter_le_atTop
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Real.Hyperreal (goal)
Goal:
f : ℕ → ℝ
hf : Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) atTop
⊢ (ofSeq f).InfinitePos
have rw : 0 < ofSeq f ∧ LT.lt (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (ofSeq f)) 0
Tactic: rw [infinitePos_iff]