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 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H :
  Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
⊢ Tendsto F ℱ (𝓝 f)

Tactic:
exact UniformFun.uniformContinuous_toFun.continuous.tendsto _ |>.comp H

Premises used: UniformContinuous.continuous, Continuous.tendsto, UniformFun.uniformContinuous_toFun, Filter.Tendsto.comp
-- 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 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter (↑S : Type (max u_2 u_3)) := comap (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) (map F ℱ)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (F_eqcont : Equicontinuous (ι := { x : X → α // x ∈ range F }) (Subtype.val (p := fun (x : X → α) ↦ x ∈ range F)))
    (ℱ : Filter ι) (f : X → α) (ℱ_ne : ℱ.NeBot) (H : Tendsto F ℱ (𝓝 f)),
    Equicontinuous (ι := (↑(range F) : Type (max u_3 u_2))) (id ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ range F))
⊢ Equicontinuous (ι := (↑(range F) : Type (max u_3 u_2))) (id ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ range F))

Tactic:
rwa [equicontinuous_iff_range] at F_eqcont

Premises used: equicontinuous_iff_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 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter (↑S : Type (max u_2 u_3)) := comap (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) (map F ℱ)
⊢ S.Equicontinuous

Tactic:
have hS : S.Equicontinuous := closure' (by rwa [equicontinuous_iff_range] at F_eqcont)
      continuous_id
-- 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 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter (↑S : Type (max u_2 u_3)) := comap (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) (map F ℱ)
hS : S.Equicontinuous
⊢ IsInducing (X := (↑S : Type (max u_2 u_3))) (Y := X →ᵤ α)
    ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ S))

Tactic:
have ind : IsInducing (UniformFun.ofFun ∘ (↑) : S → X →ᵤ α) :=
      hS.inducing_uniformFun_iff_pi.mpr ⟨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 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter (↑S : Type (max u_2 u_3)) := comap (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) (map F ℱ)
hS : S.Equicontinuous
ind :
  IsInducing (X := (↑S : Type (max u_2 u_3))) (Y := X →ᵤ α)
    ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ S))
⊢ f ∈ S

Tactic:
have f_mem : f ∈ S := mem_closure_of_tendsto H range_mem_map
-- 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 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter (↑S : Type (max u_2 u_3)) := comap (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) (map F ℱ)
hS : S.Equicontinuous
ind :
  IsInducing (X := (↑S : Type (max u_2 u_3))) (Y := X →ᵤ α)
    ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ S))
f_mem : f ∈ S
⊢ map (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) 𝒢 = map F ℱ

Tactic:
have h𝒢ℱ : map (↑) 𝒢 = map F ℱ := Filter.map_comap_of_mem
      (Subtype.range_coe ▸ mem_of_superset range_mem_map subset_closure)
-- 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 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter (↑S : Type (max u_2 u_3)) := comap (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) (map F ℱ)
hS : S.Equicontinuous
ind :
  IsInducing (X := (↑S : Type (max u_2 u_3))) (Y := X →ᵤ α)
    ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ S))
f_mem : f ∈ S
h𝒢ℱ : map (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) 𝒢 = map F ℱ
rwa : 𝒢 ≤ 𝓝 (Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem)
rwa₁ :
  𝒢 ≤
    comap (Subtype.val (p := fun (x : X → α) ↦ x ∈ S))
      (𝓝 (↑(Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem) : X → α))
rwa₂ :
  map (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) 𝒢 ≤ 𝓝 (↑(Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem) : X → α)
rwa₃ rwa₄ rwa₅ rwa₆ : map F ℱ ≤ 𝓝 (↑(Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem) : X → α)
⊢ Tendsto id 𝒢 (𝓝 (Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem))

Tactic:
rwa [tendsto_id', nhds_induced, ← map_le_iff_le_comap, h𝒢ℱ]

Premises used: Filter.tendsto_id', nhds_induced, Filter.map_le_iff_le_comap
-- 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 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter (↑S : Type (max u_2 u_3)) := comap (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) (map F ℱ)
hS : S.Equicontinuous
ind :
  IsInducing (X := (↑S : Type (max u_2 u_3))) (Y := X →ᵤ α)
    ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ S))
f_mem : f ∈ S
h𝒢ℱ : map (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) 𝒢 = map F ℱ
⊢ Tendsto id 𝒢 (𝓝 (Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem))

Tactic:
have H' : Tendsto id 𝒢 (𝓝 ⟨f, f_mem⟩) := by
      rwa [tendsto_id', nhds_induced, ← map_le_iff_le_comap, 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 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter (↑S : Type (max u_2 u_3)) := comap (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) (map F ℱ)
hS : S.Equicontinuous
ind :
  IsInducing (X := (↑S : Type (max u_2 u_3))) (Y := X →ᵤ α)
    ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ S))
f_mem : f ∈ S
h𝒢ℱ : map (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) 𝒢 = map F ℱ
H' : Tendsto id 𝒢 (𝓝 (Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem))
inr :
  ∀
    (H' :
      Tendsto (β := X →ᵤ α)
        (((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) ∘ id) 𝒢
        (𝓝
          (((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ S))
            (Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem)))),
    Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
inr₁ :
  ∀
    (H' :
      Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) 𝒢
        (𝓝
          (((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ S))
            (Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem)))),
    Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
inr₂ :
  ∀
    (H' :
      Tendsto (β := X →ᵤ α) (⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α)
        (map (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) 𝒢)
        (𝓝
          (((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ S))
            (Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem)))),
    Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
inr₃ inr₄ inr₅ inr₆ :
  ∀
    (H' :
      Tendsto (β := X →ᵤ α) (⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) (map F ℱ)
        (𝓝
          (((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ S))
            (Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem)))),
    Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))

Tactic:
rwa [ind.tendsto_nhds_iff, comp_id, ← tendsto_map'_iff, h𝒢ℱ] at H'

Premises used: Function.comp_id, Filter.tendsto_map'_iff, Topology.IsInducing.tendsto_nhds_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 → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)

Tactic:
have H1 : (UniformOnFun.uniformSpace X α 𝔖).comap F =
      ⨅ (K ∈ 𝔖), (UniformFun.uniformSpace _ _).comap (K.restrict ∘ F) := by
    simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, ← UniformSpace.comap_comap,
      UniformFun.ofFun, Equiv.coe_fn_mk, UniformOnFun.toFun, UniformOnFun.ofFun, Function.comp_def,
      UniformFun, Equiv.coe_fn_symm_mk]
-- 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
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
simp_rw :
  UniformSpace.comap F
      (UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α))
        (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α)) =
    ⨅ K ∈ 𝔖,
      UniformSpace.comap F
        (UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α)) (Pi.uniformSpace fun (i : (↑K : Type u_2)) ↦ α))
simp_rw₁ :
  UniformSpace.comap F
      (⨅ S ∈ 𝔖,
        UniformSpace.comap (S.restrict (π := fun (x : X) ↦ α)) (Pi.uniformSpace fun (i : (↑S : Type u_2)) ↦ α)) =
    ⨅ K ∈ 𝔖,
      UniformSpace.comap F
        (UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α)) (Pi.uniformSpace fun (i : (↑K : Type u_2)) ↦ α))
⊢ UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑K : Type u_2)) ↦ α)

Tactic:
simp_rw [UniformSpace.comap_comap, Pi.uniformSpace_comap_restrict_sUnion (fun _ ↦ α) 𝔖,
      UniformSpace.comap_iInf]

Premises used: UniformSpace.comap_comap, UniformSpace.comap_iInf, Pi.uniformSpace_comap_restrict_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 → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
⊢ UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑K : Type u_2)) ↦ α)

Tactic:
have H2 : (Pi.uniformSpace _).comap ((⋃₀ 𝔖).restrict ∘ F) =
      ⨅ (K ∈ 𝔖), (Pi.uniformSpace _).comap (K.restrict ∘ F) := by
    simp_rw [UniformSpace.comap_comap, Pi.uniformSpace_comap_restrict_sUnion (fun _ ↦ α) 𝔖,
      UniformSpace.comap_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
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
H2 :
  UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑K : Type u_2)) ↦ α)
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
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
H2 :
  UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑K : Type u_2)) ↦ α)
K : Set X
hK : K ∈ 𝔖
this : CompactSpace.{u_2} (↑K : Type u_2)
⊢ UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α) =
    UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑K : Type u_2)) ↦ α)

Tactic:
(equicontinuous_restrict_iff _ |>.mpr <| F_eqcont K hK).comap_uniformFun_eq

Premises used: Iff.mpr, equicontinuous_restrict_iff, Equicontinuous.comap_uniformFun_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
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
H2 :
  UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑K : Type u_2)) ↦ α)
K : Set X
hK : K ∈ 𝔖
this : CompactSpace.{u_2} (↑K : Type u_2)
⊢ UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α) =
    UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑K : Type u_2)) ↦ α)

Tactic:
exact (equicontinuous_restrict_iff _ |>.mpr <| F_eqcont K hK).comap_uniformFun_eq

Premises used: Iff.mpr, equicontinuous_restrict_iff, Equicontinuous.comap_uniformFun_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
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
H2 :
  UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑K : Type u_2)) ↦ α)
⊢ ∀ K ∈ 𝔖,
    UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α) =
      UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑K : Type u_2)) ↦ α)

Tactic:
have H3 : ∀ K ∈ 𝔖, (UniformFun.uniformSpace K α).comap (K.restrict ∘ F) =
      (Pi.uniformSpace _).comap (K.restrict ∘ F) := fun K hK ↦ by
    have : CompactSpace K := isCompact_iff_compactSpace.mp (𝔖_compact K hK)
    exact (equicontinuous_restrict_iff _ |>.mpr <| F_eqcont K hK).comap_uniformFun_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
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
H2 :
  UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑K : Type u_2)) ↦ α)
H3 :
  ∀ K ∈ 𝔖,
    UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α) =
      UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑K : Type u_2)) ↦ α)
simp_rw :
  ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α) =
    UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α)
simp_rw₁ :
  Eq.{u_1 + 1} (α := UniformSpace ι)
    (⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α))
    (⨅ K ∈ 𝔖,
      UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑K : Type u_2)) ↦ α))
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α)

Tactic:
simp_rw [H1, H2, iInf_congr fun K ↦ iInf_congr fun hK ↦ H3 K hK]

Premises used: iInf_congr
-- 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)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
rw :
  UniformSpace.comap ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) (UniformOnFun.uniformSpace X α 𝔖) =
      inst_2 ↔
    UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = inst_2
⊢ IsUniformInducing (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) ↔
    IsUniformInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)

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

Premises used: isUniformInducing_iff_uniformSpace, 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 : UniformSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ UniformSpace.comap ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) (UniformOnFun.uniformSpace X α 𝔖) =
      inst_2 ↔
    UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = inst_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 → α
inst_2 : UniformSpace ι
𝔖 : 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 : UniformSpace ι
𝔖 : 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 : UniformSpace ι
𝔖 : 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 : 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)
⊢ (⋃₀ 𝔖).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 : 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)
rw :
  IsUniformInducing (β := (a : (↑(⋃₀ 𝔖) : Type u_2)) → α) ((⇑φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) ∘ F) ↔
    IsUniformInducing F
⊢ IsUniformInducing (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) ↔ IsUniformInducing F

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

Premises used: EquicontinuousOn.isUniformInducing_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 : 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:
⟨fun H ↦ φ.isUniformInducing.comp H, fun H ↦ φ.symm.isUniformInducing.comp H⟩

Premises used: UniformEquiv.symm, Iff.intro, UniformEquiv.isUniformInducing, IsUniformInducing.comp