awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      ∀ (U : Set β),
        IsOpen[inst_1.toTopologicalSpace] U →
          MapsTo (⇑f : (a : α) → β) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
K : Set α
hK : IsCompact K
U : Set (β × β)
hU : U ∈ 𝓤 β
x : α
h_1 : x ∈ K
V : Set (β × β)
hV : V ∈ 𝓤 β
hVo : IsOpen[instTopologicalSpaceProd] V
hVsymm : SetRel.IsSymm V
hVU : SetRel.comp V V ⊆ U
W : Set (β × β)
hW : W ∈ 𝓤 β
hWc : IsClosed[instTopologicalSpaceProd] W
hWU : W ⊆ V
s : Set α := K ∩ preimage.{u₁, u₂} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) (ball ((f : (a : α) → β) x) W : Set β)
hnhds : s ∈ 𝓝[K] x
hcomp : IsCompact s
hmaps : MapsTo.{u₁, u₂} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) s (ball ((f : (a : α) → β) x) V : Set β)
⊢ ∀ᶠ (n : ι) in p,
    ∀ y ∈ s,
      Membership.mem (α := β × β) U
        (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
have right : ∀ (g : ι)
  (hg : MapsTo.{u₁, u₂} (β := β) ((⇑(F g) : (a : α) → β) : (a : α) → β) s (ball ((f : (a : α) → β) x) V : Set β))
  (y : α) (hy : y ∈ s),
  Membership.mem (α := β × β) U (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) g y) : β × β)
Tactic: refine (h s hcomp _ (isOpen_ball _ hVo) hmaps).mono fun g hg y hy ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen[inst_1.toTopologicalSpace] U
hf : MapsTo (⇑f : (a : α) → β) K U
⊢ ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
have mpr : ∀ (V : Set (β × β)) (hV : V ∈ 𝓤 β)
  (hVf : ∀ (x : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' K) x → ball x V ⊆ U),
  ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
Tactic: rcases lebesgue_number_of_compact_open (hK.image (map_continuous f)) hU hf.image_subset
        with ⟨V, hV, -, hVf⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen[inst_1.toTopologicalSpace] U
hf : MapsTo (⇑f : (a : α) → β) K U
V : Set (β × β)
hV : V ∈ 𝓤 β
hVf : ∀ (x : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' K) x → ball x V ⊆ U
⊢ ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
have h₁ : ∀ (a : ι),
  Membership.mem (γ := Set ι)
    {x : ι |
      Membership.mem (γ := Set ι)
          {x : ι |
            (fun (n : ι) ↦
                ∀ x ∈ K,
                  Membership.mem (α := β × β) V
                    (((f : (a : α) → β) x, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n x) : β × β))
              x}
          x →
        Membership.mem (γ := Set ι) {x : ι | (fun (a : ι) ↦ MapsTo (⇑(F a) : (a : α) → β) K U) x} x}
    a
Tactic: filter_upwards [h K hK V hV] with g hg x hx using hVf _ (mem_image_of_mem f hx) (hg x hx)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen[inst_1.toTopologicalSpace] U
hf : MapsTo (⇑f : (a : α) → β) K U
V : Set (β × β)
hV : V ∈ 𝓤 β
hVf : ∀ (x : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' K) x → ball x V ⊆ U
h₁ :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι)
            {x : ι |
              (fun (n : ι) ↦
                  ∀ x ∈ K,
                    Membership.mem (α := β × β) V
                      (((f : (a : α) → β) x, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n x) : β × β))
                x}
            x →
          Membership.mem (γ := Set ι) {x : ι | (fun (a : ι) ↦ MapsTo (⇑(F a) : (a : α) → β) K U) x} x}
      a
⊢ ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
have h₂ : ∀ (a : ι),
  (∀ x ∈ K, Membership.mem (α := β × β) V (((f : (a : α) → β) x, (F a : (a : α) → β) x) : β × β)) →
    MapsTo (⇑(F a) : (a : α) → β) K U
Tactic: filter_upwards [h K hK V hV] with g hg x hx using hVf _ (mem_image_of_mem f hx) (hg x hx)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
f : C(α, β)
h :
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
K : Set α
hK : IsCompact K
U : Set β
hU : IsOpen[inst_1.toTopologicalSpace] U
hf : MapsTo (⇑f : (a : α) → β) K U
V : Set (β × β)
hV : V ∈ 𝓤 β
hVf : ∀ (x : β), Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' K) x → ball x V ⊆ U
h₁ :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι)
            {x : ι |
              (fun (n : ι) ↦
                  ∀ x ∈ K,
                    Membership.mem (α := β × β) V
                      (((f : (a : α) → β) x, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n x) : β × β))
                x}
            x →
          Membership.mem (γ := Set ι) {x : ι | (fun (a : ι) ↦ MapsTo (⇑(F a) : (a : α) → β) K U) x} x}
      a
h₂ :
  ∀ (a : ι),
    (∀ x ∈ K, Membership.mem (α := β × β) V (((f : (a : α) → β) x, (F a : (a : α) → β) x) : β × β)) →
      MapsTo (⇑(F a) : (a : α) → β) K U
⊢ ∀ᶠ (a : ι) in p, MapsTo (⇑(F a) : (a : α) → β) K U
have h₃ : ∀ (g : ι) (hg : ∀ x ∈ K, Membership.mem (α := β × β) V (((f : (a : α) → β) x, (F g : (a : α) → β) x) : β × β)) ⦃x : α⦄
  (hx : x ∈ K), Membership.mem (α := β) U ((F g : (a : α) → β) x : β)
Tactic: filter_upwards [h K hK V hV] with g hg x hx using hVf _ (mem_image_of_mem f hx) (hg x hx)
-- 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(α, β)
⊢ Eq (α := TopologicalSpace C(α, β)) compactOpen toTopologicalSpace
have refine : ∀ (f : C(α, β)) (l : Filter C(α, β)), l ≤ 𝓝 f ↔ l ≤ 𝓝 f
Tactic: refine TopologicalSpace.ext_nhds fun f ↦ eq_of_forall_le_iff fun l ↦ ?_
-- 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_1 f : C(α, β)
l : Filter C(α, β)
⊢ l ≤ 𝓝 f ↔ l ≤ 𝓝 f
have simp_rw : (∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn (β := β) (fun (i : C(α, β)) (a : α) ↦ (id i : (a : α) → β) a) (⇑f : (a : α) → β) l K) ↔
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {K : Set α | IsCompact K} s →
      TendstoUniformlyOn (β := β)
        ((⇑(UniformOnFun.toFun {K : Set α | IsCompact K}) : (a : α →ᵤ[{K : Set α | IsCompact K}] β) → α → β) ∘
          toUniformOnFunIsCompact ∘ id)
        ((UniformOnFun.toFun {K : Set α | IsCompact K} : (a : α →ᵤ[{K : Set α | IsCompact K}] β) → α → β)
          f.toUniformOnFunIsCompact)
        l s
Tactic: simp_rw [← tendsto_id', tendsto_iff_forall_isCompact_tendstoUniformlyOn,
      nhds_induced, tendsto_comap_iff, UniformOnFun.tendsto_iff_tendstoUniformlyOn]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p
⊢ Tendsto F p (𝓝 f)
have rw : ∀ (K : Set α),
  IsCompact K →
    TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
Tactic: rw [tendsto_iff_forall_isCompact_tendstoUniformlyOn]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
h : TendstoLocallyUniformly.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p
K : Set α
hK : IsCompact K
⊢ TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
have rw : TendstoLocallyUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
Tactic: rw [← tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact hK]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst_2 : WeaklyLocallyCompactSpace α
⊢ Tendsto F p (𝓝 f) ↔
    TendstoLocallyUniformly.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p
have refine : ∀ (h : Tendsto F p (𝓝 f)) (V : Set (β × β)) (hV : V ∈ 𝓤 β) (x : α),
  ∃ t ∈ 𝓝 x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) V
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
Tactic: refine ⟨fun h V hV x ↦ ?_, tendsto_of_tendstoLocallyUniformly⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst_2 : WeaklyLocallyCompactSpace α
h : Tendsto F p (𝓝 f)
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
⊢ ∃ t ∈ 𝓝 x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) V
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
have rw : ∀
  (h :
    ∀ (K : Set α),
      IsCompact K →
        TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K)
  (V : Set (β × β)) (hV : V ∈ 𝓤 β) (x : α),
  ∃ t ∈ 𝓝 x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) V
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
Tactic: rw [tendsto_iff_forall_isCompact_tendstoUniformlyOn] at h
Cleared hypotheses: h, V, hV, x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
f : C(α, β)
ι : Type u₃
p : Filter ι
F : ι → C(α, β)
inst_2 : WeaklyLocallyCompactSpace α
h :
  ∀ (K : Set α),
    IsCompact K →
      TendstoUniformlyOn.{u₁, u₂, u₃} (β := β) (fun (i : ι) (a : α) ↦ (F i : (a : α) → β) a) (⇑f : (a : α) → β) p K
V : Set (β × β)
hV : V ∈ 𝓤 β
x : α
⊢ ∃ t ∈ 𝓝 x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) V
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
have obtain : ∀ (n : Set α) (hn₁ : IsCompact n) (hn₂ : n ∈ 𝓝 x),
  ∃ t ∈ 𝓝 x,
    ∀ᶠ (n : ι) in p,
      ∀ y ∈ t,
        Membership.mem (α := β × β) V
          (((f : (a : α) → β) y, (fun (i : ι) (a : α) ↦ ((F i : (a : α) → β) a : β)) n y) : β × β)
Tactic: obtain ⟨n, hn₁, hn₂⟩ := exists_compact_mem_nhds x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
s : Set α
inst_2 : CompactSpace.{u₁} (↑s : Type u₁)
f : α → β
hf : ContinuousOn f s
ι : Type u_1
p : Filter ι
F : ι → α → β
hF : ∀ (i : ι), ContinuousOn (F i) s
⊢ Tendsto (fun (i : ι) ↦ { toFun := s.restrict (π := fun (a : α) ↦ β) (F i), continuous_toFun := ⋯ }) p
      (𝓝
        { toFun := s.restrict (π := fun (a : α) ↦ β) f, continuous_toFun := ⋯ :
          ContinuousMap.{u₁, u₂} (↑s : Type u₁) β }) ↔
    TendstoUniformlyOn F f p s
have rw : TendstoUniformly.{u₁, u₂, u_1} (β := β)
    (fun (i : ι) (a : (↑s : Type u₁)) ↦
      ({ toFun := s.restrict (π := fun (a : α) ↦ β) (F i), continuous_toFun := sorry :
            ContinuousMap.{u₁, u₂} (↑s : Type u₁) β } :
          (a : (↑s : Type u₁)) → β)
        a)
    (⇑{ toFun := s.restrict (π := fun (a : α) ↦ β) f, continuous_toFun := sorry :
          ContinuousMap.{u₁, u₂} (↑s : Type u₁) β } :
      (a : (↑s : Type u₁)) → β)
    p ↔
  TendstoUniformly (fun (i : ι) (x : (↑s : Type u₁)) ↦ F i (↑x : α)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)) p
Tactic: rw [ContinuousMap.tendsto_iff_tendstoUniformly, tendstoUniformlyOn_iff_tendstoUniformly_comp_coe]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
X : Type u_1
inst_2 : TopologicalSpace X
f : X → α → β
s : Set α
hf : ∀ (x : X), ContinuousOn (f x) s
inst_3 : CompactSpace.{u₁} (↑s : Type u₁)
⊢ (Continuous[inst_2, _] fun (x : X) ↦ { toFun := s.restrict (π := fun (a : α) ↦ β) (f x), continuous_toFun := ⋯ }) ↔
    Continuous[inst_2, topologicalSpace α β {s}] fun (x : X) ↦ (ofFun {s} : (a : α → β) → α →ᵤ[{s}] β) (f x)
have rw : (Continuous[inst_2, UniformFun.topologicalSpace (↑s : Type u₁) β] fun (x : X) ↦
    (UniformFun.ofFun : (a : (↑s : Type u₁) → β) → (↑s : Type u₁) →ᵤ β)
      (⇑{ toFun := s.restrict (π := fun (a : α) ↦ β) (f x), continuous_toFun := sorry :
            ContinuousMap.{u₁, u₂} (↑s : Type u₁) β } :
        (a : (↑s : Type u₁)) → β)) ↔
  ∀ (s_1 : Set α),
    Membership.mem (γ := Set (Set α)) {s} s_1 →
      Continuous[inst_2, UniformFun.topologicalSpace (↑s_1 : Type u₁) β]
        (Function.comp (β := (↑s_1 : Type u₁) → β)
          ((⇑UniformFun.ofFun : (a : (↑s_1 : Type u₁) → β) → UniformFun.{u₁, u₂} (↑s_1 : Type u₁) β) :
            (a : (↑s_1 : Type u₁) → β) → UniformFun.{u₁, u₂} (↑s_1 : Type u₁) β)
          (Function.comp (β := α → β) (s_1.restrict (π := fun (a : α) ↦ β))
              (Function.comp (β := α →ᵤ[{s}] β) (⇑(toFun {s}) : (a : α →ᵤ[{s}] β) → α → β) fun (x : X) ↦
                (ofFun {s} : (a : α → β) → α →ᵤ[{s}] β) (f x)) :
            X → (↑s_1 : Type u₁) → β))
Tactic: rw [ContinuousMap.continuous_iff_continuous_uniformFun, UniformOnFun.continuous_rng_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (hypothesis)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst_2 : TopologicalSpace δ₁
inst_3 : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap.{u_1, u₁} (X := δ₁) (Y := α) (⇑φ₁ : (a : δ₁) → α)
h_proper₂ : IsProperMap.{u_2, u₁} (X := δ₂) (Y := α) (⇑φ₂ : (a : δ₂) → α)
h_cover :
  Eq.{u₁ + 1} (α := Set α)
    (range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K : Set δ₁ | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K : Set δ₂ | IsCompact K}
⊢ Eq (α := UniformSpace C(α, β)) inferInstance
    (UniformSpace.comap (β := C(δ₁, β)) (fun (x : C(α, β)) ↦ x.comp φ₁) inferInstance ⊓
      UniformSpace.comap (β := C(δ₂, β)) (fun (x : C(α, β)) ↦ x.comp φ₂) inferInstance)
have h_image₁ : MapsTo (fun (x : Set δ₁) ↦ (⇑φ₁ : (a : δ₁) → α) '' x) 𝔗₁ 𝔖
Tactic: have h_image₁ : MapsTo (φ₁ '' ·) 𝔗₁ 𝔖 := fun K hK ↦ hK.image φ₁.continuous
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (hypothesis)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst_2 : TopologicalSpace δ₁
inst_3 : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap.{u_1, u₁} (X := δ₁) (Y := α) (⇑φ₁ : (a : δ₁) → α)
h_proper₂ : IsProperMap.{u_2, u₁} (X := δ₂) (Y := α) (⇑φ₂ : (a : δ₂) → α)
h_cover :
  Eq.{u₁ + 1} (α := Set α)
    (range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K : Set δ₁ | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K : Set δ₂ | IsCompact K}
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ (⇑φ₁ : (a : δ₁) → α) '' x) 𝔗₁ 𝔖
⊢ Eq (α := UniformSpace C(α, β)) inferInstance
    (UniformSpace.comap (β := C(δ₁, β)) (fun (x : C(α, β)) ↦ x.comp φ₁) inferInstance ⊓
      UniformSpace.comap (β := C(δ₂, β)) (fun (x : C(α, β)) ↦ x.comp φ₂) inferInstance)
have h_image₂ : MapsTo (fun (x : Set δ₂) ↦ (⇑φ₂ : (a : δ₂) → α) '' x) 𝔗₂ 𝔖
Tactic: have h_image₂ : MapsTo (φ₂ '' ·) 𝔗₂ 𝔖 := fun K hK ↦ hK.image φ₂.continuous
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (hypothesis)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst_2 : TopologicalSpace δ₁
inst_3 : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap.{u_1, u₁} (X := δ₁) (Y := α) (⇑φ₁ : (a : δ₁) → α)
h_proper₂ : IsProperMap.{u_2, u₁} (X := δ₂) (Y := α) (⇑φ₂ : (a : δ₂) → α)
h_cover :
  Eq.{u₁ + 1} (α := Set α)
    (range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K : Set δ₁ | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K : Set δ₂ | IsCompact K}
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ (⇑φ₁ : (a : δ₁) → α) '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ (⇑φ₂ : (a : δ₂) → α) '' x) 𝔗₂ 𝔖
⊢ Eq (α := UniformSpace C(α, β)) inferInstance
    (UniformSpace.comap (β := C(δ₁, β)) (fun (x : C(α, β)) ↦ x.comp φ₁) inferInstance ⊓
      UniformSpace.comap (β := C(δ₂, β)) (fun (x : C(α, β)) ↦ x.comp φ₂) inferInstance)
have h_preimage₁ : MapsTo (fun (x : Set α) ↦ (⇑φ₁ : (a : δ₁) → α) ⁻¹' x) 𝔖 𝔗₁
Tactic: have h_preimage₁ : MapsTo (φ₁ ⁻¹' ·) 𝔖 𝔗₁ := fun K ↦ h_proper₁.isCompact_preimage
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (hypothesis)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst_2 : TopologicalSpace δ₁
inst_3 : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap.{u_1, u₁} (X := δ₁) (Y := α) (⇑φ₁ : (a : δ₁) → α)
h_proper₂ : IsProperMap.{u_2, u₁} (X := δ₂) (Y := α) (⇑φ₂ : (a : δ₂) → α)
h_cover :
  Eq.{u₁ + 1} (α := Set α)
    (range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K : Set δ₁ | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K : Set δ₂ | IsCompact K}
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ (⇑φ₁ : (a : δ₁) → α) '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ (⇑φ₂ : (a : δ₂) → α) '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ (⇑φ₁ : (a : δ₁) → α) ⁻¹' x) 𝔖 𝔗₁
⊢ Eq (α := UniformSpace C(α, β)) inferInstance
    (UniformSpace.comap (β := C(δ₁, β)) (fun (x : C(α, β)) ↦ x.comp φ₁) inferInstance ⊓
      UniformSpace.comap (β := C(δ₂, β)) (fun (x : C(α, β)) ↦ x.comp φ₂) inferInstance)
have h_preimage₂ : MapsTo (fun (x : Set α) ↦ (⇑φ₂ : (a : δ₂) → α) ⁻¹' x) 𝔖 𝔗₂
Tactic: have h_preimage₂ : MapsTo (φ₂ ⁻¹' ·) 𝔖 𝔗₂ := fun K ↦ h_proper₂.isCompact_preimage
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (hypothesis)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst_2 : TopologicalSpace δ₁
inst_3 : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap.{u_1, u₁} (X := δ₁) (Y := α) (⇑φ₁ : (a : δ₁) → α)
h_proper₂ : IsProperMap.{u_2, u₁} (X := δ₂) (Y := α) (⇑φ₂ : (a : δ₂) → α)
h_cover :
  Eq.{u₁ + 1} (α := Set α)
    (range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K : Set δ₁ | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K : Set δ₂ | IsCompact K}
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ (⇑φ₁ : (a : δ₁) → α) '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ (⇑φ₂ : (a : δ₂) → α) '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ (⇑φ₁ : (a : δ₁) → α) ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ (⇑φ₂ : (a : δ₂) → α) ⁻¹' x) 𝔖 𝔗₂
⊢ Eq (α := UniformSpace C(α, β)) inferInstance
    (UniformSpace.comap (β := C(δ₁, β)) (fun (x : C(α, β)) ↦ x.comp φ₁) inferInstance ⊓
      UniformSpace.comap (β := C(δ₂, β)) (fun (x : C(α, β)) ↦ x.comp φ₂) inferInstance)
have h_cover' : ∀ S ∈ 𝔖, S ⊆ range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)
Tactic: have h_cover' : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂ := fun S _ ↦ h_cover ▸ subset_univ _
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.CompactConvergence (goal)
Goal:
α : Type u₁
β : Type u₂
inst : TopologicalSpace α
inst_1 : UniformSpace β
δ₁ : Type u_1
δ₂ : Type u_2
inst_2 : TopologicalSpace δ₁
inst_3 : TopologicalSpace δ₂
φ₁ : C(δ₁, α)
φ₂ : C(δ₂, α)
h_proper₁ : IsProperMap.{u_1, u₁} (X := δ₁) (Y := α) (⇑φ₁ : (a : δ₁) → α)
h_proper₂ : IsProperMap.{u_2, u₁} (X := δ₂) (Y := α) (⇑φ₂ : (a : δ₂) → α)
h_cover :
  Eq.{u₁ + 1} (α := Set α)
    (range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)) univ
𝔖 : Set (Set α) := {K : Set α | IsCompact K}
𝔗₁ : Set (Set δ₁) := {K : Set δ₁ | IsCompact K}
𝔗₂ : Set (Set δ₂) := {K : Set δ₂ | IsCompact K}
h_image₁ : MapsTo (fun (x : Set δ₁) ↦ (⇑φ₁ : (a : δ₁) → α) '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun (x : Set δ₂) ↦ (⇑φ₂ : (a : δ₂) → α) '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun (x : Set α) ↦ (⇑φ₁ : (a : δ₁) → α) ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun (x : Set α) ↦ (⇑φ₂ : (a : δ₂) → α) ⁻¹' x) 𝔖 𝔗₂
h_cover' :
  ∀ S ∈ 𝔖, S ⊆ range.{u₁, u_1 + 1} (ι := δ₁) (⇑φ₁ : (a : δ₁) → α) ∪ range.{u₁, u_2 + 1} (ι := δ₂) (⇑φ₂ : (a : δ₂) → α)
⊢ Eq (α := UniformSpace C(α, β)) inferInstance
    (UniformSpace.comap (β := C(δ₁, β)) (fun (x : C(α, β)) ↦ x.comp φ₁) inferInstance ⊓
      UniformSpace.comap (β := C(δ₂, β)) (fun (x : C(α, β)) ↦ x.comp φ₂) inferInstance)
have simp_rw : Eq (α := UniformSpace C(α, β)) inferInstance
  (UniformSpace.comap (β := δ₁ →ᵤ[{K : Set δ₁ | IsCompact K}] β)
      (Function.comp (β := C(δ₁, β)) toUniformOnFunIsCompact fun (x : C(α, β)) ↦ x.comp φ₁) inferInstance ⊓
    UniformSpace.comap (β := δ₂ →ᵤ[{K : Set δ₂ | IsCompact K}] β)
      (Function.comp (β := C(δ₂, β)) toUniformOnFunIsCompact fun (x : C(α, β)) ↦ x.comp φ₂) inferInstance)
Tactic: simp_rw +zetaDelta [compactConvergenceUniformSpace, replaceTopology_eq,
    UniformOnFun.uniformSpace_eq_inf_precomp_of_cover _ _ _ _ _
      h_image₁ h_image₂ h_preimage₁ h_preimage₂ h_cover',
    UniformSpace.comap_inf, ← UniformSpace.comap_comap]
-- 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}
⊢ Eq (α := UniformSpace C(α, β)) inferInstance
    (⨅ (i : ι),
      UniformSpace.comap (β := ContinuousMap.{u_1, u₂} (δ i) β) (fun (x : C(α, β)) ↦ x.comp (φ i)) inferInstance)
have h_image : ∀ (i : ι), MapsTo (fun (x : Set (δ i)) ↦ (⇑(φ i) : (a : δ i) → α) '' x) (𝔗 i) 𝔖
Tactic: have h_image : ∀ i, MapsTo (φ i '' ·) (𝔗 i) 𝔖 := fun i K hK ↦ hK.image (φ i).continuous