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
𝔖_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
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
⊢ IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) ↔
    IsClosed[Pi.topologicalSpace] (range F)
have simp_rw₃ : (∀ (a : X →ᵤ[𝔖] α),
    (∃ (U : Ultrafilter ι),
        (↑U : Filter ι) ≤ ⊤ ∧ Tendsto ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) (↑U : Filter ι) (𝓝 a)) →
      Membership.mem (γ := Set (X →ᵤ[𝔖] α)) (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) a) ↔
  ∀ (a : X → α), (∃ (U : Ultrafilter ι), (↑U : Filter ι) ≤ ⊤ ∧ Tendsto F (↑U : Filter ι) (𝓝 a)) → 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
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
simp_rw₃ :
  (∀ (a : X →ᵤ[𝔖] α),
      (∃ (U : Ultrafilter ι),
          (↑U : Filter ι) ≤ ⊤ ∧
            Tendsto ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) (↑U : Filter ι) (𝓝 a)) →
        Membership.mem (γ := Set (X →ᵤ[𝔖] α)) (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) a) ↔
    ∀ (a : X → α), (∃ (U : Ultrafilter ι), (↑U : Filter ι) ≤ ⊤ ∧ Tendsto F (↑U : Filter ι) (𝓝 a)) → a ∈ range F
⊢ IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) ↔
    IsClosed[Pi.topologicalSpace] (range F)
have simp_rw₄ : (∀ (a : X →ᵤ[𝔖] α),
    (∃ (U : Ultrafilter ι),
        (↑U : Filter ι) ≤ ⊤ ∧ Tendsto ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) (↑U : Filter ι) (𝓝 a)) →
      Membership.mem (γ := Set (X →ᵤ[𝔖] α)) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) '' range F) a) ↔
  ∀ (a : X → α), (∃ (U : Ultrafilter ι), (↑U : Filter ι) ≤ ⊤ ∧ Tendsto F (↑U : Filter ι) (𝓝 a)) → 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
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
simp_rw₃ :
  (∀ (a : X →ᵤ[𝔖] α),
      (∃ (U : Ultrafilter ι),
          (↑U : Filter ι) ≤ ⊤ ∧
            Tendsto ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) (↑U : Filter ι) (𝓝 a)) →
        Membership.mem (γ := Set (X →ᵤ[𝔖] α)) (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) a) ↔
    ∀ (a : X → α), (∃ (U : Ultrafilter ι), (↑U : Filter ι) ≤ ⊤ ∧ Tendsto F (↑U : Filter ι) (𝓝 a)) → a ∈ range F
simp_rw₄ :
  (∀ (a : X →ᵤ[𝔖] α),
      (∃ (U : Ultrafilter ι),
          (↑U : Filter ι) ≤ ⊤ ∧
            Tendsto ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) (↑U : Filter ι) (𝓝 a)) →
        Membership.mem (γ := Set (X →ᵤ[𝔖] α)) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) '' range F) a) ↔
    ∀ (a : X → α), (∃ (U : Ultrafilter ι), (↑U : Filter ι) ≤ ⊤ ∧ Tendsto F (↑U : Filter ι) (𝓝 a)) → a ∈ range F
⊢ IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)) ↔
    IsClosed[Pi.topologicalSpace] (range F)
have simp_rw₅ : (∀ (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 →ᵤ[𝔖] α))) →
      Membership.mem (α := X →ᵤ[𝔖] α) (γ := Set (X →ᵤ[𝔖] α))
        ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) '' range F)
        ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) x : X →ᵤ[𝔖] α)) ↔
  ∀ (a : X → α), (∃ (U : Ultrafilter ι), (↑U : Filter ι) ≤ ⊤ ∧ Tendsto F (↑U : Filter ι) (𝓝 a)) → 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 → α
inst_2 : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing (Y := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
⊢ IsInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)
have rwa : ∀ (F_ind : IsInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))
  (F_cl :
    IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)))
  (F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K)
  (F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q),
  IsInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)
Tactic: rwa [EquicontinuousOn.inducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont] at F_ind
Cleared hypotheses: F_ind, F_cl, F_eqcont, F_pointwiseCompact
-- 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 → α
inst_2 : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing (Y := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
⊢ CompactSpace ι
have this : IsInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)
Tactic: have : IsInducing (restrict (⋃₀ 𝔖) ∘ F) := by
    rwa [EquicontinuousOn.inducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont] at F_ind
-- 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 → α
inst_2 : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing (Y := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
this : IsInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)
⊢ CompactSpace ι
have rw : IsCompact (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))
Tactic: rw [← isCompact_univ_iff, this.isCompact_iff, image_univ]
-- 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 → α
inst_2 : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing (Y := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
this : IsInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)
⊢ IsCompact (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))
have F_pointwiseCompact₁ : ∀ x ∈ ⋃₀ 𝔖, ∃ (Q : Set α), IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
Tactic: rw [← forall_sUnion] at F_pointwiseCompact
Cleared hypotheses: F_pointwiseCompact, this
-- 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 → α
inst_2 : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_ind : IsInducing (Y := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)
F_cl : IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F))
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
F_pointwiseCompact : ∀ x ∈ ⋃₀ 𝔖, ∃ (Q : Set α), IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
this : IsInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)
⊢ IsCompact (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))
have choose! : ∀ (Q : (x : X) → Set α) (Q_compact : ∀ x ∈ ⋃₀ 𝔖, IsCompact (Q x)) (F_in_Q : ∀ x ∈ ⋃₀ 𝔖, ∀ (i : ι), F i x ∈ Q x),
  IsCompact (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))
Tactic: choose! Q Q_compact F_in_Q using F_pointwiseCompact
Cleared hypotheses: F_pointwiseCompact
-- 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 → α
inst_2 : TopologicalSpace ι
inst_3 : T2Space α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_clemb : IsClosedEmbedding (Y := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)
s : Set ι
s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (ι := { x : ι // x ∈ s }) (F ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) K
s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q
⊢ IsCompact (closure[inst_2] s)
have rw : CompactSpace.{u_1} (↑(closure[inst_2] s) : Type u_1)
Tactic: rw [isCompact_iff_compactSpace]
-- 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 → α
inst_2 : TopologicalSpace ι
inst_3 : T2Space α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_clemb : IsClosedEmbedding (Y := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)
s : Set ι
s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (ι := { x : ι // x ∈ s }) (F ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) K
s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q
⊢ CompactSpace.{u_1} (↑(closure[inst_2] s) : Type u_1)
have this : ∀ K ∈ 𝔖, ∀ x ∈ K, Continuous[inst_2, inst_1.toTopologicalSpace] (eval (β := fun (x : X) ↦ α) x ∘ F)
Tactic: have : ∀ K ∈ 𝔖, ∀ x ∈ K, Continuous (eval x ∘ F) := fun K hK x hx ↦
    UniformOnFun.uniformContinuous_eval_of_mem _ _ hx hK |>.continuous.comp F_clemb.continuous
-- 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 → α
inst_2 : TopologicalSpace ι
inst_3 : T2Space α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_clemb : IsClosedEmbedding (Y := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)
s : Set ι
s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (ι := { x : ι // x ∈ s }) (F ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) K
s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q
this : ∀ K ∈ 𝔖, ∀ x ∈ K, Continuous[inst_2, inst_1.toTopologicalSpace] (eval (β := fun (x : X) ↦ α) x ∘ F)
⊢ CompactSpace.{u_1} (↑(closure[inst_2] s) : Type u_1)
have cls_eqcont : ∀ K ∈ 𝔖,
  EquicontinuousOn (ι := { x : ι // x ∈ closure[inst_2] s })
    (F ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ closure[inst_2] s)) K
Tactic: have cls_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (F ∘ ((↑) : closure s → ι)) K :=
    fun K hK ↦ (s_eqcont K hK).closure' <| show Continuous (K.restrict ∘ F) from
      continuous_pi fun ⟨x, hx⟩ ↦ this K hK x hx
-- 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 → α
inst_2 : TopologicalSpace ι
inst_3 : T2Space α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_clemb : IsClosedEmbedding (Y := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)
s : Set ι
s_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn (ι := { x : ι // x ∈ s }) (F ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) K
s_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ ∀ i ∈ s, F i x ∈ Q
this : ∀ K ∈ 𝔖, ∀ x ∈ K, Continuous[inst_2, inst_1.toTopologicalSpace] (eval (β := fun (x : X) ↦ α) x ∘ F)
cls_eqcont :
  ∀ K ∈ 𝔖,
    EquicontinuousOn (ι := { x : ι // x ∈ closure[inst_2] s })
      (F ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ closure[inst_2] s)) K
⊢ CompactSpace.{u_1} (↑(closure[inst_2] s) : Type u_1)
have cls_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ closure[inst_2] s ⊆ {i : ι | F i x ∈ Q}
Tactic: have cls_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ closure s ⊆ {i | F i x ∈ Q} :=
    fun K hK x hx ↦ (s_pointwiseCompact K hK x hx).imp fun Q hQ ↦ ⟨hQ.1, closure_minimal hQ.2 <|
      hQ.1.isClosed.preimage (this K hK x hx)⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous (X := X) (α := α) fun (x : (↑S : Type (max u_2 u_3))) ↦ (⇑(↑x : C(X, α)) : (a : X) → α)
h :
  IsInducing (X := (↑S : Type (max u_2 u_3))) (Y :=
    (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
    (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S ⋯) :
      (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
⊢ IsCompact S
have rw : ∀ (hS1 : CompactSpace (↑(ContinuousMap.toFun '' S) : Type (max u_2 u_3)))
  (hS2 : Equicontinuous (X := X) (α := α) fun (x : (↑S : Type (max u_2 u_3))) ↦ (⇑(↑x : C(X, α)) : (a : X) → α))
  (h :
    IsInducing (X := (↑S : Type (max u_2 u_3))) (Y :=
      (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
      (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S sorry) :
        (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))),
  CompactSpace (↑S : Type (max u_2 u_3))
Tactic: rw [isCompact_iff_compactSpace] at hS1 ⊢
Cleared hypotheses: hS1, hS2, h
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous (X := X) (α := α) fun (x : (↑S : Type (max u_2 u_3))) ↦ (⇑(↑x : C(X, α)) : (a : X) → α)
⊢ IsCompact S
have suffices : IsInducing (X := (↑S : Type (max u_2 u_3))) (Y :=
  (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
  (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S sorry) :
    (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
Tactic: suffices h : IsInducing (Equiv.Set.image _ S DFunLike.coe_injective) by
    rw [isCompact_iff_compactSpace] at hS1 ⊢
    exact (Equiv.toHomeomorphOfIsInducing _ h).symm.compactSpace
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous (X := X) (α := α) fun (x : (↑S : Type (max u_2 u_3))) ↦ (⇑(↑x : C(X, α)) : (a : X) → α)
⊢ IsInducing (X := (↑S : Type (max u_2 u_3))) (Y :=
    (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
    (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S ⋯) :
      (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
have rw : IsInducing (X := (↑S : Type (max u_2 u_3))) (Y := X →ᵤ[{K : Set X | IsCompact K}] α)
  (comp (β := X → α) (⇑(UniformOnFun.ofFun {K : Set X | IsCompact K}) : (a : X → α) → X →ᵤ[{K : Set X | IsCompact K}] α)
    (comp (β :=
      { x : (a : X) → α // Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x })
      (Subtype.val (p := fun (x : (a : X) → α) ↦
        Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x))
      (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S sorry) :
        (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))))
Tactic: rw [← IsInducing.subtypeVal.of_comp_iff, ← EquicontinuousOn.isInducing_uniformOnFun_iff_pi _ _ _]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous (X := X) (α := α) fun (x : (↑S : Type (max u_2 u_3))) ↦ (⇑(↑x : C(X, α)) : (a : X) → α)
rw :
  IsInducing (X := (↑S : Type (max u_2 u_3))) (Y := X →ᵤ[{K : Set X | IsCompact K}] α)
    (comp (β := X → α)
      (⇑(UniformOnFun.ofFun {K : Set X | IsCompact K}) : (a : X → α) → X →ᵤ[{K : Set X | IsCompact K}] α)
      (comp (β :=
        { x : (a : X) → α //
          Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x })
        (Subtype.val (p := fun (x : (a : X) → α) ↦
          Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x))
        (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S ⋯) :
          (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))))
⊢ IsInducing (X := (↑S : Type (max u_2 u_3))) (Y :=
    (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
    (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S ⋯) :
      (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
have rw₁ : Set (Set X)
Tactic: rw [← IsInducing.subtypeVal.of_comp_iff, ← EquicontinuousOn.isInducing_uniformOnFun_iff_pi _ _ _]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Ascoli (goal)
Goal:
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous (X := X) (α := α) fun (x : (↑S : Type (max u_2 u_3))) ↦ (⇑(↑x : C(X, α)) : (a : X) → α)
rw :
  IsInducing (X := (↑S : Type (max u_2 u_3))) (Y := X →ᵤ[{K : Set X | IsCompact K}] α)
    (comp (β := X → α)
      (⇑(UniformOnFun.ofFun {K : Set X | IsCompact K}) : (a : X → α) → X →ᵤ[{K : Set X | IsCompact K}] α)
      (comp (β :=
        { x : (a : X) → α //
          Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x })
        (Subtype.val (p := fun (x : (a : X) → α) ↦
          Membership.mem (γ := Set ((a : X) → α)) ((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) x))
        (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S ⋯) :
          (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))))
rw₁ : Set (Set X)
⊢ IsInducing (X := (↑S : Type (max u_2 u_3))) (Y :=
    (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
    (⇑(Equiv.Set.image (fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) S ⋯) :
      (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
have rw₂ : Eq.{u_2 + 1} (α := Set X) (⋃₀ {K : Set X | IsCompact K}) univ
Tactic: rw [← IsInducing.subtypeVal.of_comp_iff, ← EquicontinuousOn.isInducing_uniformOnFun_iff_pi _ _ _]