awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
⊢ IsComplete (α := C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
have intro : ∀ (l : Filter C(α, β)),
  Cauchy l →
    l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} →
      ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
Tactic: classical
  intro l hlc hlf
  rcases CompleteSpace.complete hlc with ⟨f', hf'⟩
  have := hlc.1
  have H₁ : ∀ x ∈ s, Inseparable (f x) (f' x) := fun x hx ↦ by
    refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
    refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
    exact fun _ h ↦ (h hx).symm
  have H₂ (x) : Inseparable (s.piecewise f f' x) (f' x) := by
    by_cases hx : x ∈ s <;> simp [hx, H₁, Inseparable.refl]
  set g : C(α, β) :=
    ⟨s.piecewise f f', (continuous_congr_of_inseparable H₂).mpr <| map_continuous f'⟩
  refine ⟨g, Set.piecewise_eqOn _ _ _, hf'.trans_eq ?_⟩
  rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
intro intro₁ intro₂ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
⊢ IsComplete (α := C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
have intro₃ : ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
  (hf' : l ≤ 𝓝 f'),
  ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
Tactic: classical
  intro l hlc hlf
  rcases CompleteSpace.complete hlc with ⟨f', hf'⟩
  have := hlc.1
  have H₁ : ∀ x ∈ s, Inseparable (f x) (f' x) := fun x hx ↦ by
    refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
    refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
    exact fun _ h ↦ (h hx).symm
  have H₂ (x) : Inseparable (s.piecewise f f' x) (f' x) := by
    by_cases hx : x ∈ s <;> simp [hx, H₁, Inseparable.refl]
  set g : C(α, β) :=
    ⟨s.piecewise f f', (continuous_congr_of_inseparable H₂).mpr <| map_continuous f'⟩
  refine ⟨g, Set.piecewise_eqOn _ _ _, hf'.trans_eq ?_⟩
  rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
intro intro₁ intro₂ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₃ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f'),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
⊢ IsComplete (α := C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
have intro₄ : ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
  (hf' : l ≤ 𝓝 f') (this : l.NeBot),
  ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
Tactic: classical
  intro l hlc hlf
  rcases CompleteSpace.complete hlc with ⟨f', hf'⟩
  have := hlc.1
  have H₁ : ∀ x ∈ s, Inseparable (f x) (f' x) := fun x hx ↦ by
    refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
    refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
    exact fun _ h ↦ (h hx).symm
  have H₂ (x) : Inseparable (s.piecewise f f' x) (f' x) := by
    by_cases hx : x ∈ s <;> simp [hx, H₁, Inseparable.refl]
  set g : C(α, β) :=
    ⟨s.piecewise f f', (continuous_congr_of_inseparable H₂).mpr <| map_continuous f'⟩
  refine ⟨g, Set.piecewise_eqOn _ _ _, hf'.trans_eq ?_⟩
  rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
intro intro₁ intro₂ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₃ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f'),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₄ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f') (this : l.NeBot),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
⊢ IsComplete (α := C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
have intro₅ : ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
  (hf' : l ≤ 𝓝 f') (this : l.NeBot) (H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)),
  ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
Tactic: classical
  intro l hlc hlf
  rcases CompleteSpace.complete hlc with ⟨f', hf'⟩
  have := hlc.1
  have H₁ : ∀ x ∈ s, Inseparable (f x) (f' x) := fun x hx ↦ by
    refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
    refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
    exact fun _ h ↦ (h hx).symm
  have H₂ (x) : Inseparable (s.piecewise f f' x) (f' x) := by
    by_cases hx : x ∈ s <;> simp [hx, H₁, Inseparable.refl]
  set g : C(α, β) :=
    ⟨s.piecewise f f', (continuous_congr_of_inseparable H₂).mpr <| map_continuous f'⟩
  refine ⟨g, Set.piecewise_eqOn _ _ _, hf'.trans_eq ?_⟩
  rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
intro intro₁ intro₂ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₃ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f'),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₄ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f') (this : l.NeBot),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₅ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f') (this : l.NeBot) (H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
⊢ IsComplete (α := C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
have intro₆ : ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
  (hf' : l ≤ 𝓝 f') (this : l.NeBot) (H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x))
  (H₂ : ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)),
  ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
Tactic: classical
  intro l hlc hlf
  rcases CompleteSpace.complete hlc with ⟨f', hf'⟩
  have := hlc.1
  have H₁ : ∀ x ∈ s, Inseparable (f x) (f' x) := fun x hx ↦ by
    refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
    refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
    exact fun _ h ↦ (h hx).symm
  have H₂ (x) : Inseparable (s.piecewise f f' x) (f' x) := by
    by_cases hx : x ∈ s <;> simp [hx, H₁, Inseparable.refl]
  set g : C(α, β) :=
    ⟨s.piecewise f f', (continuous_congr_of_inseparable H₂).mpr <| map_continuous f'⟩
  refine ⟨g, Set.piecewise_eqOn _ _ _, hf'.trans_eq ?_⟩
  rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
intro intro₁ intro₂ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₃ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f'),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₄ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f') (this : l.NeBot),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₅ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f') (this : l.NeBot) (H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
intro₆ intro₇ :
  ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
    (hf' : l ≤ 𝓝 f') (this : l.NeBot) (H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x))
    (H₂ : ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)),
    ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
⊢ IsComplete (α := C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
have intro₈ : ∀ (l : Filter C(α, β)) (hlc : Cauchy l) (hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (f' : C(α, β))
  (hf' : l ≤ 𝓝 f') (this : l.NeBot) (H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x))
  (H₂ : ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)),
  let g : C(α, β) := { toFun := s.piecewise (β := fun (a : α) ↦ β) f (⇑f' : (a : α) → β), continuous_toFun := sorry };
  𝓝 f' = 𝓝 g
Tactic: classical
  intro l hlc hlf
  rcases CompleteSpace.complete hlc with ⟨f', hf'⟩
  have := hlc.1
  have H₁ : ∀ x ∈ s, Inseparable (f x) (f' x) := fun x hx ↦ by
    refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
    refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
    exact fun _ h ↦ (h hx).symm
  have H₂ (x) : Inseparable (s.piecewise f f' x) (f' x) := by
    by_cases hx : x ∈ s <;> simp [hx, H₁, Inseparable.refl]
  set g : C(α, β) :=
    ⟨s.piecewise f f', (continuous_congr_of_inseparable H₂).mpr <| map_continuous f'⟩
  refine ⟨g, Set.piecewise_eqOn _ _ _, hf'.trans_eq ?_⟩
  rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompareReals (goal)
Goal:
⊢ Eq (α := UniformSpace ℚ) (AbsoluteValue.uniformSpace AbsoluteValue.abs) PseudoMetricSpace.toUniformSpace
have h : ∀ (s : Set (ℚ × ℚ)), s ∈ uniformity ℚ ↔ s ∈ uniformity ℚ
Tactic: ext s
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompareReals (goal)
Goal:
s : Set (ℚ × ℚ)
⊢ s ∈ uniformity ℚ ↔ s ∈ uniformity ℚ
have h : (∃ (i : ℚ), 0 < i ∧ {p : ℚ × ℚ | (AbsoluteValue.abs : (a : ℚ) → ℚ) (p.2 - p.1) < i} ⊆ s) ↔
  ∃ (i : ℚ), 0 < i ∧ {p : ℚ × ℚ | dist p.1 p.2 < (↑i : ℝ)} ⊆ s
Tactic: rw [(AbsoluteValue.hasBasis_uniformity _).mem_iff, Metric.uniformity_basis_dist_rat.mem_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompareReals (goal)
Goal:
⊢ IsUniformInducing (β := ℝ) Rat.cast
have rw : IsUniformInducing (β := ℝ) Rat.cast
Tactic: rw [Rat.uniformSpace_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompleteSeparated (hypothesis)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
⊢ a ∈ s
have this : Cauchy f
Tactic: have : Cauchy f := cauchy_nhds.mono' ha inf_le_left
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompleteSeparated (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
s : Set α
h : IsComplete s
a : α
ha : ClusterPt a (𝓟 s)
f : Filter α := 𝓝[s] a
this : Cauchy f
⊢ a ∈ s
have rcases : ∀ (y : α) (ys : y ∈ s) (fy : f ≤ 𝓝 y), a ∈ s
Tactic: rcases h f this inf_le_right with ⟨y, ys, fy⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
f : (s : SetRel α α) → Set (CauchyFilter α × CauchyFilter α) :=
  fun (s : SetRel α α) ↦ {p : CauchyFilter α × CauchyFilter α | s ∈ (↑p.2 : Filter α) ×ˢ (↑p.1 : Filter α)}
⊢ LE.le (α := Filter (CauchyFilter α × CauchyFilter α)) (map Prod.swap ((𝓤 α).lift' gen)) ((𝓤 α).lift' gen)
have h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
Tactic: have h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f := by
    delta gen
    simp [f, map_lift'_eq, monotone_setOf, Filter.monotone_mem, Function.comp_def,
      image_swap_eq_preimage_swap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
f : (s : SetRel α α) → Set (CauchyFilter α × CauchyFilter α) :=
  fun (s : SetRel α α) ↦ {p : CauchyFilter α × CauchyFilter α | s ∈ (↑p.2 : Filter α) ×ˢ (↑p.1 : Filter α)}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
⊢ LE.le (α := Filter (CauchyFilter α × CauchyFilter α)) ((𝓤 α).lift fun (s : Set (α × α)) ↦ (𝓟 ∘ f) (Prod.swap ⁻¹' s))
    ((𝓤 α).lift' gen)
have h : ∀ (p : CauchyFilter α × CauchyFilter α),
  (↑p.2 : Filter α) ×ˢ (↑p.1 : Filter α) = map Prod.swap ((↑p.1 : Filter α) ×ˢ (↑p.2 : Filter α))
Tactic: have h := fun p : CauchyFilter α × CauchyFilter α => @Filter.prod_comm _ _ p.2.val p.1.val
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
f : (s : SetRel α α) → Set (CauchyFilter α × CauchyFilter α) :=
  fun (s : SetRel α α) ↦ {p : CauchyFilter α × CauchyFilter α | s ∈ (↑p.2 : Filter α) ×ˢ (↑p.1 : Filter α)}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
h :
  ∀ (p : CauchyFilter α × CauchyFilter α),
    (↑p.2 : Filter α) ×ˢ (↑p.1 : Filter α) = map Prod.swap ((↑p.1 : Filter α) ×ˢ (↑p.2 : Filter α))
⊢ LE.le (α := Filter (CauchyFilter α × CauchyFilter α)) ((𝓤 α).lift fun (s : Set (α × α)) ↦ (𝓟 ∘ f) (Prod.swap ⁻¹' s))
    ((𝓤 α).lift' gen)
have simp : LE.le (α := Filter (CauchyFilter α × CauchyFilter α))
  ((𝓤 α).lift fun (s : Set (α × α)) ↦
    𝓟 {p : CauchyFilter α × CauchyFilter α | Prod.swap ⁻¹' Prod.swap ⁻¹' s ∈ (↑p.1 : Filter α) ×ˢ (↑p.2 : Filter α)})
  ((𝓤 α).lift' gen)
Tactic: simp only [Function.comp, h, mem_map, f]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
f : (s : SetRel α α) → Set (CauchyFilter α × CauchyFilter α) :=
  fun (s : SetRel α α) ↦ {p : CauchyFilter α × CauchyFilter α | s ∈ (↑p.2 : Filter α) ×ˢ (↑p.1 : Filter α)}
h₁ : map Prod.swap ((𝓤 α).lift' gen) = (𝓤 α).lift' f
⊢ LE.le (α := Filter (CauchyFilter α × CauchyFilter α)) (map Prod.swap ((𝓤 α).lift' gen)) ((𝓤 α).lift' gen)
have h₂ : (𝓤 α).lift' f ≤ (𝓤 α).lift' gen
Tactic: have h₂ : (𝓤 α).lift' f ≤ (𝓤 α).lift' gen :=
    uniformity_lift_le_swap
      (monotone_principal.comp
        (monotone_setOf fun p => @Filter.monotone_mem _ (p.2.val ×ˢ p.1.val)))
      (by
        have h := fun p : CauchyFilter α × CauchyFilter α => @Filter.prod_comm _ _ p.2.val p.1.val
        simp only [Function.comp, h, mem_map, f]
        exact le_rfl)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
⊢ Eq (α := Filter (CauchyFilter α × CauchyFilter α))
    (Filter.lift' (α := CauchyFilter α × CauchyFilter α) ((𝓤 α).lift' gen)
      fun (s : Set (CauchyFilter α × CauchyFilter α)) ↦ s ○ s)
    ((𝓤 α).lift' fun (s : Set (α × α)) ↦ gen s ○ gen s)
have hg : Monotone.{u, u} (α := Set (α × α)) (β := Set (CauchyFilter α × CauchyFilter α)) gen
Tactic: rw [lift'_lift'_assoc]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
hg : Monotone.{u, u} (α := Set (α × α)) (β := Set (CauchyFilter α × CauchyFilter α)) gen
⊢ Eq (α := Filter (CauchyFilter α × CauchyFilter α))
    (Filter.lift' (α := CauchyFilter α × CauchyFilter α) ((𝓤 α).lift' gen)
      fun (s : Set (CauchyFilter α × CauchyFilter α)) ↦ s ○ s)
    ((𝓤 α).lift' fun (s : Set (α × α)) ↦ gen s ○ gen s)
have hh : Monotone (β := Set (CauchyFilter α × CauchyFilter α)) fun (s : Set (CauchyFilter α × CauchyFilter α)) ↦ s ○ s
Tactic: rw [lift'_lift'_assoc]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
⊢ Eq (α := Filter (CauchyFilter α × CauchyFilter α)) ((𝓤 α).lift' fun (s : Set (α × α)) ↦ gen (s ○ s))
    (Filter.lift' ((𝓤 α).lift' fun (s : SetRel α α) ↦ s ○ s) gen)
have hg : Monotone (β := Set (α × α)) fun (s : SetRel α α) ↦ s ○ s
Tactic: rw [lift'_lift'_assoc]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
hg : Monotone (β := Set (α × α)) fun (s : SetRel α α) ↦ s ○ s
⊢ Eq (α := Filter (CauchyFilter α × CauchyFilter α)) ((𝓤 α).lift' fun (s : Set (α × α)) ↦ gen (s ○ s))
    (Filter.lift' ((𝓤 α).lift' fun (s : SetRel α α) ↦ s ○ s) gen)
have hh : Monotone.{u, u} (α := Set (α × α)) (β := Set (CauchyFilter α × CauchyFilter α)) gen
Tactic: rw [lift'_lift'_assoc]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
s : Set (CauchyFilter α × CauchyFilter α)
⊢ Membership.mem (γ := Filter (CauchyFilter α × CauchyFilter α)) (𝓤 (CauchyFilter α)) s ↔
    ∃ t ∈ 𝓤 α, ∀ (f g : CauchyFilter α), t ∈ (↑f : Filter α) ×ˢ (↑g : Filter α) → (f, g) ∈ s
have refine : ∀ (t : Set (α × α)) (_h : t ∈ 𝓤 α),
  gen t ⊆ s ↔ ∀ (f g : CauchyFilter α), t ∈ (↑f : Filter α) ×ˢ (↑g : Filter α) → (f, g) ∈ s
Tactic: refine mem_uniformity.trans (exists_congr (fun t => and_congr_right_iff.mpr (fun _h => ?_)))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
f : CauchyFilter α
s : Set (CauchyFilter α × CauchyFilter α)
hs : Membership.mem (γ := Filter (CauchyFilter α × CauchyFilter α)) (𝓤 (CauchyFilter α)) s
t'' : Set (α × α)
ht''₁ : t'' ∈ 𝓤 α
ht''₂ : gen t'' ⊆ s
t' : Set (α × α)
ht'₁ : t' ∈ 𝓤 α
ht'₂ : t' ○ t' ⊆ t''
this_1 : t' ∈ (↑f : Filter α) ×ˢ (↑f : Filter α)
t : Set α
ht : t ∈ (↑f : Filter α)
h : t ×ˢ t ⊆ t'
x : α
hx : x ∈ t
this : t'' ∈ SProd.sprod (β := Filter α) (↑f : Filter α) (pure x)
⊢ Membership.mem (γ := Set (CauchyFilter α × CauchyFilter α)) (gen t'') (f, pureCauchy x)
have dsimp : t'' ∈ (↑f : Filter α) ×ˢ (↑(pureCauchy x) : Filter α)
Tactic: dsimp [gen]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (hypothesis)
Goal:
α : Type u
inst : UniformSpace α
f : CauchyFilter α
⊢ Membership.mem (γ := Set (CauchyFilter α)) (closure (range pureCauchy)) f
have h_ex : ∀ (s : Set (CauchyFilter α × CauchyFilter α)),
  Membership.mem (γ := Filter (CauchyFilter α × CauchyFilter α)) (𝓤 (CauchyFilter α)) s →
    ∃ (y : α), (f, pureCauchy y) ∈ s
Tactic: have h_ex : ∀ s ∈ 𝓤 (CauchyFilter α), ∃ y : α, (f, pureCauchy y) ∈ s := fun s hs =>
    let ⟨t'', ht''₁, (ht''₂ : gen t'' ⊆ s)⟩ := (mem_lift'_sets monotone_gen).mp hs
    let ⟨t', ht'₁, ht'₂⟩ := comp_mem_uniformity_sets ht''₁
    have : t' ∈ f.val ×ˢ f.val := f.property.right ht'₁
    let ⟨t, ht, (h : t ×ˢ t ⊆ t')⟩ := mem_prod_same_iff.mp this
    let ⟨x, (hx : x ∈ t)⟩ := f.property.left.nonempty_of_mem ht
    have : t'' ∈ f.val ×ˢ pure x :=
      mem_prod_iff.mpr
        ⟨t, ht, { y : α | (x, y) ∈ t' }, h <| mk_mem_prod hx hx,
          fun ⟨a, b⟩ ⟨(h₁ : a ∈ t), (h₂ : (x, b) ∈ t')⟩ =>
          ht'₂ <| SetRel.prodMk_mem_comp (@h (a, x) ⟨h₁, hx⟩) h₂⟩
    ⟨x, ht''₂ <| by dsimp [gen]; exact this⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
f : CauchyFilter α
h_ex :
  ∀ (s : Set (CauchyFilter α × CauchyFilter α)),
    Membership.mem (γ := Filter (CauchyFilter α × CauchyFilter α)) (𝓤 (CauchyFilter α)) s →
      ∃ (y : α), (f, pureCauchy y) ∈ s
⊢ Membership.mem (γ := Set (CauchyFilter α)) (closure (range pureCauchy)) f
have simp : NeBot.{u} (α := CauchyFilter α)
  (Filter.lift' (α := CauchyFilter α × CauchyFilter α) (𝓤 (CauchyFilter α))
    fun (t : Set (CauchyFilter α × CauchyFilter α)) ↦ range pureCauchy ∩ UniformSpace.ball f t)
Tactic: simp only [closure_eq_cluster_pts, ClusterPt, nhds_eq_uniformity, lift'_inf_principal_eq,
    Set.inter_comm _ (range pureCauchy), mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
f : CauchyFilter α
h_ex :
  ∀ (s : Set (CauchyFilter α × CauchyFilter α)),
    Membership.mem (γ := Filter (CauchyFilter α × CauchyFilter α)) (𝓤 (CauchyFilter α)) s →
      ∃ (y : α), (f, pureCauchy y) ∈ s
⊢ NeBot.{u} (α := CauchyFilter α)
    (Filter.lift' (α := CauchyFilter α × CauchyFilter α) (𝓤 (CauchyFilter α))
      fun (t : Set (CauchyFilter α × CauchyFilter α)) ↦ range pureCauchy ∩ UniformSpace.ball f t)
have refine_1 : Monotone (β := Set (CauchyFilter α)) fun (t : Set (CauchyFilter α × CauchyFilter α)) ↦
  range pureCauchy ∩ UniformSpace.ball f t
Tactic: refine (lift'_neBot_iff ?_).mpr (fun s hs => ?_)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
f : CauchyFilter α
h_ex :
  ∀ (s : Set (CauchyFilter α × CauchyFilter α)),
    Membership.mem (γ := Filter (CauchyFilter α × CauchyFilter α)) (𝓤 (CauchyFilter α)) s →
      ∃ (y : α), (f, pureCauchy y) ∈ s
refine_1 :
  Monotone (β := Set (CauchyFilter α)) fun (t : Set (CauchyFilter α × CauchyFilter α)) ↦
    range pureCauchy ∩ UniformSpace.ball f t
⊢ NeBot.{u} (α := CauchyFilter α)
    (Filter.lift' (α := CauchyFilter α × CauchyFilter α) (𝓤 (CauchyFilter α))
      fun (t : Set (CauchyFilter α × CauchyFilter α)) ↦ range pureCauchy ∩ UniformSpace.ball f t)
have refine_2 : ∀ (s : Set (CauchyFilter α × CauchyFilter α))
  (hs : Membership.mem (γ := Filter (CauchyFilter α × CauchyFilter α)) (𝓤 (CauchyFilter α)) s),
  (range pureCauchy ∩ UniformSpace.ball f s).Nonempty
Tactic: refine (lift'_neBot_iff ?_).mpr (fun s hs => ?_)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Completion (goal)
Goal:
α : Type u
inst : UniformSpace α
f : CauchyFilter α
h_ex :
  ∀ (s : Set (CauchyFilter α × CauchyFilter α)),
    Membership.mem (γ := Filter (CauchyFilter α × CauchyFilter α)) (𝓤 (CauchyFilter α)) s →
      ∃ (y : α), (f, pureCauchy y) ∈ s
s : Set (CauchyFilter α × CauchyFilter α)
hs : Membership.mem (γ := Filter (CauchyFilter α × CauchyFilter α)) (𝓤 (CauchyFilter α)) s
⊢ (range pureCauchy ∩ UniformSpace.ball f s).Nonempty
have refine_2 : ∀ (y : α) (hy : (f, pureCauchy y) ∈ s), (range pureCauchy ∩ UniformSpace.ball f s).Nonempty
Tactic: let ⟨y, hy⟩ := h_ex s hs