awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α)) (map (Prod.map mk mk) (𝓤 α)) t
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen[instTopologicalSpaceProd] U
hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t
⊢ Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α))
    (Filter.lift' (α := SeparationQuotient α × SeparationQuotient α) (map (Prod.map mk mk) (𝓤 α))
      fun (s : Set (SeparationQuotient α × SeparationQuotient α)) ↦ SetRel.comp s s)
    t
have refine : SetRel.comp (β := SeparationQuotient α) (Prod.map mk mk '' U) (Prod.map mk mk '' U) ⊆ t
Tactic: refine mem_of_superset (mem_lift' <| image_mem_map hU) ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α)) (map (Prod.map mk mk) (𝓤 α)) t
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen[instTopologicalSpaceProd] U
hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t
⊢ SetRel.comp (β := SeparationQuotient α) (Prod.map mk mk '' U) (Prod.map mk mk '' U) ⊆ t
have simp : ∀ (a b : SeparationQuotient α),
  (∃ (b_1 : SeparationQuotient α),
      (∃ x ∈ U, (Prod.map mk mk x).1 = a ∧ (Prod.map mk mk x).2 = b_1) ∧
        ∃ x ∈ U, (Prod.map mk mk x).1 = b_1 ∧ (Prod.map mk mk x).2 = b) →
    (a, b) ∈ t
Tactic: simp only [subset_def, Prod.forall, SetRel.mem_comp, mem_image, Prod.ext_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (hypothesis)
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
t : Set (SeparationQuotient α × SeparationQuotient α)
ht : Membership.mem (γ := Filter (SeparationQuotient α × SeparationQuotient α)) (map (Prod.map mk mk) (𝓤 α)) t
U : Set (α × α)
hU : U ∈ 𝓤 α
hUo : IsOpen[instTopologicalSpaceProd] U
hUt : SetRel.comp U U ⊆ Prod.map mk mk ⁻¹' t
x y : α
hxyU : (x, y) ∈ U
y' z : α
hyzU : (y', z) ∈ U
hy : Eq (α := SeparationQuotient α) (Prod.map mk mk (y', z)).1 (Prod.map mk mk (x, y)).2
⊢ ((Prod.map mk mk (x, y)).1, (Prod.map mk mk (y', z)).2) ∈ t
have this : y' ⤳ y
Tactic: have : y' ⤳ y := (mk_eq_mk.1 hy).specializes
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
x : α
| Filter.comap (β := SeparationQuotient α) mk (𝓝 (mk x))
have rw : Filter.comap (Prod.mk x)
  (Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)))
Tactic: rw [comap_mk_nhds_mk, nhds_eq_comap_uniformity, ← comap_map_mk_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
x : α
⊢ Filter.comap (β := SeparationQuotient α) mk (𝓝 (mk x)) =
    Filter.comap (β := SeparationQuotient α) mk
      (Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.mk (mk x)) (map (Prod.map mk mk) (𝓤 α)))
have conv_lhs : Filter.comap (Prod.mk x)
    (Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α))) =
  Filter.comap (β := SeparationQuotient α) mk
    (Filter.comap (β := SeparationQuotient α × SeparationQuotient α) (Prod.mk (mk x)) (map (Prod.map mk mk) (𝓤 α)))
Tactic: conv_lhs => rw [comap_mk_nhds_mk, nhds_eq_comap_uniformity, ← comap_map_mk_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
γ : Type w
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
f : Prod.{u, v} (SeparationQuotient α) (SeparationQuotient β) → γ
⊢ UniformContinuous f ↔ UniformContinuous (β := γ) fun (p : α × β) ↦ f (mk p.1, mk p.2)
have simp : Tendsto
    (comp (β := Prod.{u, v} (SeparationQuotient α × SeparationQuotient α) (SeparationQuotient β × SeparationQuotient β))
      ((fun
            (x :
              Prod.{u, v} (SeparationQuotient α) (SeparationQuotient β) ×
                Prod.{u, v} (SeparationQuotient α) (SeparationQuotient β)) ↦
          (f x.1, f x.2)) ∘
        fun
          (p :
            Prod.{u, v} (SeparationQuotient α × SeparationQuotient α) (SeparationQuotient β × SeparationQuotient β)) ↦
        ((p.1.1, p.2.1), p.1.2, p.2.2))
      fun (p : Prod.{u, v} (α × α) (β × β)) ↦ (Prod.map mk mk p.1, Prod.map mk mk p.2))
    (𝓤 α ×ˢ 𝓤 β) (𝓤 γ) ↔
  Tendsto
    ((fun (x : (α × β) × α × β) ↦ (f (mk x.1.1, mk x.1.2), f (mk x.2.1, mk x.2.2))) ∘
      fun (p : Prod.{u, v} (α × α) (β × β)) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
    (𝓤 α ×ˢ 𝓤 β) (𝓤 γ)
Tactic: simp only [UniformContinuous, uniformity_prod_eq_prod, uniformity_eq, prod_map_map_eq,
    tendsto_map'_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
h : UniformContinuous f
a : α
⊢ lift' f (mk a) = f a
have rw : (if hc : UniformContinuous f then lift f sorry else fun (x : SeparationQuotient α) ↦ f sorry.some) (mk a) = f a
Tactic: rw [lift', dif_pos h, lift_mk]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
h : UniformContinuous f
a : α
rw : (if hc : UniformContinuous f then lift f ⋯ else fun (x : SeparationQuotient α) ↦ f ⋯.some) (mk a) = f a
⊢ lift' f (mk a) = f a
have rw₁ : lift f sorry (mk a) = f a
Tactic: rw [lift', dif_pos h, lift_mk]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
h : UniformContinuous f
a : α
rw : (if hc : UniformContinuous f then lift f ⋯ else fun (x : SeparationQuotient α) ↦ f ⋯.some) (mk a) = f a
rw₁ : lift f ⋯ (mk a) = f a
⊢ lift' f (mk a) = f a
have rw₂ : f a = f a
Tactic: rw [lift', dif_pos h, lift_mk]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
⊢ UniformContinuous (α := SeparationQuotient α) (lift' f)
have pos : ∀ (hf : UniformContinuous f), UniformContinuous (α := SeparationQuotient α) (lift' f)
Tactic: by_cases hf : UniformContinuous f
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
pos : ∀ (hf : UniformContinuous f), UniformContinuous (α := SeparationQuotient α) (lift' f)
⊢ UniformContinuous (α := SeparationQuotient α) (lift' f)
have neg : ∀ (hf : ¬UniformContinuous f), UniformContinuous (α := SeparationQuotient α) (lift' f)
Tactic: by_cases hf : UniformContinuous f
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
hf : UniformContinuous f
⊢ UniformContinuous (α := SeparationQuotient α) (lift' f)
have pos : UniformContinuous.{u, v} (α := SeparationQuotient α) (β := β)
  (if hc : UniformContinuous f then lift f sorry else fun (x : SeparationQuotient α) ↦ f sorry.some)
Tactic: rwa [lift', dif_pos hf, uniformContinuous_lift]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
hf : UniformContinuous f
pos :
  UniformContinuous.{u, v} (α := SeparationQuotient α) (β := β)
    (if hc : UniformContinuous f then lift f ⋯ else fun (x : SeparationQuotient α) ↦ f ⋯.some)
⊢ UniformContinuous (α := SeparationQuotient α) (lift' f)
have pos₁ : UniformContinuous (lift f sorry)
Tactic: rwa [lift', dif_pos hf, uniformContinuous_lift]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (α := SeparationQuotient α) (lift' f)
have neg : UniformContinuous.{u, v} (β := β) fun (x : SeparationQuotient α) ↦ f sorry.some
Tactic: rw [lift', dif_neg hf]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
h : UniformContinuous f
a : α
⊢ Eq (α := SeparationQuotient β) (map f (mk a)) (mk (f a))
have rw : Eq (α := SeparationQuotient β) ((mk ∘ f) a) (mk (f a))
Tactic: rw [map, lift'_mk (uniformContinuous_mk.comp h)]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u
β : Type v
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : UniformContinuous f
g : SeparationQuotient α → SeparationQuotient β
comm : mk ∘ f = g ∘ mk
⊢ map f = g
have h : ∀ (x : SeparationQuotient α) (a : α),
  map f (Quot.mk (⇑(inseparableSetoid α) : α → α → Prop) a) = g (Quot.mk (⇑(inseparableSetoid α) : α → α → Prop) a)
Tactic: ext ⟨a⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u_1
u : UniformSpace α
inst : IndiscreteTopology α
⊢ u = ⊤
have refine : 𝓤 α = 𝓤 α
Tactic: refine UniformSpace.ext ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u_1
u : UniformSpace α
inst : IndiscreteTopology α
⊢ 𝓤 α = 𝓤 α
have rw : (𝓤 α).ker = univ
Tactic: rw [top_uniformity, ← Filter.ker_eq_univ]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u_1
u : UniformSpace α
inst : IndiscreteTopology α
⊢ (𝓤 α).ker = univ
have h : ∀ (x : α × α), x ∈ (𝓤 α).ker ↔ Membership.mem (γ := Set (α × α)) univ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
α : Type u_1
u : UniformSpace α
inst : IndiscreteTopology α
x : α × α
⊢ x ∈ (𝓤 α).ker ↔ Membership.mem (γ := Set (α × α)) univ x
have h : Inseparable x.1 x.2 ↔ Membership.mem (γ := Set (α × α)) univ x
Tactic: rw [← inseparable_iff_ker_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Separation (goal)
Goal:
β : Type v
inst : UniformSpace β
α : Type u_1
u : UniformSpace α
inst_1 : IndiscreteTopology β
f : α → β
⊢ UniformContinuous f
have rw : Tendsto.{u_1, v} (β := β × β) (fun (x : α × α) ↦ (f x.1, f x.2)) (𝓤 α) ⊤
Tactic: rw [UniformContinuous, eq_top_uniformSpace (α := β), top_uniformity]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Basic (hypothesis)
Goal:
X : Type u_1
s : SetRel X X
t u v : Set X
inst : s.IsTrans
htu : t ×ˢ u ⊆ s
huv : u ×ˢ v ⊆ s
hu : u.Nonempty
a b : X
hab : (a, b) ∈ t ×ˢ v
⊢ (a, b) ∈ s
have hab₁ : a ∈ t ∧ b ∈ v
Tactic: simp only [mem_prod] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
s : SetRel X X
t u v : Set X
inst : s.IsTrans
htu : t ×ˢ u ⊆ s
huv : u ×ˢ v ⊆ s
hu : u.Nonempty
a b : X
hab : a ∈ t ∧ b ∈ v
⊢ (a, b) ∈ s
have obtain : ∀ (x : X) (hx : x ∈ u), (a, b) ∈ s
Tactic: obtain ⟨x, hx⟩ := hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
V : SetRel X X
inst : V.IsSymm
inst_1 : V.IsTrans
x y : X
hy : y ∈ ball x V
⊢ ball x V = ball y V
have refine : x ∈ ball y V
Tactic: refine le_antisymm (ball_subset_of_mem ?_) (ball_subset_of_mem hy)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
s : Set X
⊢ s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s
have rw : (∃ V ∈ 𝓤 X, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s
Tactic: rw [UniformSpace.mem_nhds_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
s : Set X
⊢ (∃ V ∈ 𝓤 X, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s
have mp : (∃ V ∈ 𝓤 X, ball x V ⊆ s) → ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
s : Set X
mp : (∃ V ∈ 𝓤 X, ball x V ⊆ s) → ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s
⊢ (∃ V ∈ 𝓤 X, ball x V ⊆ s) ↔ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s
have mpr : (∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s) → ∃ V ∈ 𝓤 X, ball x V ⊆ s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Basic (hypothesis)
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
s : Set X
V : Set (X × X)
V_in : V ∈ 𝓤 X
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s
have V_in₁ : ∃ (i : SetRel X X), (i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans) ∧ id i ⊆ V
Tactic: rw [IsUltraUniformity.hasBasis.mem_iff'] at V_in
Cleared hypotheses: V_in, V_sub
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
s : Set X
V : Set (X × X)
V_in : ∃ (i : SetRel X X), (i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans) ∧ id i ⊆ V
V_sub : ball x V ⊆ s
⊢ ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s
have mp : ∀ (U : SetRel X X) (U_sub : id U ⊆ V) (U_in : U ∈ 𝓤 X) (U_sym : U.IsSymm) (U_trans : U.IsTrans),
  ∃ V ∈ 𝓤 X, SetRel.IsSymm V ∧ SetRel.IsTrans V ∧ ball x V ⊆ s
Tactic: obtain ⟨U, ⟨U_in, U_sym, U_trans⟩, U_sub⟩ := V_in
Cleared hypotheses: V_in
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : UniformSpace X
x : X
V : SetRel X X
inst_1 : V.IsTrans
h' : V ∈ 𝓤 X
⊢ IsOpen[inst.toTopologicalSpace] (ball x V)
have rw : ∀ x_1 ∈ ball x V, ∃ V_1 ∈ 𝓤 X, ball x_1 V_1 ⊆ ball x V
Tactic: rw [isOpen_iff_ball_subset]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : UniformSpace X
x : X
V : SetRel X X
inst_1 : V.IsSymm
inst_2 : V.IsTrans
h' : V ∈ 𝓤 X
⊢ IsClosed[inst.toTopologicalSpace] (ball x V)
have rw : ∀ x_1 ∈ (ball x V)ᶜ, ∃ V_1 ∈ 𝓤 X, ball x_1 V_1 ⊆ (ball x V)ᶜ
Tactic: rw [← isOpen_compl_iff, isOpen_iff_ball_subset]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ x ∈ s ∧ IsClopen s) id
have refine_1 : ∀ (i : SetRel X X), i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → ∃ (i' : Set X), (x ∈ i' ∧ IsClopen i') ∧ id i' ⊆ ball x (id i)
Tactic: refine (nhds_basis_uniformity' (IsUltraUniformity.hasBasis)).to_hasBasis' ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
refine_1 :
  ∀ (i : SetRel X X), i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → ∃ (i' : Set X), (x ∈ i' ∧ IsClopen i') ∧ id i' ⊆ ball x (id i)
⊢ (𝓝 x).HasBasis (fun (s : Set X) ↦ x ∈ s ∧ IsClopen s) id
have refine_2 : ∀ (i' : Set X), x ∈ i' ∧ IsClopen i' → id i' ∈ 𝓝 x
Tactic: refine (nhds_basis_uniformity' (IsUltraUniformity.hasBasis)).to_hasBasis' ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Basic (goal)
Goal:
X : Type u_1
inst : UniformSpace X
inst_1 : IsUltraUniformity X
x : X
V : SetRel X X
⊢ V ∈ 𝓤 X ∧ V.IsSymm ∧ V.IsTrans → ∃ (i' : Set X), (x ∈ i' ∧ IsClopen i') ∧ id i' ⊆ ball x (id V)
have refine_1 : ∀ (hV : V ∈ 𝓤 X) (h_symm : V.IsSymm) (h_trans : V.IsTrans),
  ∃ (i' : Set X), (x ∈ i' ∧ IsClopen i') ∧ id i' ⊆ ball x (id V)
Tactic: ⟨hV, h_symm, h_trans⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Completion (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
⊢ IsUltraUniformity.{u_1} (CauchyFilter X)
have h_symm : ∀ (i : SetRel X X), i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsSymm (α := CauchyFilter X) ((CauchyFilter.gen ∘ id) i)
Tactic: apply mk_of_hasBasis (CauchyFilter.basis_uniformity IsUltraUniformity.hasBasis)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Completion (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
h_symm :
  ∀ (i : SetRel X X), i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsSymm (α := CauchyFilter X) ((CauchyFilter.gen ∘ id) i)
⊢ IsUltraUniformity.{u_1} (CauchyFilter X)
have h_trans : ∀ (i : SetRel X X), i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsTrans (α := CauchyFilter X) ((CauchyFilter.gen ∘ id) i)
Tactic: apply mk_of_hasBasis (CauchyFilter.basis_uniformity IsUltraUniformity.hasBasis)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Completion (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
x : SetRel X X
h : x ∈ 𝓤 X ∧ x.IsSymm ∧ x.IsTrans
left : x ∈ 𝓤 X
hU : x.IsSymm
right : x.IsTrans
⊢ SetRel.IsSymm (α := CauchyFilter X) ((CauchyFilter.gen ∘ id) x)
have simp : SetRel.IsSymm (α := CauchyFilter X) (CauchyFilter.gen x)
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Completion (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
x : SetRel X X
h : x ∈ 𝓤 X ∧ x.IsSymm ∧ x.IsTrans
left : x ∈ 𝓤 X
left_1 : x.IsSymm
hU : x.IsTrans
⊢ SetRel.IsTrans (α := CauchyFilter X) ((CauchyFilter.gen ∘ id) x)
have simp : SetRel.IsTrans (α := CauchyFilter X) (CauchyFilter.gen x)
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Completion (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
⊢ IsUltraUniformity.{u_1} (SeparationQuotient X)
have this : HasBasis (α := SeparationQuotient X × SeparationQuotient X)
  (map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (𝓤 X))
  (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
  Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
Tactic: have := IsUltraUniformity.hasBasis.map
    (Prod.map SeparationQuotient.mk (SeparationQuotient.mk (X := X)))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Completion (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X)
    (map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (𝓤 X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
⊢ IsUltraUniformity.{u_1} (SeparationQuotient X)
have this₁ : HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
  (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
  Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
Tactic: rw [← SeparationQuotient.uniformity_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Completion (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
⊢ IsUltraUniformity.{u_1} (SeparationQuotient X)
have h_symm : ∀ (i : SetRel X X),
  i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans →
    SetRel.IsSymm (α := SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i)
Tactic: apply mk_of_hasBasis this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Completion (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
h_symm :
  ∀ (i : SetRel X X),
    i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans →
      SetRel.IsSymm (α := SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i)
⊢ IsUltraUniformity.{u_1} (SeparationQuotient X)
have h_trans : ∀ (i : SetRel X X),
  i ∈ 𝓤 X ∧ i.IsSymm ∧ i.IsTrans →
    SetRel.IsTrans (α := SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i)
Tactic: apply mk_of_hasBasis this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Completion (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
x : SetRel X X
h : x ∈ 𝓤 X ∧ x.IsSymm ∧ x.IsTrans
left : x ∈ 𝓤 X
hU : x.IsSymm
right : x.IsTrans
⊢ SetRel.IsSymm (α := SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id x)
have simp : SetRel.IsSymm (α := SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' x)
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Completion (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left : U.IsSymm
hU : U.IsTrans
⊢ SetRel.IsTrans (α := SeparationQuotient X) (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U)
have h_trans : ∀ (a b c : SeparationQuotient X),
  Membership.mem (γ := SetRel (SeparationQuotient X) (SeparationQuotient X))
      (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U) (a, b) →
    Membership.mem (γ := SetRel (SeparationQuotient X) (SeparationQuotient X))
        (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U) (b, c) →
      Membership.mem (γ := SetRel (SeparationQuotient X) (SeparationQuotient X))
        (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U) (a, c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Completion (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : UniformSpace Y
inst_2 : IsUltraUniformity X
this :
  HasBasis (α := SeparationQuotient X × SeparationQuotient X) (𝓤 (SeparationQuotient X))
    (fun (s : SetRel X X) ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun (i : SetRel X X) ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left : U.IsSymm
hU : U.IsTrans
x y z : SeparationQuotient X
⊢ Membership.mem (γ := SetRel (SeparationQuotient X) (SeparationQuotient X))
      (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U) (x, y) →
    Membership.mem (γ := SetRel (SeparationQuotient X) (SeparationQuotient X))
        (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U) (y, z) →
      Membership.mem (γ := SetRel (SeparationQuotient X) (SeparationQuotient X))
        (Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id U) (x, z)
have h_trans : ∀ (x_1 x_2 : X),
  (x_1, x_2) ∈ U →
    SeparationQuotient.mk x_1 = x →
      SeparationQuotient.mk x_2 = y →
        ∀ (x_3 x_4 : X),
          (x_3, x_4) ∈ U →
            SeparationQuotient.mk x_3 = y →
              SeparationQuotient.mk x_4 = z →
                ∃ (a : X) (b : X), (a, b) ∈ U ∧ SeparationQuotient.mk a = x ∧ SeparationQuotient.mk b = z
Tactic: simp only [id_eq, Set.mem_image, Prod.exists, Prod.map_apply, Prod.mk.injEq,
      forall_exists_index, and_imp]