awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a b : ℝ
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
h : 0 < b - a
⊢ #(↑(Inv.inv '' Ioo 0 (b - a)) : Type) ≤ #(↑(Ioo 0 (b - a)) : Type)

Tactic:
have h2 : #(Inv.inv '' Ioo 0 (b - a)) ≤ #(Ioo 0 (b - a)) := mk_image_le
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a b : ℝ
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
h : 0 < b - a
h2 : #(↑(Inv.inv '' Ioo 0 (b - a)) : Type) ≤ #(↑(Ioo 0 (b - a)) : Type)
⊢ 𝔠 ≤ #(↑(Ioo 0 (b - a)) : Type)

Tactic:
le_trans ?_ h2

Premises used: le_trans
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a b : ℝ
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
h : 0 < b - a
h2 : #(↑(Inv.inv '' Ioo 0 (b - a)) : Type) ≤ #(↑(Ioo 0 (b - a)) : Type)
refine : 𝔠 ≤ #(↑(Inv.inv '' Ioo 0 (b - a)) : Type)
⊢ 𝔠 ≤ #(↑(Ioo 0 (b - a)) : Type)

Tactic:
refine le_trans ?_ h2

Premises used: le_trans
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a b : ℝ
h1 : #(↑((fun (x : ℝ) ↦ x - a) '' Ioo a b) : Type) ≤ #(↑(Ioo a b) : Type)
h : 0 < b - a
h2 : #(↑(Inv.inv '' Ioo 0 (b - a)) : Type) ≤ #(↑(Ioo 0 (b - a)) : Type)
rw : 𝔠 ≤ #(↑(Ioo 0 (b - a))⁻¹ : Type)
rw₁ : 𝔠 ≤ #(↑(Ioi (b - a)⁻¹) : Type)
rw₂ rw₃ : 𝔠 ≤ 𝔠
⊢ 𝔠 ≤ #(↑(Inv.inv '' Ioo 0 (b - a)) : Type)

Tactic:
rw [image_inv_eq_inv, inv_Ioo_0_left h, mk_Ioi_real]

Premises used: Set.inv_Ioo_0_left, Set.image_inv_eq_inv, Cardinal.mk_Ioi_real
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a b : ℝ
h : a < b
⊢ #(↑(Ico a b) : Type) = 𝔠

Tactic:
le_antisymm (mk_real ▸ mk_set_le _) (mk_Ioo_real h ▸ mk_le_mk_of_subset Ioo_subset_Ico_self)

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a b : ℝ
h : a < b
⊢ #(↑(Icc a b) : Type) = 𝔠

Tactic:
le_antisymm (mk_real ▸ mk_set_le _) (mk_Ioo_real h ▸ mk_le_mk_of_subset Ioo_subset_Icc_self)

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
a b : ℝ
h : a < b
⊢ #(↑(Ioc a b) : Type) = 𝔠

Tactic:
le_antisymm (mk_real ▸ mk_set_le _) (mk_Ioo_real h ▸ mk_le_mk_of_subset Ioo_subset_Ioc_self)

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : y ≤ x
⊢ (Ioo x y).Countable

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
refine : ∀ (h : (Ioo x y).Countable), y ≤ x
⊢ (Ioo x y).Countable ↔ y ≤ x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : (Ioo x y).Countable
contrapose! : ∀ (h : x < y), ¬(Ioo x y).Countable
⊢ y ≤ x

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : x < y
rw : ℵ₀ < 𝔠
⊢ ¬(Ioo x y).Countable

Tactic:
rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real h, not_le]

Premises used: not_le, Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioo_real
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : x < y
⊢ ℵ₀ < 𝔠

Tactic:
Cardinal.aleph0_lt_continuum

Premises used: Cardinal.aleph0_lt_continuum
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : x < y
⊢ ℵ₀ < 𝔠

Tactic:
exact Cardinal.aleph0_lt_continuum

Premises used: Cardinal.aleph0_lt_continuum
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : y ≤ x
⊢ (Ico x y).Countable

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
refine : ∀ (h : (Ico x y).Countable), y ≤ x
⊢ (Ico x y).Countable ↔ y ≤ x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : (Ico x y).Countable
contrapose! : ∀ (h : x < y), ¬(Ico x y).Countable
⊢ y ≤ x

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : x < y
rw : ℵ₀ < 𝔠
⊢ ¬(Ico x y).Countable

Tactic:
rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ico_real h, not_le]

Premises used: not_le, Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ico_real
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : y ≤ x
⊢ (Ioc x y).Countable

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
refine : ∀ (h : (Ioc x y).Countable), y ≤ x
⊢ (Ioc x y).Countable ↔ y ≤ x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : (Ioc x y).Countable
contrapose! : ∀ (h : x < y), ¬(Ioc x y).Countable
⊢ y ≤ x

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : x < y
rw : ℵ₀ < 𝔠
⊢ ¬(Ioc x y).Countable

Tactic:
rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioc_real h, not_le]

Premises used: not_le, Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Ioc_real
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : y ≤ x
inl : ∀ (heq : y = x), (Icc x y).Countable
inr : ∀ (hlt : y < x), (Icc x y).Countable
⊢ (Icc x y).Countable

Tactic:
rcases le_iff_eq_or_lt.mp h with heq | hlt

Premises used: le_iff_eq_or_lt, Iff.mp
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : y ≤ x
heq : y = x
⊢ (Icc x y).Countable

Tactic:
simp [heq]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : y ≤ x
hlt : y < x
⊢ (Icc x y).Countable

Tactic:
simp [hlt]
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
refine : ∀ (h : (Icc x y).Countable), y ≤ x
⊢ (Icc x y).Countable ↔ y ≤ x

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by
    rcases le_iff_eq_or_lt.mp h with heq | hlt
    · simp [heq]
    · simp [hlt]⟩
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : (Icc x y).Countable
contrapose! : ∀ (h : x < y), ¬(Icc x y).Countable
⊢ y ≤ x

Tactic:
contrapose! h
-- Module: Mathlib.Analysis.Real.Cardinality
Goal:
x y : ℝ
h : x < y
rw : ℵ₀ < 𝔠
⊢ ¬(Icc x y).Countable

Tactic:
rw [← Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Icc_real h, not_le]

Premises used: not_le, Cardinal.le_aleph0_iff_set_countable, Cardinal.mk_Icc_real
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ IsStrictOrderedRing ℝ*

Tactic:
inferInstanceAs (IsStrictOrderedRing (Germ _ _))

Premises used: _private.0.Hyperreal.instIsStrictOrderedRing._proof_1
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ
⊢ (↑x : ℝ*) = (↑y : ℝ*) ↔ x = y

Tactic:
Germ.const_inj

Premises used: Filter.Germ.const_inj, Hyperreal.ofReal, Hyperreal
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ
⊢ (↑x : ℝ*) ≠ (↑y : ℝ*) ↔ x ≠ y

Tactic:
coe_eq_coe.not

Premises used: Hyperreal.coe_eq_coe, Iff.not
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ
⊢ (↑x : ℝ*) = 0 ↔ x = 0

Tactic:
coe_eq_coe

Premises used: Filter.Germ.ofFun, Hyperreal.coe_eq_coe, Filter.Germ.const, Hyperreal.ofReal, Quotient.mk'
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ
⊢ (↑x : ℝ*) = 1 ↔ x = 1

Tactic:
coe_eq_coe

Premises used: Filter.Germ.ofFun, Hyperreal.coe_eq_coe, Filter.Germ.const, Hyperreal.ofReal, Quotient.mk'
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ
⊢ (↑x : ℝ*) ≠ 0 ↔ x ≠ 0

Tactic:
coe_ne_coe

Premises used: Filter.Germ.ofFun, Hyperreal.coe_ne_coe, Filter.Germ.const, Hyperreal.ofReal, Quotient.mk'
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ
⊢ (↑x : ℝ*) ≠ 1 ↔ x ≠ 1

Tactic:
coe_ne_coe

Premises used: Filter.Germ.ofFun, Hyperreal.coe_ne_coe, Filter.Germ.const, Hyperreal.ofReal, Quotient.mk'
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ (↑1 : ℝ*) = 1

Tactic:
rfl

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

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Hyperreal.ofReal, Quotient.mk', rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ
⊢ (↑x⁻¹ : ℝ*) = (↑x : ℝ*)⁻¹

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Filter.Germ.map', Hyperreal.ofReal, Quotient.mk', Quot.map, Quotient.map', Filter.Germ.map, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ
⊢ (↑(-x) : ℝ*) = -(↑x : ℝ*)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Filter.Germ.map', Hyperreal.ofReal, Quotient.mk', Quot.map, Quotient.map', Filter.Germ.map, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ
⊢ (↑(x + y) : ℝ*) = (↑x : ℝ*) + (↑y : ℝ*)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Quotient.map₂, Filter.Germ.map₂, Hyperreal.ofReal, Quotient.mk', rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ (↑(OfNat.ofNat n) : ℝ*) = OfNat.ofNat n

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Hyperreal.ofReal, Quotient.mk', rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ
⊢ (↑(x * y) : ℝ*) = (↑x : ℝ*) * (↑y : ℝ*)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Quotient.map₂, Filter.Germ.map₂, Hyperreal.ofReal, Quotient.mk', rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ
⊢ (↑(x / y) : ℝ*) = (↑x : ℝ*) / (↑y : ℝ*)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Quotient.map₂, Filter.Germ.map₂, Hyperreal.ofReal, Quotient.mk', rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ
⊢ (↑(x - y) : ℝ*) = (↑x : ℝ*) - (↑y : ℝ*)

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Quotient.map₂, Filter.Germ.map₂, Hyperreal.ofReal, Quotient.mk', rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ
⊢ (↑x : ℝ*) ≤ (↑y : ℝ*) ↔ x ≤ y

Tactic:
Germ.const_le_iff

Premises used: Filter.Germ.const_le_iff, Hyperreal.ofReal
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ
⊢ (↑x : ℝ*) < (↑y : ℝ*) ↔ x < y

Tactic:
Germ.const_lt_iff

Premises used: Hyperreal.ofReal, Filter.Germ.const_lt_iff
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ
⊢ 0 ≤ (↑x : ℝ*) ↔ 0 ≤ x

Tactic:
coe_le_coe

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Hyperreal.ofReal, Quotient.mk', Hyperreal.coe_le_coe
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ
⊢ 0 < (↑x : ℝ*) ↔ 0 < x

Tactic:
coe_lt_coe

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Hyperreal.ofReal, Quotient.mk', Hyperreal.coe_lt_coe
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ
⊢ (↑|x| : ℝ*) = |(↑x : ℝ*)|

Tactic:
const_abs x

Premises used: Filter.Germ.const_abs, Hyperreal.ofReal, Hyperreal
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ
⊢ (↑(max x y) : ℝ*) = max (↑x : ℝ*) (↑y : ℝ*)

Tactic:
Germ.const_max _ _

Premises used: Quotient.map₂, Filter.Germ.map₂, Hyperreal.ofReal, Hyperreal, Filter.Germ.const_max
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ
⊢ (↑(min x y) : ℝ*) = min (↑x : ℝ*) (↑y : ℝ*)

Tactic:
Germ.const_min _ _

Premises used: Quotient.map₂, Filter.Germ.map₂, Hyperreal.ofReal, Hyperreal, Filter.Germ.const_min
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ
⊢ LE.le (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk (↑x : ℝ*))

Tactic:
mk_map_nonneg_of_archimedean coeRingHom x

Premises used: Filter.Germ.ofFun, Filter.Germ.const, ArchimedeanClass.mk_map_nonneg_of_archimedean, Hyperreal.ofReal, Quotient.mk', Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ
hx : x ≠ 0
⊢ Eq (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk (↑x : ℝ*)) 0

Tactic:
mk_map_of_archimedean' coeRingHom hx

Premises used: Filter.Germ.ofFun, Filter.Germ.const, Hyperreal.ofReal, Quotient.mk', Hyperreal.coeRingHom, ArchimedeanClass.mk_map_of_archimedean'
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ
⊢ stdPart (↑x : ℝ*) = x

Tactic:
stdPart_map_real coeRingHom x

Premises used: Filter.Germ.ofFun, Filter.Germ.const, ArchimedeanClass.stdPart_map_real, Hyperreal.ofReal, Quotient.mk', Hyperreal.coeRingHom
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ Function.Surjective ofSeq

Tactic:
Quot.exists_rep

Premises used: Filter.Germ.ofFun, Quot.exists_rep, Quotient, Quotient.mk', Filter.Germ, Hyperreal, Function.Surjective, Hyperreal.ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f g : ℕ → ℝ
⊢ ofSeq f < ofSeq g ↔ ∀ᶠ (n : ℕ) in (↑(hyperfilter ℕ) : Filter ℕ), f n < g n

Tactic:
Germ.coe_lt

Premises used: Filter.Germ.coe_lt, Hyperreal.ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f g : ℕ → ℝ
⊢ ofSeq f ≤ ofSeq g ↔ ∀ᶠ (n : ℕ) in (↑(hyperfilter ℕ) : Filter ℕ), f n ≤ g n

Tactic:
Germ.coe_le

Premises used: Filter.Germ.coe_le, Filter.EventuallyLE, Hyperreal.ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
apply : ∀ᶠ (x : ℕ) in atTop, r < (↑x : ℝ)
⊢ (↑r : ℝ*) < ω

Tactic:
apply ofSeq_lt_ofSeq.2 <| Filter.Eventually.filter_mono Nat.hyperfilter_le_atTop _

Premises used: Iff.mpr, Filter.Eventually.filter_mono, Nat.hyperfilter_le_atTop, Hyperreal.ofSeq_lt_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
obtain : ∀ (n : ℕ) (hn : r < (↑n : ℝ)), ∀ᶠ (x : ℕ) in atTop, r < (↑x : ℝ)
⊢ ∀ᶠ (x : ℕ) in atTop, r < (↑x : ℝ)

Tactic:
obtain ⟨n, hn⟩ := exists_nat_gt r

Premises used: exists_nat_gt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
n : ℕ
hn : r < (↑n : ℝ)
rw : ∃ (a : ℕ), ∀ b ≥ a, r < (↑b : ℝ)
⊢ ∀ᶠ (x : ℕ) in atTop, r < (↑x : ℝ)

Tactic:
rw [eventually_atTop]

Premises used: Filter.eventually_atTop
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
n : ℕ
hn : r < (↑n : ℝ)
⊢ ∃ (a : ℕ), ∀ b ≥ a, r < (↑b : ℝ)

Tactic:
⟨n, fun m hm ↦ hn.trans_le (mod_cast hm)⟩

Premises used: cast, Nat.cast_le._simp_1, LT.lt.trans_le, Exists.intro, Eq.symm
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
n : ℕ
hn : r < (↑n : ℝ)
⊢ ∃ (a : ℕ), ∀ b ≥ a, r < (↑b : ℝ)

Tactic:
exact ⟨n, fun m hm ↦ hn.trans_le (mod_cast hm)⟩
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ 0 < ω

Tactic:
coe_lt_omega 0

Premises used: Filter.Germ.ofFun, Hyperreal.coe_lt_omega, Filter.Germ.const, Hyperreal.ofReal, Quotient.mk', OfNat.ofNat
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ ω ≠ 0

Tactic:
omega_pos.ne'

Premises used: LT.lt.ne', Hyperreal.omega_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ |ω| = ω

Tactic:
abs_of_pos omega_pos

Premises used: Hyperreal.omega_pos, abs_of_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
n : ℕ
⊢ HSMul.hSMul (β := ℝ*) n
      (|(ArchimedeanOrder.val : (a : ArchimedeanOrder ℝ*) → ℝ*)
            ((ArchimedeanOrder.of : (a : ℝ*) → ArchimedeanOrder ℝ*) 1)| :
        ℝ*) <
    |(ArchimedeanOrder.val : (a : ArchimedeanOrder ℝ*) → ℝ*) ((ArchimedeanOrder.of : (a : ℝ*) → ArchimedeanOrder ℝ*) ω)|

Tactic:
simpa using coe_lt_omega n

Premises used: Hyperreal.coe_lt_omega, Nat.cast
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
rw : Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk ω) 0
⊢ stdPart ω = 0

Tactic:
rw [stdPart_eq_zero]

Premises used: ArchimedeanClass.stdPart_eq_zero
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk ω) 0

Tactic:
archimedeanClassMk_omega_neg.ne

Premises used: Hyperreal.archimedeanClassMk_omega_neg, LT.lt.ne
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ Ne (α := ArchimedeanClass ℝ*) (ArchimedeanClass.mk ω) 0

Tactic:
exact archimedeanClassMk_omega_neg.ne

Premises used: Hyperreal.archimedeanClassMk_omega_neg, LT.lt.ne
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ ω⁻¹ = ε

Tactic:
rfl

Premises used: Filter.Germ.ofFun, Filter.Germ.map', Quotient.mk', Hyperreal.epsilon, Quot.map, Quotient.map', Filter.Germ.map, Hyperreal.ofSeq, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ ε⁻¹ = ω

Tactic:
@inv_inv _ _ ω

Premises used: Filter.Germ.ofFun, Filter.Germ.map', Hyperreal.omega, Quotient.mk', inv_inv, Hyperreal.epsilon, Quot.map, Quotient.map', Filter.Germ.map, Hyperreal.ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ 0 < ε

Tactic:
inv_pos_of_pos omega_pos

Premises used: Filter.Germ.ofFun, Filter.Germ.map', inv_pos_of_pos, Quotient.mk', Hyperreal.epsilon, Hyperreal.omega_pos, Quot.map, Quotient.map', Filter.Germ.map, Hyperreal.ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ ε ≠ 0

Tactic:
epsilon_pos.ne'

Premises used: LT.lt.ne', Hyperreal.epsilon_pos
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ ε * ω = 1

Tactic:
@inv_mul_cancel₀ _ _ ω omega_ne_zero

Premises used: Filter.Germ.ofFun, Hyperreal.omega_ne_zero, Filter.Germ.map', Quotient.mk', Hyperreal.epsilon, Quot.map, Quotient.map', Filter.Germ.map, inv_mul_cancel₀, Hyperreal.ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
⊢ LT.lt (α := ArchimedeanClass ℝ*) 0 (ArchimedeanClass.mk ε)

Tactic:
simp [← inv_omega]

Premises used: Hyperreal.inv_omega
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
f : ℕ → ℝ
lb : Filter ℝ
⊢ Germ.Tendsto (ofSeq f) lb ↔ Tendsto f (↑(hyperfilter ℕ) : Filter ℕ) lb

Tactic:
.rfl

Premises used: Quotient.liftOn', Filter.Germ.Tendsto, Iff.rfl, Filter.Tendsto, Filter.Germ.liftOn
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
hxr : Germ.Tendsto x (𝓝 r)
rcases : ∀ (g : ℕ → ℝ) (hxr : Germ.Tendsto (ofSeq g) (𝓝 r)), (Germ.map f (ofSeq g)).Tendsto (𝓝 (f r))
⊢ (Germ.map f x).Tendsto (𝓝 (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 : Germ.Tendsto (ofSeq g) (𝓝 r)
⊢ (Germ.map f (ofSeq g)).Tendsto (𝓝 (f r))

Tactic:
hf.tendsto.comp hxr

Premises used: Quotient.liftOn', Set.Mem, Filter.Germ.Tendsto, ContinuousAt.tendsto, Filter.Tendsto, Filter.Germ.liftOn, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℝ → ℝ
hf : ContinuousAt f r
g : ℕ → ℝ
hxr : Germ.Tendsto (ofSeq g) (𝓝 r)
⊢ (Germ.map f (ofSeq g)).Tendsto (𝓝 (f r))

Tactic:
exact hf.tendsto.comp hxr

Premises used: ContinuousAt.tendsto, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x y : ℝ*
r s : ℝ
f : ℝ → ℝ → ℝ
hxr : Germ.Tendsto x (𝓝 r)
hys : Germ.Tendsto y (𝓝 s)
hf : ContinuousAt (Function.uncurry f) (r, s)
rcases : ∀ (x : ℕ → ℝ) (hxr : Germ.Tendsto (ofSeq x) (𝓝 r)), (Germ.map₂ f (ofSeq x) y).Tendsto (𝓝 (f r s))
⊢ (Germ.map₂ f x y).Tendsto (𝓝 (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 : ℝ
f : ℝ → ℝ → ℝ
hys : Germ.Tendsto y (𝓝 s)
hf : ContinuousAt (Function.uncurry f) (r, s)
x : ℕ → ℝ
hxr : Germ.Tendsto (ofSeq x) (𝓝 r)
rcases : ∀ (y : ℕ → ℝ) (hys : Germ.Tendsto (ofSeq y) (𝓝 s)), (Germ.map₂ f (ofSeq x) (ofSeq y)).Tendsto (𝓝 (f r s))
⊢ (Germ.map₂ f (ofSeq x) y).Tendsto (𝓝 (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 : Germ.Tendsto (ofSeq x) (𝓝 r)
y : ℕ → ℝ
hys : Germ.Tendsto (ofSeq y) (𝓝 s)
⊢ (Germ.map₂ f (ofSeq x) (ofSeq y)).Tendsto (𝓝 (f r s))

Tactic:
hf.tendsto.comp (hxr.prodMk_nhds hys)

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

Tactic:
exact hf.tendsto.comp (hxr.prodMk_nhds hys)

Premises used: ContinuousAt.tendsto, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
x : ℝ*
r : ℝ
rcases : ∀ (f : ℕ → ℝ), Germ.Tendsto (ofSeq f) (𝓝 r) ↔ (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
⊢ Germ.Tendsto x (𝓝 r) ↔ (∀ s < r, (↑s : ℝ*) ≤ x) ∧ ∀ s > r, x ≤ (↑s : ℝ*)

Tactic:
rcases ofSeq_surjective x with ⟨f, rfl⟩

Premises used: Hyperreal.ofSeq_surjective, rfl
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
rw :
  (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → ∀ᶠ (x : ℕ) in (↑(hyperfilter ℕ) : Filter ℕ), f x ∈ Set.Ioo i.1 i.2) ↔
    (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
⊢ Germ.Tendsto (ofSeq f) (𝓝 r) ↔ (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)

Tactic:
rw [tendsto_ofSeq, (nhds_basis_Ioo _).tendsto_right_iff]

Premises used: nhds_basis_Ioo, Filter.HasBasis.tendsto_right_iff, Hyperreal.tendsto_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
simp_rw :
  (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2) ↔
    (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)
⊢ (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → ∀ᶠ (x : ℕ) in (↑(hyperfilter ℕ) : Filter ℕ), f x ∈ Set.Ioo i.1 i.2) ↔
    (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)

Tactic:
simp_rw [Set.mem_Ioo, eventually_and, ← ofSeq_lt_ofSeq]

Premises used: Filter.eventually_and, Set.mem_Ioo, Hyperreal.ofSeq_lt_ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
⊢ (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2) ↔
    (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)

Tactic:
⟨fun H ↦ ⟨fun s hs ↦ ?_, fun s hs ↦ ?_⟩, fun H ⟨s, t⟩ ⟨hs, ht⟩ ↦ ⟨?_, ?_⟩⟩

Premises used: _private.0.Hyperreal.tendsto_iff_forall.match_4, Prod.mk, Prod.fst, And, And.intro, LT.lt, Iff.intro, _private.0.Hyperreal.tendsto_iff_forall.match_5, Prod.snd, Hyperreal.ofSeq
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
refine_1 :
  ∀ (H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2)
    (s : ℝ) (hs : s < r), (↑s : ℝ*) ≤ ofSeq f
refine_2 :
  ∀ (H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2)
    (s : ℝ) (hs : s > r), ofSeq f ≤ (↑s : ℝ*)
refine_3 :
  ∀ (H : (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)) (x : ℝ × ℝ) (s t : ℝ),
    (s, t).1 < r ∧ r < (s, t).2 → ∀ (hs : (s, t).1 < r) (ht : r < (s, t).2), (ofSeq fun (n : ℕ) ↦ (s, t).1) < ofSeq f
refine_4 :
  ∀ (H : (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)) (x : ℝ × ℝ) (s t : ℝ),
    (s, t).1 < r ∧ r < (s, t).2 → ∀ (hs : (s, t).1 < r) (ht : r < (s, t).2), ofSeq f < ofSeq fun (n : ℕ) ↦ (s, t).2
⊢ (∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2) ↔
    (∀ s < r, (↑s : ℝ*) ≤ ofSeq f) ∧ ∀ s > r, ofSeq f ≤ (↑s : ℝ*)

Tactic:
refine ⟨fun H ↦ ⟨fun s hs ↦ ?_, fun s hs ↦ ?_⟩, fun H ⟨s, t⟩ ⟨hs, ht⟩ ↦ ⟨?_, ?_⟩⟩
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2
s : ℝ
hs : s < r
refine_1 : ∀ (t : ℝ) (ht : r < t), (↑s : ℝ*) ≤ ofSeq f
⊢ (↑s : ℝ*) ≤ ofSeq f

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

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2
s : ℝ
hs : s < r
t : ℝ
ht : r < t
⊢ (↑s : ℝ*) ≤ ofSeq f

Tactic:
(H ⟨s, t⟩ ⟨hs, ht⟩).1.le

Premises used: Filter.Germ.const, LT.lt.le, Prod.mk, Hyperreal.ofReal, And.left, And.intro
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2
s : ℝ
hs : s < r
t : ℝ
ht : r < t
⊢ (↑s : ℝ*) ≤ ofSeq f

Tactic:
exact (H ⟨s, t⟩ ⟨hs, ht⟩).1.le

Premises used: LT.lt.le, Prod.mk, And.left, And.intro
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2
s : ℝ
hs : s > r
refine_2 : ∀ (t : ℝ) (ht : t < r), ofSeq f ≤ (↑s : ℝ*)
⊢ ofSeq f ≤ (↑s : ℝ*)

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

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

Tactic:
(H ⟨t, s⟩ ⟨ht, hs⟩).2.le

Premises used: Filter.Germ.const, LT.lt.le, Prod.mk, Hyperreal.ofReal, And.right, And.intro
-- Module: Mathlib.Analysis.Real.Hyperreal
Goal:
r : ℝ
f : ℕ → ℝ
H : ∀ (i : ℝ × ℝ), i.1 < r ∧ r < i.2 → (ofSeq fun (n : ℕ) ↦ i.1) < ofSeq f ∧ ofSeq f < ofSeq fun (n : ℕ) ↦ i.2
s : ℝ
hs : s > r
t : ℝ
ht : t < r
⊢ ofSeq f ≤ (↑s : ℝ*)

Tactic:
exact (H ⟨t, s⟩ ⟨ht, hs⟩).2.le

Premises used: LT.lt.le, Prod.mk, And.right, And.intro