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
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
have simp_rw : UniformSpace.comap F
    (⨅ s ∈ 𝔖,
      UniformSpace.comap (β := UniformFun.{u_2, u_3} (↑s : Type u_2) α)
        (Function.comp (β := (↑s : Type u_2) → α)
          ((⇑UniformFun.ofFun : (a : (↑s : Type u_2) → α) → UniformFun.{u_2, u_3} (↑s : Type u_2) α) :
            (a : (↑s : Type u_2) → α) → UniformFun.{u_2, u_3} (↑s : Type u_2) α)
          (Function.comp (β := X → α) (s.restrict (π := fun (a : X) ↦ α))
              (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
            (X →ᵤ[𝔖] α) → (↑s : Type u_2) → α))
        (UniformFun.uniformSpace (↑s : Type u_2) α)) =
  ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
Tactic: 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]
-- 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
simp_rw :
  UniformSpace.comap F
      (⨅ s ∈ 𝔖,
        UniformSpace.comap (β := UniformFun.{u_2, u_3} (↑s : Type u_2) α)
          (Function.comp (β := (↑s : Type u_2) → α)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_2) → α) → UniformFun.{u_2, u_3} (↑s : Type u_2) α) :
              (a : (↑s : Type u_2) → α) → UniformFun.{u_2, u_3} (↑s : Type u_2) α)
            (Function.comp (β := X → α) (s.restrict (π := fun (a : X) ↦ α))
                (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
              (X →ᵤ[𝔖] α) → (↑s : Type u_2) → α))
          (UniformFun.uniformSpace (↑s : Type u_2) α)) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
have simp_rw₁ : Eq.{u_1 + 1} (α := UniformSpace ι)
  (⨅ i ∈ 𝔖,
    UniformSpace.comap F
      (UniformSpace.comap (β := UniformFun.{u_2, u_3} (↑i : Type u_2) α)
        (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) → α))
        (UniformFun.uniformSpace (↑i : Type u_2) α)))
  (⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α))
Tactic: 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]
-- 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
simp_rw :
  UniformSpace.comap F
      (⨅ s ∈ 𝔖,
        UniformSpace.comap (β := UniformFun.{u_2, u_3} (↑s : Type u_2) α)
          (Function.comp (β := (↑s : Type u_2) → α)
            ((⇑UniformFun.ofFun : (a : (↑s : Type u_2) → α) → UniformFun.{u_2, u_3} (↑s : Type u_2) α) :
              (a : (↑s : Type u_2) → α) → UniformFun.{u_2, u_3} (↑s : Type u_2) α)
            (Function.comp (β := X → α) (s.restrict (π := fun (a : X) ↦ α))
                (⇑(UniformOnFun.toFun 𝔖) : (a : X →ᵤ[𝔖] α) → X → α) :
              (X →ᵤ[𝔖] α) → (↑s : Type u_2) → α))
          (UniformFun.uniformSpace (↑s : Type u_2) α)) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
simp_rw₁ :
  Eq.{u_1 + 1} (α := UniformSpace ι)
    (⨅ i ∈ 𝔖,
      UniformSpace.comap F
        (UniformSpace.comap (β := UniformFun.{u_2, u_3} (↑i : Type u_2) α)
          (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) → α))
          (UniformFun.uniformSpace (↑i : Type u_2) α)))
    (⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α))
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
have simp_rw₂ : Eq.{u_1 + 1} (α := UniformSpace ι)
  (⨅ i ∈ 𝔖,
    UniformSpace.comap (β := UniformFun.{u_2, u_3} (↑i : Type u_2) α)
      (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) → α) ∘
        F)
      (UniformFun.uniformSpace (↑i : Type u_2) α))
  (⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α))
Tactic: 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]
-- 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
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α)
have H1 : 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]
-- 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
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)) ↦ α)
have 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)) ↦ α))
Tactic: simp_rw [UniformSpace.comap_comap, Pi.uniformSpace_comap_restrict_sUnion (fun _ ↦ α) 𝔖,
      UniformSpace.comap_iInf]
-- 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
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)) ↦ α))
⊢ 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)) ↦ α)
have 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)) ↦ α))
Tactic: simp_rw [UniformSpace.comap_comap, Pi.uniformSpace_comap_restrict_sUnion (fun _ ↦ α) 𝔖,
      UniformSpace.comap_iInf]
-- 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
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.restrict (π := fun (a : X) ↦ α) ∘ F) (UniformFun.uniformSpace (↑K : Type u_2) α)
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α)
have 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)) ↦ α)
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]
-- 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
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 ∈ 𝔖
⊢ 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)) ↦ α)
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 (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
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)) ↦ α)
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α)
have 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)) ↦ α)
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
-- 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
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)) ↦ α)
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α)
have 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)) ↦ α)
Tactic: simp_rw [H1, H2, iInf_congr fun K ↦ iInf_congr fun hK ↦ H3 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
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)) ↦ α)
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    UniformSpace.comap ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) (Pi.uniformSpace fun (i : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α)
have 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)) ↦ α))
Tactic: simp_rw [H1, H2, iInf_congr fun K ↦ iInf_congr fun hK ↦ H3 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 → α
inst_2 : UniformSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsUniformInducing (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) ↔
    IsUniformInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)
have rw : UniformSpace.comap ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) (UniformOnFun.uniformSpace X α 𝔖) =
    inst_2 ↔
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = inst_2
Tactic: rw [isUniformInducing_iff_uniformSpace, isUniformInducing_iff_uniformSpace,
      ← EquicontinuousOn.comap_uniformOnFun_eq 𝔖_compact F_eqcont]
-- 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 : UniformSpace ι
𝔖 : Set (Set X)
𝔖_covers : ⋃₀ 𝔖 = univ
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsUniformInducing (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) ↔ IsUniformInducing F
have 𝔖_covers₁ : ∀ (x : X), x ∈ ⋃₀ 𝔖
Tactic: rw [eq_univ_iff_forall] at 𝔖_covers
Cleared hypotheses: 𝔖_covers, 𝔖_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 → α
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 (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) ↔ IsUniformInducing F
have rw : IsUniformInducing (β := (a : (↑(⋃₀ 𝔖) : Type u_2)) → α) ((⇑φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) ∘ F) ↔
  IsUniformInducing F
Tactic: rw [EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont,
      show restrict (⋃₀ 𝔖) ∘ F = φ.symm ∘ F by rfl]
-- 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_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsInducing (Y := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) ↔
    IsInducing ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)
have rw : inst_2 =
    TopologicalSpace.induced ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)
      (UniformOnFun.topologicalSpace X α 𝔖) ↔
  inst_2 =
    TopologicalSpace.induced ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)
      (Pi.topologicalSpace (Y := fun (a : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α))
Tactic: rw [isInducing_iff, isInducing_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 → α
inst_2 : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ inst_2 =
      TopologicalSpace.induced ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F)
        (UniformOnFun.topologicalSpace X α 𝔖) ↔
    inst_2 =
      TopologicalSpace.induced ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F)
        (Pi.topologicalSpace (Y := fun (a : (↑(⋃₀ 𝔖) : Type u_2)) ↦ α))
have change : inst_2 = UniformSpace.toTopologicalSpace ↔ inst_2 = UniformSpace.toTopologicalSpace
Tactic: change (_ = ((UniformOnFun.uniformSpace X α 𝔖).comap F).toTopologicalSpace) ↔
    (_ = ((Pi.uniformSpace _).comap ((⋃₀ 𝔖).restrict ∘ F)).toTopologicalSpace)
-- 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_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ inst_2 = UniformSpace.toTopologicalSpace ↔ inst_2 = UniformSpace.toTopologicalSpace
have rw : inst_2 = UniformSpace.toTopologicalSpace ↔ inst_2 = UniformSpace.toTopologicalSpace
Tactic: rw [← EquicontinuousOn.comap_uniformOnFun_eq 𝔖_compact F_eqcont]
-- 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)
𝔖_covers : ⋃₀ 𝔖 = univ
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsInducing (Y := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) ↔ IsInducing F
have 𝔖_covers₁ : ∀ (x : X), x ∈ ⋃₀ 𝔖
Tactic: rw [eq_univ_iff_forall] at 𝔖_covers
Cleared hypotheses: 𝔖_covers, 𝔖_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 → α
inst_2 : TopologicalSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : ((↑(⋃₀ 𝔖) : Type u_2) → α) ≃ₜ (X → α) :=
  Homeomorph.piCongrLeft (Y := fun (x : X) ↦ α) (Equiv.subtypeUnivEquiv (p := Membership.mem (⋃₀ 𝔖)) 𝔖_covers)
⊢ IsInducing (Y := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F) ↔ IsInducing F
have rw : IsInducing (Y := (a : (↑(⋃₀ 𝔖) : Type u_2)) → α) ((⇑φ.symm : (a : X → α) → (↑(⋃₀ 𝔖) : Type u_2) → α) ∘ F) ↔ IsInducing F
Tactic: rw [EquicontinuousOn.inducing_uniformOnFun_iff_pi' 𝔖_compact F_eqcont,
      show restrict (⋃₀ 𝔖) ∘ F = φ.symm ∘ F by rfl]
-- 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 ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) ∘ F) ℱ (𝓝 ((⋃₀ 𝔖).restrict (π := fun (a : X) ↦ α) f))
have rw : Tendsto (β := X →ᵤ[𝔖] α) ((⇑(UniformOnFun.ofFun 𝔖) : (a : X → α) → X →ᵤ[𝔖] α) ∘ F : ι → X →ᵤ[𝔖] α) ℱ
    (𝓝 ((UniformOnFun.ofFun 𝔖 : (a : X → α) → X →ᵤ[𝔖] α) f) : Filter (X →ᵤ[𝔖] α)) ↔
  Tendsto F ℱ (𝓝 f)
Tactic: rw [← Filter.tendsto_comap_iff (g := (⋃₀ 𝔖).restrict), ← nhds_induced]