awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
s : Set α
inst_2 : CompactSpace.{u₁} (↑s : Type u₁)
f : α → β
hf : ContinuousOn f s
ι : Type u_1
p : Filter ι
F : ι → α → β
hF : ∀ (i : ι), ContinuousOn (F i) s
rw :
  TendstoUniformly.{u₁, u₂, u_1} (β := β)
      (fun (i : ι) (a : (↑s : Type u₁)) ↦
        ({ toFun := s.restrict (π := fun (a : α) ↦ β) (F i), continuous_toFun := ⋯ :
              ContinuousMap.{u₁, u₂} (↑s : Type u₁) β } :
            (a : (↑s : Type u₁)) → β)
          a)
      (⇑{ toFun := s.restrict (π := fun (a : α) ↦ β) f, continuous_toFun := ⋯ :
            ContinuousMap.{u₁, u₂} (↑s : Type u₁) β } :
        (a : (↑s : Type u₁)) → β)
      p ↔
    TendstoUniformly (fun (i : ι) (x : (↑s : Type u₁)) ↦ F i (↑x : α)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) p
⊢ Tendsto (fun (i : ι) ↦ { toFun := s.restrict (π := fun (a : α) ↦ β) (F i), continuous_toFun := ⋯ }) p
      (𝓝
        { toFun := s.restrict (π := fun (a : α) ↦ β) f, continuous_toFun := ⋯ :
          ContinuousMap.{u₁, u₂} (↑s : Type u₁) β }) ↔
    TendstoUniformlyOn F f p s

Tactic:
rw [ContinuousMap.tendsto_iff_tendstoUniformly, tendstoUniformlyOn_iff_tendstoUniformly_comp_coe]

Premises used: ContinuousMap.tendsto_iff_tendstoUniformly, tendstoUniformlyOn_iff_tendstoUniformly_comp_coe
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
s : Set α
inst_2 : CompactSpace.{u₁} (↑s : Type u₁)
f : α → β
hf : ContinuousOn f s
ι : Type u_1
p : Filter ι
F : ι → α → β
hF : ∀ (i : ι), ContinuousOn (F i) s
⊢ TendstoUniformly.{u₁, u₂, u_1} (β := β)
      (fun (i : ι) (a : (↑s : Type u₁)) ↦
        ({ toFun := s.restrict (π := fun (a : α) ↦ β) (F i), continuous_toFun := ⋯ :
              ContinuousMap.{u₁, u₂} (↑s : Type u₁) β } :
            (a : (↑s : Type u₁)) → β)
          a)
      (⇑{ toFun := s.restrict (π := fun (a : α) ↦ β) f, continuous_toFun := ⋯ :
            ContinuousMap.{u₁, u₂} (↑s : Type u₁) β } :
        (a : (↑s : Type u₁)) → β)
      p ↔
    TendstoUniformly (fun (i : ι) (x : (↑s : Type u₁)) ↦ F i (↑x : α)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) p

Tactic:
congr!
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
X : Type u_1
inst_2 : TopologicalSpace X
f : X → α → β
s : Set α
hf : ∀ (x : X), ContinuousOn (f x) s
inst_3 : CompactSpace.{u₁} (↑s : Type u₁)
rw :
  (Continuous[inst_2, UniformFun.topologicalSpace (↑s : Type u₁) β] fun (x : X) ↦
      (UniformFun.ofFun : (a : (↑s : Type u₁) → β) → (↑s : Type u₁) →ᵤ β)
        (⇑{ toFun := s.restrict (π := fun (a : α) ↦ β) (f x), continuous_toFun := ⋯ :
              ContinuousMap.{u₁, u₂} (↑s : Type u₁) β } :
          (a : (↑s : Type u₁)) → β)) ↔
    ∀ (s_1 : Set α),
      Membership.mem (γ := Set (Set α)) {s} s_1 →
        Continuous[inst_2, UniformFun.topologicalSpace (↑s_1 : Type u₁) β]
          (Function.comp (β := (↑s_1 : Type u₁) → β)
            ((⇑UniformFun.ofFun : (a : (↑s_1 : Type u₁) → β) → UniformFun.{u₁, u₂} (↑s_1 : Type u₁) β) :
              (a : (↑s_1 : Type u₁) → β) → UniformFun.{u₁, u₂} (↑s_1 : Type u₁) β)
            (Function.comp (β := α → β) (s_1.restrict (π := fun (a : α) ↦ β))
                (Function.comp (β := α →ᵤ[{s}] β) (⇑(toFun {s}) : (a : α →ᵤ[{s}] β) → α → β) fun (x : X) ↦
                  (ofFun {s} : (a : α → β) → α →ᵤ[{s}] β) (f x)) :
              X → (↑s_1 : Type u₁) → β))
⊢ (Continuous[inst_2, _] fun (x : X) ↦ { toFun := s.restrict (π := fun (a : α) ↦ β) (f x), continuous_toFun := ⋯ }) ↔
    Continuous[inst_2, topologicalSpace α β {s}] fun (x : X) ↦ (ofFun {s} : (a : α → β) → α →ᵤ[{s}] β) (f x)

Tactic:
rw [ContinuousMap.continuous_iff_continuous_uniformFun, UniformOnFun.continuous_rng_iff]

Premises used: UniformOnFun.continuous_rng_iff, ContinuousMap.continuous_iff_continuous_uniformFun
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
X : Type u_1
inst_2 : TopologicalSpace X
f : X → α → β
s : Set α
hf : ∀ (x : X), ContinuousOn (f x) s
inst_3 : CompactSpace.{u₁} (↑s : Type u₁)
⊢ (Continuous[inst_2, UniformFun.topologicalSpace (↑s : Type u₁) β] fun (x : X) ↦
      (UniformFun.ofFun : (a : (↑s : Type u₁) → β) → (↑s : Type u₁) →ᵤ β)
        (⇑{ toFun := s.restrict (π := fun (a : α) ↦ β) (f x), continuous_toFun := ⋯ :
              ContinuousMap.{u₁, u₂} (↑s : Type u₁) β } :
          (a : (↑s : Type u₁)) → β)) ↔
    ∀ (s_1 : Set α),
      Membership.mem (γ := Set (Set α)) {s} s_1 →
        Continuous[inst_2, UniformFun.topologicalSpace (↑s_1 : Type u₁) β]
          (Function.comp (β := (↑s_1 : Type u₁) → β)
            ((⇑UniformFun.ofFun : (a : (↑s_1 : Type u₁) → β) → UniformFun.{u₁, u₂} (↑s_1 : Type u₁) β) :
              (a : (↑s_1 : Type u₁) → β) → UniformFun.{u₁, u₂} (↑s_1 : Type u₁) β)
            (Function.comp (β := α → β) (s_1.restrict (π := fun (a : α) ↦ β))
                (Function.comp (β := α →ᵤ[{s}] β) (⇑(toFun {s}) : (a : α →ᵤ[{s}] β) → α → β) fun (x : X) ↦
                  (ofFun {s} : (a : α → β) → α →ᵤ[{s}] β) (f x)) :
              X → (↑s_1 : Type u₁) → β))

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst_2 : TopologicalSpace δ₁
inst_3 : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap.{u_1, u₁} (X := δ₁) (Y := α) (⇑φ₁ : (a : δ₁) → α)
h_proper₂ : IsProperMap.{u_2, u₁} (X := δ₂) (Y := α) (⇑φ₂ : (a : δ₂) → α)
h_cover :
  Eq.{u₁ + 1} (α := Set α)
    (range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K : Set δ₁ | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K : Set δ₂ | IsCompact K}
⊢ MapsTo (fun (x : Set δ₁) ↦ (⇑φ₁ : (a : δ₁) → α) '' x) 𝔗₁ 𝔖

Tactic:
have h_image₁ : MapsTo (φ₁ '' ·) 𝔗₁ 𝔖 := fun K hK ↦ hK.image φ₁.continuous
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst_2 : TopologicalSpace δ₁
inst_3 : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap.{u_1, u₁} (X := δ₁) (Y := α) (⇑φ₁ : (a : δ₁) → α)
h_proper₂ : IsProperMap.{u_2, u₁} (X := δ₂) (Y := α) (⇑φ₂ : (a : δ₂) → α)
h_cover :
  Eq.{u₁ + 1} (α := Set α)
    (range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K : Set δ₁ | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K : Set δ₂ | IsCompact K}
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ (⇑φ₁ : (a : δ₁) → α) '' x) 𝔗₁ 𝔖
⊢ MapsTo (fun (x : Set δ₂) ↦ (⇑φ₂ : (a : δ₂) → α) '' x) 𝔗₂ 𝔖

Tactic:
have h_image₂ : MapsTo (φ₂ '' ·) 𝔗₂ 𝔖 := fun K hK ↦ hK.image φ₂.continuous
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst_2 : TopologicalSpace δ₁
inst_3 : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap.{u_1, u₁} (X := δ₁) (Y := α) (⇑φ₁ : (a : δ₁) → α)
h_proper₂ : IsProperMap.{u_2, u₁} (X := δ₂) (Y := α) (⇑φ₂ : (a : δ₂) → α)
h_cover :
  Eq.{u₁ + 1} (α := Set α)
    (range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K : Set δ₁ | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K : Set δ₂ | IsCompact K}
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ (⇑φ₁ : (a : δ₁) → α) '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ (⇑φ₂ : (a : δ₂) → α) '' x) 𝔗₂ 𝔖
⊢ MapsTo (fun (x : Set α) ↦ (⇑φ₁ : (a : δ₁) → α) ⁻¹' x) 𝔖 𝔗₁

Tactic:
have h_preimage₁ : MapsTo (φ₁ ⁻¹' ·) 𝔖 𝔗₁ := fun K ↦ h_proper₁.isCompact_preimage
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst_2 : TopologicalSpace δ₁
inst_3 : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap.{u_1, u₁} (X := δ₁) (Y := α) (⇑φ₁ : (a : δ₁) → α)
h_proper₂ : IsProperMap.{u_2, u₁} (X := δ₂) (Y := α) (⇑φ₂ : (a : δ₂) → α)
h_cover :
  Eq.{u₁ + 1} (α := Set α)
    (range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K : Set δ₁ | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K : Set δ₂ | IsCompact K}
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ (⇑φ₁ : (a : δ₁) → α) '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ (⇑φ₂ : (a : δ₂) → α) '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ (⇑φ₁ : (a : δ₁) → α) ⁻¹' x) 𝔖 𝔗₁
⊢ MapsTo (fun (x : Set α) ↦ (⇑φ₂ : (a : δ₂) → α) ⁻¹' x) 𝔖 𝔗₂

Tactic:
have h_preimage₂ : MapsTo (φ₂ ⁻¹' ·) 𝔖 𝔗₂ := fun K ↦ h_proper₂.isCompact_preimage
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst_2 : TopologicalSpace δ₁
inst_3 : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap.{u_1, u₁} (X := δ₁) (Y := α) (⇑φ₁ : (a : δ₁) → α)
h_proper₂ : IsProperMap.{u_2, u₁} (X := δ₂) (Y := α) (⇑φ₂ : (a : δ₂) → α)
h_cover :
  Eq.{u₁ + 1} (α := Set α)
    (range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K : Set δ₁ | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K : Set δ₂ | IsCompact K}
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ (⇑φ₁ : (a : δ₁) → α) '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ (⇑φ₂ : (a : δ₂) → α) '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ (⇑φ₁ : (a : δ₁) → α) ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ (⇑φ₂ : (a : δ₂) → α) ⁻¹' x) 𝔖 𝔗₂
⊢ ∀ S ∈ 𝔖, S ⊆ range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)

Tactic:
have h_cover' : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂ := fun S _ ↦ h_cover ▸ subset_univ _
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst_2 : TopologicalSpace δ₁
inst_3 : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap.{u_1, u₁} (X := δ₁) (Y := α) (⇑φ₁ : (a : δ₁) → α)
h_proper₂ : IsProperMap.{u_2, u₁} (X := δ₂) (Y := α) (⇑φ₂ : (a : δ₂) → α)
h_cover :
  Eq.{u₁ + 1} (α := Set α)
    (range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K : Set δ₁ | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K : Set δ₂ | IsCompact K}
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ (⇑φ₁ : (a : δ₁) → α) '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ (⇑φ₂ : (a : δ₂) → α) '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ (⇑φ₁ : (a : δ₁) → α) ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ (⇑φ₂ : (a : δ₂) → α) ⁻¹' x) 𝔖 𝔗₂
h_cover' :
  ∀ S ∈ 𝔖, S ⊆ range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)
simp_rw :
  Eq (α := UniformSpace C(α, β)) inferInstance
    (UniformSpace.comap (β := δ₁ →ᵤ[{K : Set δ₁ | IsCompact K}] β)
        (Function.comp (β := C(δ₁, β)) toUniformOnFunIsCompact fun (x : C(α, β)) ↦ x.comp φ₁) inferInstance ⊓
      UniformSpace.comap (β := δ₂ →ᵤ[{K : Set δ₂ | IsCompact K}] β)
        (Function.comp (β := C(δ₂, β)) toUniformOnFunIsCompact fun (x : C(α, β)) ↦ x.comp φ₂) inferInstance)
⊢ Eq (α := UniformSpace C(α, β)) inferInstance
    (UniformSpace.comap (β := C(δ₁, β)) (fun (x : C(α, β)) ↦ x.comp φ₁) inferInstance ⊓
      UniformSpace.comap (β := C(δ₂, β)) (fun (x : C(α, β)) ↦ x.comp φ₂) inferInstance)

Tactic:
simp_rw +zetaDelta [compactConvergenceUniformSpace, replaceTopology_eq,
    UniformOnFun.uniformSpace_eq_inf_precomp_of_cover _ _ _ _ _
      h_image₁ h_image₂ h_preimage₁ h_preimage₂ h_cover',
    UniformSpace.comap_inf, ← UniformSpace.comap_comap]

Premises used: UniformSpace.replaceTopology_eq, UniformSpace.comap_inf, UniformSpace.comap_comap, UniformOnFun.uniformSpace_eq_inf_precomp_of_cover, ContinuousMap.compactConvergenceUniformSpace
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst_2 : TopologicalSpace δ₁
inst_3 : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap.{u_1, u₁} (X := δ₁) (Y := α) (⇑φ₁ : (a : δ₁) → α)
h_proper₂ : IsProperMap.{u_2, u₁} (X := δ₂) (Y := α) (⇑φ₂ : (a : δ₂) → α)
h_cover :
  Eq.{u₁ + 1} (α := Set α)
    (range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K : Set δ₁ | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K : Set δ₂ | IsCompact K}
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ (⇑φ₁ : (a : δ₁) → α) '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ (⇑φ₂ : (a : δ₂) → α) '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ (⇑φ₁ : (a : δ₁) → α) ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ (⇑φ₂ : (a : δ₂) → α) ⁻¹' x) 𝔖 𝔗₂
h_cover' :
  ∀ S ∈ 𝔖, S ⊆ range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)
⊢ Eq (α := UniformSpace C(α, β)) inferInstance
    (UniformSpace.comap (β := δ₁ →ᵤ[{K : Set δ₁ | IsCompact K}] β)
        (Function.comp (β := C(δ₁, β)) toUniformOnFunIsCompact fun (x : C(α, β)) ↦ x.comp φ₁) inferInstance ⊓
      UniformSpace.comap (β := δ₂ →ᵤ[{K : Set δ₂ | IsCompact K}] β)
        (Function.comp (β := C(δ₂, β)) toUniformOnFunIsCompact fun (x : C(α, β)) ↦ x.comp φ₂) inferInstance)

Tactic:
rfl
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
⊢ ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖

Tactic:
have h_image : ∀ i, MapsTo (φ i '' ·) (𝔗 i) 𝔖 := fun i K hK ↦ hK.image (φ i).continuous
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
⊢ ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)

Tactic:
have h_preimage : ∀ i, MapsTo (φ i ⁻¹' ·) 𝔖 (𝔗 i) := fun i K ↦ (h_proper i).isCompact_preimage
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
⊢ ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)

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

Premises used: setOf, Set.inter_eq_right, Inter.inter, Set.Nonempty, And.intro, Exists.intro, Iff.mp, Set.range, LocallyFinite.finite_nonempty_inter_compact, DFunLike.coe
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
refine :
  (⋃ (i : ι),
        ⋃ (_ :
          Membership.mem (γ := Set ι) {i : ι | (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty}
            i),
          range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) ∩
      S =
    S
⊢ ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)

Tactic:
refine ⟨{i | (range (φ i) ∩ S).Nonempty}, h_lf.finite_nonempty_inter_compact hS,
      inter_eq_right.mp ?_⟩
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
simp_rw :
  ⋃ (i : ι),
      ⋃ (_ :
        Membership.mem (γ := Set ι) {i : ι | (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty} i),
        range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S =
    S
simp_rw₁ :
  ⋃ (i : ι),
      ⋃ (_ : (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty),
        range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S =
    S
simp_rw₂ : ⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S = S
simp_rw₃ : (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) ∩ S = S
simp_rw₄ : univ ∩ S = S
⊢ (⋃ (i : ι),
        ⋃ (_ :
          Membership.mem (γ := Set ι) {i : ι | (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty}
            i),
          range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) ∩
      S =
    S

Tactic:
simp_rw [iUnion₂_inter, mem_setOf, iUnion_nonempty_self, ← iUnion_inter, h_cover, univ_inter]

Premises used: Set.univ_inter, Set.iUnion_inter, Set.mem_setOf, Set.iUnion_nonempty_self, Set.iUnion₂_inter
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
⊢ ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)

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]
-- Module: Mathlib.Topology.UniformSpace.CompactConvergence
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
simp_rw :
  Eq (α := UniformSpace C(α, β)) inferInstance
    (⨅ (i : ι),
      UniformSpace.comap (β := UniformOnFun.{u_1, u₂} (δ i) β {K : Set (δ i) | IsCompact K})
        (Function.comp (β := ContinuousMap.{u_1, u₂} (δ i) β) toUniformOnFunIsCompact fun (x : C(α, β)) ↦ x.comp (φ i))
        inferInstance)
⊢ Eq (α := UniformSpace C(α, β)) inferInstance
    (⨅ (i : ι),
      UniformSpace.comap (β := ContinuousMap.{u_1, u₂} (δ i) β) (fun (x : C(α, β)) ↦ 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]

Premises used: UniformSpace.replaceTopology_eq, UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover, UniformSpace.comap_comap, UniformSpace.comap_iInf, ContinuousMap.compactConvergenceUniformSpace