awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
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 → α
⊢ Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α) ℱ
      (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f) : Filter (X →ᵤ[𝔖] α)) ↔
    Tendsto F ℱ (𝓝 f)
have 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))
Tactic: simp_rw +instances [UniformOnFun.topologicalSpace_eq,
    Pi.induced_restrict_sUnion 𝔖 (A := fun _ ↦ α), _root_.nhds_iInf, nhds_induced, tendsto_iInf,
    tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
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 → α
⊢ (∀ (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))
have 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))
Tactic: congrm ∀ K (hK : K ∈ 𝔖), ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (hypothesis)
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 ∈ 𝔖
⊢ 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))
have this : CompactSpace.{u_2} (↑K : Type u_2)
Tactic: have : CompactSpace K := isCompact_iff_compactSpace.mp (𝔖_compact K hK)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
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 (K.restrict (π := fun (x : X) ↦ α) ∘ F) ℱ (𝓝 (K.restrict (π := fun (x : X) ↦ α) f))
have a : 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: rw [← (equicontinuous_restrict_iff _ |>.mpr <| F_eqcont K hK).tendsto_uniformFun_iff_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
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 → α
⊢ Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α) ℱ
      (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f) : Filter (X →ᵤ[𝔖] α)) ↔
    Tendsto F ℱ (𝓝 f)
have 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)
Tactic: rw [eq_univ_iff_forall] at 𝔖_covers
Cleared hypotheses: 𝔖_covers, F_eqcont, ℱ, f
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
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)
⊢ Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α) ℱ
      (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f) : Filter (X →ᵤ[𝔖] α)) ↔
    Tendsto F ℱ (𝓝 f)
have rw : Tendsto ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) ℱ (𝓝 ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) f)) ↔
  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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
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)
⊢ Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α) ℱ
      (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f) : Filter (X →ᵤ[𝔖] α)) ↔
    Tendsto F ℱ (𝓝 f)
have rw₁ : Tendsto ((⇑φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) ∘ F) ℱ (𝓝 ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) f)) ↔
  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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
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)
⊢ Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α) ℱ
      (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f) : Filter (X →ᵤ[𝔖] α)) ↔
    Tendsto F ℱ (𝓝 f)
have 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)
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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
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)
⊢ Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α) ℱ
      (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f) : Filter (X →ᵤ[𝔖] α)) ↔
    Tendsto F ℱ (𝓝 f)
have 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) → α))
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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
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))
⊢ IsClosed[Pi.topologicalSpace] (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))
have inl : IsEmpty α → IsClosed[Pi.topologicalSpace] (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))
Tactic: rcases isEmpty_or_nonempty α with _ | _
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
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))
⊢ IsClosed[Pi.topologicalSpace] (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))
have inr : Nonempty α → IsClosed[Pi.topologicalSpace] (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))
Tactic: rcases isEmpty_or_nonempty α with _ | _
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
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 α
⊢ IsClosed[Pi.topologicalSpace] (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))
have 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
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]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
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
⊢ IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) ↔
    IsClosed[Pi.topologicalSpace] (range F)
have simp_rw : (∀ (a : X →ᵤ[𝔖] α),
    ClusterPt a (𝓟 (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))) →
      Membership.mem (γ := Set (X →ᵤ[𝔖] α)) (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) a) ↔
  ∀ (a : X → α), ClusterPt a (𝓟 (range F)) → a ∈ range F
Tactic: simp_rw [isClosed_iff_clusterPt, ← Filter.map_top, ← mapClusterPt_def,
    mapClusterPt_iff_ultrafilter, range_comp, (UniformOnFun.ofFun 𝔖).surjective.forall,
    ← EquicontinuousOn.tendsto_uniformOnFun_iff_pi 𝔖_compact 𝔖_covers F_eqcont,
    (UniformOnFun.ofFun 𝔖).injective.mem_set_image]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
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
simp_rw :
  (∀ (a : X →ᵤ[𝔖] α),
      ClusterPt a (𝓟 (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))) →
        Membership.mem (γ := Set (X →ᵤ[𝔖] α)) (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) a) ↔
    ∀ (a : X → α), ClusterPt a (𝓟 (range F)) → a ∈ range F
⊢ IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) ↔
    IsClosed[Pi.topologicalSpace] (range F)
have simp_rw₁ : (∀ (a : X →ᵤ[𝔖] α),
    ClusterPt a (map ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) ⊤) →
      Membership.mem (γ := Set (X →ᵤ[𝔖] α)) (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) a) ↔
  ∀ (a : X → α), ClusterPt a (map F ⊤) → a ∈ range F
Tactic: simp_rw [isClosed_iff_clusterPt, ← Filter.map_top, ← mapClusterPt_def,
    mapClusterPt_iff_ultrafilter, range_comp, (UniformOnFun.ofFun 𝔖).surjective.forall,
    ← EquicontinuousOn.tendsto_uniformOnFun_iff_pi 𝔖_compact 𝔖_covers F_eqcont,
    (UniformOnFun.ofFun 𝔖).injective.mem_set_image]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
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
simp_rw :
  (∀ (a : X →ᵤ[𝔖] α),
      ClusterPt a (𝓟 (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))) →
        Membership.mem (γ := Set (X →ᵤ[𝔖] α)) (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) a) ↔
    ∀ (a : X → α), ClusterPt a (𝓟 (range F)) → a ∈ range F
simp_rw₁ :
  (∀ (a : X →ᵤ[𝔖] α),
      ClusterPt a (map ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) ⊤) →
        Membership.mem (γ := Set (X →ᵤ[𝔖] α)) (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) a) ↔
    ∀ (a : X → α), ClusterPt a (map F ⊤) → a ∈ range F
⊢ IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) ↔
    IsClosed[Pi.topologicalSpace] (range F)
have simp_rw₂ : (∀ (a : X →ᵤ[𝔖] α),
    MapClusterPt a ⊤ ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) →
      Membership.mem (γ := Set (X →ᵤ[𝔖] α)) (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) a) ↔
  ∀ (a : X → α), MapClusterPt a ⊤ F → a ∈ range F
Tactic: simp_rw [isClosed_iff_clusterPt, ← Filter.map_top, ← mapClusterPt_def,
    mapClusterPt_iff_ultrafilter, range_comp, (UniformOnFun.ofFun 𝔖).surjective.forall,
    ← EquicontinuousOn.tendsto_uniformOnFun_iff_pi 𝔖_compact 𝔖_covers F_eqcont,
    (UniformOnFun.ofFun 𝔖).injective.mem_set_image]