awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
γ : Type uγ
inst_1 : TopologicalSpace γ
inst_2 : T3Space γ
f : α → γ
cont_f : Continuous[inst.toTopologicalSpace, inst_1] f
x : UniformSpace pkg'.space := pkg'.uniformStruct
x_1 : UniformSpace pkg.space := pkg.uniformStruct
h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))
this : ∀ (x : α), (⋯.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x
hf : ∀ (b : pkg.space), ∃ (c : γ), Tendsto f (comap pkg.coe (𝓝 b)) (𝓝 c)
⊢ Continuous[_, inst_1] (⋯.extend f)

Tactic:
apply IsDenseInducing.continuous_extend

Premises used: IsDenseInducing.continuous_extend
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
γ : Type uγ
inst_1 : TopologicalSpace γ
inst_2 : T3Space γ
f : α → γ
cont_f : Continuous[inst.toTopologicalSpace, inst_1] f
x : UniformSpace pkg'.space := pkg'.uniformStruct
x_1 : UniformSpace pkg.space := pkg.uniformStruct
h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))
this : ∀ (x : α), (⋯.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x
⊢ ∀ (b : pkg.space), ∃ (c : γ), Tendsto f (comap pkg.coe (𝓝 b)) (𝓝 c)

Tactic:
fun a ↦ ⟨(pkg.isDenseInducing.extend f) a, h a⟩

Premises used: Exists.intro, IsDenseInducing.extend, AbstractCompletion.isDenseInducing
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
pkg' : AbstractCompletion.{vα', uα} α
γ : Type uγ
inst_1 : TopologicalSpace γ
inst_2 : T3Space γ
f : α → γ
cont_f : Continuous[inst.toTopologicalSpace, inst_1] f
x : UniformSpace pkg'.space := pkg'.uniformStruct
x_1 : UniformSpace pkg.space := pkg.uniformStruct
h : ∀ (a : pkg.space), Tendsto f (comap pkg.coe (𝓝 a)) (𝓝 (⋯.extend f a))
this : ∀ (x : α), (⋯.extend f ∘ pkg'.compare pkg) (pkg'.coe x) = f x
⊢ ∀ (b : pkg.space), ∃ (c : γ), Tendsto f (comap pkg.coe (𝓝 b)) (𝓝 c)

Tactic:
exact fun a ↦ ⟨(pkg.isDenseInducing.extend f) a, h a⟩
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst_2 : UniformSpace γ
inst_3 : T0Space γ
f : α → β → γ
hf : UniformContinuous (uncurry f)
a : α
b : β
⊢ pkg.extend₂ pkg' f (pkg.coe a) (pkg'.coe b) = f a b

Tactic:
show (pkg.prod pkg').extend (uncurry f) ((pkg.prod pkg').coe (a, b)) = uncurry f (a, b) from
    (pkg.prod pkg').extend_coe hf _

Premises used: AbstractCompletion.extend₂, Prod.mk, AbstractCompletion.extend_coe, AbstractCompletion.prod, AbstractCompletion.extend, ite
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst_2 : UniformSpace γ
f : α → β → γ
inst_3 : CompleteSpace γ
rw : UniformContinuous ((pkg.prod pkg').extend (uncurry f))
⊢ UniformContinuous₂ (pkg.extend₂ pkg' f)

Tactic:
rw [uniformContinuous₂_def, AbstractCompletion.extend₂, uncurry_curry]

Premises used: Function.uncurry_curry, uniformContinuous₂_def, AbstractCompletion.extend₂
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{vβ, uβ} β
γ : Type uγ
inst_2 : UniformSpace γ
f : α → β → γ
inst_3 : CompleteSpace γ
⊢ UniformContinuous ((pkg.prod pkg').extend (uncurry f))

Tactic:
apply uniformContinuous_extend

Premises used: AbstractCompletion.uniformContinuous_extend
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{u_1, uβ} β
γ : Type uγ
inst_2 : UniformSpace γ
pkg'' : AbstractCompletion.{vγ, uγ} γ
f : α → β → γ
⊢ UniformContinuous₂ (pkg.map₂ pkg' pkg'' f)

Tactic:
AbstractCompletion.uniformContinuous_extension₂ pkg pkg' _

Premises used: AbstractCompletion.map₂, AbstractCompletion.uniformContinuous_extension₂
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{u_2, uβ} β
γ : Type uγ
inst_2 : UniformSpace γ
pkg'' : AbstractCompletion.{vγ, uγ} γ
δ : Type u_1
inst_3 : TopologicalSpace δ
f : α → β → γ
a : δ → pkg.space
b : δ → pkg'.space
ha : Continuous a
hb : Continuous b
⊢ Continuous.{u_1, vγ} (Y := pkg''.space) fun (d : δ) ↦ pkg.map₂ pkg' pkg'' f (a d) (b d)

Tactic:
(pkg.uniformContinuous_map₂ pkg' pkg'' f).continuous.comp₂ ha hb

Premises used: AbstractCompletion.uniformContinuous_map₂, Continuous.comp₂, AbstractCompletion.extend₂, UniformContinuous.continuous, AbstractCompletion.map₂, AbstractCompletion.extend, ite
-- Module: Mathlib.Topology.UniformSpace.AbstractCompletion
Goal:
α : Type uα
inst : UniformSpace α
pkg : AbstractCompletion.{vα, uα} α
β : Type uβ
inst_1 : UniformSpace β
pkg' : AbstractCompletion.{u_1, uβ} β
γ : Type uγ
inst_2 : UniformSpace γ
pkg'' : AbstractCompletion.{vγ, uγ} γ
a : α
b : β
f : α → β → γ
hf : UniformContinuous₂ f
⊢ pkg.map₂ pkg' pkg'' f (pkg.coe a) (pkg'.coe b) = pkg''.coe (f a b)

Tactic:
pkg.extension₂_coe_coe (f := pkg''.coe ∘₂ f) pkg' (pkg''.uniformContinuous_coe.comp hf) a b

Premises used: AbstractCompletion.uniformContinuous_coe, AbstractCompletion.extension₂_coe_coe, UniformContinuous.comp, AbstractCompletion.map₂, Function.bicompr
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
⊢ UniformSpace.comap F (UniformFun.uniformSpace X α) = UniformSpace.comap F (Pi.uniformSpace fun (i : X) ↦ α)

Tactic:
le_antisymm (UniformSpace.comap_mono UniformFun.uniformContinuous_toFun) ?_

Premises used: le_antisymm, UniformSpace.comap_mono, UniformFun.uniformContinuous_toFun
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
refine : UniformSpace.comap F (Pi.uniformSpace fun (i : X) ↦ α) ≤ UniformSpace.comap F (UniformFun.uniformSpace X α)
⊢ UniformSpace.comap F (UniformFun.uniformSpace X α) = UniformSpace.comap F (Pi.uniformSpace fun (i : X) ↦ α)

Tactic:
refine le_antisymm (UniformSpace.comap_mono UniformFun.uniformContinuous_toFun) ?_

Premises used: le_antisymm, UniformSpace.comap_mono
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
simp_rw :
  ⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α) ≤
    comap (Prod.map F F) (𝓤 (X → α))
⊢ UniformSpace.comap F (Pi.uniformSpace fun (i : X) ↦ α) ≤ UniformSpace.comap F (UniformFun.uniformSpace X α)

Tactic:
simp_rw [UniformSpace.comap, UniformSpace.le_def, uniformity_comap, Pi.uniformity,
    Filter.comap_iInf, comap_comap, Function.comp_def]

Premises used: Filter.comap_iInf, Function.comp_def, UniformSpace.le_def, Filter.comap_comap, UniformSpace.comap, uniformity_comap, Pi.uniformity
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
⊢ ⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α) ≤
    comap (Prod.map F F) (𝓤 (X → α))

Tactic:
((UniformFun.hasBasis_uniformity X α).comap (Prod.map F F)).ge_iff.mpr ?_

Premises used: Iff.mpr, Set.Mem, UniformFun.hasBasis_uniformity, setOf, Prod.map, Filter.HasBasis.ge_iff, Filter.HasBasis.comap
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
refine :
  ∀ i' ∈ 𝓤 α,
    Membership.mem (γ := Filter (ι × ι))
      (⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α))
      (Prod.map F F ⁻¹' UniformFun.gen X α i')
⊢ ⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α) ≤
    comap (Prod.map F F) (𝓤 (X → α))

Tactic:
refine ((UniformFun.hasBasis_uniformity X α).comap (Prod.map F F)).ge_iff.mpr ?_

Premises used: Iff.mpr, UniformFun.hasBasis_uniformity, Prod.map, Filter.HasBasis.ge_iff, Filter.HasBasis.comap
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
rcases :
  ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (Vsymm : SetRel.IsSymm V) (hVU : (SetRel.comp V V).comp V ⊆ U),
    Membership.mem (γ := Filter (ι × ι))
      (⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α))
      (Prod.map F F ⁻¹' UniformFun.gen X α U)
⊢ Membership.mem (γ := Filter (ι × ι))
    (⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α))
    (Prod.map F F ⁻¹' UniformFun.gen X α U)

Tactic:
rcases comp_comp_symm_mem_uniformity_sets hU with ⟨V, hV, Vsymm, hVU⟩

Premises used: comp_comp_symm_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : (x : X) → Set X := fun (x : X) ↦ {y : X | ∀ (i : ι), (F i x, F i y) ∈ V}
rcases :
  ∀ (A : Finset X) (Acover : Eq.{u_2 + 1} (α := Set X) (⋃ x ∈ A, Ω x) ⊤),
    Membership.mem (γ := Filter (ι × ι))
      (⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α))
      (Prod.map F F ⁻¹' UniformFun.gen X α U)
⊢ Membership.mem (γ := Filter (ι × ι))
    (⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α))
    (Prod.map F F ⁻¹' UniformFun.gen X α U)

Tactic:
rcases CompactSpace.elim_nhds_subcover Ω (fun x ↦ F_eqcont x V hV) with ⟨A, Acover⟩

Premises used: CompactSpace.elim_nhds_subcover
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : (x : X) → Set X := fun (x : X) ↦ {y : X | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : Eq.{u_2 + 1} (α := Set X) (⋃ x ∈ A, Ω x) ⊤
i j : ι
hij : Membership.mem (γ := Set (ι × ι)) (⋂ a ∈ A, {ij : ι × ι | (F ij.1 a, F ij.2 a) ∈ V}) (i, j)
x : X
rw :
  ∀
    (hij :
      ∀ (i_1 : X) (j_1 : i_1 ∈ A), Membership.mem (γ := Set (ι × ι)) {ij : ι × ι | (F ij.1 i_1, F ij.2 i_1) ∈ V} (i, j))
    (x : X),
    Membership.mem (α := α × α) U
      (((UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).1 x,
          (UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).2 x) :
        α × α)
⊢ Membership.mem (α := α × α) U
    (((UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).1 x,
        (UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).2 x) :
      α × α)

Tactic:
rw [mem_iInter₂] at hij

Premises used: Set.mem_iInter₂
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : (x : X) → Set X := fun (x : X) ↦ {y : X | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : Eq.{u_2 + 1} (α := Set X) (⋃ x ∈ A, Ω x) ⊤
i j : ι
hij : ∀ (i_1 : X) (j_1 : i_1 ∈ A), Membership.mem (γ := Set (ι × ι)) {ij : ι × ι | (F ij.1 i_1, F ij.2 i_1) ∈ V} (i, j)
x : X
rcases :
  ∀ (a : X) (ha : a ∈ A) (hax : x ∈ Ω a),
    Membership.mem (α := α × α) U
      (((UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).1 x,
          (UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).2 x) :
        α × α)
⊢ Membership.mem (α := α × α) U
    (((UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).1 x,
        (UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).2 x) :
      α × α)

Tactic:
rcases mem_iUnion₂.mp (Acover.symm.subset <| mem_univ x) with ⟨a, ha, hax⟩

Premises used: Set.mem_iUnion₂, Eq.subset, Iff.mp, Set.mem_univ, Eq.symm
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : (x : X) → Set X := fun (x : X) ↦ {y : X | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : Eq.{u_2 + 1} (α := Set X) (⋃ x ∈ A, Ω x) ⊤
i j : ι
hij : ∀ (i_1 : X) (j_1 : i_1 ∈ A), Membership.mem (γ := Set (ι × ι)) {ij : ι × ι | (F ij.1 i_1, F ij.2 i_1) ∈ V} (i, j)
x a : X
ha : a ∈ A
hax : x ∈ Ω a
⊢ Membership.mem (α := α × α) U
    (((UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).1 x,
        (UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).2 x) :
      α × α)

Tactic:
hVU <| SetRel.prodMk_mem_comp (SetRel.prodMk_mem_comp (SetRel.symm V <| hax i) (hij a ha))
      (hax j)

Premises used: SetRel.symm, SetRel.prodMk_mem_comp
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : (x : X) → Set X := fun (x : X) ↦ {y : X | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : Eq.{u_2 + 1} (α := Set X) (⋃ x ∈ A, Ω x) ⊤
i j : ι
hij : ∀ (i_1 : X) (j_1 : i_1 ∈ A), Membership.mem (γ := Set (ι × ι)) {ij : ι × ι | (F ij.1 i_1, F ij.2 i_1) ∈ V} (i, j)
x a : X
ha : a ∈ A
hax : x ∈ Ω a
⊢ Membership.mem (α := α × α) U
    (((UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).1 x,
        (UniformFun.toFun : (a : X →ᵤ α) → X → α) (Prod.map F F (i, j)).2 x) :
      α × α)

Tactic:
exact hVU <| SetRel.prodMk_mem_comp (SetRel.prodMk_mem_comp (SetRel.symm V <| hax i) (hij a ha))
      (hax j)

Premises used: SetRel.symm, SetRel.prodMk_mem_comp
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : (x : X) → Set X := fun (x : X) ↦ {y : X | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : Eq.{u_2 + 1} (α := Set X) (⋃ x ∈ A, Ω x) ⊤
⊢ ⋂ a ∈ A, {ij : ι × ι | (F ij.1 a, F ij.2 a) ∈ V} ⊆ Prod.map F F ⁻¹' UniformFun.gen X α U

Tactic:
have : (⋂ a ∈ A, {ij : ι × ι | (F ij.1 a, F ij.2 a) ∈ V}) ⊆
      (Prod.map F F) ⁻¹' UniformFun.gen X α U := by
    -- Given `(i, j) ∈ ⋂ a ∈ A, 𝐒(V, a)` and `x : X`, we have to prove that `(F i x, F j x) ∈ U`.
    rintro ⟨i, j⟩ hij x
    rw [mem_iInter₂] at hij
    -- We know that `x ∈ Ω a` for some `a ∈ A`, so that both `(F i x, F i a)` and `(F j a, F j x)`
    -- are in `V`.
    rcases mem_iUnion₂.mp (Acover.symm.subset <| mem_univ x) with ⟨a, ha, hax⟩
    -- Since `(i, j) ∈ 𝐒(V, a)` we also have `(F i a, F j a) ∈ V`, and finally we get
    -- `(F i x, F j x) ∈ V ○ V ○ V ⊆ U`.
    exact hVU <| SetRel.prodMk_mem_comp (SetRel.prodMk_mem_comp (SetRel.symm V <| hax i) (hij a ha))
      (hax j)
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : (x : X) → Set X := fun (x : X) ↦ {y : X | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : Eq.{u_2 + 1} (α := Set X) (⋃ x ∈ A, Ω x) ⊤
this : ⋂ a ∈ A, {ij : ι × ι | (F ij.1 a, F ij.2 a) ∈ V} ⊆ Prod.map F F ⁻¹' UniformFun.gen X α U
⊢ Membership.mem (γ := Filter (ι × ι))
    (⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α))
    (Prod.map F F ⁻¹' UniformFun.gen X α U)

Tactic:
mem_of_superset
    (A.iInter_mem_sets.mpr fun x _ ↦ mem_iInf_of_mem x <| preimage_mem_comap hV) this

Premises used: Iff.mpr, Filter.mem_iInf_of_mem, Finset.iInter_mem_sets, Filter.preimage_mem_comap, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : (x : X) → Set X := fun (x : X) ↦ {y : X | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : Eq.{u_2 + 1} (α := Set X) (⋃ x ∈ A, Ω x) ⊤
this : ⋂ a ∈ A, {ij : ι × ι | (F ij.1 a, F ij.2 a) ∈ V} ⊆ Prod.map F F ⁻¹' UniformFun.gen X α U
⊢ Membership.mem (γ := Filter (ι × ι))
    (⨅ (i : X), comap (fun (x : ι × ι) ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α))
    (Prod.map F F ⁻¹' UniformFun.gen X α U)

Tactic:
exact mem_of_superset
    (A.iInter_mem_sets.mpr fun x _ ↦ mem_iInf_of_mem x <| preimage_mem_comap hV) this

Premises used: Iff.mpr, Filter.mem_iInf_of_mem, Finset.iInter_mem_sets, Filter.preimage_mem_comap, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : UniformSpace ι
inst_3 : CompactSpace X
F_eqcont : Equicontinuous F
rw :
  UniformSpace.comap ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F) (UniformFun.uniformSpace X α) = inst_2 ↔
    UniformSpace.comap F (UniformFun.uniformSpace X α) = inst_2
⊢ IsUniformInducing (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F) ↔ IsUniformInducing F

Tactic:
rw [isUniformInducing_iff_uniformSpace, isUniformInducing_iff_uniformSpace,
      ← F_eqcont.comap_uniformFun_eq]

Premises used: Equicontinuous.comap_uniformFun_eq, isUniformInducing_iff_uniformSpace
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : UniformSpace ι
inst_3 : CompactSpace X
F_eqcont : Equicontinuous F
⊢ UniformSpace.comap ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F) (UniformFun.uniformSpace X α) = inst_2 ↔
    UniformSpace.comap F (UniformFun.uniformSpace X α) = inst_2

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : TopologicalSpace ι
inst_3 : CompactSpace X
F_eqcont : Equicontinuous F
rw :
  inst_2 = TopologicalSpace.induced ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F) (UniformFun.topologicalSpace X α) ↔
    inst_2 = TopologicalSpace.induced F (Pi.topologicalSpace (Y := fun (a : X) ↦ α))
⊢ IsInducing (Y := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F) ↔ IsInducing F

Tactic:
rw [isInducing_iff, isInducing_iff]

Premises used: Topology.isInducing_iff
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : TopologicalSpace ι
inst_3 : CompactSpace X
F_eqcont : Equicontinuous F
change : inst_2 = UniformSpace.toTopologicalSpace ↔ inst_2 = UniformSpace.toTopologicalSpace
⊢ inst_2 = TopologicalSpace.induced ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F) (UniformFun.topologicalSpace X α) ↔
    inst_2 = TopologicalSpace.induced F (Pi.topologicalSpace (Y := fun (a : X) ↦ α))

Tactic:
change (_ = (UniformFun.uniformSpace X α |>.comap F |>.toTopologicalSpace)) ↔
         (_ = (Pi.uniformSpace _ |>.comap F |>.toTopologicalSpace))

Premises used: UniformSpace.toTopologicalSpace, Eq
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : TopologicalSpace ι
inst_3 : CompactSpace X
F_eqcont : Equicontinuous F
rw rw₁ : inst_2 = UniformSpace.toTopologicalSpace ↔ inst_2 = UniformSpace.toTopologicalSpace
⊢ inst_2 = UniformSpace.toTopologicalSpace ↔ inst_2 = UniformSpace.toTopologicalSpace

Tactic:
rw [F_eqcont.comap_uniformFun_eq]

Premises used: Equicontinuous.comap_uniformFun_eq
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
inl :
  Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ⊥
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) ↔
    Tendsto F ⊥ (𝓝 f)
inr :
  ∀ (ℱ_ne : ℱ.NeBot),
    Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
        (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) ↔
      Tendsto F ℱ (𝓝 f)
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) ↔
    Tendsto F ℱ (𝓝 f)

Tactic:
rcases ℱ.eq_or_neBot with rfl | ℱ_ne

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
f : X → α
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ⊥
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) ↔
    Tendsto F ⊥ (𝓝 f)

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
inr :
  Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) →
    Tendsto F ℱ (𝓝 f)
inr₁ :
  Tendsto F ℱ (𝓝 f) →
    Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) ↔
    Tendsto F ℱ (𝓝 f)

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H :
  Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
⊢ Tendsto F ℱ (𝓝 f)

Tactic:
UniformFun.uniformContinuous_toFun.continuous.tendsto _ |>.comp H

Premises used: UniformContinuous.continuous, Continuous.tendsto, UniformFun.uniformContinuous_toFun, Filter.Tendsto.comp