-- Mathlib/Topology/UniformSpace/Ascoli.lean
theorem Equicontinuous.comap_uniformFun_eq [CompactSpace X] (F_eqcont : Equicontinuous F) :
    (UniformFun.uniformSpace X α).comap F =
    (Pi.uniformSpace _).comap F

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α)

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

Result:
case intro.intro.intro
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
⊢ Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α)

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ UniformSpace.comap F (UniformFun.uniformSpace X α) = UniformSpace.comap F (Pi.uniformSpace fun i => α)

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

Result:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ UniformSpace.comap F (Pi.uniformSpace fun i => α) ≤ UniformSpace.comap F (UniformFun.uniformSpace X α)

Proof state:
case intro.intro.intro
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
Ω : X → Set X := fun x => {y | ∀ (i : ι), (F i x, F i y) ∈ V}
⊢ Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α)

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

Result:
case intro.intro.intro.intro
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
Ω : X → Set X := fun x => {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
⊢ Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α)

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
Ω : X → Set X := fun x => {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
⊢ ⋂ a ∈ A, {ij | (F ij.1 a, F ij.2 a) ∈ V} ⊆ Prod.map F F ⁻¹' UniformFun.gen X α U

Tactic:
rintro ⟨i, j⟩ hij x

Result:
case mk
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
Ω : X → Set X := fun x => {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
i j : ι
hij : (i, j) ∈ ⋂ a ∈ A, {ij | (F ij.1 a, F ij.2 a) ∈ V}
x : X
⊢ (UniformFun.toFun (Prod.map F F (i, j)).1 x, UniformFun.toFun (Prod.map F F (i, j)).2 x) ∈ U

Proof state:
case intro.intro.intro.intro
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
Ω : X → Set X := fun x => {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
⊢ Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α)

Tactic:
have : (⋂ a ∈ A, {ij : ι × ι | (F ij.1 a, F ij.2 a) ∈ V}) ⊆
    (Prod.map F F) ⁻¹' UniformFun.gen X α U := by
  rintro ⟨i, j⟩ hij x
  rw [mem_iInter₂] at hij
  rcases mem_iUnion₂.mp (Acover.symm.subset <| mem_univ x) with ⟨a, ha, hax⟩
  exact hVU (prod_mk_mem_compRel (prod_mk_mem_compRel
    (Vsymm.mk_mem_comm.mp (hax i)) (hij a ha)) (hax j))

Result:
case intro.intro.intro.intro
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
Ω : X → Set X := fun x => {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
this : ⋂ a ∈ A, {ij | (F ij.1 a, F ij.2 a) ∈ V} ⊆ Prod.map F F ⁻¹' UniformFun.gen X α U
⊢ Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α)

Proof state:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α) ≤ comap (fun p => (F p.1, F p.2)) (𝓤 (X → α))

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

Result:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ ∀ i' ∈ 𝓤 α, Prod.map F F ⁻¹' UniformFun.gen X α i' ∈ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α)

Proof state:
case intro.intro.intro.intro
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
Ω : X → Set X := fun x => {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
this : ⋂ a ∈ A, {ij | (F ij.1 a, F ij.2 a) ∈ V} ⊆ Prod.map F F ⁻¹' UniformFun.gen X α U
⊢ Prod.map F F ⁻¹' UniformFun.gen X α U ∈ ⨅ i, comap (fun x => (F x.1 i, F x.2 i)) (𝓤 α)

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

Result:
no goals

Proof state:
case mk
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
Ω : X → Set X := fun x => {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
i j : ι
hij : (i, j) ∈ ⋂ a ∈ A, {ij | (F ij.1 a, F ij.2 a) ∈ V}
x : X
⊢ (UniformFun.toFun (Prod.map F F (i, j)).1 x, UniformFun.toFun (Prod.map F F (i, j)).2 x) ∈ U

Tactic:
rw [mem_iInter₂] at hij

Result:
case mk
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SymmetricRel V
hVU : V ○ V ○ V ⊆ U
Ω : X → Set X := fun x => {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
i j : ι
hij : ∀ i_1 ∈ A, (i, j) ∈ {ij | (F ij.1 i_1, F ij.2 i_1) ∈ V}
x : X
⊢ (UniformFun.toFun (Prod.map F F (i, j)).1 x, UniformFun.toFun (Prod.map F F (i, j)).2 x) ∈ U