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 : 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
rwa rwa₁ rwa₂ 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)
⊢ IsInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)

Tactic:
rwa [EquicontinuousOn.inducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont] at F_ind

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)
𝔖_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)

Tactic:
have : IsInducing (restrict (⋃₀ 𝔖) ∘ F) := by
    rwa [EquicontinuousOn.inducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont] at F_ind
-- 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_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)
rw : IsCompact (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))
⊢ CompactSpace ι

Tactic:
rw [← isCompact_univ_iff, this.isCompact_iff, image_univ]

Premises used: Set.image_univ, isCompact_univ_iff, Topology.IsInducing.isCompact_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_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)
⊢ ∀ x ∈ ⋃₀ 𝔖, ∃ (Q : Set α), IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q

Tactic:
rw [← forall_sUnion] at F_pointwiseCompact

Premises used: forall_sUnion
-- 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_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)
F_pointwiseCompact₁ : ∀ x ∈ ⋃₀ 𝔖, ∃ (Q : Set α), IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q
⊢ IsInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)

Tactic:
rw [← forall_sUnion] at F_pointwiseCompact

Premises used: forall_sUnion
-- 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_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)
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))
⊢ IsCompact (range ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F))

Tactic:
choose! Q Q_compact F_in_Q using F_pointwiseCompact
-- 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_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
this : IsInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)
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:
IsCompact.of_isClosed_subset (isCompact_univ_pi fun x ↦ Q_compact x x.2)
    (EquicontinuousOn.isClosed_range_pi_of_uniformOnFun' 𝔖_compact F_eqcont F_cl)
    (range_subset_iff.mpr fun i x _ ↦ F_in_Q x x.2 i)

Premises used: Iff.mpr, EquicontinuousOn.isClosed_range_pi_of_uniformOnFun', isCompact_univ_pi, IsCompact.of_isClosed_subset, Set.range_subset_iff, Subtype.val, Subtype.property
-- 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_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
this : IsInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)
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:
refine IsCompact.of_isClosed_subset (isCompact_univ_pi fun x ↦ Q_compact x x.2)
    (EquicontinuousOn.isClosed_range_pi_of_uniformOnFun' 𝔖_compact F_eqcont F_cl)
    (range_subset_iff.mpr fun i x _ ↦ F_in_Q x x.2 i)
-- 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_clemb : IsClosedEmbedding (Y := X →ᵤ[𝔖] α) ((⇑(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 ι

Tactic:
compactSpace_of_closed_inducing' 𝔖_compact F_clemb.isInducing F_clemb.isClosed_range
    F_eqcont F_pointwiseCompact

Premises used: Topology.IsClosedEmbedding.isInducing, ArzelaAscoli.compactSpace_of_closed_inducing', Topology.IsClosedEmbedding.isClosed_range
-- 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 ι
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
rw : CompactSpace.{u_1} (↑(closure[inst_2] s) : Type u_1)
⊢ IsCompact (closure[inst_2] s)

Tactic:
rw [isCompact_iff_compactSpace]

Premises used: isCompact_iff_compactSpace
-- 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 ι
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
⊢ ∀ 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
-- 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 ι
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)
⊢ ∀ 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
-- 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 ι
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
⊢ ∀ 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)⟩
-- 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 ι
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
cls_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ closure[inst_2] s ⊆ {i : ι | F i x ∈ Q}
K : Set X
hK : K ∈ 𝔖
x : X
hx : x ∈ K
Q : Set α
hQ : IsCompact Q ∧ closure[inst_2] s ⊆ {i : ι | F i x ∈ Q}
⊢ ∀ (i : (↑(closure[inst_2] s) : Type u_1)), F (↑i : ι) x ∈ Q

Tactic:
simpa using hQ.2

Premises used: And.right
-- 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 ι
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
cls_pointwiseCompact : ∀ K ∈ 𝔖, ∀ x ∈ K, ∃ (Q : Set α), IsCompact Q ∧ closure[inst_2] s ⊆ {i : ι | F i x ∈ Q}
⊢ CompactSpace.{u_1} (↑(closure[inst_2] s) : Type u_1)

Tactic:
exact ArzelaAscoli.compactSpace_of_isClosedEmbedding 𝔖_compact
    (F_clemb.comp isClosed_closure.isClosedEmbedding_subtypeVal) cls_eqcont
    fun K hK x hx ↦ (cls_pointwiseCompact K hK x hx).imp fun Q hQ ↦ ⟨hQ.1, by simpa using hQ.2⟩

Premises used: ArzelaAscoli.compactSpace_of_isClosedEmbedding, Topology.IsClosedEmbedding.comp, Exists.imp, And.intro, IsClosed.isClosedEmbedding_subtypeVal, isClosed_closure
-- Module: Mathlib.Topology.UniformSpace.Ascoli
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)))
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 ⋯) :
          (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))
⊢ IsCompact S

Tactic:
rw [isCompact_iff_compactSpace] at hS1 ⊢

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
S : Set C(X, α)
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 ⋯) :
      (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:
(Equiv.toHomeomorphOfIsInducing _ h).symm.compactSpace

Premises used: Homeomorph.compactSpace, Homeomorph.symm, Equiv.toHomeomorphOfIsInducing
-- Module: Mathlib.Topology.UniformSpace.Ascoli
Goal:
X : Type u_2
α : Type u_3
inst : TopologicalSpace X
inst_1 : UniformSpace α
S : Set C(X, α)
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 ⋯) :
      (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:
exact (Equiv.toHomeomorphOfIsInducing _ h).symm.compactSpace

Premises used: Homeomorph.compactSpace, Homeomorph.symm, Equiv.toHomeomorphOfIsInducing
-- Module: Mathlib.Topology.UniformSpace.Ascoli
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) → α)
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 ⋯) :
      (a : (↑S : Type (max u_2 u_3))) → (↑((fun (f : C(X, α)) ↦ (⇑f : (a : X) → α)) '' S) : Type (max u_2 u_3)))
⊢ IsCompact S

Tactic:
suffices h : IsInducing (Equiv.Set.image _ S DFunLike.coe_injective) by
    rw [isCompact_iff_compactSpace] at hS1 ⊢
    exact (Equiv.toHomeomorphOfIsInducing _ h).symm.compactSpace
-- Module: Mathlib.Topology.UniformSpace.Ascoli
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)
rw₂ : Eq.{u_2 + 1} (α := Set X) (⋃₀ {K : Set X | IsCompact K}) univ
rw₃ : ∀ (K : Set X), Membership.mem (γ := Set (Set X)) {K : Set X | IsCompact K} K → IsCompact K
rw₄ :
  ∀ (K : Set X),
    Membership.mem (γ := Set (Set X)) {K : Set X | IsCompact K} K →
      EquicontinuousOn (ι := (↑S : Type (max u_2 u_3))) (α := α)
        (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))))
        K
⊢ 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)))

Tactic:
rw [← IsInducing.subtypeVal.of_comp_iff, ← EquicontinuousOn.isInducing_uniformOnFun_iff_pi _ _ _]

Premises used: Topology.IsInducing.of_comp_iff, EquicontinuousOn.isInducing_uniformOnFun_iff_pi, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.UniformSpace.Ascoli
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 := 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)))))

Tactic:
ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact.isInducing.comp .subtypeVal

Premises used: Topology.IsInducing.comp, IsUniformEmbedding.toIsUniformInducing, IsUniformInducing.isInducing, ContinuousMap.toUniformOnFunIsCompact, ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.UniformSpace.Ascoli
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 := 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)))))

Tactic:
exact ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact.isInducing.comp .subtypeVal

Premises used: Topology.IsInducing.comp, IsUniformEmbedding.toIsUniformInducing, IsUniformInducing.isInducing, ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.UniformSpace.Ascoli
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) → α)
⊢ Eq.{u_2 + 1} (α := Set X) (⋃₀ {K : Set X | IsCompact K}) univ

Tactic:
eq_univ_iff_forall.mpr (fun x ↦ mem_sUnion_of_mem (mem_singleton x) isCompact_singleton)

Premises used: Iff.mpr, Set.mem_singleton, Set.eq_univ_iff_forall, isCompact_singleton, Set.mem_sUnion_of_mem