-- Mathlib/Topology/UniformSpace/CompactConvergence.lean
theorem uniformSpace_eq_iInf_precomp_of_cover {δ : ι → Type*} [∀ i, TopologicalSpace (δ i)]
    (φ : Π i, C(δ i, α)) (h_proper : ∀ i, IsProperMap (φ i))
    (h_lf : LocallyFinite fun i ↦ range (φ i)) (h_cover : ⋃ i, range (φ i) = univ) :
    (inferInstanceAs <| UniformSpace C(α, β)) = ⨅ i, .comap (comp · (φ i)) inferInstance

Proof state:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i => range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
⊢ inferInstanceAs (UniformSpace C(α, β)) = ⨅ i, UniformSpace.comap (fun x => x.comp (φ i)) inferInstance

Tactic:
set 𝔖 : Set (Set α) := {K | IsCompact K}

Result:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i => range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
⊢ inferInstanceAs (UniformSpace C(α, β)) = ⨅ i, UniformSpace.comap (fun x => x.comp (φ i)) inferInstance

Proof state:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i => range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i => {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)
⊢ inferInstanceAs (UniformSpace C(α, β)) = ⨅ i, UniformSpace.comap (fun x => x.comp (φ i)) inferInstance

Tactic:
simp_rw +zetaDelta [compactConvergenceUniformSpace, replaceTopology_eq,
  UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover _ _ _ h_image h_preimage h_cover',
  UniformSpace.comap_iInf, ← UniformSpace.comap_comap]

Result:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i => range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i => {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)
⊢ inferInstanceAs (UniformSpace C(α, β)) =
    ⨅ i,
      ⨅ i_1 ∈ {K | IsCompact K},
        UniformSpace.comap
          (((⇑UniformFun.ofFun ∘ i_1.restrict ∘ ⇑(UniformOnFun.toFun {K | IsCompact K})) ∘ toUniformOnFunIsCompact) ∘
            fun x => x.comp (φ i))
          (UniformFun.uniformSpace (↑i_1) β)

Proof state:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i => range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
⊢ inferInstanceAs (UniformSpace C(α, β)) = ⨅ i, UniformSpace.comap (fun x => x.comp (φ i)) inferInstance

Tactic:
set 𝔗 : Π i, Set (Set (δ i)) := fun i ↦ {K | IsCompact K}

Result:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i => range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i => {K | IsCompact K}
⊢ inferInstanceAs (UniformSpace C(α, β)) = ⨅ i, UniformSpace.comap (fun x => x.comp (φ i)) inferInstance

Proof state:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i => range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i => {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
⊢ inferInstanceAs (UniformSpace C(α, β)) = ⨅ i, UniformSpace.comap (fun x => x.comp (φ i)) inferInstance

Tactic:
have h_cover' : ∀ S ∈ 𝔖, ∃ I : Set ι, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i) := fun S hS ↦ by
  refine ⟨{i | (range (φ i) ∩ S).Nonempty}, h_lf.finite_nonempty_inter_compact hS,
    inter_eq_right.mp ?_⟩
  simp_rw [iUnion₂_inter, mem_setOf, iUnion_nonempty_self, ← iUnion_inter, h_cover, univ_inter]

Result:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i => range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i => {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)
⊢ inferInstanceAs (UniformSpace C(α, β)) = ⨅ i, UniformSpace.comap (fun x => x.comp (φ i)) inferInstance

Proof state:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i => range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i => {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
⊢ ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)

Tactic:
refine ⟨{i | (range (φ i) ∩ S).Nonempty}, h_lf.finite_nonempty_inter_compact hS,
  inter_eq_right.mp ?_⟩

Result:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i => range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i => {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
⊢ (⋃ i ∈ {i | (range ⇑(φ i) ∩ S).Nonempty}, range ⇑(φ i)) ∩ S = S

Proof state:
α : Type u₁
β : Type u₂
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst✝ : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → C(δ i, α)
h_proper : ∀ (i : ι), IsProperMap ⇑(φ i)
h_lf : LocallyFinite fun i => range ⇑(φ i)
h_cover : ⋃ i, range ⇑(φ i) = univ
𝔖 : Set (Set α) := {K | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun i => {K | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun x => ⇑(φ i) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ I, I.Finite ∧ S ⊆ ⋃ i ∈ I, range ⇑(φ i)
⊢ inferInstanceAs (UniformSpace C(α, β)) =
    ⨅ i,
      ⨅ i_1 ∈ {K | IsCompact K},
        UniformSpace.comap
          (((⇑UniformFun.ofFun ∘ i_1.restrict ∘ ⇑(UniformOnFun.toFun {K | IsCompact K})) ∘ toUniformOnFunIsCompact) ∘
            fun x => x.comp (φ i))
          (UniformFun.uniformSpace (↑i_1) β)

Tactic:
rfl

Result:
no goals