awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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)
h : i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X).Finite
h_1 :
  ∀ (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
h_2 :
  ∀ (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
h_3 :
  ∀ (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:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
ι : Type u_3
U : (i : ι) → UniformSpace X
hU : ∀ (i : ι), IsUltraUniformity X
this : UniformSpace X := ⨅ (i : ι), U i
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))
⊢ ∀ (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:
simp only [forall_and, Subtype.forall, id_eq, Set.iInter_coe_set, and_imp]

Premises used: and_imp, Subtype.forall, Set.iInter_coe_set, forall_and, id_eq
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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)
h : i.fst (β := fun (I : Set ι) ↦ (i : (↑I : Type u_3)) → SetRel X X).Finite
h_1 :
  ∀ (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
h_2 :
  ∀ (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
h_3 :
  ∀ (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:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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)
this : IsUltraUniformity ((x : ι) → X x)
⊢ IsUltraUniformity ((i : ι) → X i)

Tactic:
simpa +instances [Pi.uniformSpace_eq _] using this

Premises used: Pi.uniformSpace_eq
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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)
suffices : IsUltraUniformity ((x : ι) → X x)
⊢ IsUltraUniformity ((i : ι) → X i)

Tactic:
suffices @IsUltraUniformity _ (⨅ i, UniformSpace.comap (Function.eval i) (U i)) by
    simpa +instances [Pi.uniformSpace_eq _] using this
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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 ((x : ι) → X x)

Tactic:
.iInf fun i ↦ .comap (h i) (Function.eval i)

Premises used: Function.eval, IsUltraUniformity.iInf, IsUltraUniformity.comap
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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 ((x : ι) → X x)

Tactic:
exact .iInf fun i ↦ .comap (h i) (Function.eval i)
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
Y : Type u_2
inst : UniformSpace X
inst_1 : DiscreteUniformity X
⊢ 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))
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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
⊢ (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ SetRel.id

Tactic:
rw [← DiscreteUniformity.eq_principal_setRelId] at this

Premises used: DiscreteUniformity.eq_principal_setRelId
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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
h_trans : ∀ (i : Unit), True → SetRel.IsTrans.{u_1} (α := X) SetRel.id
⊢ IsUltraUniformity X

Tactic:
apply mk_of_hasBasis this

Premises used: IsUltraUniformity.mk_of_hasBasis
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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 : SetRel.IsSymm.{u_1} (α := X) SetRel.id
⊢ ∀ (i : Unit), True → SetRel.IsSymm.{u_1} (α := X) SetRel.id

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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
⊢ SetRel.IsSymm.{u_1} (α := X) SetRel.id

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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 h_symm₁ : SetRel.IsSymm.{u_1} (α := X) SetRel.id
⊢ ∀ (i : Unit), True → SetRel.IsSymm.{u_1} (α := X) SetRel.id

Tactic:
{ simp; infer_instance }
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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_trans : SetRel.IsTrans.{u_1} (α := X) SetRel.id
⊢ ∀ (i : Unit), True → SetRel.IsTrans.{u_1} (α := X) SetRel.id

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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
⊢ SetRel.IsTrans.{u_1} (α := X) SetRel.id

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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_trans h_trans₁ : SetRel.IsTrans.{u_1} (α := X) SetRel.id
⊢ ∀ (i : Unit), True → SetRel.IsTrans.{u_1} (α := X) SetRel.id

Tactic:
{ simp; infer_instance }
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
this : UniformSpace X := ⊤
⊢ Filter.HasBasis.{u_1, 1} (α := X × X) ⊤ (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ

Tactic:
have := Filter.hasBasis_top (α := (X × X))
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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
⊢ (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ

Tactic:
rw [← top_uniformity] at this

Premises used: top_uniformity
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
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
h_trans : ∀ (i : Unit), True → SetRel.IsTrans.{u_1} (α := X) Set.univ
⊢ IsUltraUniformity X

Tactic:
apply mk_of_hasBasis this

Premises used: IsUltraUniformity.mk_of_hasBasis
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
this_1 : UniformSpace X := ⊤
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
h_symm : SetRel.IsSymm.{u_1} (α := X) Set.univ
⊢ ∀ (i : Unit), True → SetRel.IsSymm.{u_1} (α := X) Set.univ

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
this_1 : UniformSpace X := ⊤
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
⊢ SetRel.IsSymm.{u_1} (α := X) Set.univ

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
this_1 : UniformSpace X := ⊤
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
h_symm h_symm₁ : SetRel.IsSymm.{u_1} (α := X) Set.univ
⊢ ∀ (i : Unit), True → SetRel.IsSymm.{u_1} (α := X) Set.univ

Tactic:
{ simp; infer_instance }
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
this_1 : UniformSpace X := ⊤
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
h_trans : SetRel.IsTrans.{u_1} (α := X) Set.univ
⊢ ∀ (i : Unit), True → SetRel.IsTrans.{u_1} (α := X) Set.univ

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
this_1 : UniformSpace X := ⊤
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
⊢ SetRel.IsTrans.{u_1} (α := X) Set.univ

Tactic:
infer_instance
-- Module: Mathlib.Topology.UniformSpace.Ultra.Constructions
Goal:
X : Type u_1
this_1 : UniformSpace X := ⊤
this : (uniformity X).HasBasis (fun (x : Unit) ↦ True) fun (x : Unit) ↦ Set.univ
h_trans h_trans₁ : SetRel.IsTrans.{u_1} (α := X) Set.univ
⊢ ∀ (i : Unit), True → SetRel.IsTrans.{u_1} (α := X) Set.univ

Tactic:
{ simp; infer_instance }
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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

Tactic:
Uniform.continuousWithinAt_iff'_left.2 fun u₀ hu₀ => ?_

Premises used: Iff.mpr, Uniform.continuousWithinAt_iff'_left
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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
refine :
  ∀ (u₀ : Set (β × β)) (hu₀ : u₀ ∈ 𝓤 β),
    Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) u₀
⊢ ContinuousWithinAt f s x

Tactic:
refine Uniform.continuousWithinAt_iff'_left.2 fun u₀ hu₀ => ?_

Premises used: Iff.mpr, Uniform.continuousWithinAt_iff'_left
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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 ∈ 𝓤 β, u ○ u ⊆ u₀

Tactic:
comp_mem_uniformity_sets hu₀

Premises used: comp_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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₀ ∈ 𝓤 β
obtain :
  ∀ (u₁ : Set (β × β)) (h₁ : u₁ ∈ 𝓤 β) (u₁₀ : u₁ ○ u₁ ⊆ u₀),
    Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) 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₀

Premises used: uniformity, comp_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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 ∈ 𝓤 β, (∀ {a b : β}, (a, b) ∈ u → (b, a) ∈ u) ∧ u ○ u ⊆ u₁

Tactic:
comp_symm_of_uniformity h₁

Premises used: comp_symm_of_uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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₀
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₀
⊢ 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₁

Premises used: comp_symm_of_uniformity, uniformity
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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₁
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₀
⊢ 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⟩
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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₂
⊢ ∀ᶠ (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
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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₂
⊢ ∀ᶠ (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₂
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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₂
⊢ ∀ᶠ (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)
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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₂
C : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F x) ∈ u₁
⊢ (F x, f x) ∈ u₁

Tactic:
have : (F x, f x) ∈ u₁ :=
    u₂₁ (prodMk_mem_comp (refl_mem_uniformity h₂) (hsymm (A.self_of_nhdsWithin hx)))
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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₂
C : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F x) ∈ u₁
this : (F x, f x) ∈ u₁
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) u₀

Tactic:
C.mono fun y hy => u₁₀ <| prodMk_mem_comp hy this

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.Eventually.mono, Set.preimage, SetRel.prodMk_mem_comp
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
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₂
C : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F x) ∈ u₁
this : (F x, f x) ∈ u₁
⊢ Membership.mem (γ := Filter (β × β)) (map (fun (x_1 : α) ↦ (f x_1, f x)) (𝓝[s] x)) u₀

Tactic:
exact C.mono fun y hy => u₁₀ <| prodMk_mem_comp hy this

Premises used: Filter.Eventually.mono, SetRel.prodMk_mem_comp
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
x : α
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ (F : α → β), ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
rw : ContinuousWithinAt f univ x
⊢ ContinuousAt f x

Tactic:
rw [← continuousWithinAt_univ]

Premises used: continuousWithinAt_univ
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
x : α
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ (F : α → β), ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
apply : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∃ (F : α → β), ContinuousWithinAt F univ x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ContinuousWithinAt f univ x

Tactic:
apply continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt (mem_univ _) _

Premises used: Set.mem_univ, continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt
-- Module: Mathlib.Topology.UniformSpace.UniformApproximation
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : α → β
x : α
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝 x, ∃ (F : α → β), ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u
⊢ ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[univ] x, ∃ (F : α → β), ContinuousWithinAt F univ x ∧ ∀ y ∈ t, (f y, F y) ∈ u

Tactic:
simpa only [exists_prop, nhdsWithin_univ, continuousWithinAt_univ] using L

Premises used: nhdsWithin_univ, continuousWithinAt_univ, exists_prop