awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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) (𝓤 (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
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : Eq (α := SeparationQuotient X) (SeparationQuotient.mk c) (SeparationQuotient.mk b)
⊢ (b, c) ∈ U
have hc₁ : ∀ s ∈ 𝓤 X, (b, c) ∈ s
Tactic: rw [eq_comm, SeparationQuotient.mk_eq_mk, inseparable_iff_ker_uniformity,
          Filter.mem_ker] at hc
Cleared hypotheses: hc
-- 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) (𝓤 (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
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : Eq (α := SeparationQuotient X) (SeparationQuotient.mk c) (SeparationQuotient.mk b)
⊢ ∃ (a_1 : X) (b : X),
    (a_1, b) ∈ U ∧
      Eq (α := SeparationQuotient X) (SeparationQuotient.mk a_1) (SeparationQuotient.mk a) ∧
        Eq (α := SeparationQuotient X) (SeparationQuotient.mk b) (SeparationQuotient.mk d)
have hbc : (b, c) ∈ U
Tactic: have hbc : (b, c) ∈ U := by
      rw [eq_comm, SeparationQuotient.mk_eq_mk, inseparable_iff_ker_uniformity,
          Filter.mem_ker] at hc
      exact hc _ hU'
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Completion (goal)
Goal:
X : Type u_1
inst : UniformSpace X
⊢ IsUltraUniformity.{u_1} (UniformSpace.Completion X) ↔ IsUltraUniformity X
have rw : IsUltraUniformity.{u_1} (SeparationQuotient (CauchyFilter X)) ↔ IsUltraUniformity.{u_1} (UniformSpace.Completion X)
Tactic: rw [iff_comm, ← cauchyFilter_iff, ← separationQuotient_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
⊢ IsUltraUniformity X
have refine_1 : ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsSymm (Prod.map f f ⁻¹' id i)
Tactic: refine .mk_of_hasBasis (h.hasBasis.comap (Prod.map f f)) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_2
u : UniformSpace Y
h : IsUltraUniformity Y
f : X → Y
this : UniformSpace X := UniformSpace.comap f u
refine_1 : ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsSymm (Prod.map f f ⁻¹' id i)
⊢ IsUltraUniformity X
have refine_2 : ∀ (i : SetRel Y Y), i ∈ uniformity Y ∧ i.IsSymm ∧ i.IsTrans → SetRel.IsTrans (Prod.map f f ⁻¹' id i)
Tactic: refine .mk_of_hasBasis (h.hasBasis.comap (Prod.map f f)) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
⊢ IsUltraUniformity X
have refine_1 : ∀ (i : SetRel X X × SetRel X X),
  (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
    SetRel.IsSymm (id i.1 ∩ id i.2)
Tactic: refine .mk_of_hasBasis (h.hasBasis.inf h'.hasBasis) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
refine_1 :
  ∀ (i : SetRel X X × SetRel X X),
    (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
      SetRel.IsSymm (id i.1 ∩ id i.2)
⊢ IsUltraUniformity X
have refine_2 : ∀ (i : SetRel X X × SetRel X X),
  (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
    SetRel.IsTrans (id i.1 ∩ id i.2)
Tactic: refine .mk_of_hasBasis (h.hasBasis.inf h'.hasBasis) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
ι : Type u_3
U : (i : ι) → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ (i : ι), U i
⊢ IsUltraUniformity X
have refine_1 : ∀ (i : (I : Set ι) × ((i : (↑I : Type u_3)) → SetRel X X)),
  (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X).Finite ∧
      ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
        i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1 ∈ uniformity X ∧
          (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsSymm ∧
            (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsTrans) →
    SetRel.IsSymm.{u_1} (α := X)
      (⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
        id (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1))
Tactic: refine .mk_of_hasBasis (iInf_uniformity ▸ Filter.HasBasis.iInf fun i ↦ (hU i).hasBasis) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
ι : Type u_3
U : (i : ι) → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ (i : ι), U i
refine_1 :
  ∀ (i : (I : Set ι) × ((i : (↑I : Type u_3)) → SetRel X X)),
    (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X).Finite ∧
        ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
          i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1 ∈ uniformity X ∧
            (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsSymm ∧
              (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsTrans) →
      SetRel.IsSymm.{u_1} (α := X)
        (⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
          id (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1))
⊢ IsUltraUniformity X
have refine_2 : ∀ (i : (I : Set ι) × ((i : (↑I : Type u_3)) → SetRel X X)),
  (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X).Finite ∧
      ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
        i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1 ∈ uniformity X ∧
          (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsSymm ∧
            (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsTrans) →
    SetRel.IsTrans.{u_1} (α := X)
      (⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
        id (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1))
Tactic: refine .mk_of_hasBasis (iInf_uniformity ▸ Filter.HasBasis.iInf fun i ↦ (hU i).hasBasis) ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
ι : Type u_3
U : (i : ι) → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ (i : ι), U i
⊢ ∀ (i : (I : Set ι) × ((i : (↑I : Type u_3)) → SetRel X X)),
    (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X).Finite ∧
        ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
          i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1 ∈ uniformity X ∧
            (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsSymm ∧
              (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsTrans) →
      SetRel.IsSymm.{u_1} (α := X)
        (⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
          id (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1))
have refine_1 : ∀ (i : (I : Set ι) × ((i : (↑I : Type u_3)) → SetRel X X)),
  i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X).Finite →
    (∀ (a : ι) (b : a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)),
        i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)
            (Subtype.mk (p := fun (a : ι) ↦ a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) a
              b) ∈
          uniformity X) →
      (∀ (a : ι) (b : a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)),
          (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)
              (Subtype.mk (p := fun (a : ι) ↦ a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) a
                b)).IsSymm) →
        (∀ (a : ι) (b : a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)),
            (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)
                (Subtype.mk (p := fun (a : ι) ↦ a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) a
                  b)).IsTrans) →
          SetRel.IsSymm.{u_1} (α := X)
            (⋂ (i_1 : ι),
              ⋂ (h : i_1 ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)),
                i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X))
                    i_1 h))
Tactic: simp only [forall_and, Subtype.forall, id_eq, Set.iInter_coe_set, and_imp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
ι : Type u_3
U : (i : ι) → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ (i : ι), U i
⊢ ∀ (i : (I : Set ι) × ((i : (↑I : Type u_3)) → SetRel X X)),
    (i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X).Finite ∧
        ∀ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
          i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1 ∈ uniformity X ∧
            (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsSymm ∧
              (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1).IsTrans) →
      SetRel.IsTrans.{u_1} (α := X)
        (⋂ (i_1 : (↑(i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) : Type u_3)),
          id (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X) i_1))
have refine_2 : ∀ (i : (I : Set ι) × ((i : (↑I : Type u_3)) → SetRel X X)),
  i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X).Finite →
    (∀ (a : ι) (b : a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)),
        i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)
            (Subtype.mk (p := fun (a : ι) ↦ a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) a
              b) ∈
          uniformity X) →
      (∀ (a : ι) (b : a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)),
          (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)
              (Subtype.mk (p := fun (a : ι) ↦ a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) a
                b)).IsSymm) →
        (∀ (a : ι) (b : a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)),
            (i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)
                (Subtype.mk (p := fun (a : ι) ↦ a ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)) a
                  b)).IsTrans) →
          SetRel.IsTrans.{u_1} (α := X)
            (⋂ (i_1 : ι),
              ⋂ (h : i_1 ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)),
                i.snd (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X)
                  (Subtype.mk (p := fun (x : ι) ↦ x ∈ i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X))
                    i_1 h))
Tactic: simp only [forall_and, Subtype.forall, id_eq, Set.iInter_coe_set, and_imp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X_1 : Type u_1
Y : Type u_2
ι : Type u_3
X : ι → Type u_4
U : (i : ι) → UniformSpace (X i)
h : ∀ (i : ι), IsUltraUniformity.{u_4} (X i)
⊢ IsUltraUniformity ((i : ι) → X i)
have suffices : IsUltraUniformity ((x : ι) → X x)
Tactic: suffices @IsUltraUniformity _ (⨅ i, UniformSpace.comap (Function.eval i) (U i)) by
    simpa +instances [Pi.uniformSpace_eq _] using this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : DiscreteUniformity X
⊢ IsUltraUniformity X
have this : Filter.HasBasis.{u_1, 1} (α := X × X) (Filter.principal SetRel.id) (fun (x : Unit) ↦ True) fun (x : Unit) ↦ SetRel.id
Tactic: have := Filter.hasBasis_principal (SetRel.id (α := X))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (hypothesis)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : DiscreteUniformity X
this :
  Filter.HasBasis.{u_1, 1} (α := X × X) (Filter.principal SetRel.id) (fun (x : Unit) ↦ True) fun (x : Unit) ↦ SetRel.id
⊢ IsUltraUniformity X
have this₁ : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ SetRel.id
Tactic: rw [← DiscreteUniformity.eq_principal_setRelId] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : DiscreteUniformity X
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ SetRel.id
⊢ IsUltraUniformity X
have h_symm : ∀ (i : Unit), True → SetRel.IsSymm.{u_1} (α := X) SetRel.id
Tactic: apply mk_of_hasBasis this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : DiscreteUniformity X
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ SetRel.id
h_symm : ∀ (i : Unit), True → SetRel.IsSymm.{u_1} (α := X) SetRel.id
⊢ IsUltraUniformity X
have h_trans : ∀ (i : Unit), True → SetRel.IsTrans.{u_1} (α := X) SetRel.id
Tactic: apply mk_of_hasBasis this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : DiscreteUniformity X
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ SetRel.id
⊢ ∀ (i : Unit), True → SetRel.IsSymm.{u_1} (α := X) SetRel.id
have h_symm : SetRel.IsSymm.{u_1} (α := X) SetRel.id
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : DiscreteUniformity X
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ SetRel.id
⊢ ∀ (i : Unit), True → SetRel.IsSymm.{u_1} (α := X) SetRel.id
have h_symm : SetRel.IsSymm.{u_1} (α := X) SetRel.id
Tactic: { simp; infer_instance }
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : DiscreteUniformity X
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ SetRel.id
⊢ ∀ (i : Unit), True → SetRel.IsTrans.{u_1} (α := X) SetRel.id
have h_trans : SetRel.IsTrans.{u_1} (α := X) SetRel.id
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : DiscreteUniformity X
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ SetRel.id
⊢ ∀ (i : Unit), True → SetRel.IsTrans.{u_1} (α := X) SetRel.id
have h_trans : SetRel.IsTrans.{u_1} (α := X) SetRel.id
Tactic: { simp; infer_instance }
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (hypothesis)
Goal:
X : Type u_1
this : UniformSpace X := ⊤
⊢ IsUltraUniformity X
have this₁ : Filter.HasBasis.{u_1, 1} (α := X × X) ⊤ (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
Tactic: have := Filter.hasBasis_top (α := (X × X))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (hypothesis)
Goal:
X : Type u_1
this_1 : UniformSpace X := ⊤
this : Filter.HasBasis.{u_1, 1} (α := X × X) ⊤ (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
⊢ IsUltraUniformity X
have this₁ : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
Tactic: rw [← top_uniformity] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
this_1 : UniformSpace X := ⊤
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
⊢ IsUltraUniformity X
have h_symm : ∀ (i : Unit), True → SetRel.IsSymm.{u_1} (α := X) Set.univ
Tactic: apply mk_of_hasBasis this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
this_1 : UniformSpace X := ⊤
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
h_symm : ∀ (i : Unit), True → SetRel.IsSymm.{u_1} (α := X) Set.univ
⊢ IsUltraUniformity X
have h_trans : ∀ (i : Unit), True → SetRel.IsTrans.{u_1} (α := X) Set.univ
Tactic: apply mk_of_hasBasis this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
this_1 : UniformSpace X := ⊤
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
⊢ ∀ (i : Unit), True → SetRel.IsSymm.{u_1} (α := X) Set.univ
have h_symm : SetRel.IsSymm.{u_1} (α := X) Set.univ
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
this_1 : UniformSpace X := ⊤
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
⊢ ∀ (i : Unit), True → SetRel.IsSymm.{u_1} (α := X) Set.univ
have h_symm : SetRel.IsSymm.{u_1} (α := X) Set.univ
Tactic: { simp; infer_instance }
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
this_1 : UniformSpace X := ⊤
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
⊢ ∀ (i : Unit), True → SetRel.IsTrans.{u_1} (α := X) Set.univ
have h_trans : SetRel.IsTrans.{u_1} (α := X) Set.univ
Tactic: simp
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ultra.Constructions (goal)
Goal:
X : Type u_1
this_1 : UniformSpace X := ⊤
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
⊢ ∀ (i : Unit), True → SetRel.IsTrans.{u_1} (α := X) Set.univ
have h_trans : SetRel.IsTrans.{u_1} (α := X) Set.univ
Tactic: { simp; infer_instance }
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ContinuousWithinAt f s x
have refine : ∀ (u₀ : Set (β × β)) (hu₀ : u₀ ∈ 𝓤 β),
  Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) u₀
Tactic: refine Uniform.continuousWithinAt_iff'_left.2 fun u₀ hu₀ => ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) u₀
have obtain : ∀ (u₁ : Set (β × β)) (h₁ : u₁ ∈ 𝓤 β) (u₁₀ : u₁ ○ u₁ ⊆ u₀),
  Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) u₀
Tactic: obtain ⟨u₁, h₁, u₁₀⟩ : ∃ u ∈ 𝓤 β, u ○ u ⊆ u₀ := comp_mem_uniformity_sets hu₀
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) u₀
have obtain : ∀ (u₂ : Set (β × β)) (h₂ : u₂ ∈ 𝓤 β) (hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂) (u₂₁ : u₂ ○ u₂ ⊆ u₁),
  Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) u₀
Tactic: obtain ⟨u₂, h₂, hsymm, u₂₁⟩ : ∃ u ∈ 𝓤 β, (∀ {a b}, (a, b) ∈ u → (b, a) ∈ u) ∧ u ○ u ⊆ u₁ :=
    comp_symm_of_uniformity h₁
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) u₀
have rcases : ∀ (t : Set α) (tx : t ∈ 𝓝[s] x) (F : α → β) (hFc : ContinuousWithinAt F s x) (hF : ∀ y ∈ t, (f y, F y) ∈ u₂),
  Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) u₀
Tactic: rcases L u₂ h₂ with ⟨t, tx, F, hFc, hF⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
t : Set α
tx : t ∈ 𝓝[s] x
F : α → β
hFc : ContinuousWithinAt F s x
hF : ∀ y ∈ t, (f y, F y) ∈ u₂
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) u₀
have A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂
Tactic: have A : ∀ᶠ y in 𝓝[s] x, (f y, F y) ∈ u₂ := Eventually.mono tx hF
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
t : Set α
tx : t ∈ 𝓝[s] x
F : α → β
hFc : ContinuousWithinAt F s x
hF : ∀ y ∈ t, (f y, F y) ∈ u₂
A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) u₀
have B : ∀ᶠ (y : α) in 𝓝[s] x, (F y, F x) ∈ u₂
Tactic: have B : ∀ᶠ y in 𝓝[s] x, (F y, F x) ∈ u₂ := Uniform.continuousWithinAt_iff'_left.1 hFc h₂
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.UniformApproximation (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
t : Set α
tx : t ∈ 𝓝[s] x
F : α → β
hFc : ContinuousWithinAt F s x
hF : ∀ y ∈ t, (f y, F y) ∈ u₂
A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂
B : ∀ᶠ (y : α) in 𝓝[s] x, (F y, F x) ∈ u₂
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) u₀
have C : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F x) ∈ u₁
Tactic: have C : ∀ᶠ y in 𝓝[s] x, (f y, F x) ∈ u₁ :=
    (A.and B).mono fun y hy => u₂₁ (prodMk_mem_comp hy.1 hy.2)