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 → α
inst_2 : TopologicalSpace ι
inst_3 : CompactSpace X
F_eqcont : Equicontinuous F
⊢ IsInducing (Y := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F) ↔ IsInducing F
have rw : inst_2 = TopologicalSpace.induced ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F) (UniformFun.topologicalSpace X α) ↔
  inst_2 = TopologicalSpace.induced F (Pi.topologicalSpace (Y := fun (a : X) ↦ α))
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 ι
inst_3 : CompactSpace X
F_eqcont : Equicontinuous F
⊢ inst_2 = TopologicalSpace.induced ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F) (UniformFun.topologicalSpace X α) ↔
    inst_2 = TopologicalSpace.induced F (Pi.topologicalSpace (Y := fun (a : X) ↦ α))
have change : inst_2 = UniformSpace.toTopologicalSpace ↔ inst_2 = UniformSpace.toTopologicalSpace
Tactic: change (_ = (UniformFun.uniformSpace X α |>.comap F |>.toTopologicalSpace)) ↔
         (_ = (Pi.uniformSpace _ |>.comap 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 ι
inst_3 : CompactSpace X
F_eqcont : Equicontinuous F
⊢ inst_2 = UniformSpace.toTopologicalSpace ↔ inst_2 = UniformSpace.toTopologicalSpace
have rw : inst_2 = UniformSpace.toTopologicalSpace ↔ inst_2 = UniformSpace.toTopologicalSpace
Tactic: rw [F_eqcont.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 → α
inst_2 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) ↔
    Tendsto F ℱ (𝓝 f)
have inl : Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ⊥
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) ↔
  Tendsto F ⊥ (𝓝 f)
Tactic: rcases ℱ.eq_or_neBot with rfl | ℱ_ne
Cleared hypotheses: ℱ
-- 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 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
inl :
  Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ⊥
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) ↔
    Tendsto F ⊥ (𝓝 f)
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) ↔
    Tendsto F ℱ (𝓝 f)
have inr : ∀ (ℱ_ne : ℱ.NeBot),
  Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) ↔
    Tendsto F ℱ (𝓝 f)
Tactic: rcases ℱ.eq_or_neBot with rfl | ℱ_ne
-- 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 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) ↔
    Tendsto F ℱ (𝓝 f)
have inr : Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) →
  Tendsto F ℱ (𝓝 f)
Tactic: constructor
-- 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 : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
inr :
  Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) →
    Tendsto F ℱ (𝓝 f)
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
      (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α)) ↔
    Tendsto F ℱ (𝓝 f)
have inr₁ : Tendsto F ℱ (𝓝 f) →
  Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
Tactic: constructor
-- 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 : 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 ℱ)
⊢ Equicontinuous (ι := (↑(range F) : Type (max u_3 u_2))) (id ∘ Subtype.val (p := fun (x : X → α) ↦ x ∈ range F))
have 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))
Tactic: rwa [equicontinuous_iff_range] at F_eqcont
Cleared hypotheses: F_eqcont, ℱ, f, ℱ_ne, H, S, 𝒢
-- 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 : 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 ℱ)
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
have hS : S.Equicontinuous
Tactic: have hS : S.Equicontinuous := closure' (by rwa [equicontinuous_iff_range] at F_eqcont)
      continuous_id
-- 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 : 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
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
have 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))
Tactic: have ind : IsInducing (UniformFun.ofFun ∘ (↑) : S → X →ᵤ α) :=
      hS.inducing_uniformFun_iff_pi.mpr ⟨rfl⟩
-- 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 : 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))
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
have f_mem : f ∈ S
Tactic: have f_mem : f ∈ S := mem_closure_of_tendsto H range_mem_map
-- 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 : 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
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
have h𝒢ℱ : 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)
-- 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 : 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))
have rwa : 𝒢 ≤ 𝓝 (Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem)
Tactic: rwa [tendsto_id', nhds_induced, ← map_le_iff_le_comap, h𝒢ℱ]
-- 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 : 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)
⊢ Tendsto id 𝒢 (𝓝 (Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem))
have rwa₁ : 𝒢 ≤
  comap (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) (𝓝 (↑(Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem) : X → α))
Tactic: rwa [tendsto_id', nhds_induced, ← map_le_iff_le_comap, h𝒢ℱ]
-- 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 : 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 → α))
⊢ Tendsto id 𝒢 (𝓝 (Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem))
have rwa₂ : map (Subtype.val (p := fun (x : X → α) ↦ x ∈ S)) 𝒢 ≤ 𝓝 (↑(Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem) : X → α)
Tactic: rwa [tendsto_id', nhds_induced, ← map_le_iff_le_comap, h𝒢ℱ]
-- 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 : 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 → α)
⊢ Tendsto id 𝒢 (𝓝 (Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem))
have rwa₃ : map F ℱ ≤ 𝓝 (↑(Subtype.mk (p := fun (x : X → α) ↦ x ∈ S) f f_mem) : X → α)
Tactic: rwa [tendsto_id', nhds_induced, ← map_le_iff_le_comap, h𝒢ℱ]
-- 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 : 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 (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
have H' : 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𝒢ℱ]
-- 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 : 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))
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
have 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 →ᵤ α))
Tactic: rwa [ind.tendsto_nhds_iff, comp_id, ← tendsto_map'_iff, h𝒢ℱ] at H'
Cleared hypotheses: H'
-- 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 : 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 →ᵤ α))
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
have 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 →ᵤ α))
Tactic: rwa [ind.tendsto_nhds_iff, comp_id, ← tendsto_map'_iff, h𝒢ℱ] at H'
Cleared hypotheses: H'
-- 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 : 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 →ᵤ α))
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
have 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 →ᵤ α))
Tactic: rwa [ind.tendsto_nhds_iff, comp_id, ← tendsto_map'_iff, h𝒢ℱ] at H'
Cleared hypotheses: H'
-- 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 : 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 →ᵤ α))
⊢ Tendsto (β := X →ᵤ α) ((⇑UniformFun.ofFun : (a : X → α) → X →ᵤ α) ∘ F : ι → X →ᵤ α) ℱ
    (𝓝 ((UniformFun.ofFun : (a : X → α) → X →ᵤ α) f) : Filter (X →ᵤ α))
have 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 →ᵤ α))
Tactic: rwa [ind.tendsto_nhds_iff, comp_id, ← tendsto_map'_iff, h𝒢ℱ] at H'
Cleared hypotheses: H'