awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
u₂ : UniformSpace α
toTopologicalSpace : TopologicalSpace α
uniformity : Filter (α × α)
symm : Tendsto Prod.swap uniformity uniformity
comp : (uniformity.lift' fun (s : Set (α × α)) ↦ s ○ s) ≤ uniformity
nhds_eq_comap_uniformity : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity
h : 𝓤 α = 𝓤 α
this : Eq.{ua + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace, uniformity := uniformity, symm := symm, comp := comp,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity : UniformSpace α } =
    u₂
have mk : ∀ [toTopologicalSpace_1 : TopologicalSpace α] (uniformity_1 : Filter (α × α))
  (symm_1 : Tendsto Prod.swap uniformity_1 uniformity_1)
  (comp_1 : (uniformity_1.lift' fun (s : Set (α × α)) ↦ s ○ s) ≤ uniformity_1)
  (nhds_eq_comap_uniformity_1 : ∀ (x : α), 𝓝 x = comap (Prod.mk x) uniformity_1) (h : 𝓤 α = 𝓤 α)
  (this : Eq.{ua + 1} (α := TopologicalSpace α) UniformSpace.toTopologicalSpace UniformSpace.toTopologicalSpace),
  { toTopologicalSpace := toTopologicalSpace, uniformity := uniformity, symm := symm, comp := comp,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity : UniformSpace α } =
    { toTopologicalSpace := toTopologicalSpace_1, uniformity := uniformity_1, symm := symm_1, comp := comp_1,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity_1 }
Tactic: cases u₂
Cleared hypotheses: u₂, h, this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α_1 : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u_2
i : TopologicalSpace α
u : UniformSpace α
h : i = toTopologicalSpace
x : α
⊢ 𝓝 x = comap (Prod.mk x) UniformSpace.uniformity
have rw : 𝓝 x = comap (Prod.mk x) UniformSpace.uniformity
Tactic: rw [h, u.nhds_eq_comap_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α_1 : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
α : Type u_2
i : TopologicalSpace α
u : UniformSpace α
h : i = toTopologicalSpace
x : α
rw : 𝓝 x = comap (Prod.mk x) UniformSpace.uniformity
⊢ 𝓝 x = comap (Prod.mk x) UniformSpace.uniformity
have rw₁ : comap (Prod.mk x) UniformSpace.uniformity = comap (Prod.mk x) UniformSpace.uniformity
Tactic: rw [h, u.nhds_eq_comap_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun (x : β) ↦ (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun (x : β) ↦ (f₂ x, f₃ x)) l (𝓤 α)
⊢ Tendsto (fun (x : β) ↦ (f₁ x, f₃ x)) l (𝓤 α)
have refine : ∀ (s : Set (α × α)) (hs : s ∈ 𝓤 α), (fun (x : β) ↦ (f₁ x, f₃ x)) ⁻¹' (s ○ s) ∈ l
Tactic: refine le_trans (le_lift'.2 fun s hs => mem_map.2 ?_) comp_le_uniformity
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun (x : β) ↦ (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun (x : β) ↦ (f₂ x, f₃ x)) l (𝓤 α)
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ (fun (x : β) ↦ (f₁ x, f₃ x)) ⁻¹' (s ○ s) ∈ l
have h : ∀ (a : β),
  Membership.mem (γ := Set β)
    {x : β |
      Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₁ x, f₂ x)) ⁻¹' s) x →
        Membership.mem (γ := Set β)
          {x : β |
            Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₂ x, f₃ x)) ⁻¹' s) x →
              Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₁ x, f₃ x)) ⁻¹' (s ○ s)) x}
          x}
    a
Tactic: filter_upwards [mem_map.1 (h₁₂ hs), mem_map.1 (h₂₃ hs)] with x hx₁₂ hx₂₃ using ⟨_, hx₁₂, hx₂₃⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
l : Filter β
f₁ f₂ f₃ : β → α
h₁₂ : Tendsto (fun (x : β) ↦ (f₁ x, f₂ x)) l (𝓤 α)
h₂₃ : Tendsto (fun (x : β) ↦ (f₂ x, f₃ x)) l (𝓤 α)
s : Set (α × α)
hs : s ∈ 𝓤 α
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₁ x, f₂ x)) ⁻¹' s) x →
          Membership.mem (γ := Set β)
            {x : β |
              Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₂ x, f₃ x)) ⁻¹' s) x →
                Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₁ x, f₃ x)) ⁻¹' (s ○ s)) x}
            x}
      a
⊢ (fun (x : β) ↦ (f₁ x, f₃ x)) ⁻¹' (s ○ s) ∈ l
have h₁ : ∀ (a : β),
  Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₁ x, f₂ x)) ⁻¹' s) a →
    Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₂ x, f₃ x)) ⁻¹' s) a →
      Membership.mem (γ := Set β) ((fun (x : β) ↦ (f₁ x, f₃ x)) ⁻¹' (s ○ s)) a
Tactic: filter_upwards [mem_map.1 (h₁₂ hs), mem_map.1 (h₂₃ hs)] with x hx₁₂ hx₂₃ using ⟨_, hx₁₂, hx₂₃⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
⊢ 𝓤 α ≤ map Prod.swap (𝓤 α)
have rw : 𝓤 α ≤ comap Prod.swap (𝓤 α)
Tactic: rw [map_swap_eq_comap_swap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.symmetrize ∈ 𝓤 α
have apply : V.inv ∈ (𝓤 α).sets
Tactic: apply (𝓤 α).inter_sets h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.inv ∈ (𝓤 α).sets
have rw : V.inv ∈ (comap Prod.swap (𝓤 α)).sets
Tactic: rw [← comap_swap_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
g : SetRel α α → Filter β
f : Filter β
hg : Monotone g
h : ((𝓤 α).lift fun (s : Set (α × α)) ↦ g (Prod.swap ⁻¹' s)) ≤ f
⊢ (map Prod.swap (𝓤 α)).lift g ≤ f
have rw : (𝓤 α).lift (g ∘ preimage Prod.swap) ≤ f
Tactic: rw [map_lift_eq2 hg, image_swap_eq_preimage_swap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
f : SetRel α α → Filter β
h : Monotone f
⊢ ((𝓤 α).lift fun (s : Set (α × α)) ↦ f (s ○ s)) = Filter.lift ((𝓤 α).lift' fun (s : SetRel α α) ↦ s ○ s) f
have hg : Monotone (β := Set (α × α)) fun (s : SetRel α α) ↦ s ○ s
Tactic: rw [lift_lift'_assoc]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ⊆ s
have obtain : ∀ (w : Set (α × α)) (w_in : w ∈ 𝓤 α) (w_sub : w ○ w ⊆ s), ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ⊆ s
Tactic: obtain ⟨w, w_in, w_sub⟩ : ∃ w ∈ 𝓤 α, w ○ w ⊆ s := comp_mem_uniformity_sets hs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ⊆ s
have right : SetRel.symmetrize w ○ SetRel.symmetrize w ⊆ s
Tactic: use SetRel.symmetrize w, symmetrize_mem_uniformity w_in, inferInstance
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (hypothesis)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
⊢ SetRel.symmetrize w ○ SetRel.symmetrize w ⊆ s
have this : SetRel.symmetrize w ⊆ w
Tactic: have : SetRel.symmetrize w ⊆ w := SetRel.symmetrize_subset_self
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
w_sub : w ○ w ⊆ s
this : SetRel.symmetrize w ⊆ w
⊢ SetRel.symmetrize w ○ SetRel.symmetrize w ⊆ s
have calc : SetRel.symmetrize w ○ SetRel.symmetrize w ⊆ w ○ w
Tactic: calc SetRel.symmetrize w ○ SetRel.symmetrize w
    _ ⊆ w ○ w := by gcongr
    _ ⊆ s := w_sub
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s
have rcases : ∀ (w : Set (α × α)) (w_in : w ∈ 𝓤 α),
  SetRel.IsSymm w → ∀ (w_sub : w ○ w ⊆ s), ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s
Tactic: rcases comp_symm_mem_uniformity_sets hs with ⟨w, w_in, _, w_sub⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s
have rcases : ∀ (t : Set (α × α)) (t_in : t ∈ 𝓤 α) (t_symm : SetRel.IsSymm t) (t_sub : t ○ t ⊆ w),
  ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s
Tactic: rcases comp_symm_mem_uniformity_sets w_in with ⟨t, t_in, t_symm, t_sub⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
⊢ ∃ t ∈ 𝓤 α, SetRel.IsSymm t ∧ t ○ t ○ t ⊆ s
have right : t ○ t ○ t ⊆ s
Tactic: use t, t_in, t_symm
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (hypothesis)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
⊢ t ○ t ○ t ⊆ s
have this : t ⊆ t ○ t
Tactic: have : t ⊆ t ○ t := subset_comp_self_of_mem_uniformity t_in
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
⊢ t ○ t ○ t ⊆ s
have t₁ : t ○ t ○ t ⊆ w ○ (t ○ t)
Tactic: calc
    t ○ t ○ t ⊆ w ○ (t ○ t) := by gcongr
    _ ⊆ w ○ w := by gcongr
    _ ⊆ s := w_sub
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : SetRel α α
hs : s ∈ 𝓤 α
w : Set (α × α)
w_in : w ∈ 𝓤 α
left : SetRel.IsSymm w
w_sub : w ○ w ⊆ s
t : Set (α × α)
t_in : t ∈ 𝓤 α
t_symm : SetRel.IsSymm t
t_sub : t ○ t ⊆ w
this : t ⊆ t ○ t
t₁ : t ○ t ○ t ⊆ w ○ (t ○ t)
⊢ t ○ t ○ t ⊆ s
have t₂ : w ○ (t ○ t) ⊆ w ○ w
Tactic: calc
    t ○ t ○ t ⊆ w ○ (t ○ t) := by gcongr
    _ ⊆ w ○ w := by gcongr
    _ ⊆ s := w_sub
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
β : Type ub
V : SetRel β β
inst : V.IsSymm
x : β
⊢ ball x V = {y : β | (y, x) ∈ V}
have h : ∀ (y : β), y ∈ ball x V ↔ Membership.mem (γ := Set β) {y : β | (y, x) ∈ V} y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
β : Type ub
V : SetRel β β
inst : V.IsSymm
x y : β
⊢ y ∈ ball x V ↔ Membership.mem (γ := Set β) {y : β | (y, x) ∈ V} y
have h : x ∈ ball y V ↔ Membership.mem (γ := Set β) {y : β | (y, x) ∈ V} y
Tactic: rw [mem_ball_symmetry]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (hypothesis)
Goal:
β : Type ub
V W : SetRel β β
x y z : β
inst : V.IsSymm
hx : x ∈ ball z V
hy : y ∈ ball z W
⊢ (x, y) ∈ V ○ W
have hx₁ : z ∈ ball x V
Tactic: rw [mem_ball_symmetry] at hx
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
β : Type ub
V W M : SetRel β β
inst : W.IsSymm
p : β × β
⊢ p ∈ V ○ M ○ W ↔ (ball p.1 V ×ˢ ball p.2 W ∩ M).Nonempty
have obtain : ∀ (x y : β), (x, y) ∈ V ○ M ○ W ↔ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty
Tactic: obtain ⟨x, y⟩ := p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
β : Type ub
V W M : SetRel β β
inst : W.IsSymm
x y : β
⊢ (x, y) ∈ V ○ M ○ W ↔ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty
have mp : (x, y) ∈ V ○ M ○ W → (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
β : Type ub
V W M : SetRel β β
inst : W.IsSymm
x y : β
mp : (x, y) ∈ V ○ M ○ W → (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty
⊢ (x, y) ∈ V ○ M ○ W ↔ (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty
have mpr : (ball (x, y).1 V ×ˢ ball (x, y).2 W ∩ M).Nonempty → (x, y) ∈ V ○ M ○ W
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
β : Type ub
V W M : SetRel β β
inst : W.IsSymm
x y z : β
hzy : (z, y) ∈ W
w : β
hpw : (x, w) ∈ V
hwz : (w, z) ∈ M
⊢ (w, z).2 ∈ ball (x, y).2 W
have rwa : (x, y).2 ∈ ball (w, z).2 W
Tactic: rwa [mem_ball_symmetry]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (hypothesis)
Goal:
β : Type ub
V W M : SetRel β β
inst : W.IsSymm
x y w z : β
hwz : (w, z) ∈ M
w_in : (w, z).1 ∈ ball (x, y).1 V
z_in : (w, z).2 ∈ ball (x, y).2 W
⊢ (x, y) ∈ V ○ M ○ W
have z_in₁ : (x, y).2 ∈ ball (w, z).2 W
Tactic: rw [mem_ball_symmetry] at z_in
Cleared hypotheses: z_in
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ {p : α × α | p.2 = x → p.1 ∈ s} ∈ 𝓤 α
have rw : {p : α × α | p.1 = x → p.2 ∈ s} ∈ 𝓤 α ↔ {p : α × α | p.2 = x → p.1 ∈ s} ∈ map Prod.swap (𝓤 α)
Tactic: rw [uniformity_eq_symm, mem_nhds_uniformity_iff_right]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
⊢ IsOpen[inst.toTopologicalSpace] s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
have simp_rw : (∀ x ∈ s, s ∈ 𝓝 x) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
Tactic: simp_rw [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap, ball]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
simp_rw : (∀ x ∈ s, s ∈ 𝓝 x) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
⊢ IsOpen[inst.toTopologicalSpace] s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
have simp_rw₁ : (∀ x ∈ s, s ∈ comap (Prod.mk x) (𝓤 α)) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
Tactic: simp_rw [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap, ball]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
s : Set α
simp_rw : (∀ x ∈ s, s ∈ 𝓝 x) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
simp_rw₁ : (∀ x ∈ s, s ∈ comap (Prod.mk x) (𝓤 α)) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
⊢ IsOpen[inst.toTopologicalSpace] s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
have simp_rw₂ : (∀ x ∈ s, ∃ t ∈ 𝓤 α, Prod.mk x ⁻¹' t ⊆ s) ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s
Tactic: simp_rw [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap, ball]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
h : (𝓤 α).HasBasis p s
x : α
⊢ (𝓝 x).HasBasis p fun (i : ι) ↦ ball x (s i)
have rw : (comap (Prod.mk x) (𝓤 α)).HasBasis p fun (i : ι) ↦ ball x (s i)
Tactic: rw [nhds_eq_comap_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (hypothesis)
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
h : (𝓤 α).HasBasis p s
x : α
⊢ (𝓝 x).HasBasis p fun (i : ι) ↦ {y : α | (y, x) ∈ s i}
have h₁ : (comap Prod.swap (𝓤 α)).HasBasis p fun (i : ι) ↦ Prod.swap ⁻¹' s i
Tactic: replace h := h.comap Prod.swap
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (hypothesis)
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
x : α
h : (comap Prod.swap (𝓤 α)).HasBasis p fun (i : ι) ↦ Prod.swap ⁻¹' s i
⊢ (𝓝 x).HasBasis p fun (i : ι) ↦ {y : α | (y, x) ∈ s i}
have h₁ : (𝓤 α).HasBasis p fun (i : ι) ↦ Prod.swap ⁻¹' s i
Tactic: rw [comap_swap_uniformity] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s
have rw : (∃ t ∈ 𝓤 α, Prod.mk x ⁻¹' t ⊆ s) ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s
Tactic: rw [nhds_eq_comap_uniformity, mem_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
x : α
V : SetRel α α
V_in : V ∈ 𝓤 α
⊢ ball x V ∈ 𝓝 x
have rw : ∃ V_1 ∈ 𝓤 α, ball x V_1 ⊆ ball x V
Tactic: rw [UniformSpace.mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
x : α
S : Set α
V : SetRel α α
x_in : x ∈ S
V_in : V ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S)
⊢ ball x V ∈ 𝓝[S] x
have rw : ∃ t ∈ 𝓤 α ⊓ 𝓟 (S ×ˢ S), Prod.mk x ⁻¹' t ⊆ ball x V
Tactic: rw [nhdsWithin_eq_comap_uniformity_of_mem x_in, mem_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s
have rw : (∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s
Tactic: rw [UniformSpace.mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
⊢ (∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s
have mp : (∃ V ∈ 𝓤 α, ball x V ⊆ s) → ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
mp : (∃ V ∈ 𝓤 α, ball x V ⊆ s) → ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s
⊢ (∃ V ∈ 𝓤 α, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s
have mpr : (∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 α, ball x V ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
x : α
s : Set α
V : Set (α × α)
V_in : V ∈ 𝓤 α
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 α, SetRel.IsSymm V ∧ ball x V ⊆ s
have right : ball x (SetRel.symmetrize V) ⊆ s
Tactic: use SetRel.symmetrize V, symmetrize_mem_uniformity V_in, inferInstance
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
U : SetRel α α
hU : U ∈ 𝓤 α
s : Set α
x : α
hx : x ∈ closure[inst.toTopologicalSpace] s
⊢ x ∈ U.preimage s
have obtain : ∀ (y : α) (hxy : y ∈ ball x U) (hy : y ∈ s), x ∈ U.preimage s
Tactic: obtain ⟨y, hxy, hy⟩ := mem_closure_iff_ball.mp hx hU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓝 x).lift g = (𝓤 α).lift fun (s : SetRel α α) ↦ g (ball x s)
have rw : (𝓤 α).lift (g ∘ preimage (Prod.mk x)) = (𝓤 α).lift fun (s : SetRel α α) ↦ g (ball x s)
Tactic: rw [nhds_eq_comap_uniformity, comap_lift_eq2 hg]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓤 α).lift (g ∘ preimage (Prod.mk x)) = (𝓤 α).lift fun (s : SetRel α α) ↦ g (ball x s)
have simp_rw : (𝓤 α).lift (g ∘ preimage (Prod.mk x)) = (𝓤 α).lift fun (s : SetRel α α) ↦ g (Prod.mk x ⁻¹' s)
Tactic: simp_rw [ball, Function.comp_def]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓝 x).lift g = (𝓤 α).lift fun (s : SetRel α α) ↦ g {y : α | (y, x) ∈ s}
have rw : (𝓤 α).lift (g ∘ preimage fun (y : α) ↦ (y, x)) = (𝓤 α).lift fun (s : SetRel α α) ↦ g {y : α | (y, x) ∈ s}
Tactic: rw [nhds_eq_comap_uniformity', comap_lift_eq2 hg]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
x : α
g : Set α → Filter β
hg : Monotone g
⊢ (𝓤 α).lift (g ∘ preimage fun (y : α) ↦ (y, x)) = (𝓤 α).lift fun (s : SetRel α α) ↦ g {y : α | (y, x) ∈ s}
have simp_rw : Eq.{ub + 1} (α := Filter β) ((𝓤 α).lift fun (x_1 : Set (α × α)) ↦ g ((fun (y : α) ↦ (y, x)) ⁻¹' x_1))
  ((𝓤 α).lift fun (s : SetRel α α) ↦ g {y : α | (y, x) ∈ s})
Tactic: simp_rw [Function.comp_def, preimage]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
a b : α
⊢ 𝓝 a ×ˢ 𝓝 b =
    (𝓤 α).lift fun (s : SetRel α α) ↦
      (𝓤 α).lift' fun (t : Set (α × α)) ↦
        SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t}
have rw : Eq (α := Filter (α × α))
  ((𝓤 α).lift fun (s : Set (α × α)) ↦
    (𝓤 α).lift' fun (t : Set (α × α)) ↦ SProd.sprod (α := Set α) {y : α | (y, a) ∈ s} (ball b t))
  ((𝓤 α).lift fun (s : SetRel α α) ↦
    (𝓤 α).lift' fun (t : Set (α × α)) ↦ SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t})
Tactic: rw [nhds_eq_uniformity', nhds_eq_uniformity, prod_lift'_lift']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
a b : α
rw :
  Eq (α := Filter (α × α))
    ((𝓤 α).lift fun (s : Set (α × α)) ↦
      (𝓤 α).lift' fun (t : Set (α × α)) ↦ SProd.sprod (α := Set α) {y : α | (y, a) ∈ s} (ball b t))
    ((𝓤 α).lift fun (s : SetRel α α) ↦
      (𝓤 α).lift' fun (t : Set (α × α)) ↦
        SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t})
⊢ 𝓝 a ×ˢ 𝓝 b =
    (𝓤 α).lift fun (s : SetRel α α) ↦
      (𝓤 α).lift' fun (t : Set (α × α)) ↦
        SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t}
have hg₁ : Monotone (β := Set α) fun (s : Set (α × α)) ↦ {y : α | (y, a) ∈ s}
Tactic: rw [nhds_eq_uniformity', nhds_eq_uniformity, prod_lift'_lift']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
inst : UniformSpace α
a b : α
rw :
  Eq (α := Filter (α × α))
    ((𝓤 α).lift fun (s : Set (α × α)) ↦
      (𝓤 α).lift' fun (t : Set (α × α)) ↦ SProd.sprod (α := Set α) {y : α | (y, a) ∈ s} (ball b t))
    ((𝓤 α).lift fun (s : SetRel α α) ↦
      (𝓤 α).lift' fun (t : Set (α × α)) ↦
        SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t})
hg₁ : Monotone (β := Set α) fun (s : Set (α × α)) ↦ {y : α | (y, a) ∈ s}
⊢ 𝓝 a ×ˢ 𝓝 b =
    (𝓤 α).lift fun (s : SetRel α α) ↦
      (𝓤 α).lift' fun (t : Set (α × α)) ↦
        SProd.sprod (α := Set α) (β := Set α) {y : α | (y, a) ∈ s} {y : α | (b, y) ∈ t}
have hg₂ : Monotone (ball b)
Tactic: rw [nhds_eq_uniformity', nhds_eq_uniformity, prod_lift'_lift']
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
U : ι → SetRel α α
h : (𝓤 α).HasBasis p U
s : Set α
⊢ ⋂ (i : ι), ⋂ (_ : p i), ⋃ x ∈ s, ball x (U i) = closure[inst.toTopologicalSpace] s
have h₁ : ∀ (x : α),
  Membership.mem (γ := Set α) (⋂ (i : ι), ⋂ (_ : p i), ⋃ x ∈ s, ball x (U i)) x ↔ x ∈ closure[inst.toTopologicalSpace] s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
⊢ UniformContinuousOn f univ ↔ UniformContinuous f
have rw : Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (SProd.sprod (α := Set α) (β := Set α) univ univ)) (𝓤 β) ↔
  UniformContinuous f
Tactic: rw [UniformContinuousOn, UniformContinuous, univ_prod_univ, principal_univ, inf_top_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
rw :
  Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (SProd.sprod (α := Set α) (β := Set α) univ univ)) (𝓤 β) ↔
    UniformContinuous f
⊢ UniformContinuousOn f univ ↔ UniformContinuous f
have rw₁ : Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (SProd.sprod (α := Set α) (β := Set α) univ univ)) (𝓤 β) ↔
  Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Tactic: rw [UniformContinuousOn, UniformContinuous, univ_prod_univ, principal_univ, inf_top_eq]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Defs (goal)
Goal:
α : Type ua
β : Type ub
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
rw :
  Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (SProd.sprod (α := Set α) (β := Set α) univ univ)) (𝓤 β) ↔
    UniformContinuous f
rw₁ :
  Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 (SProd.sprod (α := Set α) (β := Set α) univ univ)) (𝓤 β) ↔
    Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
⊢ UniformContinuousOn f univ ↔ UniformContinuous f
have rw₂ : Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α ⊓ 𝓟 univ) (𝓤 β) ↔ Tendsto (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)
Tactic: rw [UniformContinuousOn, UniformContinuous, univ_prod_univ, principal_univ, inf_top_eq]