awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous (X := X) (α := α) fun (x : (↑S : Type (max u_2 u_3))) ↦ (⇑(↑x : C(X, α)) : (a : X) → α)
rw :
  IsInducing (X := (↑S : Type (max u_2 u_3))) (Y := X →ᵤ[{K : Set X | IsCompact K}] α)
    (comp (β := X → α)
      (⇑(UniformOnFun.ofFun {K : Set X | IsCompact K}) : (a : X → α) → X →ᵤ[{K : Set X | IsCompact K}] α)
      (comp (β :=
        { x : (a : X) → α //
          Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x })
        (Subtype.val (p := fun (x : (a : X) → α) ↦
          Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x))
        (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S ⋯) :
          (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))))
rw₁ : Set (Set X)
rw₂ : Eq.{u_2 + 1} (α := Set X) (⋃₀ {K : Set X | IsCompact K}) univ
⊢ IsInducing (X := (↑S : Type (max u_2 u_3))) (Y :=
    (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
    (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S ⋯) :
      (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
have rw₃ : ∀ (K : Set X), Membership.mem (γ := Set (Set X)) {K : Set X | IsCompact K} K → IsCompact K
Tactic: rw [← IsInducing.subtypeVal.of_comp_iff, ← EquicontinuousOn.isInducing_uniformOnFun_iff_pi _ _ _]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous (X := X) (α := α) fun (x : (↑S : Type (max u_2 u_3))) ↦ (⇑(↑x : C(X, α)) : (a : X) → α)
rw :
  IsInducing (X := (↑S : Type (max u_2 u_3))) (Y := X →ᵤ[{K : Set X | IsCompact K}] α)
    (comp (β := X → α)
      (⇑(UniformOnFun.ofFun {K : Set X | IsCompact K}) : (a : X → α) → X →ᵤ[{K : Set X | IsCompact K}] α)
      (comp (β :=
        { x : (a : X) → α //
          Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x })
        (Subtype.val (p := fun (x : (a : X) → α) ↦
          Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x))
        (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S ⋯) :
          (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))))
rw₁ : Set (Set X)
rw₂ : Eq.{u_2 + 1} (α := Set X) (⋃₀ {K : Set X | IsCompact K}) univ
rw₃ : ∀ (K : Set X), Membership.mem (γ := Set (Set X)) {K : Set X | IsCompact K} K → IsCompact K
⊢ IsInducing (X := (↑S : Type (max u_2 u_3))) (Y :=
    (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
    (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S ⋯) :
      (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
have rw₄ : ∀ (K : Set X),
  Membership.mem (γ := Set (Set X)) {K : Set X | IsCompact K} K →
    EquicontinuousOn (ι := (↑S : Type (max u_2 u_3))) (α := α)
      (comp (β :=
        { x : (a : X) → α //
          Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x })
        (Subtype.val (p := fun (x : (a : X) → α) ↦
          Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x))
        (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S sorry) :
          (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3))))
      K
Tactic: rw [← IsInducing.subtypeVal.of_comp_iff, ← EquicontinuousOn.isInducing_uniformOnFun_iff_pi _ _ _]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
| IsOpen[instTopologicalSpaceProd] (s ○ t)
have arg : s ○ t
Tactic: arg 1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
⊢ s ○ t = ⋃ (b : β), (fun (p : α × γ) ↦ (p.1, b)) ⁻¹' s ∩ (fun (p : α × γ) ↦ (b, p.2)) ⁻¹' t
have h : ∀ (fst : α) (snd : γ),
  (fst, snd) ∈ s ○ t ↔
    Membership.mem (γ := Set (α × γ))
      (⋃ (b : β), (fun (p : α × γ) ↦ (p.1, b)) ⁻¹' s ∩ (fun (p : α × γ) ↦ (b, p.2)) ⁻¹' t) (fst, snd)
Tactic: ext ⟨_, _⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
| IsOpen[instTopologicalSpaceProd] (s ○ t)
have arg : s ○ t
Tactic: arg 1; equals ⋃ b, (fun p => (p.1, b)) ⁻¹' s ∩ (fun p => (b, p.2)) ⁻¹' t => ext ⟨_, _⟩; simp
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
γ : Type uc
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
s : SetRel α β
t : SetRel β γ
hs : IsOpen[instTopologicalSpaceProd] s
ht : IsOpen[instTopologicalSpaceProd] t
⊢ IsOpen[instTopologicalSpaceProd] (s ○ t)
have conv : IsOpen[instTopologicalSpaceProd] (⋃ (b : β), (fun (p : α × γ) ↦ (p.1, b)) ⁻¹' s ∩ (fun (p : α × γ) ↦ (b, p.2)) ⁻¹' t)
Tactic: conv =>
    arg 1; equals ⋃ b, (fun p => (p.1, b)) ⁻¹' s ∩ (fun p => (b, p.2)) ⁻¹' t => ext ⟨_, _⟩; simp
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsOpen[instTopologicalSpaceProd] s
t : Set α
⊢ IsOpen[inst_1] (s.image t)
have simp_rw : IsOpen[inst_1] (⋃ i ∈ t, {x : β | (i, x) ∈ s})
Tactic: simp_rw [SetRel.image, ← exists_prop, Set.setOf_exists]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
β : Type ub
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
s : SetRel α β
hs : IsClosed[instTopologicalSpaceProd] s
t : Set α
ht : t.Finite
⊢ IsClosed[inst_1] (s.image t)
have simp_rw : IsClosed[inst_1] (⋃ i ∈ t, {x : β | (i, x) ∈ s})
Tactic: simp_rw [SetRel.image, ← exists_prop, Set.setOf_exists]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
n : ℕ
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
have suffices : ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
Tactic: suffices ∀ᶠ t in (𝓤 α).smallSets, t ⊆ s ∧ (t ○ ·)^[n] t ⊆ s from (eventually_and.1 this).2
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
n : ℕ
ihn :
  ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n + 1] t ⊆ s
have succ : ∀ (t : Set (α × α)) (htU : t ∈ 𝓤 α) (hts : t ○ t ⊆ s),
  ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n + 1] t ⊆ s
Tactic: rcases comp_mem_uniformity_sets hs with ⟨t, htU, hts⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
n : ℕ
ihn :
  ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n + 1] t ⊆ s
have succ : ∀ (U : SetRel α α) (hU : U ⊆ t ∧ (fun (x : SetRel α α) ↦ U ○ x)^[n] U ⊆ t),
  U ⊆ s ∧ (fun (x : SetRel α α) ↦ U ○ x)^[n + 1] U ⊆ s
Tactic: refine (ihn htU).mono fun U hU => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
n : ℕ
ihn :
  ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : SetRel α α
hU : U ⊆ t ∧ (fun (x : SetRel α α) ↦ U ○ x)^[n] U ⊆ t
⊢ U ⊆ s ∧ (fun (x : SetRel α α) ↦ U ○ x)^[n + 1] U ⊆ s
have succ : U ⊆ s ∧ U ○ (fun (x : SetRel α α) ↦ U ○ x)^[n] U ⊆ s
Tactic: rw [Function.iterate_succ_apply']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
inst : UniformSpace α
n : ℕ
ihn :
  ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : SetRel α α
hU : U ⊆ t ∧ (fun (x : SetRel α α) ↦ U ○ x)^[n] U ⊆ t
⊢ U ⊆ s ∧ U ○ (fun (x : SetRel α α) ↦ U ○ x)^[n] U ⊆ s
have this : SetRel.IsRefl t
Tactic: have := isRefl_of_mem_uniformity htU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
n : ℕ
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
have zero : ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
  ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[0] t ⊆ s
Tactic: induction n generalizing s with
  | zero => simpa
  | succ _ ihn =>
    rcases comp_mem_uniformity_sets hs with ⟨t, htU, hts⟩
    refine (ihn htU).mono fun U hU => ?_
    rw [Function.iterate_succ_apply']
    have := isRefl_of_mem_uniformity htU
    exact ⟨hU.1.trans <| SetRel.left_subset_comp.trans hts,
     (SetRel.comp_subset_comp hU.1 hU.2).trans hts⟩
Cleared hypotheses: s, hs, n
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
n : ℕ
zero :
  ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
    ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[0] t ⊆ s
⊢ ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s
have succ : ∀ (n : ℕ)
  (ihn :
    ∀ {s : SetRel α α} (hs : s ∈ 𝓤 α),
      ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n] t ⊆ s)
  {s : SetRel α α} (hs : s ∈ 𝓤 α),
  ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun (x : SetRel α α) ↦ t ○ x)^[n + 1] t ⊆ s
Tactic: induction n generalizing s with
  | zero => simpa
  | succ _ ihn =>
    rcases comp_mem_uniformity_sets hs with ⟨t, htU, hts⟩
    refine (ihn htU).mono fun U hU => ?_
    rw [Function.iterate_succ_apply']
    have := isRefl_of_mem_uniformity htU
    exact ⟨hU.1.trans <| SetRel.left_subset_comp.trans hts,
     (SetRel.comp_subset_comp hU.1 hU.2).trans hts⟩
Cleared hypotheses: s, hs, n
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
x y : α
⊢ (𝓝 (x, y)).HasBasis (fun (s : Set (α × α)) ↦ s ∈ 𝓤 α ∧ SetRel.IsSymm s) fun (s : Set (α × α)) ↦ ball x s ×ˢ ball y s
have rw : (𝓝 x ×ˢ 𝓝 y).HasBasis (fun (s : Set (α × α)) ↦ s ∈ 𝓤 α ∧ SetRel.IsSymm s) fun (s : Set (α × α)) ↦ ball x s ×ˢ ball y s
Tactic: rw [nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
x y : α
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis (fun (s : Set (α × α)) ↦ s ∈ 𝓤 α ∧ SetRel.IsSymm s) fun (s : Set (α × α)) ↦ ball x s ×ˢ ball y s
have apply : ∀ {i j : SetRel α α},
  i ∈ 𝓤 α ∧ i.IsSymm →
    j ∈ 𝓤 α ∧ j.IsSymm → ∃ (k : SetRel α α), (k ∈ 𝓤 α ∧ k.IsSymm) ∧ ball x k ⊆ ball x i ∧ ball y k ⊆ ball y j
Tactic: apply (hasBasis_nhds x).prod_same_index (hasBasis_nhds y)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
a b : α
⊢ 𝓝 (a, b) =
    (𝓤 α).lift' fun (s : SetRel α α) ↦ SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ s}
have hg₁ : ∀ (s : Set (α × α)),
  Monotone (β := Set (α × α)) fun (t : Set (α × α)) ↦
    SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t}
Tactic: rw [nhds_prod_eq, nhds_nhds_eq_uniformity_uniformity_prod, lift_lift'_same_eq_lift']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
a b : α
hg₁ :
  ∀ (s : Set (α × α)),
    Monotone (β := Set (α × α)) fun (t : Set (α × α)) ↦
      SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t}
⊢ 𝓝 (a, b) =
    (𝓤 α).lift' fun (s : SetRel α α) ↦ SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ s}
have hg₂ : ∀ (t : Set (α × α)),
  Monotone (β := Set (α × α)) fun (s : Set (α × α)) ↦
    SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t}
Tactic: rw [nhds_prod_eq, nhds_nhds_eq_uniformity_uniformity_prod, lift_lift'_same_eq_lift']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
a b : α
⊢ ∀ (t : Set (α × α)),
    Monotone (β := Set (α × α)) fun (s : Set (α × α)) ↦
      SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t}
have hg₂ : ∀ (t : Set (α × α)), Monotone (β := Set α) fun (s : Set (α × α)) ↦ {y : α | (y, a) ∈ s}
Tactic: refine fun t => Monotone.set_prod ?_ monotone_const
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x_1 : α × α
x y : α
hp : (x, y) ∈ s
⊢ cl_d ∈ 𝓝 (x, y)
have rw : ∃ t ∈ 𝓤 α, SProd.sprod (α := Set α) (β := Set α) {y : α | (y, x) ∈ t} {y_1 : α | (y, y_1) ∈ t} ⊆ cl_d
Tactic: rw [nhds_eq_uniformity_prod, mem_lift'_sets]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
x_1 : α × α
x y : α
hp : (x, y) ∈ s
rw : ∃ t ∈ 𝓤 α, SProd.sprod (α := Set α) (β := Set α) {y : α | (y, x) ∈ t} {y_1 : α | (y, y_1) ∈ t} ⊆ cl_d
⊢ cl_d ∈ 𝓝 (x, y)
have hh : Monotone (β := Set (α × α)) fun (s : SetRel α α) ↦
  SProd.sprod (α := Set α) (β := Set α) {y : α | (y, x) ∈ s} {y_1 : α | (y, y_1) ∈ s}
Tactic: rw [nhds_eq_uniformity_prod, mem_lift'_sets]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
⊢ ∃ (t : SetRel α α),
    IsOpen[instTopologicalSpaceProd] t ∧
      s ⊆ t ∧ t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
have this : ∀ p ∈ s, ∃ t ⊆ cl_d, IsOpen[instTopologicalSpaceProd] t ∧ p ∈ t
Tactic: have : ∀ p ∈ s, ∃ t, t ⊆ cl_d ∧ IsOpen t ∧ p ∈ t := fun ⟨x, y⟩ hp =>
    mem_nhds_iff.mp <|
      show cl_d ∈ 𝓝 (x, y) by
        rw [nhds_eq_uniformity_prod, mem_lift'_sets]
        · exact ⟨d, hd, fun ⟨a, b⟩ ⟨ha, hb⟩ => ⟨x, y, ha, hp, hb⟩⟩
        · exact fun _ _ h _ h' => ⟨h h'.1, h h'.2⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
this : ∀ p ∈ s, ∃ t ⊆ cl_d, IsOpen[instTopologicalSpaceProd] t ∧ p ∈ t
⊢ ∃ (t : SetRel α α),
    IsOpen[instTopologicalSpaceProd] t ∧
      s ⊆ t ∧ t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
have choose : ∀ (t : (p : α × α) → p ∈ s → Set (α × α))
  (ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen[instTopologicalSpaceProd] (t p a) ∧ p ∈ t p a),
  ∃ (t : SetRel α α),
    IsOpen[instTopologicalSpaceProd] t ∧
      s ⊆ t ∧ t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
Tactic: choose t ht using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
d s : SetRel α α
hd : d ∈ 𝓤 α
cl_d : Set (α × α) := {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ d ∧ (x, y) ∈ s ∧ (y, p.2) ∈ d}
t : (p : α × α) → p ∈ s → Set (α × α)
ht : ∀ (p : α × α) (a : p ∈ s), t p a ⊆ cl_d ∧ IsOpen[instTopologicalSpaceProd] (t p a) ∧ p ∈ t p a
x : α × α
a b : α
hp : (a, b) ∈ s
⊢ Membership.mem (γ := Set (α × α)) (⋃ (p : α × α), ⋃ (h : p ∈ s), t p h) (a, b)
have simp : ∃ (a_1 : α) (b_1 : α) (i : (a_1, b_1) ∈ s), (a, b) ∈ t (a_1, b_1) i
Tactic: simp only [mem_iUnion, Prod.exists]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
⊢ V ∈ 𝓝 (x, x)
have rcases : ∀ (w : Set (α × α)) (w_in : w ∈ 𝓤 α) (w_symm : SetRel.IsSymm w) (w_sub : w ○ w ⊆ V), V ∈ 𝓝 (x, x)
Tactic: rcases comp_symm_mem_uniformity_sets V_in with ⟨w, w_in, w_symm, w_sub⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
⊢ ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
have rw : ball x w ×ˢ ball x w ∈ 𝓝 x ×ˢ 𝓝 x
Tactic: rw [nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
⊢ V ∈ 𝓝 (x, x)
have this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
Tactic: have : ball x w ×ˢ ball x w ∈ 𝓝 (x, x) := by
    rw [nhds_prod_eq]
    exact prod_mem_prod (ball_mem_nhds x w_in) (ball_mem_nhds x w_in)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : Set (α × α)
V_in : V ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
w_sub : w ○ w ⊆ V
this : ball x w ×ˢ ball x w ∈ 𝓝 (x, x)
⊢ V ∈ 𝓝 (x, x)
have apply : ball x w ×ˢ ball x w ⊆ V
Tactic: apply mem_of_superset this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : Set (α × α)
⊢ closure[instTopologicalSpaceProd] s =
    ⋂ (V : Set (α × α)),
      ⋂ (_ : Membership.mem (γ := Set (Set (α × α))) {V : Set (α × α) | V ∈ 𝓤 α ∧ SetRel.IsSymm V} V), V ○ s ○ V
have h : ∀ (x y : α),
  (x, y) ∈ closure[instTopologicalSpaceProd] s ↔
    Membership.mem (γ := Set (α × α))
      (⋂ (V : Set (α × α)),
        ⋂ (_ : Membership.mem (γ := Set (Set (α × α))) {V : Set (α × α) | V ∈ 𝓤 α ∧ SetRel.IsSymm V} V), V ○ s ○ V)
      (x, y)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
⊢ (𝓤 α).HasBasis (fun (V : SetRel α α) ↦ V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V) id
have refine : ∀ (t : Set (α × α)) (h : t ∈ 𝓤 α), ∃ r ∈ 𝓤 α, IsClosed[instTopologicalSpaceProd] r ∧ r ⊆ t
Tactic: refine Filter.hasBasis_self.2 fun t h => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
⊢ ∃ r ∈ 𝓤 α, IsClosed[instTopologicalSpaceProd] r ∧ r ⊆ t
have rcases : ∀ (w : Set (α × α)) (w_in : w ∈ 𝓤 α) (w_symm : SetRel.IsSymm w) (r : w ○ w ○ w ⊆ t),
  ∃ r ∈ 𝓤 α, IsClosed[instTopologicalSpaceProd] r ∧ r ⊆ t
Tactic: rcases comp_comp_symm_mem_uniformity_sets h with ⟨w, w_in, w_symm, r⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ ∃ r ∈ 𝓤 α, IsClosed[instTopologicalSpaceProd] r ∧ r ⊆ t
have refine : closure[instTopologicalSpaceProd] w ⊆ t
Tactic: refine ⟨closure w, mem_of_superset w_in subset_closure, isClosed_closure, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ closure[instTopologicalSpaceProd] w ⊆ t
have refine : closure[instTopologicalSpaceProd] w ⊆ w ○ w ○ w
Tactic: refine Subset.trans ?_ r
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ closure[instTopologicalSpaceProd] w ⊆ w ○ w ○ w
have rw : ⋂ (V : Set (α × α)),
    ⋂ (_ : Membership.mem (γ := Set (Set (α × α))) {V : Set (α × α) | V ∈ 𝓤 α ∧ SetRel.IsSymm V} V), V ○ w ○ V ⊆
  w ○ w ○ w
Tactic: rw [closure_eq_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
t : Set (α × α)
h : t ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_symm : SetRel.IsSymm w
r : w ○ w ○ w ⊆ t
⊢ ⋂ (V : Set (α × α)),
      ⋂ (_ : Membership.mem (γ := Set (Set (α × α))) {V : Set (α × α) | V ∈ 𝓤 α ∧ SetRel.IsSymm V} V), V ○ w ○ V ⊆
    w ○ w ○ w
have h₁ : ⋂ (_ : Membership.mem (γ := Set (Set (α × α))) {V : Set (α × α) | V ∈ 𝓤 α ∧ SetRel.IsSymm V} w), w ○ w ○ w ⊆ w ○ w ○ w
Tactic: apply iInter_subset_of_subset
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
have let : ∀ (s : Set (α × α)) (hs : s ∈ 𝓤 α) (hs_comp : s ○ (s ○ s) ⊆ d), 𝓤 α ≤ (𝓟 ∘ interior) d
Tactic: let ⟨s, hs, hs_comp⟩ := comp3_mem_uniformity hd
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
have let : ∀ (t : SetRel α α) (ht : IsOpen[instTopologicalSpaceProd] t) (hst : s ⊆ t)
  (ht_comp : t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}), 𝓤 α ≤ (𝓟 ∘ interior) d
Tactic: let ⟨t, ht, hst, ht_comp⟩ := nhdset_of_mem_uniformity s hs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (hypothesis)
Goal:
α : Type ua
inst : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
⊢ 𝓤 α ≤ (𝓟 ∘ interior) d
have this : s ⊆ interior d
Tactic: have : s ⊆ interior d :=
        calc
          s ⊆ t := hst
          _ ⊆ interior d :=
            ht.subset_interior_iff.mpr fun x (hx : x ∈ t) =>
              let ⟨x, y, h₁, h₂, h₃⟩ := ht_comp hx
              hs_comp ⟨x, h₁, y, h₂, h₃⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this : s ⊆ interior d
⊢ interior d ∈ 𝓤 α
have h : ∀ (a : α × α), Membership.mem (γ := Set (α × α)) {x : α × α | x ∈ s → x ∈ interior d} a
Tactic: filter_upwards [hs] using this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Basic (goal)
Goal:
α : Type ua
inst : UniformSpace α
d : Set (α × α)
hd : d ∈ 𝓤 α
s : Set (α × α)
hs : s ∈ 𝓤 α
hs_comp : s ○ (s ○ s) ⊆ d
t : SetRel α α
ht : IsOpen[instTopologicalSpaceProd] t
hst : s ⊆ t
ht_comp : t ⊆ {p : α × α | ∃ (x : α) (y : α), (p.1, x) ∈ s ∧ (x, y) ∈ s ∧ (y, p.2) ∈ s}
this : s ⊆ interior d
h : ∀ (a : α × α), Membership.mem (γ := Set (α × α)) {x : α × α | x ∈ s → x ∈ interior d} a
⊢ interior d ∈ 𝓤 α
have h₁ : ∀ a ∈ s, a ∈ interior d
Tactic: filter_upwards [hs] using this