awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (hypothesis)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
⊢ Eq (α := UniformSpace C(α, β)) inferInstance
    (⨅ (i : ι),
      UniformSpace.comap (β := ContinuousMap.{u_1, u₂} (δ i) β) (fun (x : C(α, β)) ↦ x.comp (φ i)) inferInstance)
have h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
Tactic: have h_preimage : ∀ i, MapsTo (φ i ⁻¹' ·) 𝔖 (𝔗 i) := fun i K ↦ (h_proper i).isCompact_preimage
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
⊢ ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
have refine : (⋃ (i : ι),
      ⋃ (_ :
        Membership.mem (γ := Set ι) {i : ι | (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty} i),
        range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) ∩
    S =
  S
Tactic: refine ⟨{i | (range (φ i) ∩ S).Nonempty}, h_lf.finite_nonempty_inter_compact hS,
      inter_eq_right.mp ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
⊢ (⋃ (i : ι),
        ⋃ (_ :
          Membership.mem (γ := Set ι) {i : ι | (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty}
            i),
          range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) ∩
      S =
    S
have simp_rw : ⋃ (i : ι),
    ⋃ (_ :
      Membership.mem (γ := Set ι) {i : ι | (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty} i),
      range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S =
  S
Tactic: simp_rw [iUnion₂_inter, mem_setOf, iUnion_nonempty_self, ← iUnion_inter, h_cover, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
simp_rw :
  ⋃ (i : ι),
      ⋃ (_ :
        Membership.mem (γ := Set ι) {i : ι | (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty} i),
        range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S =
    S
⊢ (⋃ (i : ι),
        ⋃ (_ :
          Membership.mem (γ := Set ι) {i : ι | (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty}
            i),
          range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) ∩
      S =
    S
have simp_rw₁ : ⋃ (i : ι),
    ⋃ (_ : (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty),
      range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S =
  S
Tactic: simp_rw [iUnion₂_inter, mem_setOf, iUnion_nonempty_self, ← iUnion_inter, h_cover, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
simp_rw :
  ⋃ (i : ι),
      ⋃ (_ :
        Membership.mem (γ := Set ι) {i : ι | (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty} i),
        range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S =
    S
simp_rw₁ :
  ⋃ (i : ι),
      ⋃ (_ : (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty),
        range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S =
    S
⊢ (⋃ (i : ι),
        ⋃ (_ :
          Membership.mem (γ := Set ι) {i : ι | (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty}
            i),
          range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) ∩
      S =
    S
have simp_rw₂ : ⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S = S
Tactic: simp_rw [iUnion₂_inter, mem_setOf, iUnion_nonempty_self, ← iUnion_inter, h_cover, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
simp_rw :
  ⋃ (i : ι),
      ⋃ (_ :
        Membership.mem (γ := Set ι) {i : ι | (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty} i),
        range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S =
    S
simp_rw₁ :
  ⋃ (i : ι),
      ⋃ (_ : (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty),
        range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S =
    S
simp_rw₂ : ⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S = S
⊢ (⋃ (i : ι),
        ⋃ (_ :
          Membership.mem (γ := Set ι) {i : ι | (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty}
            i),
          range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) ∩
      S =
    S
have simp_rw₃ : (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) ∩ S = S
Tactic: simp_rw [iUnion₂_inter, mem_setOf, iUnion_nonempty_self, ← iUnion_inter, h_cover, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
S : Set α
hS : S ∈ 𝔖
simp_rw :
  ⋃ (i : ι),
      ⋃ (_ :
        Membership.mem (γ := Set ι) {i : ι | (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty} i),
        range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S =
    S
simp_rw₁ :
  ⋃ (i : ι),
      ⋃ (_ : (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty),
        range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S =
    S
simp_rw₂ : ⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S = S
simp_rw₃ : (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) ∩ S = S
⊢ (⋃ (i : ι),
        ⋃ (_ :
          Membership.mem (γ := Set ι) {i : ι | (range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α) ∩ S).Nonempty}
            i),
          range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) ∩
      S =
    S
have simp_rw₄ : univ ∩ S = S
Tactic: simp_rw [iUnion₂_inter, mem_setOf, iUnion_nonempty_self, ← iUnion_inter, h_cover, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (hypothesis)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
⊢ Eq (α := UniformSpace C(α, β)) inferInstance
    (⨅ (i : ι),
      UniformSpace.comap (β := ContinuousMap.{u_1, u₂} (δ i) β) (fun (x : C(α, β)) ↦ x.comp (φ i)) inferInstance)
have h_cover' : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
Tactic: have h_cover' : ∀ S ∈ 𝔖, ∃ I : Set ι, I.Finite ∧ S ⊆ ⋃ i ∈ I, range (φ i) := fun S hS ↦ by
    refine ⟨{i | (range (φ i) ∩ S).Nonempty}, h_lf.finite_nonempty_inter_compact hS,
      inter_eq_right.mp ?_⟩
    simp_rw [iUnion₂_inter, mem_setOf, iUnion_nonempty_self, ← iUnion_inter, h_cover, univ_inter]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
δ : ι → Type u_1
inst_2 : (i : ι) → TopologicalSpace (δ i)
φ : (i : ι) → ContinuousMap.{u_1, u₁} (δ i) α
h_proper : ∀ (i : ι), IsProperMap.{u_1, u₁} (X := δ i) (Y := α) (⇑(φ i) : (a : δ i) → α)
h_lf : LocallyFinite.{u₃, u₁} (X := α) fun (i : ι) ↦ range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
h_cover : Eq.{u₁ + 1} (α := Set α) (⋃ (i : ι), range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗 : (i : ι) → Set (Set (δ i)) := fun (i : ι) ↦ {K : Set (δ i) | IsCompact K}
h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
h_preimage : ∀ (i : ι), MapsTo (fun (x : Set α) ↦ (⇑(φ i) : (a : δ i) → α) ⁻¹' x) 𝔖 (𝔗 i)
h_cover' : ∀ S ∈ 𝔖, ∃ (I : Set ι), I.Finite ∧ S ⊆ ⋃ i ∈ I, range.{u₁, u_1 + 1} (ι := δ i) (⇑(φ i) : (a : δ i) → α)
⊢ Eq (α := UniformSpace C(α, β)) inferInstance
    (⨅ (i : ι),
      UniformSpace.comap (β := ContinuousMap.{u_1, u₂} (δ i) β) (fun (x : C(α, β)) ↦ x.comp (φ i)) inferInstance)
have simp_rw : Eq (α := UniformSpace C(α, β)) inferInstance
  (⨅ (i : ι),
    UniformSpace.comap (β := UniformOnFun.{u_1, u₂} (δ i) β {K : Set (δ i) | IsCompact K})
      (Function.comp (β := ContinuousMap.{u_1, u₂} (δ i) β) toUniformOnFunIsCompact fun (x : C(α, β)) ↦ x.comp (φ i))
      inferInstance)
Tactic: simp_rw +zetaDelta [compactConvergenceUniformSpace, replaceTopology_eq,
    UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover _ _ _ h_image h_preimage h_cover',
    UniformSpace.comap_iInf, ← UniformSpace.comap_comap]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
K : Set α
V : Set (β × β)
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst_2 : CompleteSpace β
inst_3 : CompactlyCoherentSpace α
⊢ CompleteSpace C(α, β)
have rw : CompleteSpace
  (↑{f : α →ᵤ[{K : Set α | IsCompact K}] β | Continuous[inst, inst_1.toTopologicalSpace] f} : Type (max u₁ u₂))
Tactic: rw [completeSpace_iff_isComplete_range
    isUniformEmbedding_toUniformOnFunIsCompact.isUniformInducing,
    range_toUniformOnFunIsCompact, ← completeSpace_coe_iff_isComplete]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
⊢ ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
have rcases : ∀ (f' : C(α, β)) (hf' : l ≤ 𝓝 f'),
  ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
Tactic: rcases CompleteSpace.complete hlc with ⟨f', hf'⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (hypothesis)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
⊢ ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
have this : l.NeBot
Tactic: have := hlc.1
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
x : α
hx : x ∈ s
⊢ Inseparable (f x) ((f' : (a : α) → β) x)
have refine : Tendsto (fun (f : C(α, β)) ↦ (f : (a : α) → β) x) l (𝓝 (f x))
Tactic: refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
x : α
hx : x ∈ s
⊢ Tendsto (fun (f : C(α, β)) ↦ (f : (a : α) → β) x) l (𝓝 (f x))
have refine : EventuallyEq (β := β) (𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}) (fun (x_1 : C(α, β)) ↦ f x) fun (f : C(α, β)) ↦
  (f : (a : α) → β) x
Tactic: refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (hypothesis)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
⊢ ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
have H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
Tactic: have H₁ : ∀ x ∈ s, Inseparable (f x) (f' x) := fun x hx ↦ by
    refine tendsto_nhds_unique_inseparable ?_ ((continuous_eval_const x).continuousAt.mono_left hf')
    refine tendsto_const_nhds.congr' <| .filter_mono ?_ hlf
    exact fun _ h ↦ (h hx).symm
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
x : α
⊢ Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
have pos : ∀ (hx : x ∈ s), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
x : α
pos : ∀ (hx : x ∈ s), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
⊢ Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
have neg : ∀ (hx : x ∉ s), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
Tactic: by_cases hx : x ∈ s
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (hypothesis)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
⊢ ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
have H₂ : ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
Tactic: have H₂ (x) : Inseparable (s.piecewise f f' x) (f' x) := by
    by_cases hx : x ∈ s <;> simp [hx, H₁, Inseparable.refl]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
H₂ : ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
g : C(α, β) := { toFun := s.piecewise (β := fun (a : α) ↦ β) f (⇑f' : (a : α) → β), continuous_toFun := ⋯ }
⊢ ∃ (x : C(α, β)), Membership.mem (γ := Set C(α, β)) {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s} x ∧ l ≤ 𝓝 x
have refine : 𝓝 f' = 𝓝 g
Tactic: refine ⟨g, Set.piecewise_eqOn _ _ _, hf'.trans_eq ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
H₂ : ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
g : C(α, β) := { toFun := s.piecewise (β := fun (a : α) ↦ β) f (⇑f' : (a : α) → β), continuous_toFun := ⋯ }
⊢ 𝓝 f' = 𝓝 g
have rwa : 𝓝 g = 𝓝 f'
Tactic: rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
H₂ : ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
g : C(α, β) := { toFun := s.piecewise (β := fun (a : α) ↦ β) f (⇑f' : (a : α) → β), continuous_toFun := ⋯ }
rwa : 𝓝 g = 𝓝 f'
⊢ 𝓝 f' = 𝓝 g
have rwa₁ : Inseparable g f'
Tactic: rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
H₂ : ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
g : C(α, β) := { toFun := s.piecewise (β := fun (a : α) ↦ β) f (⇑f' : (a : α) → β), continuous_toFun := ⋯ }
rwa : 𝓝 g = 𝓝 f'
rwa₁ : Inseparable g f'
⊢ 𝓝 f' = 𝓝 g
have rwa₂ : Inseparable (X := (a : α) → β) (⇑g : (a : α) → β) (⇑f' : (a : α) → β)
Tactic: rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
inst_2 : CompleteSpace C(α, β)
f : α → β
s : Set α
l : Filter C(α, β)
hlc : Cauchy l
hlf : l ≤ 𝓟 {g : C(α, β) | EqOn (⇑g : (a : α) → β) f s}
f' : C(α, β)
hf' : l ≤ 𝓝 f'
this : l.NeBot
H₁ : ∀ x ∈ s, Inseparable (f x) ((f' : (a : α) → β) x)
H₂ : ∀ (x : α), Inseparable (s.piecewise (β := fun (i : α) ↦ β) f (⇑f' : (a : α) → β) x) ((f' : (a : α) → β) x)
g : C(α, β) := { toFun := s.piecewise (β := fun (a : α) ↦ β) f (⇑f' : (a : α) → β), continuous_toFun := ⋯ }
rwa : 𝓝 g = 𝓝 f'
rwa₁ : Inseparable g f'
rwa₂ : Inseparable (X := (a : α) → β) (⇑g : (a : α) → β) (⇑f' : (a : α) → β)
⊢ 𝓝 f' = 𝓝 g
have rwa₃ : ∀ (i : α), Inseparable.{u₂} (X := β) ((g : (a : α) → β) i : β) ((f' : (a : α) → β) i : β)
Tactic: rwa [eq_comm, ← Inseparable, ← inseparable_coe, inseparable_pi]