awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
⊢ ∃ (i : ℕ) (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} i),
    Membership.mem (γ := Set α) {x : α | (x, s i) ∈ a} (s m)
have inl : ∀ (hm : m ≤ n),
  ∃ (i : ℕ) (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} i),
    Membership.mem (γ := Set α) {x : α | (x, s i) ∈ a} (s m)
Tactic: rcases le_total m n with hm | hm
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
s : ℕ → α
hs : CauchySeq s
a : Set (α × α)
ha : a ∈ 𝓤 α
n : ℕ
hn : ∀ k ≥ n, ∀ l ≥ n, (s k, s l) ∈ a
m : ℕ
inl :
  ∀ (hm : m ≤ n),
    ∃ (i : ℕ) (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} i),
      Membership.mem (γ := Set α) {x : α | (x, s i) ∈ a} (s m)
⊢ ∃ (i : ℕ) (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} i),
    Membership.mem (γ := Set α) {x : α | (x, s i) ∈ a} (s m)
have inr : ∀ (hm : n ≤ m),
  ∃ (i : ℕ) (_ : Membership.mem (γ := Set ℕ) {k : ℕ | k ≤ n} i),
    Membership.mem (γ := Set α) {x : α | (x, s i) ∈ a} (s m)
Tactic: rcases le_total m n with hm | hm
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (interUnionBalls xs u U)
have rw : ∀ (i : ℕ), p i → ∃ (t : Set α), t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U i}
Tactic: rw [Filter.HasBasis.totallyBounded_iff H]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
h : p i
⊢ ∃ (t : Set α), t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U i}
have h_subset : interUnionBalls xs u U ⊆ ⋃ (m : ℕ), ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
Tactic: have h_subset : interUnionBalls xs u U
      ⊆ ⋃ m ≤ u i, UniformSpace.ball (xs m) (Prod.swap ⁻¹' U i) :=
    fun x hx ↦ Set.mem_iInter.1 hx i
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
h : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ (m : ℕ), ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
⊢ ∃ (t : Set α), t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U i}
have refine : ∀ (x : α) (hx : x ∈ interUnionBalls xs u U),
  Membership.mem (γ := Set α) (⋃ y ∈ (↑(Finset.image xs (Finset.range (u i + 1))) : Set α), {x : α | (x, y) ∈ U i}) x
Tactic: refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
h : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ (m : ℕ), ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
x : α
hx : x ∈ interUnionBalls xs u U
⊢ Membership.mem (γ := Set α) (⋃ y ∈ (↑(Finset.image xs (Finset.range (u i + 1))) : Set α), {x : α | (x, y) ∈ U i}) x
have simp : Membership.mem (γ := Set α) (⋃ (y : ℕ), ⋃ (_ : y ≤ u i), {x : α | (x, xs y) ∈ U i}) x
Tactic: simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
    iUnion_iUnion_eq_right, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
h : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ (m : ℕ), ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
⊢ ∃ (t : Set α), t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U i}
have refine : ∀ (x : α) (hx : x ∈ interUnionBalls xs u U),
  Membership.mem (γ := Set α) (⋃ y ∈ (↑(Finset.image xs (Finset.range (u i + 1))) : Set α), {x : α | (x, y) ∈ U i}) x
Tactic: classical
  refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
  simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
    iUnion_iUnion_eq_right, Nat.lt_succ_iff]
  exact h_subset hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
i : ℕ
h : p i
h_subset : interUnionBalls xs u U ⊆ ⋃ (m : ℕ), ⋃ (_ : m ≤ u i), ball (xs m) (Prod.swap ⁻¹' U i)
refine :
  ∀ (x : α) (hx : x ∈ interUnionBalls xs u U),
    Membership.mem (γ := Set α) (⋃ y ∈ (↑(Finset.image xs (Finset.range (u i + 1))) : Set α), {x : α | (x, y) ∈ U i}) x
⊢ ∃ (t : Set α), t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ U i}
have refine₁ : ∀ (x : α) (hx : x ∈ interUnionBalls xs u U),
  Membership.mem (γ := Set α) (⋃ (y : ℕ), ⋃ (_ : y ≤ u i), {x : α | (x, xs y) ∈ U i}) x
Tactic: classical
  refine ⟨Finset.image xs (Finset.range (u i + 1)), Finset.finite_toSet _, fun x hx ↦ ?_⟩
  simp only [Finset.coe_image, Finset.coe_range, mem_image, mem_Iio, iUnion_exists, biUnion_and',
    iUnion_iUnion_eq_right, Nat.lt_succ_iff]
  exact h_subset hx
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
inst : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
⊢ IsCompact (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U))
have rw : TotallyBounded (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U)) ∧
  IsComplete (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U))
Tactic: rw [isCompact_iff_totallyBounded_isComplete]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
inst : CompleteSpace α
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U)) ∧
    IsComplete (closure[uniformSpace.toTopologicalSpace] (interUnionBalls xs u U))
have refine : TotallyBounded (interUnionBalls xs u U)
Tactic: refine ⟨TotallyBounded.closure ?_, isClosed_closure.isComplete⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf (U := U) U_mem m ×ˢ setSeq hf (U := U) U_mem n
⊢ p ∈ U N
have refine_1 : p.1 ∈ (↑(setSeqAux hf (U := U) U_mem N) : Set α)
Tactic: refine (setSeqAux hf U_mem N).2.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf (U := U) U_mem m ×ˢ setSeq hf (U := U) U_mem n
refine_1 : p.1 ∈ (↑(setSeqAux hf (U := U) U_mem N) : Set α)
⊢ p ∈ U N
have refine_2 : p.2 ∈ (↑(setSeqAux hf (U := U) U_mem N) : Set α)
Tactic: refine (setSeqAux hf U_mem N).2.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf (U := U) U_mem m ×ˢ setSeq hf (U := U) U_mem n
⊢ p.1 ∈ (↑(setSeqAux hf (U := U) U_mem N) : Set α)
have refine_1 : p.1 ∈ setSeq hf (U := U) U_mem N
Tactic: apply setSeq_sub_aux
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf (U := U) U_mem m ×ˢ setSeq hf (U := U) U_mem n
⊢ p.2 ∈ (↑(setSeqAux hf (U := U) U_mem N) : Set α)
have refine_2 : p.2 ∈ setSeq hf (U := U) U_mem N
Tactic: apply setSeq_sub_aux
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
a : α
ha : Tendsto (seq hf (U := U) U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (a, y) ∈ s ∧ y ∈ t
have rcases : ∀ (m : ℕ) (hm : U m ⊆ s), ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (a, y) ∈ s ∧ y ∈ t
Tactic: rcases U_le s hs with ⟨m, hm⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
a : α
ha : Tendsto (seq hf (U := U) U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (a, y) ∈ s ∧ y ∈ t
have rcases : ∀ (n : ℕ) (hn : ∀ b ≥ n, Membership.mem (γ := Set α) {y : α | (a, y) ∈ U m} (seq hf (U := U) U_mem b)),
  ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (a, y) ∈ s ∧ y ∈ t
Tactic: rcases tendsto_atTop'.1 ha _ (mem_nhds_left a (U_mem m)) with ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
a : α
ha : Tendsto (seq hf (U := U) U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ b ≥ n, Membership.mem (γ := Set α) {y : α | (a, y) ∈ U m} (seq hf (U := U) U_mem b)
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (a, y) ∈ s ∧ y ∈ t
have refine_1 : setSeq hf (U := U) U_mem (max m n) ×ˢ setSeq hf (U := U) U_mem (max m n) ⊆ s
Tactic: refine
        ⟨setSeq hf U_mem (max m n), setSeq_mem hf U_mem _, ?_, seq hf U_mem (max m n), ?_,
          seq_mem hf U_mem _⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
a : α
ha : Tendsto (seq hf (U := U) U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ b ≥ n, Membership.mem (γ := Set α) {y : α | (a, y) ∈ U m} (seq hf (U := U) U_mem b)
refine_1 : setSeq hf (U := U) U_mem (max m n) ×ˢ setSeq hf (U := U) U_mem (max m n) ⊆ s
⊢ ∃ t ∈ f, t ×ˢ t ⊆ s ∧ ∃ (y : α), (a, y) ∈ s ∧ y ∈ t
have refine_2 : (a, seq hf (U := U) U_mem (max m n)) ∈ s
Tactic: refine
        ⟨setSeq hf U_mem (max m n), setSeq_mem hf U_mem _, ?_, seq hf U_mem (max m n), ?_,
          seq_mem hf U_mem _⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
U_le : ∀ s ∈ 𝓤 α, ∃ (n : ℕ), U n ⊆ s
a : α
ha : Tendsto (seq hf (U := U) U_mem) atTop (𝓝 a)
s : Set (α × α)
hs : s ∈ 𝓤 α
m : ℕ
hm : U m ⊆ s
n : ℕ
hn : ∀ b ≥ n, Membership.mem (γ := Set α) {y : α | (a, y) ∈ U m} (seq hf (U := U) U_mem b)
⊢ setSeq hf (U := U) U_mem (max m n) ×ˢ setSeq hf (U := U) U_mem (max m n) ⊆ s
have this : m ≤ max m n
Tactic: have := le_max_left m n
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Tendsto u atTop (𝓝 a)
⊢ CompleteSpace α
have obtain : ∀ (U' : ℕ → Set (α × α)) (hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ (i : ℕ), U' i ⊆ s), CompleteSpace α
Tactic: obtain ⟨U', -, hU'⟩ := (𝓤 α).exists_antitone_seq
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ (i : ℕ), U' i ⊆ s
⊢ CompleteSpace α
have Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
Tactic: have Hmem : ∀ n, U n ∩ U' n ∈ 𝓤 α := fun n => inter_mem (U_mem n) (hU'.2 ⟨n, Subset.refl _⟩)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ (i : ℕ), U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
⊢ CompleteSpace α
have refine_1 : ∀ {f : Filter α} (hf : Cauchy f) (N m n : ℕ) (hm : N ≤ m) (hn : N ≤ n),
  (SequentiallyComplete.seq hf (U := fun (n : ℕ) ↦ U n ∩ U' n) Hmem m,
      SequentiallyComplete.seq hf (U := fun (n : ℕ) ↦ U n ∩ U' n) Hmem n) ∈
    U N
Tactic: refine ⟨fun hf => (HU (seq hf Hmem) fun N m n hm hn => ?_).imp <|
    le_nhds_of_seq_tendsto_nhds _ _ fun s hs => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ (i : ℕ), U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
refine_1 :
  ∀ {f : Filter α} (hf : Cauchy f) (N m n : ℕ) (hm : N ≤ m) (hn : N ≤ n),
    (SequentiallyComplete.seq hf (U := fun (n : ℕ) ↦ U n ∩ U' n) Hmem m,
        SequentiallyComplete.seq hf (U := fun (n : ℕ) ↦ U n ∩ U' n) Hmem n) ∈
      U N
⊢ CompleteSpace α
have refine_2 : ∀ {f : Filter α} (hf : Cauchy f) (s : Set (α × α)) (hs : s ∈ 𝓤 α), ∃ (n : ℕ), U n ∩ U' n ⊆ s
Tactic: refine ⟨fun hf => (HU (seq hf Hmem) fun N m n hm hn => ?_).imp <|
    le_nhds_of_seq_tendsto_nhds _ _ fun s hs => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ (a : α), Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ (i : ℕ), U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f : Filter α
hf : Cauchy f
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ (n : ℕ), U n ∩ U' n ⊆ s
have refine_2 : ∀ (N : ℕ) (hN : U' N ⊆ s), ∃ (n : ℕ), U n ∩ U' n ⊆ s
Tactic: rcases hU'.1 hs with ⟨N, hN⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
a : α
⊢ (𝓝 a).IsCountablyGenerated
have rw : (Filter.comap (Prod.mk a) (𝓤 α)).IsCountablyGenerated
Tactic: rw [nhds_eq_comap_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
⊢ SecondCountableTopology α
have rcases : ∀ (s : Set α) (hsc : s.Countable) (hsd : Dense s), SecondCountableTopology α
Tactic: rcases exists_countable_dense α with ⟨s, hsc, hsd⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
⊢ SecondCountableTopology α
have ℕ : ∀ (t : ℕ → SetRel α α) (hto : ∀ (i : ℕ), t i ∈ (𝓤 α).sets ∧ IsOpen[instTopologicalSpaceProd] (t i) ∧ (t i).IsSymm)
  (h_basis : (𝓤 α).HasAntitoneBasis t), SecondCountableTopology α
Tactic: obtain
    ⟨t : ℕ → SetRel α α, hto : ∀ i : ℕ, t i ∈ (𝓤 α).sets ∧ IsOpen (t i) ∧ (t i).IsSymm,
      h_basis : (𝓤 α).HasAntitoneBasis t⟩ :=
    (@uniformity_hasBasis_open_symmetric α _).exists_antitone_subbasis
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
hto : ∀ (i : ℕ), t i ∈ (𝓤 α).sets ∧ IsOpen[instTopologicalSpaceProd] (t i) ∧ (t i).IsSymm
h_basis : (𝓤 α).HasAntitoneBasis t
⊢ SecondCountableTopology α
have ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
Tactic: choose ht_mem hto hts using hto
Cleared hypotheses: hto
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
hto : ∀ (i : ℕ), t i ∈ (𝓤 α).sets ∧ IsOpen[instTopologicalSpaceProd] (t i) ∧ (t i).IsSymm
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
⊢ SecondCountableTopology α
have hto₁ : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
Tactic: choose ht_mem hto hts using hto
Cleared hypotheses: hto
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (hypothesis)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
hto : ∀ (i : ℕ), t i ∈ (𝓤 α).sets ∧ IsOpen[instTopologicalSpaceProd] (t i) ∧ (t i).IsSymm
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto₁ : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
⊢ SecondCountableTopology α
have hts : ∀ (i : ℕ), (t i).IsSymm
Tactic: choose ht_mem hto hts using hto
Cleared hypotheses: hto
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ SecondCountableTopology α
have refine : Eq.{u + 1} (α := TopologicalSpace α) toTopologicalSpace (generateFrom (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)))
Tactic: refine ⟨⟨⋃ x ∈ s, range fun k => ball x (t k), hsc.biUnion fun x _ => countable_range _, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ Eq.{u + 1} (α := TopologicalSpace α) toTopologicalSpace (generateFrom (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)))
have refine_1 : ∀ (u : Set α),
  Membership.mem (γ := Set (Set α)) (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)) u →
    IsOpen[uniformSpace.toTopologicalSpace] u
Tactic: refine (isTopologicalBasis_of_isOpen_of_nhds ?_ ?_).eq_generateFrom
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
refine_1 :
  ∀ (u : Set α),
    Membership.mem (γ := Set (Set α)) (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)) u →
      IsOpen[uniformSpace.toTopologicalSpace] u
⊢ Eq.{u + 1} (α := TopologicalSpace α) toTopologicalSpace (generateFrom (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)))
have refine_2 : ∀ (a : α) (u : Set α),
  a ∈ u →
    IsOpen[uniformSpace.toTopologicalSpace] u →
      ∃ (v : Set α), Membership.mem (γ := Set (Set α)) (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)) v ∧ a ∈ v ∧ v ⊆ u
Tactic: refine (isTopologicalBasis_of_isOpen_of_nhds ?_ ?_).eq_generateFrom
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ ∀ (u : Set α),
    Membership.mem (γ := Set (Set α)) (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)) u →
      IsOpen[uniformSpace.toTopologicalSpace] u
have refine_1 : ∀ (u : Set α), (∃ (i : α) (_ : i ∈ s) (y : ℕ), ball i (t y) = u) → IsOpen[uniformSpace.toTopologicalSpace] u
Tactic: simp only [mem_iUnion₂, mem_range]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
⊢ ∃ (v : Set α), Membership.mem (γ := Set (Set α)) (⋃ x ∈ s, range fun (k : ℕ) ↦ ball x (t k)) v ∧ x ∈ v ∧ v ⊆ V
have refine_2 : ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
Tactic: simp only [mem_iUnion₂, mem_range, exists_prop]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
⊢ ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
have refine_2 : ∀ (U : Set (α × α)) (hU : U ∈ 𝓤 α) (hUV : ball x U ⊆ V),
  ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
Tactic: rcases UniformSpace.mem_nhds_iff.1 (IsOpen.mem_nhds hVo hxV) with ⟨U, hU, hUV⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
⊢ ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
have refine_2 : ∀ (U' : Set (α × α)) (hU' : U' ∈ 𝓤 α),
  (∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U') →
    ∀ (hUU' : U' ○ U' ⊆ U), ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
Tactic: rcases comp_symm_of_uniformity hU with ⟨U', hU', _, hUU'⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Cauchy (goal)
Goal:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst : (𝓤 α).IsCountablyGenerated
inst_1 : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
U : Set (α × α)
hU : U ∈ 𝓤 α
hUV : ball x U ⊆ V
U' : Set (α × α)
hU' : U' ∈ 𝓤 α
left : ∀ {a b : α}, (a, b) ∈ U' → (b, a) ∈ U'
hUU' : U' ○ U' ⊆ U
⊢ ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
have refine_2 : ∀ (k : ℕ) (hk : t k ⊆ U'), ∃ (v : Set α), (∃ i ∈ s, ∃ (y : ℕ), ball i (t y) = v) ∧ x ∈ v ∧ v ⊆ V
Tactic: rcases h_basis.toHasBasis.mem_iff.1 hU' with ⟨k, -, hk⟩