awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
α : Type u_3
f : α → ℝ≥0
hf : Summable f
⊢ Tendsto f cofinite (𝓝 0)
have simp : ∀ (hf : Summable (α := ℝ) fun (a : α) ↦ (↑(f a) : ℝ)), Tendsto (fun (a : α) ↦ (↑(f a) : ℝ)) cofinite (𝓝 (↑0 : ℝ))
Tactic: simp only [← summable_coe, ← tendsto_coe] at hf ⊢
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
f : ℕ → ℝ≥0
hf : Summable f
⊢ Tendsto f atTop (𝓝 0)
have rw : Tendsto f cofinite (𝓝 0)
Tactic: rw [← Nat.cofinite_eq_atTop]
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
α : Type u_3
f : α → ℝ≥0
⊢ Tendsto (β := ℝ≥0) (fun (s : Finset α) ↦ ∑' (b : { x : α // x ∉ s }), f (↑b : α)) atTop (𝓝 0)
have simp_rw : Tendsto (β := ℝ) (fun (a : Finset α) ↦ ∑' (a_1 : { x : α // x ∉ a }), (↑(f (↑a_1 : α)) : ℝ)) atTop (𝓝 0)
Tactic: simp_rw [← tendsto_coe, coe_tsum, NNReal.coe_zero]
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ≥0
n : ℕ
⊢ HPow.hPow (α := ℝ≥0) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
have pos : ∀ (hn : n = 0), HPow.hPow (α := ℝ≥0) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ≥0
n : ℕ
pos : ∀ (hn : n = 0), HPow.hPow (α := ℝ≥0) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
⊢ HPow.hPow (α := ℝ≥0) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
have neg : ∀ (hn : ¬n = 0), HPow.hPow (α := ℝ≥0) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
ι : Sort u_1
n_1 n : ℕ
hn : n ≠ 0
⊢ Eq (α := WithTop NNReal → WithTop NNReal) (fun (x : WithTop NNReal) ↦ x ^ n)
    (⇑(NNReal.powOrderIso n hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal)
have zero : ∀ (hn : Ne (α := ℕ) 0 0),
  Eq (α := WithTop NNReal → WithTop NNReal) (fun (x : WithTop NNReal) ↦ HPow.hPow (β := ℕ) x 0)
    (⇑(NNReal.powOrderIso 0 hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal)
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
ι : Sort u_1
n_1 n : ℕ
hn : n ≠ 0
zero :
  ∀ (hn : Ne (α := ℕ) 0 0),
    Eq (α := WithTop NNReal → WithTop NNReal) (fun (x : WithTop NNReal) ↦ HPow.hPow (β := ℕ) x 0)
      (⇑(NNReal.powOrderIso 0 hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal)
⊢ Eq (α := WithTop NNReal → WithTop NNReal) (fun (x : WithTop NNReal) ↦ x ^ n)
    (⇑(NNReal.powOrderIso n hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal)
have succ : ∀ (n : ℕ) (hn : n + 1 ≠ 0),
  Eq (α := WithTop NNReal → WithTop NNReal) (fun (x : WithTop NNReal) ↦ x ^ (n + 1))
    (⇑(NNReal.powOrderIso (n + 1) hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal)
Tactic: cases n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
ι : Sort u_1
n n_1 : ℕ
hn : n_1 + 1 ≠ 0
⊢ Eq (α := WithTop NNReal → WithTop NNReal) (fun (x : WithTop NNReal) ↦ x ^ (n_1 + 1))
    (⇑(NNReal.powOrderIso (n_1 + 1) hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal)
have succ : HPow.hPow (α := WithTop NNReal) none (n_1 + 1) =
  ((NNReal.powOrderIso (n_1 + 1) hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal) none
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
ι : Sort u_1
n n_1 : ℕ
hn : n_1 + 1 ≠ 0
succ :
  HPow.hPow (α := WithTop NNReal) none (n_1 + 1) =
    ((NNReal.powOrderIso (n_1 + 1) hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal) none
⊢ Eq (α := WithTop NNReal → WithTop NNReal) (fun (x : WithTop NNReal) ↦ x ^ (n_1 + 1))
    (⇑(NNReal.powOrderIso (n_1 + 1) hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal)
have succ₁ : ∀ (val : NNReal),
  some val ^ (n_1 + 1) =
    ((NNReal.powOrderIso (n_1 + 1) hn).withTopCongr : (a : WithTop NNReal) → WithTop NNReal) (some val)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
⊢ HPow.hPow (α := ℝ≥0∞) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
have pos : ∀ (hn : n = 0), HPow.hPow (α := ℝ≥0∞) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ≥0∞
n : ℕ
pos : ∀ (hn : n = 0), HPow.hPow (α := ℝ≥0∞) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
⊢ HPow.hPow (α := ℝ≥0∞) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
have neg : ∀ (hn : ¬n = 0), HPow.hPow (α := ℝ≥0∞) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
ι : Sort u_1
inst : Nonempty ι
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
n : ℕ
⊢ HPow.hPow (α := ℝ) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
have lift : ∀ (f : (i : ι) → ℝ≥0),
  HPow.hPow (α := ℝ) (⨆ (i : ι), (fun (i : ι) ↦ (↑(f i) : ℝ)) i) n =
    ⨆ (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) n
Tactic: lift f to ι → ℝ≥0 using hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
⊢ HPow.hPow (α := ℝ) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
have inl : IsEmpty ι → HPow.hPow (α := ℝ) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Topology.Instances.NNReal.Lemmas (goal)
Goal:
ι : Sort u_1
n : ℕ
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
hn : n ≠ 0
inl : IsEmpty ι → HPow.hPow (α := ℝ) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
⊢ HPow.hPow (α := ℝ) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
have inr : Nonempty ι → HPow.hPow (α := ℝ) (⨆ (i : ι), f i) n = ⨆ (i : ι), f i ^ n
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Topology.Instances.Nat (goal)
Goal:
x : ℕ
r : ℝ
⊢ closedBall x r = Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊
have inl : ∀ (hr : 0 ≤ r), closedBall x r = Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊
Tactic: rcases le_or_gt 0 r with (hr | hr)
-- Lean 4 proof step from Mathlib.Topology.Instances.Nat (goal)
Goal:
x : ℕ
r : ℝ
inl : ∀ (hr : 0 ≤ r), closedBall x r = Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊
⊢ closedBall x r = Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊
have inr : ∀ (hr : r < 0), closedBall x r = Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊
Tactic: rcases le_or_gt 0 r with (hr | hr)
-- Lean 4 proof step from Mathlib.Topology.Instances.Nat (goal)
Goal:
x : ℕ
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊
have inl : 0 ≤ (↑x : ℝ) + r
Tactic: rw [← preimage_closedBall, Real.closedBall_eq_Icc, preimage_Icc]
-- Lean 4 proof step from Mathlib.Topology.Instances.Nat (goal)
Goal:
x : ℕ
r : ℝ
hr : r < 0
⊢ closedBall x r = Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊
have inr : ⌊(↑x : ℝ) + r⌋₊ < ⌈(↑x : ℝ) - r⌉₊
Tactic: rw [closedBall_eq_empty.2 hr, Icc_eq_empty_of_lt]
-- Lean 4 proof step from Mathlib.Topology.Instances.Nat (goal)
Goal:
x : ℕ
r : ℝ
hr : r < 0
⊢ (↑x : ℝ) + r ≤ (↑x : ℝ)
have linarith : (↑x : ℝ) < (↑x : ℝ) + r → r - 0 + ((↑x : ℝ) - ((↑x : ℝ) + r)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Instances.Nat (goal)
Goal:
x : ℕ
r : ℝ
hr : r < 0
⊢ floor (α := ℝ) (↑x : ℝ) < ⌈(↑x : ℝ) - r⌉₊
have rw : (↑x : ℝ) < (↑x : ℝ) - r
Tactic: rw [floor_natCast, Nat.lt_ceil]
-- Lean 4 proof step from Mathlib.Topology.Instances.Nat (goal)
Goal:
x : ℕ
r : ℝ
hr : r < 0
⊢ (↑x : ℝ) < (↑x : ℝ) - r
have linarith : (↑x : ℝ) - r ≤ (↑x : ℝ) → r - 0 + ((↑x : ℝ) - r - (↑x : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Instances.Nat (goal)
Goal:
x : ℕ
r : ℝ
hr : r < 0
⊢ ⌊(↑x : ℝ) + r⌋₊ < ⌈(↑x : ℝ) - r⌉₊
have calc : floor (α := ℝ) (↑x : ℝ) < ⌈(↑x : ℝ) - r⌉₊
Tactic: calc ⌊(x : ℝ) + r⌋₊ ≤ ⌊(x : ℝ)⌋₊ := floor_mono <| by linarith
    _ < ⌈↑x - r⌉₊ := by
      rw [floor_natCast, Nat.lt_ceil]
      linarith
-- Lean 4 proof step from Mathlib.Topology.Instances.Nat (goal)
Goal:
x : ℕ
r : ℝ
⊢ IsCompact (closedBall x r)
have rw : IsCompact (Icc ⌈(↑x : ℝ) - r⌉₊ ⌊(↑x : ℝ) + r⌋₊)
Tactic: rw [closedBall_eq_Icc]
-- Lean 4 proof step from Mathlib.Topology.Instances.PNat (goal)
Goal:
n : ℕ+
r : ℝ
⊢ IsCompact (val ⁻¹' closedBall (↑n : ℕ) r)
have rw : IsCompact (val ⁻¹' Set.Icc ⌈(↑(↑n : ℕ) : ℝ) - r⌉₊ ⌊(↑(↑n : ℕ) : ℝ) + r⌋₊)
Tactic: rw [Nat.closedBall_eq_Icc]
-- Lean 4 proof step from Mathlib.Topology.Instances.Rat (goal)
Goal:
⊢ UniformContinuous (α := ℚ × ℚ) (β := ℝ) (Rat.cast ∘ fun (p : ℚ × ℚ) ↦ p.1 + p.2)
have simp : UniformContinuous (β := ℝ) fun (x : ℚ × ℚ) ↦ HAdd.hAdd (α := ℝ) (↑x.1 : ℝ) (↑x.2 : ℝ)
Tactic: simp only [Function.comp_def, Rat.cast_add]
-- Lean 4 proof step from Mathlib.Topology.Instances.Rat (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MulAction ℚ R
inst_2 : MulAction ℚ≥0 R
inst_3 : IsScalarTower ℚ≥0 ℚ R
inst_4 : ContinuousSMul ℚ R
p : ℚ≥0 × R
| p.1 • p.2
have rw : HSMul.hSMul (α := ℚ) (↑p.1 : ℚ) p.2
Tactic: rw [← NNRat.cast_smul_eq_nnqsmul ℚ]
-- Lean 4 proof step from Mathlib.Topology.Instances.Rat (goal)
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MulAction ℚ R
inst_2 : MulAction ℚ≥0 R
inst_3 : IsScalarTower ℚ≥0 ℚ R
inst_4 : ContinuousSMul ℚ R
⊢ Continuous[instTopologicalSpaceProd, inst] fun (p : ℚ≥0 × R) ↦ p.1 • p.2
have conv : Continuous[instTopologicalSpaceProd, inst] fun (p : ℚ≥0 × R) ↦ HSMul.hSMul (α := ℚ) (↑p.1 : ℚ) p.2
Tactic: conv in _ • _ => rw [← NNRat.cast_smul_eq_nnqsmul ℚ]
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (goal)
Goal:
p : ℚ
s : Set ℚ
⊢ (cocompact ℚ ⊓ 𝓝 p).NeBot
have refine : ∀ {i : Set ℚ × Set ℚ}, IsCompact i.1 ∧ p ∈ i.2 ∧ IsOpen i.2 → (i.1ᶜ ∩ i.2).Nonempty
Tactic: refine (hasBasis_cocompact.inf (nhds_basis_opens _)).neBot_iff.2 ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (goal)
Goal:
p : ℚ
s_1 s o : Set ℚ
hs : IsCompact (s, o).1
hpo : p ∈ (s, o).2
ho : IsOpen (s, o).2
⊢ ((s, o).1ᶜ ∩ (s, o).2).Nonempty
have rw : ((s, o).2 ∩ (s, o).1ᶜ).Nonempty
Tactic: rw [inter_comm]
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (goal)
Goal:
H : (cocompact ℚ).IsCountablyGenerated
⊢ False
have rcases : ∀ (x : ℕ → ℚ) (hx : Tendsto x atTop (cocompact ℚ ⊓ 𝓝 0)), False
Tactic: rcases exists_seq_tendsto (cocompact ℚ ⊓ 𝓝 0) with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (hypothesis)
Goal:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ ⊓ 𝓝 0)
⊢ False
have hx₁ : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
Tactic: rw [tendsto_inf] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (hypothesis)
Goal:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
⊢ False
have hxc : Tendsto x atTop (cocompact ℚ)
Tactic: rcases hx with ⟨hxc, hx0⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (hypothesis)
Goal:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
hxc : Tendsto x atTop (cocompact ℚ)
⊢ False
have hx0 : Tendsto x atTop (𝓝 0)
Tactic: rcases hx with ⟨hxc, hx0⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (goal)
Goal:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hxc : Tendsto x atTop (cocompact ℚ)
hx0 : Tendsto x atTop (𝓝 0)
⊢ False
have obtain : ∀ (n : ℕ) (hn : x n ∉ insert 0 (range x)), False
Tactic: obtain ⟨n, hn⟩ : ∃ n : ℕ, x n ∉ insert (0 : ℚ) (range x) :=
    (hxc.eventually hx0.isCompact_insert_range.compl_mem_cocompact).exists
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (hypothesis)
Goal:
h : IsCountablyGenerated (α := ℚ∞) (𝓝 ∞)
⊢ False
have this : IsCountablyGenerated (α := ℚ) (comap OnePoint.some (𝓝 ∞))
Tactic: have : IsCountablyGenerated (comap (OnePoint.some : ℚ → ℚ∞) (𝓝 ∞)) := by infer_instance
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (hypothesis)
Goal:
h : IsCountablyGenerated (α := ℚ∞) (𝓝 ∞)
this : IsCountablyGenerated (α := ℚ) (comap OnePoint.some (𝓝 ∞))
⊢ False
have this₁ : (cocompact ℚ).IsCountablyGenerated
Tactic: rw [OnePoint.comap_coe_nhds_infty, coclosedCompact_eq_cocompact] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (goal)
Goal:
⊢ TotallyDisconnectedSpace ℚ
have refine : ∀ (s : Set ℚ) (hsu : s ⊆ univ) (hs : IsPreconnected s) (x : ℚ) (hx : x ∈ s) (y : ℚ) (hy : y ∈ s), x = y
Tactic: refine ⟨fun s hsu hs x hx y hy => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (goal)
Goal:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
⊢ x = y
have by_contra : ∀ (H : x ≠ y), False
Tactic: by_contra H : x ≠ y
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (goal)
Goal:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
⊢ False
have 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
Tactic: wlog hlt : x < y
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (goal)
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
⊢ False
have wlog : ∀ (s : Set ℚ) (hs : IsPreconnected s) (x : ℚ) (hx : x ∈ s) (y : ℚ) (hy : y ∈ s) (H : x ≠ y) (hlt : x < y), False
Tactic: wlog hlt : x < y
Cleared hypotheses: s, hs, x, hx, y, hy, H
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (goal)
Goal:
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
⊢ False
have rcases : ∀ (z : ℝ) (hz : Irrational z) (hxz : (↑x : ℝ) < z) (hzy : z < (↑y : ℝ)), False
Tactic: rcases exists_irrational_btwn (Rat.cast_lt.2 hlt) with ⟨z, hz, hxz, hzy⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (hypothesis)
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 : ℝ)
⊢ False
have this : IsPreconnected (α := ℝ) (Rat.cast '' s)
Tactic: have := hs.image _ continuous_coe_real.continuousOn
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (hypothesis)
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)
⊢ False
have this₁ : OrdConnected (α := ℝ) (Rat.cast '' s)
Tactic: rw [isPreconnected_iff_ordConnected] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Instances.RatLemmas (hypothesis)
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)
⊢ False
have this₁ : 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⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
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
⊢ Membership.mem (γ := Set (Set ℝ)) (⋃ (a : ℚ), ⋃ (b : ℚ), ⋃ (_ : a < b), {Ioo (↑a : ℝ) (↑b : ℝ)})
    (Ioo (↑q : ℝ) (↑p : ℝ))
have simp : ∃ (i : ℚ) (i_1 : ℚ) (_ : i < i_1), Membership.mem (γ := Set (Set ℝ)) {Ioo (↑i : ℝ) (↑i_1 : ℝ)} (Ioo (↑q : ℝ) (↑p : ℝ))
Tactic: simp only [mem_iUnion]
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
x ε : ℝ
⊢ TotallyBounded (ball x ε)
have rw : TotallyBounded (Ioo (x - ε) (x + ε))
Tactic: rw [Real.ball_eq_Ioo]
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
K : Subfield ℝ
hc : IsClosed (↑K : Set ℝ)
⊢ K = ⊤
have rw : closure (↑K : Set ℝ) = univ
Tactic: rw [SetLike.ext'_iff, Subfield.coe_top, ← hc.closure_eq]
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
K : Subfield ℝ
hc : IsClosed (↑K : Set ℝ)
⊢ closure (↑K : Set ℝ) = univ
have refine : range Rat.cast ⊆ (↑K : Set ℝ)
Tactic: refine Rat.denseRange_cast.mono ?_ |>.closure_eq
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
s : Set ℝ
conn : s.OrdConnected
nt : s.Nontrivial
x : ℝ
hx : x ∈ s
ε : ℝ
ε_pos : ε > 0
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
have have : ∀ (z : ℝ) (hz : z ∈ s) (ne : z ≠ x), ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
Tactic: have ⟨z, hz, ne⟩ := nt.exists_ne x
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
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| < ε
have refine_1 : ∀ (lt : z < x), ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
Tactic: refine ne.lt_or_gt.elim (fun lt ↦ ?_) fun lt ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
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| < ε
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
have refine_2 : ∀ (lt : x < z), ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
Tactic: refine ne.lt_or_gt.elim (fun lt ↦ ?_) fun lt ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
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
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
have refine_1 : ∀ (q : ℚ) (h₁ : max z (x - ε) < (↑q : ℝ)) (h₂ : (↑q : ℝ) < x), ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
Tactic: have ⟨q, h₁, h₂⟩ := exists_rat_btwn (max_lt lt (sub_lt_self x ε_pos))
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (hypothesis)
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
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
have h₃ : z < (↑q : ℝ) ∧ x - ε < (↑q : ℝ)
Tactic: rw [max_lt_iff] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
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| < ε
have refine_1 : |(↑q : ℝ) - x| < ε
Tactic: refine ⟨q, ⟨conn.out hz hx ⟨h₁.1.le, h₂.le⟩, q, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
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
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
have refine_2 : ∀ (q : ℚ) (h₁ : x < (↑q : ℝ)) (h₂ : (↑q : ℝ) < min z (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))
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (hypothesis)
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 + ε)
⊢ ∃ y ∈ s ∩ range Rat.cast, |y - x| < ε
have h₃ : (↑q : ℝ) < z ∧ (↑q : ℝ) < x + ε
Tactic: rw [lt_min_iff] at h₂
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
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| < ε
have refine_2 : |(↑q : ℝ) - x| < ε
Tactic: refine ⟨q, ⟨conn.out hx hz ⟨h₁.le, h₂.1.le⟩, q, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
q : ℚ
⊢ Eq (α := Set ℝ) (closure (Rat.cast '' {x : ℚ | q < x})) {r : ℝ | (↑q : ℝ) ≤ r}
have h : Eq (α := Set ℝ) (closure (Rat.cast '' {x : ℚ | q < x})) (closure (Ioi (↑q : ℝ) ∩ range Rat.cast))
Tactic: convert! closure_ordConnected_inter_rat (ordConnected_Ioi (a := (q : ℝ))) _ using 1
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
q : ℚ
h : Eq (α := Set ℝ) (closure (Rat.cast '' {x : ℚ | q < x})) (closure (Ioi (↑q : ℝ) ∩ range Rat.cast))
⊢ Eq (α := Set ℝ) (closure (Rat.cast '' {x : ℚ | q < x})) {r : ℝ | (↑q : ℝ) ≤ r}
have h₁ : Eq (α := Set ℝ) {r : ℝ | (↑q : ℝ) ≤ r} (closure (Ioi (↑q : ℝ)))
Tactic: convert! closure_ordConnected_inter_rat (ordConnected_Ioi (a := (q : ℝ))) _ using 1
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
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 : ℝ)))
⊢ Eq (α := Set ℝ) (closure (Rat.cast '' {x : ℚ | q < x})) {r : ℝ | (↑q : ℝ) ≤ r}
have convert! : Set.Nontrivial (α := ℝ) (Ioi (↑q : ℝ))
Tactic: convert! closure_ordConnected_inter_rat (ordConnected_Ioi (a := (q : ℝ))) _ using 1
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
q : ℚ
⊢ Eq (α := Set ℝ) (closure (Rat.cast '' {x : ℚ | q < x})) (closure (Ioi (↑q : ℝ) ∩ range Rat.cast))
have h : Eq (α := Set ℝ) (Rat.cast '' {x : ℚ | q < x}) (Ioi (↑q : ℝ) ∩ range Rat.cast)
Tactic: congr!
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
q : ℚ
⊢ (↑q : ℝ) < HAdd.hAdd (α := ℝ) (↑q : ℝ) 1
have linarith : HAdd.hAdd (α := ℝ) (↑q : ℝ) 1 ≤ (↑q : ℝ) → -1 + (HAdd.hAdd (α := ℝ) (↑q : ℝ) 1 - (↑q : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
q : ℚ
⊢ (↑q : ℝ) < HAdd.hAdd (α := ℝ) (↑q : ℝ) 2
have linarith : HAdd.hAdd (α := ℝ) (↑q : ℝ) 2 ≤ (↑q : ℝ) → HMul.hMul (α := ℝ) 2 (-1) + (HAdd.hAdd (α := ℝ) (↑q : ℝ) 2 - (↑q : ℝ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
q : ℚ
linarith :
  HAdd.hAdd (α := ℝ) (↑q : ℝ) 2 ≤ (↑q : ℝ) → HMul.hMul (α := ℝ) 2 (-1) + (HAdd.hAdd (α := ℝ) (↑q : ℝ) 2 - (↑q : ℝ)) = 0
⊢ (↑q : ℝ) < HAdd.hAdd (α := ℝ) (↑q : ℝ) 2
have linarith₁ : HAdd.hAdd (α := ℝ) (↑q : ℝ) 2 ≤ (↑q : ℝ) → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
α : Type u
inst : TopologicalSpace α
f : ℝ → α
c : ℝ
hp : Periodic f c
hc : c ≠ 0
hf : Continuous[_, inst] f
⊢ IsCompact (range f)
have rw : IsCompact (f '' [[0, 0 + c]])
Tactic: rw [← hp.image_uIcc hc 0]
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (hypothesis)
Goal:
f : ℕ → ℝ
k : ℕ
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (f '' Ici k)
⊢ Tendsto f atTop (𝓝 (sSup (f '' Ici k)))
have h_bdd₁ : BddAbove (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
Tactic: rw [← range_add_eq_image_Ici] at h_bdd
Cleared hypotheses: h_bdd
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (hypothesis)
Goal:
f : ℕ → ℝ
k : ℕ
h_mon : MonotoneOn f (Ici k)
h_bdd : BddAbove (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sSup (f '' Ici k)))
have h_mon₁ : Monotone (β := ℝ) fun (n : ℕ) ↦ f (n + k)
Tactic: rw [Ici, ← monotone_add_nat_iff_monotoneOn_nat_Ici] at h_mon
Cleared hypotheses: h_mon, h_bdd
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (goal)
Goal:
f : ℕ → ℝ
k : ℕ
h_mon : Monotone (β := ℝ) fun (n : ℕ) ↦ f (n + k)
h_bdd : BddAbove (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
⊢ Tendsto f atTop (𝓝 (sSup (f '' Ici k)))
have rw : Tendsto (β := ℝ) (fun (n : ℕ) ↦ f (n + k)) atTop (𝓝 (⨆ (x : ℕ), f (x + k)))
Tactic: rw [← tendsto_add_atTop_iff_nat k, ← range_add_eq_image_Ici, sSup_range]
-- Lean 4 proof step from Mathlib.Topology.Instances.Real.Lemmas (hypothesis)
Goal:
f : ℕ → ℝ
k : ℕ
h_ant : AntitoneOn f (Ici k)
h_bdd : BddBelow (f '' Ici k)
⊢ Tendsto f atTop (𝓝 (sInf (f '' Ici k)))
have h_bdd₁ : BddBelow (α := ℝ) (range fun (x : ℕ) ↦ f (x + k))
Tactic: rw [← range_add_eq_image_Ici] at h_bdd
Cleared hypotheses: h_bdd