awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
obtain : ∀ (n : ℕ) (hn : x n ∉ insert 0 (range x)), False
⊢ False

Tactic:
obtain ⟨n, hn⟩ : ∃ n : ℕ, x n ∉ insert (0 : ℚ) (range x) :=
    (hxc.eventually hx0.isCompact_insert_range.compl_mem_cocompact).exists

Premises used: IsCompact.compl_mem_cocompact, Insert.insert, Filter.Eventually.exists, Filter.Tendsto.eventually, Set.range, OfNat.ofNat, Filter.Tendsto.isCompact_insert_range
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
n : ℕ
hn : x n ∉ insert 0 (range x)
⊢ False

Tactic:
hn (Or.inr ⟨n, rfl⟩)

Premises used: Exists.intro, Or.inr, rfl
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
n : ℕ
hn : x n ∉ insert 0 (range x)
⊢ False

Tactic:
exact hn (Or.inr ⟨n, rfl⟩)

Premises used: Exists.intro, Or.inr, rfl
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
h : IsCountablyGenerated (α := ℚ∞) (𝓝 ∞)
⊢ IsCountablyGenerated (α := ℚ) (comap OnePoint.some (𝓝 ∞))

Tactic:
infer_instance
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
h : IsCountablyGenerated (α := ℚ∞) (𝓝 ∞)
⊢ IsCountablyGenerated (α := ℚ) (comap OnePoint.some (𝓝 ∞))

Tactic:
have : IsCountablyGenerated (comap (OnePoint.some : ℚ → ℚ∞) (𝓝 ∞)) := by infer_instance
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
h : IsCountablyGenerated (α := ℚ∞) (𝓝 ∞)
this : IsCountablyGenerated (α := ℚ) (comap OnePoint.some (𝓝 ∞))
⊢ (cocompact ℚ).IsCountablyGenerated

Tactic:
rw [OnePoint.comap_coe_nhds_infty, coclosedCompact_eq_cocompact] at this

Premises used: OnePoint.comap_coe_nhds_infty, Filter.coclosedCompact_eq_cocompact
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
h : IsCountablyGenerated (α := ℚ∞) (𝓝 ∞)
this : (cocompact ℚ).IsCountablyGenerated
⊢ False

Tactic:
not_countably_generated_cocompact this

Premises used: Rat.not_countably_generated_cocompact
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
h : IsCountablyGenerated (α := ℚ∞) (𝓝 ∞)
this : (cocompact ℚ).IsCountablyGenerated
⊢ False

Tactic:
exact not_countably_generated_cocompact this

Premises used: Rat.not_countably_generated_cocompact
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
h : FirstCountableTopology ℚ∞
⊢ False

Tactic:
not_countably_generated_nhds_infty_opc inferInstance

Premises used: inferInstance, Rat.not_countably_generated_nhds_infty_opc
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
h : FirstCountableTopology ℚ∞
⊢ False

Tactic:
exact not_countably_generated_nhds_infty_opc inferInstance

Premises used: inferInstance, Rat.not_countably_generated_nhds_infty_opc
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
h : SecondCountableTopology ℚ∞
⊢ False

Tactic:
not_firstCountableTopology_opc inferInstance

Premises used: Rat.not_firstCountableTopology_opc, inferInstance
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
h : SecondCountableTopology ℚ∞
⊢ False

Tactic:
exact not_firstCountableTopology_opc inferInstance

Premises used: Rat.not_firstCountableTopology_opc, inferInstance
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
⊢ TotallyDisconnectedSpace ℚ

Tactic:
⟨fun s hsu hs x hx y hy => ?_⟩

Premises used: TotallyDisconnectedSpace.mk
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
refine : ∀ (s : Set ℚ) (hsu : s ⊆ univ) (hs : IsPreconnected s) (x : ℚ) (hx : x ∈ s) (y : ℚ) (hy : y ∈ s), x = y
⊢ TotallyDisconnectedSpace ℚ

Tactic:
refine ⟨fun s hsu hs x hx y hy => ?_⟩
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
by_contra : ∀ (H : x ≠ y), False
⊢ x = y

Tactic:
by_contra H : x ≠ y
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
inr :
  ∀
    (this :
      ∀ (s : Set ℚ) (hs : IsPreconnected s) (x : ℚ) (hx : x ∈ s) (y : ℚ) (hy : y ∈ s) (H : x ≠ y) (hlt : x < y), False)
    (hlt : ¬x < y), False
wlog : ∀ (s : Set ℚ) (hs : IsPreconnected s) (x : ℚ) (hx : x ∈ s) (y : ℚ) (hy : y ∈ s) (H : x ≠ y) (hlt : x < y), False
⊢ False

Tactic:
wlog hlt : x < y
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this : ∀ (s : Set ℚ) (hs : IsPreconnected s) (x : ℚ) (hx : x ∈ s) (y : ℚ) (hy : y ∈ s) (H : x ≠ y) (hlt : x < y), False
hlt : ¬x < y
⊢ False

Tactic:
apply this s hs y hy x hx H.symm <| H.lt_or_gt.resolve_left hlt

Premises used: Or.resolve_left, Ne.symm, Ne.lt_or_gt
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
rcases : ∀ (z : ℝ) (hz : Irrational z) (hxz : (↑x : ℝ) < z) (hzy : z < (↑y : ℝ)), False
⊢ False

Tactic:
rcases exists_irrational_btwn (Rat.cast_lt.2 hlt) with ⟨z, hz, hxz, hzy⟩

Premises used: Iff.mpr, Rat.cast_lt, exists_irrational_btwn
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : (↑x : ℝ) < z
hzy : z < (↑y : ℝ)
⊢ IsPreconnected (α := ℝ) (Rat.cast '' s)

Tactic:
have := hs.image _ continuous_coe_real.continuousOn
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : (↑x : ℝ) < z
hzy : z < (↑y : ℝ)
this : IsPreconnected (α := ℝ) (Rat.cast '' s)
⊢ OrdConnected (α := ℝ) (Rat.cast '' s)

Tactic:
rw [isPreconnected_iff_ordConnected] at this

Premises used: isPreconnected_iff_ordConnected
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : (↑x : ℝ) < z
hzy : z < (↑y : ℝ)
this : OrdConnected (α := ℝ) (Rat.cast '' s)
⊢ Membership.mem (γ := Set ℝ) (Rat.cast '' s) z

Tactic:
have : z ∈ Rat.cast '' s :=
    this.out (mem_image_of_mem _ hx) (mem_image_of_mem _ hy) ⟨hxz.le, hzy.le⟩
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : (↑x : ℝ) < z
hzy : z < (↑y : ℝ)
this_1 : OrdConnected (α := ℝ) (Rat.cast '' s)
this : Membership.mem (γ := Set ℝ) (Rat.cast '' s) z
⊢ False

Tactic:
hz (image_subset_range _ _ this)

Premises used: Set.image_subset_range
-- Module: Mathlib.Topology.Instances.RatLemmas
Goal:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
z : ℝ
hz : Irrational z
hxz : (↑x : ℝ) < z
hzy : z < (↑y : ℝ)
this_1 : OrdConnected (α := ℝ) (Rat.cast '' s)
this : Membership.mem (γ := Set ℝ) (Rat.cast '' s) z
⊢ False

Tactic:
exact hz (image_subset_range _ _ this)

Premises used: Set.image_subset_range
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
⊢ ∀ (u : Set ℝ),
    Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)}) u → IsOpen u

Tactic:
simp +contextual [isOpen_Ioo]

Premises used: isOpen_Ioo
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
a : ℝ
x : Set ℝ
hav : a ∈ x
hv : IsOpen x
w w_1 : ℝ
hl : w < a
hu : a < w_1
h : Ioo w w_1 ⊆ x
q : ℚ
hlq : w < (↑q : ℝ)
hqa : (↑q : ℝ) < a
p : ℚ
hap : a < (↑p : ℝ)
hpu : (↑p : ℝ) < w_1
simp :
  ∃ (i : ℚ) (i_1 : ℚ) (_ : i < i_1), Membership.mem (γ := Set (Set ℝ)) {Ioo (↑i : ℝ) (↑i_1 : ℝ)} (Ioo (↑q : ℝ) (↑p : ℝ))
⊢ Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)})
    (Ioo (↑q : ℝ) (↑p : ℝ))

Tactic:
simp only [mem_iUnion]

Premises used: Set.mem_iUnion
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
a : ℝ
x : Set ℝ
hav : a ∈ x
hv : IsOpen x
w w_1 : ℝ
hl : w < a
hu : a < w_1
h : Ioo w w_1 ⊆ x
q : ℚ
hlq : w < (↑q : ℝ)
hqa : (↑q : ℝ) < a
p : ℚ
hap : a < (↑p : ℝ)
hpu : (↑p : ℝ) < w_1
⊢ ∃ (i : ℚ) (i_1 : ℚ) (_ : i < i_1), Membership.mem (γ := Set (Set ℝ)) {Ioo (↑i : ℝ) (↑i_1 : ℝ)} (Ioo (↑q : ℝ) (↑p : ℝ))

Tactic:
⟨q, p, Rat.cast_lt.1 <| hqa.trans hap, rfl⟩

Premises used: Rat.cast_lt, Exists.intro, Iff.mp, LT.lt.trans, rfl
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
a : ℝ
x : Set ℝ
hav : a ∈ x
hv : IsOpen x
w w_1 : ℝ
hl : w < a
hu : a < w_1
h : Ioo w w_1 ⊆ x
q : ℚ
hlq : w < (↑q : ℝ)
hqa : (↑q : ℝ) < a
p : ℚ
hap : a < (↑p : ℝ)
hpu : (↑p : ℝ) < w_1
⊢ ∃ (i : ℚ) (i_1 : ℚ) (_ : i < i_1), Membership.mem (γ := Set (Set ℝ)) {Ioo (↑i : ℝ) (↑i_1 : ℝ)} (Ioo (↑q : ℝ) (↑p : ℝ))

Tactic:
exact ⟨q, p, Rat.cast_lt.1 <| hqa.trans hap, rfl⟩
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
x : ℝ
⊢ x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, |y - x| < ε

Tactic:
simp [mem_closure_iff_nhds_basis nhds_basis_ball, Real.dist_eq]

Premises used: Real.dist_eq, Metric.nhds_basis_ball, mem_closure_iff_nhds_basis
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
r : ℝ
r0 : 0 < r
H : ∀ x ∈ s, r ≤ |x|
⊢ UniformContinuous (β := ℝ) fun (p : (↑s : Type)) ↦ (↑p : ℝ)⁻¹

Tactic:
Metric.uniformContinuous_iff.2 fun _ε ε0 =>
    let ⟨δ, δ0, Hδ⟩ := rat_inv_continuous_lemma abs ε0 r0
    ⟨δ, δ0, fun {a b} h => Hδ (H _ a.2) (H _ b.2) h⟩

Premises used: Iff.mpr, abs, Exists, _private.0.Real.uniformContinuous_inv.match_1, GT.gt, And, And.intro, Exists.intro, OfNat.ofNat, Subtype.val, Metric.uniformContinuous_iff, rat_inv_continuous_lemma, Subtype.property
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
⊢ UniformContinuous (α := ℝ) abs

Tactic:
Metric.uniformContinuous_iff.2 fun ε ε0 =>
    ⟨ε, ε0, fun _ _ ↦ lt_of_le_of_lt (abs_abs_sub_abs_le_abs_sub _ _)⟩

Premises used: Iff.mpr, lt_of_le_of_lt, And.intro, abs_abs_sub_abs_le_abs_sub, Exists.intro, Metric.uniformContinuous_iff
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
⊢ Continuous (Y := ℝ) fun (a : { r : ℝ // r ≠ 0 }) ↦ (↑a : ℝ)⁻¹

Tactic:
continuousOn_inv₀.restrict

Premises used: Set.Mem, setOf, continuousOn_inv₀, ContinuousOn.restrict, Set.singleton, Set.restrict, Not
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set (ℝ × ℝ)
r₁ r₂ : ℝ
H : ∀ x ∈ s, |x.1| < r₁ ∧ |x.2| < r₂
⊢ UniformContinuous (β := ℝ) fun (p : (↑s : Type)) ↦ (↑p : ℝ × ℝ).1 * (↑p : ℝ × ℝ).2

Tactic:
Metric.uniformContinuous_iff.2 fun _ε ε0 =>
    let ⟨δ, δ0, Hδ⟩ := rat_mul_continuous_lemma abs ε0
    ⟨δ, δ0, fun {a b} h =>
      let ⟨h₁, h₂⟩ := max_lt_iff.1 h
      Hδ (H _ a.2).1 (H _ b.2).2 h₁ h₂⟩

Premises used: Iff.mpr, _private.0.Real.uniformContinuous_mul.match_2, HMul.hMul, abs, Set.Mem, setOf, Exists, _private.0.Real.uniformContinuous_mul.match_1, max_lt_iff, rat_mul_continuous_lemma, Prod.fst, GT.gt, And, And.right, And.left, And.intro, LT.lt, Exists.intro, Iff.mp, Dist.dist, OfNat.ofNat, Subtype.val, Prod.snd, Metric.uniformContinuous_iff, Subtype.property
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
x ε : ℝ
rw : TotallyBounded (Ioo (x - ε) (x + ε))
⊢ TotallyBounded (ball x ε)

Tactic:
rw [Real.ball_eq_Ioo]

Premises used: Real.ball_eq_Ioo
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
x ε : ℝ
⊢ TotallyBounded (Ioo (x - ε) (x + ε))

Tactic:
apply totallyBounded_Ioo

Premises used: totallyBounded_Ioo
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
K : Subfield ℝ
hc : IsClosed (↑K : Set ℝ)
rw : closure (↑K : Set ℝ) = univ
⊢ K = ⊤

Tactic:
rw [SetLike.ext'_iff, Subfield.coe_top, ← hc.closure_eq]

Premises used: Subfield.coe_top, IsClosed.closure_eq, SetLike.ext'_iff
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
K : Subfield ℝ
hc : IsClosed (↑K : Set ℝ)
⊢ closure (↑K : Set ℝ) = univ

Tactic:
Rat.denseRange_cast.mono ?_ |>.closure_eq

Premises used: Dense.mono, Dense.closure_eq, Rat.denseRange_cast
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
K : Subfield ℝ
hc : IsClosed (↑K : Set ℝ)
refine : range Rat.cast ⊆ (↑K : Set ℝ)
⊢ closure (↑K : Set ℝ) = univ

Tactic:
refine Rat.denseRange_cast.mono ?_ |>.closure_eq

Premises used: Dense.mono, Dense.closure_eq, Rat.denseRange_cast
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
K : Subfield ℝ
hc : IsClosed (↑K : Set ℝ)
w : ℚ
⊢ (↑w : ℝ) ∈ (↑K : Set ℝ)

Tactic:
SubfieldClass.ratCast_mem K _

Premises used: SubfieldClass.ratCast_mem, Set.Mem
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
K : Subfield ℝ
hc : IsClosed (↑K : Set ℝ)
w : ℚ
⊢ (↑w : ℝ) ∈ (↑K : Set ℝ)

Tactic:
exact SubfieldClass.ratCast_mem K _

Premises used: SubfieldClass.ratCast_mem
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
x : ℝ
⊢ ∃ (u : ℕ → ℚ), StrictMono u ∧ (∀ (n : ℕ), (↑(u n) : ℝ) < x) ∧ Tendsto (fun (x : ℕ) ↦ (↑(u x) : ℝ)) atTop (𝓝 x)

Tactic:
Rat.denseRange_cast.exists_seq_strictMono_tendsto Rat.cast_strictMono.monotone x

Premises used: StrictMono.monotone, Set.Mem, DenseRange.exists_seq_strictMono_tendsto, Rat.cast_strictMono, Rat.denseRange_cast, Set.Iio
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
x : ℝ
⊢ ∃ (u : ℕ → ℚ), StrictAnti u ∧ (∀ (n : ℕ), x < (↑(u n) : ℝ)) ∧ Tendsto (fun (x : ℕ) ↦ (↑(u x) : ℝ)) atTop (𝓝 x)

Tactic:
Rat.denseRange_cast.exists_seq_strictAnti_tendsto Rat.cast_strictMono.monotone x

Premises used: Set.Ioi, StrictMono.monotone, Set.Mem, Rat.cast_strictMono, Rat.denseRange_cast, DenseRange.exists_seq_strictAnti_tendsto
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
have : ∀ (z : ℝ) (hz : z ∈ s) (ne : z ≠ x), ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε

Tactic:
have ⟨z, hz, ne⟩ := nt.exists_ne x
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε

Tactic:
ne.lt_or_gt.elim (fun lt ↦ ?_) fun lt ↦ ?_

Premises used: Or.elim, Ne.lt_or_gt
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
refine_1 : ∀ (lt : z < x), ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
refine_2 : ∀ (lt : x < z), ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε

Tactic:
refine ne.lt_or_gt.elim (fun lt ↦ ?_) fun lt ↦ ?_

Premises used: Or.elim, Ne.lt_or_gt
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : z < x
refine_1 : ∀ (q : ℚ) (h₁ : max z (x - ε) < (↑q : ℝ)) (h₂ : (↑q : ℝ) < x), ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε

Tactic:
have ⟨q, h₁, h₂⟩ := exists_rat_btwn (max_lt lt (sub_lt_self x ε_pos))
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : z < x
q : ℚ
h₁ : max z (x - ε) < (↑q : ℝ)
h₂ : (↑q : ℝ) < x
⊢ z < (↑q : ℝ) ∧ x - ε < (↑q : ℝ)

Tactic:
rw [max_lt_iff] at h₁

Premises used: max_lt_iff
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : z < x
q : ℚ
h₁ : max z (x - ε) < (↑q : ℝ)
h₂ : (↑q : ℝ) < x
h₃ : z < (↑q : ℝ) ∧ x - ε < (↑q : ℝ)
⊢ (↑q : ℝ) < x

Tactic:
rw [max_lt_iff] at h₁

Premises used: max_lt_iff
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : z < x
q : ℚ
h₁ : z < (↑q : ℝ) ∧ x - ε < (↑q : ℝ)
h₂ : (↑q : ℝ) < x
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε

Tactic:
⟨q, ⟨conn.out hz hx ⟨h₁.1.le, h₂.le⟩, q, rfl⟩, ?_⟩

Premises used: Set.OrdConnected.out, LT.lt.le, Rat.cast, And.left, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : z < x
q : ℚ
h₁ : z < (↑q : ℝ) ∧ x - ε < (↑q : ℝ)
h₂ : (↑q : ℝ) < x
refine_1 : |(↑q : ℝ) - x| < ε
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε

Tactic:
refine ⟨q, ⟨conn.out hz hx ⟨h₁.1.le, h₂.le⟩, q, rfl⟩, ?_⟩
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : z < x
q : ℚ
h₁ : z < (↑q : ℝ) ∧ x - ε < (↑q : ℝ)
h₂ : (↑q : ℝ) < x
⊢ |(↑q : ℝ) - x| < ε

Tactic:
simpa only [abs_sub_comm, abs_of_pos (sub_pos.mpr h₂), sub_lt_comm] using h₁.2

Premises used: Iff.mpr, sub_pos, sub_lt_comm, And.right, abs_sub_comm, abs_of_pos
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : x < z
refine_2 : ∀ (q : ℚ) (h₁ : x < (↑q : ℝ)) (h₂ : (↑q : ℝ) < min z (x + ε)), ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε

Tactic:
have ⟨q, h₁, h₂⟩ := exists_rat_btwn (lt_min lt (lt_add_of_pos_right x ε_pos))
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : x < z
q : ℚ
h₁ : x < (↑q : ℝ)
h₂ : (↑q : ℝ) < min z (x + ε)
⊢ (↑q : ℝ) < z ∧ (↑q : ℝ) < x + ε

Tactic:
rw [lt_min_iff] at h₂

Premises used: lt_min_iff
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : x < z
q : ℚ
h₁ : x < (↑q : ℝ)
h₂ : (↑q : ℝ) < z ∧ (↑q : ℝ) < x + ε
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε

Tactic:
⟨q, ⟨conn.out hx hz ⟨h₁.le, h₂.1.le⟩, q, rfl⟩, ?_⟩

Premises used: Set.OrdConnected.out, LT.lt.le, Rat.cast, And.left, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : x < z
q : ℚ
h₁ : x < (↑q : ℝ)
h₂ : (↑q : ℝ) < z ∧ (↑q : ℝ) < x + ε
refine_2 : |(↑q : ℝ) - x| < ε
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε

Tactic:
refine ⟨q, ⟨conn.out hx hz ⟨h₁.le, h₂.1.le⟩, q, rfl⟩, ?_⟩
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
z : ℝ
hz : z ∈ s
ne : z ≠ x
lt : x < z
q : ℚ
h₁ : x < (↑q : ℝ)
h₂ : (↑q : ℝ) < z ∧ (↑q : ℝ) < x + ε
⊢ |(↑q : ℝ) - x| < ε

Tactic:
simpa only [abs_of_pos (sub_pos.2 h₁), sub_lt_iff_lt_add'] using h₂.2

Premises used: Iff.mpr, sub_pos, sub_lt_iff_lt_add', And.right, abs_of_pos
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
q : ℚ
⊢ Eq (α := Set ℝ) (closure (Ioi (↑q : ℝ) ∩ range Rat.cast)) (closure (Ioi (↑q : ℝ)))

Tactic:
closure_ordConnected_inter_rat (ordConnected_Ioi (a := (q : ℝ))) _

Premises used: Set.ordConnected_Ioi, closure_ordConnected_inter_rat
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
q : ℚ
h : Eq (α := Set ℝ) (closure (Rat.cast '' {x : ℚ | q < x})) (closure (Ioi (↑q : ℝ) ∩ range Rat.cast))
h₁ : Eq (α := Set ℝ) {r : ℝ | (↑q : ℝ) ≤ r} (closure (Ioi (↑q : ℝ)))
convert! : Set.Nontrivial (α := ℝ) (Ioi (↑q : ℝ))
⊢ Eq (α := Set ℝ) (closure (Rat.cast '' {x : ℚ | q < x})) {r : ℝ | (↑q : ℝ) ≤ r}

Tactic:
convert! closure_ordConnected_inter_rat (ordConnected_Ioi (a := (q : ℝ))) _ using 1

Premises used: Set.ordConnected_Ioi, closure_ordConnected_inter_rat
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
q : ℚ
h : Eq (α := Set ℝ) (Rat.cast '' {x : ℚ | q < x}) (Ioi (↑q : ℝ) ∩ range Rat.cast)
⊢ Eq (α := Set ℝ) (closure (Rat.cast '' {x : ℚ | q < x})) (closure (Ioi (↑q : ℝ) ∩ range Rat.cast))

Tactic:
congr!
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
q : ℚ
⊢ Eq (α := Set ℝ) (Rat.cast '' {x : ℚ | q < x}) (Ioi (↑q : ℝ) ∩ range Rat.cast)

Tactic:
aesop
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
q : ℚ
⊢ Eq (α := Set ℝ) {r : ℝ | (↑q : ℝ) ≤ r} (closure (Ioi (↑q : ℝ)))

Tactic:
(closure_Ioi _).symm

Premises used: Set.Ici, setOf, Eq.symm, closure_Ioi
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
q : ℚ
⊢ Eq (α := Set ℝ) {r : ℝ | (↑q : ℝ) ≤ r} (closure (Ioi (↑q : ℝ)))

Tactic:
exact (closure_Ioi _).symm

Premises used: Eq.symm, closure_Ioi
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
q : ℚ
linarith : HAdd.hAdd (α := ℝ) (↑q : ℝ) 1 ≤ (↑q : ℝ) → -1 + (HAdd.hAdd (α := ℝ) (↑q : ℝ) 1 - (↑q : ℝ)) = 0
⊢ (↑q : ℝ) < HAdd.hAdd (α := ℝ) (↑q : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
q : ℚ
linarith :
  HAdd.hAdd (α := ℝ) (↑q : ℝ) 2 ≤ (↑q : ℝ) → HMul.hMul (α := ℝ) 2 (-1) + (HAdd.hAdd (α := ℝ) (↑q : ℝ) 2 - (↑q : ℝ)) = 0
linarith₁ : HAdd.hAdd (α := ℝ) (↑q : ℝ) 2 ≤ (↑q : ℝ) → GT.gt (α := ℝ) 2 0
⊢ (↑q : ℝ) < HAdd.hAdd (α := ℝ) (↑q : ℝ) 2

Tactic:
linarith
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
q : ℚ
⊢ HAdd.hAdd (α := ℝ) (↑q : ℝ) 1 ≠ HAdd.hAdd (α := ℝ) (↑q : ℝ) 2

Tactic:
simp
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
q : ℚ
⊢ Set.Nontrivial (α := ℝ) (Ioi (↑q : ℝ))

Tactic:
exact ⟨q + 1, show (q : ℝ) < _ by linarith, q + 2, show (q : ℝ) < _ by linarith, by simp⟩
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
α : Type u
inst : TopologicalSpace α
f : ℝ → α
c : ℝ
hp : Periodic f c
hc : c ≠ 0
hf : Continuous[_, inst] f
rw : IsCompact (f '' [[0, 0 + c]])
⊢ IsCompact (range f)

Tactic:
rw [← hp.image_uIcc hc 0]

Premises used: Function.Periodic.image_uIcc, OfNat.ofNat
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
α : Type u
inst : TopologicalSpace α
f : ℝ → α
c : ℝ
hp : Periodic f c
hc : c ≠ 0
hf : Continuous[_, inst] f
⊢ IsCompact (f '' [[0, 0 + c]])

Tactic:
isCompact_uIcc.image hf

Premises used: isCompact_uIcc, IsCompact.image
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
α : Type u
inst : TopologicalSpace α
f : ℝ → α
c : ℝ
hp : Periodic f c
hc : c ≠ 0
hf : Continuous[_, inst] f
⊢ IsCompact (f '' [[0, 0 + c]])

Tactic:
exact isCompact_uIcc.image hf

Premises used: isCompact_uIcc, IsCompact.image
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
α : Type u
inst : PseudoMetricSpace α
f : ℝ → α
c : ℝ
hp : Periodic f c
hc : c ≠ 0
hf : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
⊢ Bornology.IsBounded (range f)

Tactic:
(hp.compact_of_continuous hc hf).isBounded

Premises used: IsCompact.isBounded, Function.Periodic.compact_of_continuous
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (f '' Ici k)
⊢ BddAbove (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))

Tactic:
rw [← range_add_eq_image_Ici] at h_bdd

Premises used: Set.range_add_eq_image_Ici
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
⊢ Monotone (β := ℝ) fun (n : ℕ) ↦ f (n + k)

Tactic:
rw [Ici, ← monotone_add_nat_iff_monotoneOn_nat_Ici] at h_mon

Premises used: Set.Ici, monotone_add_nat_iff_monotoneOn_nat_Ici
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
h_mon₁ : Monotone (β := ℝ) fun (n : ℕ) ↦ f (n + k)
⊢ BddAbove (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))

Tactic:
rw [Ici, ← monotone_add_nat_iff_monotoneOn_nat_Ici] at h_mon

Premises used: Set.Ici, monotone_add_nat_iff_monotoneOn_nat_Ici
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
h_mon : Monotone (β := ℝ) fun (n : ℕ) ↦ f (n + k)
h_bdd : BddAbove (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
rw : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (n + k)) atTop (𝓝 (⨆ (x : ℕ), f (x + k)))
⊢ Tendsto f atTop (𝓝 (sSup (f '' Ici k)))

Tactic:
rw [← tendsto_add_atTop_iff_nat k, ← range_add_eq_image_Ici, sSup_range]

Premises used: Set.range_add_eq_image_Ici, Filter.tendsto_add_atTop_iff_nat, sSup_range
-- Module: Mathlib.Topology.Instances.Real.Lemmas
Goal:
f : ℕ → ℝ
k : ℕ
h_mon : Monotone (β := ℝ) fun (n : ℕ) ↦ f (n + k)
h_bdd : BddAbove (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (n + k)) atTop (𝓝 (⨆ (x : ℕ), f (x + k)))

Tactic:
tendsto_atTop_ciSup h_mon h_bdd

Premises used: tendsto_atTop_ciSup