awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : ((↑(⋃₀ 𝔖) : Type u_2) → α) ≃ᵤ (X → α) :=
  UniformEquiv.piCongrLeft (β := fun (x : X) ↦ α) (Equiv.subtypeUnivEquiv (p := Membership.mem (⋃₀ 𝔖)) 𝔖_covers)
⊢ IsUniformInducing (β := (a : (↑(⋃₀ 𝔖) : Type u_2)) → α) ((⇑φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) ∘ F) ↔
    IsUniformInducing F

Tactic:
exact ⟨fun H ↦ φ.isUniformInducing.comp H, fun H ↦ φ.symm.isUniformInducing.comp H⟩
-- 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 ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
rw :
  inst_2 =
      TopologicalSpace.induced ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)
        (UniformOnFun.topologicalSpace X α 𝔖) ↔
    inst_2 =
      TopologicalSpace.induced ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)
        (Pi.topologicalSpace (Y := fun (a : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α))
⊢ IsInducing (Y := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) ↔
    IsInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ 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 ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
change : inst_2 = UniformSpace.toTopologicalSpace ↔ inst_2 = UniformSpace.toTopologicalSpace
⊢ inst_2 =
      TopologicalSpace.induced ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)
        (UniformOnFun.topologicalSpace X α 𝔖) ↔
    inst_2 =
      TopologicalSpace.induced ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)
        (Pi.topologicalSpace (Y := fun (a : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α))

Tactic:
change (_ = ((UniformOnFun.uniformSpace X α 𝔖).comap F).toTopologicalSpace) ↔
    (_ = ((Pi.uniformSpace _).comap ((⋃₀ 𝔖).restrict ∘ 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 ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
rw rw₁ : inst_2 = UniformSpace.toTopologicalSpace ↔ inst_2 = UniformSpace.toTopologicalSpace
⊢ inst_2 = UniformSpace.toTopologicalSpace ↔ inst_2 = UniformSpace.toTopologicalSpace

Tactic:
rw [← EquicontinuousOn.comap_uniformOnFun_eq 𝔖_compact F_eqcont]

Premises used: EquicontinuousOn.comap_uniformOnFun_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 ι
𝔖 : Set (Set X)
𝔖_covers : ⋃₀ 𝔖 = univ
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ ∀ (x : X), x ∈ ⋃₀ 𝔖

Tactic:
rw [eq_univ_iff_forall] at 𝔖_covers

Premises used: Set.eq_univ_iff_forall
-- 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 ι
𝔖 : Set (Set X)
𝔖_covers : ⋃₀ 𝔖 = univ
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
𝔖_covers₁ : ∀ (x : X), x ∈ ⋃₀ 𝔖
⊢ ∀ K ∈ 𝔖, IsCompact K

Tactic:
rw [eq_univ_iff_forall] at 𝔖_covers

Premises used: Set.eq_univ_iff_forall
-- 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 ι
𝔖 : Set (Set X)
𝔖_covers : ⋃₀ 𝔖 = univ
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
𝔖_covers₁ : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact₁ : ∀ K ∈ 𝔖, IsCompact K
⊢ ∀ K ∈ 𝔖, EquicontinuousOn F K

Tactic:
rw [eq_univ_iff_forall] at 𝔖_covers

Premises used: Set.eq_univ_iff_forall
-- 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 ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : ((↑(⋃₀ 𝔖) : Type u_2) → α) ≃ₜ (X → α) :=
  Homeomorph.piCongrLeft (Y := fun (x : X) ↦ α) (Equiv.subtypeUnivEquiv (p := Membership.mem (⋃₀ 𝔖)) 𝔖_covers)
⊢ (⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F = (⇑φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) ∘ F

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 ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : ((↑(⋃₀ 𝔖) : Type u_2) → α) ≃ₜ (X → α) :=
  Homeomorph.piCongrLeft (Y := fun (x : X) ↦ α) (Equiv.subtypeUnivEquiv (p := Membership.mem (⋃₀ 𝔖)) 𝔖_covers)
rw :
  IsInducing (Y := (a : (↑(⋃₀ 𝔖) : Type u_2)) → α) ((⇑φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) ∘ F) ↔
    IsInducing F
⊢ IsInducing (Y := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) ↔ IsInducing F

Tactic:
rw [EquicontinuousOn.inducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont,
      show restrict (⋃₀ 𝔖) ∘ F = φ.symm ∘ F by rfl]

Premises used: EquicontinuousOn.inducing_uniformOnFun_iff_pi'
-- 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 ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : ((↑(⋃₀ 𝔖) : Type u_2) → α) ≃ₜ (X → α) :=
  Homeomorph.piCongrLeft (Y := fun (x : X) ↦ α) (Equiv.subtypeUnivEquiv (p := Membership.mem (⋃₀ 𝔖)) 𝔖_covers)
⊢ IsInducing (Y := (a : (↑(⋃₀ 𝔖) : Type u_2)) → α) ((⇑φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) ∘ F) ↔
    IsInducing F

Tactic:
⟨fun H ↦ φ.isInducing.comp H, fun H ↦ φ.symm.isInducing.comp H⟩

Premises used: Homeomorph.isInducing, Topology.IsInducing.comp, Homeomorph.symm, Iff.intro
-- 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 ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : ((↑(⋃₀ 𝔖) : Type u_2) → α) ≃ₜ (X → α) :=
  Homeomorph.piCongrLeft (Y := fun (x : X) ↦ α) (Equiv.subtypeUnivEquiv (p := Membership.mem (⋃₀ 𝔖)) 𝔖_covers)
⊢ IsInducing (Y := (a : (↑(⋃₀ 𝔖) : Type u_2)) → α) ((⇑φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) ∘ F) ↔
    IsInducing F

Tactic:
exact ⟨fun H ↦ φ.isInducing.comp H, fun H ↦ φ.symm.isInducing.comp H⟩
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
rw :
  Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α) ℱ
      (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f) : Filter (X →ᵤ[𝔖] α)) ↔
    Tendsto F ℱ (𝓝 f)
⊢ Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α) ℱ
      (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f) : Filter (X →ᵤ[𝔖] α)) ↔
    Tendsto ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) ℱ (𝓝 ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) f))

Tactic:
rw [← Filter.tendsto_comap_iff (g := (⋃₀ 𝔖).restrict), ← nhds_induced]

Premises used: Filter.tendsto_comap_iff, nhds_induced
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
simp_rw :
  (∀ (i : Set X) (i_1 : i ∈ 𝔖),
      Tendsto (β := UniformFun.{u_2, u_3} (↑i : Type u_2) α)
        (Function.comp (β := X →ᵤ[𝔖] α)
          (Function.comp (β := (↑i : Type u_2) → α)
            ((⇑UniformFun.ofFun : (a : (↑i : Type u_2) → α) → UniformFun.{u_2, u_3} (↑i : Type u_2) α) :
              (a : (↑i : Type u_2) → α) → UniformFun.{u_2, u_3} (↑i : Type u_2) α)
            (Function.comp (β := X → α) (i.restrict (π := fun (a : X) ↦ α))
                (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
              (X →ᵤ[𝔖] α) → (↑i : Type u_2) → α))
          ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
        ℱ
        (𝓝
          (Function.comp (α := X →ᵤ[𝔖] α) (β := (↑i : Type u_2) → α)
            ((⇑UniformFun.ofFun : (a : (↑i : Type u_2) → α) → UniformFun.{u_2, u_3} (↑i : Type u_2) α) :
              (a : (↑i : Type u_2) → α) → UniformFun.{u_2, u_3} (↑i : Type u_2) α)
            (Function.comp (β := X → α) (i.restrict (π := fun (a : X) ↦ α))
                (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
              (X →ᵤ[𝔖] α) → (↑i : Type u_2) → α)
            ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f : X →ᵤ[𝔖] α)))) ↔
    ∀ (i : Set X) (i_1 : i ∈ 𝔖),
      Tendsto (i.restrict (π := fun (x : X) ↦ α) ∘ F) ℱ (𝓝 (i.restrict (π := fun (x : X) ↦ α) f))
⊢ Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α) ℱ
      (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f) : Filter (X →ᵤ[𝔖] α)) ↔
    Tendsto F ℱ (𝓝 f)

Tactic:
simp_rw +instances [UniformOnFun.topologicalSpace_eq,
    Pi.induced_restrict_sUnion 𝔖 (A := fun _ ↦ α), _root_.nhds_iInf, nhds_induced, tendsto_iInf,
    tendsto_comap_iff]

Premises used: nhds_iInf, Filter.tendsto_comap_iff, UniformOnFun.topologicalSpace_eq, Pi.induced_restrict_sUnion, nhds_induced, Filter.tendsto_iInf
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
a :
  ∀ (K : Set X) (hK : K ∈ 𝔖),
    Tendsto (β := UniformFun.{u_2, u_3} (↑K : Type u_2) α)
        (Function.comp (β := X →ᵤ[𝔖] α)
          (Function.comp (β := (↑K : Type u_2) → α)
            ((⇑UniformFun.ofFun : (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α) :
              (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α)
            (Function.comp (β := X → α) (K.restrict (π := fun (a : X) ↦ α))
                (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
              (X →ᵤ[𝔖] α) → (↑K : Type u_2) → α))
          ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
        ℱ
        (𝓝
          (Function.comp (α := X →ᵤ[𝔖] α) (β := (↑K : Type u_2) → α)
            ((⇑UniformFun.ofFun : (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α) :
              (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α)
            (Function.comp (β := X → α) (K.restrict (π := fun (a : X) ↦ α))
                (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
              (X →ᵤ[𝔖] α) → (↑K : Type u_2) → α)
            ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f : X →ᵤ[𝔖] α))) ↔
      Tendsto (K.restrict (π := fun (x : X) ↦ α) ∘ F) ℱ (𝓝 (K.restrict (π := fun (x : X) ↦ α) f))
⊢ (∀ (i : Set X) (i_1 : i ∈ 𝔖),
      Tendsto (β := UniformFun.{u_2, u_3} (↑i : Type u_2) α)
        (Function.comp (β := X →ᵤ[𝔖] α)
          (Function.comp (β := (↑i : Type u_2) → α)
            ((⇑UniformFun.ofFun : (a : (↑i : Type u_2) → α) → UniformFun.{u_2, u_3} (↑i : Type u_2) α) :
              (a : (↑i : Type u_2) → α) → UniformFun.{u_2, u_3} (↑i : Type u_2) α)
            (Function.comp (β := X → α) (i.restrict (π := fun (a : X) ↦ α))
                (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
              (X →ᵤ[𝔖] α) → (↑i : Type u_2) → α))
          ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
        ℱ
        (𝓝
          (Function.comp (α := X →ᵤ[𝔖] α) (β := (↑i : Type u_2) → α)
            ((⇑UniformFun.ofFun : (a : (↑i : Type u_2) → α) → UniformFun.{u_2, u_3} (↑i : Type u_2) α) :
              (a : (↑i : Type u_2) → α) → UniformFun.{u_2, u_3} (↑i : Type u_2) α)
            (Function.comp (β := X → α) (i.restrict (π := fun (a : X) ↦ α))
                (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
              (X →ᵤ[𝔖] α) → (↑i : Type u_2) → α)
            ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f : X →ᵤ[𝔖] α)))) ↔
    ∀ (i : Set X) (i_1 : i ∈ 𝔖),
      Tendsto (i.restrict (π := fun (x : X) ↦ α) ∘ F) ℱ (𝓝 (i.restrict (π := fun (x : X) ↦ α) f))

Tactic:
congrm ∀ K (hK : K ∈ 𝔖), ?_
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
K : Set X
hK : K ∈ 𝔖
⊢ CompactSpace.{u_2} (↑K : Type u_2)

Tactic:
have : CompactSpace K := isCompact_iff_compactSpace.mp (𝔖_compact K hK)
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
K : Set X
hK : K ∈ 𝔖
this : CompactSpace.{u_2} (↑K : Type u_2)
⊢ Tendsto (β := UniformFun.{u_2, u_3} (↑K : Type u_2) α)
      (Function.comp (β := X →ᵤ[𝔖] α)
        (Function.comp (β := (↑K : Type u_2) → α)
          ((⇑UniformFun.ofFun : (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α) :
            (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α)
          (Function.comp (β := X → α) (K.restrict (π := fun (a : X) ↦ α))
              (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
            (X →ᵤ[𝔖] α) → (↑K : Type u_2) → α))
        ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
      ℱ
      (𝓝
        (Function.comp (α := X →ᵤ[𝔖] α) (β := (↑K : Type u_2) → α)
          ((⇑UniformFun.ofFun : (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α) :
            (a : (↑K : Type u_2) → α) → UniformFun.{u_2, u_3} (↑K : Type u_2) α)
          (Function.comp (β := X → α) (K.restrict (π := fun (a : X) ↦ α))
              (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
            (X →ᵤ[𝔖] α) → (↑K : Type u_2) → α)
          ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f : X →ᵤ[𝔖] α))) ↔
    Tendsto (β := UniformFun.{u_2, u_3} (↑K : Type u_2) α)
      ((⇑UniformFun.ofFun : (a : (↑K : Type u_2) → α) → (↑K : Type u_2) →ᵤ α) ∘ K.restrict (π := fun (a : X) ↦ α) ∘ F :
        ι → UniformFun.{u_2, u_3} (↑K : Type u_2) α)
      ℱ
      (𝓝 ((UniformFun.ofFun : (a : (↑K : Type u_2) → α) → (↑K : Type u_2) →ᵤ α) (K.restrict (π := fun (x : X) ↦ α) f)) :
        Filter (UniformFun.{u_2, u_3} (↑K : Type u_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 → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ⋃₀ 𝔖 = univ
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
rw :
  ∀ (𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖) (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K) (ℱ : Filter ι) (f : X → α),
    Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α) ℱ
        (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f) : Filter (X →ᵤ[𝔖] α)) ↔
      Tendsto F ℱ (𝓝 f)
⊢ Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α) ℱ
      (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f) : Filter (X →ᵤ[𝔖] α)) ↔
    Tendsto F ℱ (𝓝 f)

Tactic:
rw [eq_univ_iff_forall] at 𝔖_covers

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
φ : ((↑(⋃₀ 𝔖) : Type u_2) → α) ≃ₜ (X → α) :=
  Homeomorph.piCongrLeft (Y := fun (x : X) ↦ α) (Equiv.subtypeUnivEquiv (p := Membership.mem (⋃₀ 𝔖)) 𝔖_covers)
⊢ (⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F = (⇑φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) ∘ F

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 → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
φ : ((↑(⋃₀ 𝔖) : Type u_2) → α) ≃ₜ (X → α) :=
  Homeomorph.piCongrLeft (Y := fun (x : X) ↦ α) (Equiv.subtypeUnivEquiv (p := Membership.mem (⋃₀ 𝔖)) 𝔖_covers)
⊢ (⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) f = (φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) f

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 → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
φ : ((↑(⋃₀ 𝔖) : Type u_2) → α) ≃ₜ (X → α) :=
  Homeomorph.piCongrLeft (Y := fun (x : X) ↦ α) (Equiv.subtypeUnivEquiv (p := Membership.mem (⋃₀ 𝔖)) 𝔖_covers)
rw :
  Tendsto ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) ℱ (𝓝 ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) f)) ↔
    Tendsto F ℱ (𝓝 f)
rw₁ :
  Tendsto ((⇑φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) ∘ F) ℱ (𝓝 ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) f)) ↔
    Tendsto F ℱ (𝓝 f)
rw₂ :
  Tendsto (β := (a : (↑(⋃₀ 𝔖) : Type u_2)) → α)
      ((⇑φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) ∘ F : ι → (↑(⋃₀ 𝔖) : Type u_2) → α) ℱ
      (𝓝 ((φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) f) : Filter ((a : (↑(⋃₀ 𝔖) : Type u_2)) → α)) ↔
    Tendsto F ℱ (𝓝 f)
rw₃ rw₄ :
  Tendsto (β := (a : (↑(⋃₀ 𝔖) : Type u_2)) → α)
      ((⇑φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) ∘ F : ι → (↑(⋃₀ 𝔖) : Type u_2) → α) ℱ
      (𝓝 ((φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) f) : Filter ((a : (↑(⋃₀ 𝔖) : Type u_2)) → α)) ↔
    Tendsto (β := (↑(⋃₀ 𝔖) : Type u_2) → α)
      ((⇑φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) ∘ F : ι → (↑(⋃₀ 𝔖) : Type u_2) → α) ℱ
      (𝓝 ((φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) f) : Filter ((↑(⋃₀ 𝔖) : Type u_2) → α))
⊢ Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α) ℱ
      (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f) : Filter (X →ᵤ[𝔖] α)) ↔
    Tendsto F ℱ (𝓝 f)

Tactic:
rw [EquicontinuousOn.tendsto_uniformOnFun_iff_pi' 𝔖_compact F_eqcont,
      show restrict (⋃₀ 𝔖) ∘ F = φ.symm ∘ F by rfl, show restrict (⋃₀ 𝔖) f = φ.symm f by rfl,
      φ.symm.isInducing.tendsto_nhds_iff]

Premises used: Homeomorph.isInducing, EquicontinuousOn.tendsto_uniformOnFun_iff_pi', Topology.IsInducing.tendsto_nhds_iff, Homeomorph.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 → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
inl : IsEmpty α → IsClosed[Pi.topologicalSpace] (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))
inr : Nonempty α → IsClosed[Pi.topologicalSpace] (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))
⊢ IsClosed[Pi.topologicalSpace] (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))

Tactic:
rcases isEmpty_or_nonempty α with _ | _

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
h : IsEmpty α
⊢ IsClosed[Pi.topologicalSpace] (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))

Tactic:
simp [isClosed_discrete]

Premises used: isClosed_discrete
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
h : Nonempty α
inr :
  ∀ (x : X → α),
    (∃ (U : Ultrafilter ι),
        (↑U : Filter ι) ≤ ⊤ ∧
          Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α)
            (↑U : Filter ι) (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) x) : Filter (X →ᵤ[𝔖] α))) →
      (⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) x ∈ (⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) '' range F
⊢ IsClosed[Pi.topologicalSpace] (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))

Tactic:
simp_rw [isClosed_iff_clusterPt, ← Filter.map_top, ← mapClusterPt_def,
    mapClusterPt_iff_ultrafilter, range_comp, Subtype.coe_injective.surjective_comp_right.forall,
    ← restrict_eq, ← EquicontinuousOn.tendsto_uniformOnFun_iff_pi' 𝔖_compact F_eqcont]

Premises used: Set.range_comp, EquicontinuousOn.tendsto_uniformOnFun_iff_pi', Function.Surjective.forall, mapClusterPt_def, Filter.map_top, mapClusterPt_iff_ultrafilter, Function.Injective.surjective_comp_right, Subtype.coe_injective, isClosed_iff_clusterPt, Set.restrict_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 → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
h : Nonempty α
⊢ ∀ (x : X → α),
    (∃ (U : Ultrafilter ι),
        (↑U : Filter ι) ≤ ⊤ ∧
          Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α)
            (↑U : Filter ι) (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) x) : Filter (X →ᵤ[𝔖] α))) →
      (⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) x ∈ (⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) '' range F

Tactic:
fun f ⟨u, _, hu⟩ ↦ mem_image_of_mem _ <| H.mem_of_tendsto hu <|
    Eventually.of_forall mem_range_self

Premises used: Set.mem_range_self, _private.0.EquicontinuousOn.isClosed_range_pi_of_uniformOnFun'.match_6, Set.sUnion, Membership.mem, IsClosed.mem_of_tendsto, Filter.Eventually.of_forall, Set.mem_image_of_mem, Set.image, Set.range, Set.restrict
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
ι : Type u_1
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
h : Nonempty α
⊢ ∀ (x : X → α),
    (∃ (U : Ultrafilter ι),
        (↑U : Filter ι) ≤ ⊤ ∧
          Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α)
            (↑U : Filter ι) (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) x) : Filter (X →ᵤ[𝔖] α))) →
      (⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) x ∈ (⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) '' range F

Tactic:
exact fun f ⟨u, _, hu⟩ ↦ mem_image_of_mem _ <| H.mem_of_tendsto hu <|
    Eventually.of_forall mem_range_self