awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
hw : w.Finite
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite) (huw : u ⊆ w),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
huw : ¬u ⊆ w
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have inr : (↑K : Set α) ⊆ ⋃₀ (u ∪ w)
Tactic: apply this (u ∪ w)
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
hw : w.Finite
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite) (huw : u ⊆ w),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
huw : ¬u ⊆ w
inr : (↑K : Set α) ⊆ ⋃₀ (u ∪ w)
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have inr₁ : u ∪ w ⊆ B
Tactic: apply this (u ∪ w)
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
hw : w.Finite
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite) (huw : u ⊆ w),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
huw : ¬u ⊆ w
inr : (↑K : Set α) ⊆ ⋃₀ (u ∪ w)
inr₁ : u ∪ w ⊆ B
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have inr₂ : ⋃₀ (u ∪ w) ⊆ V
Tactic: apply this (u ∪ w)
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
hw : w.Finite
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite) (huw : u ⊆ w),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
huw : ¬u ⊆ w
inr : (↑K : Set α) ⊆ ⋃₀ (u ∪ w)
inr₁ : u ∪ w ⊆ B
inr₂ : ⋃₀ (u ∪ w) ⊆ V
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have inr₃ : ∀ W ∈ u ∪ w, ((↑K : Set α) ∩ W).Nonempty
Tactic: apply this (u ∪ w)
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
hw : w.Finite
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite) (huw : u ⊆ w),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
huw : ¬u ⊆ w
inr : (↑K : Set α) ⊆ ⋃₀ (u ∪ w)
inr₁ : u ∪ w ⊆ B
inr₂ : ⋃₀ (u ∪ w) ⊆ V
inr₃ : ∀ W ∈ u ∪ w, ((↑K : Set α) ∩ W).Nonempty
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have inr₄ : (u ∪ w).Finite
Tactic: apply this (u ∪ w)
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
hw : w.Finite
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : w.Finite) (huw : u ⊆ w),
    ∃ (v : Set (Compacts α)),
      Membership.mem (γ := Set (Set (Compacts α)))
          ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
          v ∧
        K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
huw : ¬u ⊆ w
inr : (↑K : Set α) ⊆ ⋃₀ (u ∪ w)
inr₁ : u ∪ w ⊆ B
inr₂ : ⋃₀ (u ∪ w) ⊆ V
inr₃ : ∀ W ∈ u ∪ w, ((↑K : Set α) ∩ W).Nonempty
inr₄ : (u ∪ w).Finite
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have inr₅ : u ⊆ u ∪ w
Tactic: apply this (u ∪ w)
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
hw : w.Finite
huw : u ⊆ w
⊢ ∃ (v : Set (Compacts α)),
    Membership.mem (γ := Set (Set (Compacts α)))
        ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        v ∧
      K ∈ v ∧ v ⊆ SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
have rw : ∃ (x : Set (Set α)),
  Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u ⊆ B} x ∧
    Membership.mem (γ := Set (Compacts α)) {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}
        K ∧
      Subset (α := Set (Compacts α)) {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}
        (SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty})
Tactic: rw [exists_mem_image]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
V : Set α
u : Set (Set α)
hV : IsOpen[inst] V
hu : u.Finite
huB : u ⊆ B
huV : ∀ U ∈ u, U ⊆ V
K : Compacts α
hKu : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
w : Set (Set α)
hKV : (↑K : Set α) ⊆ ⋃₀ w
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
hw : w.Finite
huw : u ⊆ w
⊢ ∃ (x : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u ⊆ B} x ∧
      Membership.mem (γ := Set (Compacts α))
          {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty} K ∧
        Subset (α := Set (Compacts α)) {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}
          (SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty})
have exists : Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u ⊆ B} w ∧
  Membership.mem (γ := Set (Compacts α)) {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ w ∧ ∀ U ∈ w, ((↑K : Set α) ∩ U).Nonempty}
      K ∧
    Subset (α := Set (Compacts α)) {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ w ∧ ∀ U ∈ w, ((↑K : Set α) ∩ U).Nonempty}
      (SetLike.coe ⁻¹' {s : Set α | s ⊆ V ∧ ∀ U ∈ u, (s ∩ U).Nonempty})
Tactic: exists w
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
⊢ ContinuousSup.{u_1} (Compacts α)
have continuous_sup : Continuous (Y := Compacts α) fun (p : Compacts α × Compacts α) ↦ p.1 ⊔ p.2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
⊢ Continuous (Y := Compacts α) fun (p : Compacts α × Compacts α) ↦ p.1 ⊔ p.2
have continuous_sup : Continuous[_, TopologicalSpace.vietoris α] fun (x : Compacts α × Compacts α) ↦ (↑x.1 : Set α) ∪ (↑x.2 : Set α)
Tactic: simp_rw [isEmbedding_coe.continuous_iff, Function.comp_def, coe_sup]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
⊢ Continuous (Y := Compacts (α × β)) fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦ p.1 ×ˢ p.2
have rw : ∀ (s : Set (Set (α × β))),
  Membership.mem (γ := Set (Set (Set (α × β))))
      (powerset '' {U : Set (α × β) | IsOpen[instTopologicalSpaceProd] U} ∪
        (fun (V : Set (α × β)) ↦ {s : Set (α × β) | (s ∩ V).Nonempty}) ''
          {V : Set (α × β) | IsOpen[instTopologicalSpaceProd] V})
      s →
    IsOpen (X := Prod.{u_1, u_2} (Compacts α) (Compacts β))
      ((Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
          p.1 ×ˢ p.2) ⁻¹'
        s)
Tactic: rw [continuous_induced_rng, continuous_generateFrom_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
U : Set (α × β)
hU : Membership.mem (γ := Set (Set (α × β))) {U : Set (α × β) | IsOpen[instTopologicalSpaceProd] U} U
⊢ IsOpen (X := Prod.{u_1, u_2} (Compacts α) (Compacts β))
    ((Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
        p.1 ×ˢ p.2) ⁻¹'
      𝒫 U)
have inl : ∀ (x : Prod.{u_1, u_2} (Compacts α) (Compacts β)),
  Membership.mem (γ := Set (Prod.{u_1, u_2} (Compacts α) (Compacts β)))
      ((Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
          p.1 ×ˢ p.2) ⁻¹'
        𝒫 U)
      x →
    ∃
      t ⊆
        (Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
            p.1 ×ˢ p.2) ⁻¹'
          𝒫 U,
      IsOpen t ∧ x ∈ t
Tactic: rw [isOpen_iff_forall_mem_open]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
U : Set (α × β)
hU : Membership.mem (γ := Set (Set (α × β))) {U : Set (α × β) | IsOpen[instTopologicalSpaceProd] U} U
K : Compacts α
L : Compacts β
⊢ Membership.mem (γ := Set (Prod.{u_1, u_2} (Compacts α) (Compacts β)))
      ((Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
          p.1 ×ˢ p.2) ⁻¹'
        𝒫 U)
      (K, L) →
    ∃
      t ⊆
        (Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
            p.1 ×ˢ p.2) ⁻¹'
          𝒫 U,
      IsOpen t ∧ (K, L) ∈ t
have inl : ∀ (hKL : (↑K : Set α) ×ˢ (↑L : Set β) ⊆ U),
  ∃
    t ⊆
      (Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
          p.1 ×ˢ p.2) ⁻¹'
        𝒫 U,
    IsOpen t ∧ (K, L) ∈ t
Tactic: (hKL : (K : Set α) ×ˢ (L : Set β) ⊆ U)
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
U : Set (α × β)
hU : Membership.mem (γ := Set (Set (α × β))) {U : Set (α × β) | IsOpen[instTopologicalSpaceProd] U} U
K : Compacts α
L : Compacts β
hKL : (↑K : Set α) ×ˢ (↑L : Set β) ⊆ U
⊢ ∃
    t ⊆
      (Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
          p.1 ×ˢ p.2) ⁻¹'
        𝒫 U,
    IsOpen t ∧ (K, L) ∈ t
have inl : ∀ (V : Set α) (W : Set β) (hV : IsOpen[inst] V) (hW : IsOpen[inst_1] W) (hK : (↑K : Set α) ⊆ V) (hL : (↑L : Set β) ⊆ W)
  (hVW : V ×ˢ W ⊆ U),
  ∃
    t ⊆
      (Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
          p.1 ×ˢ p.2) ⁻¹'
        𝒫 U,
    IsOpen t ∧ (K, L) ∈ t
Tactic: obtain ⟨V, W, hV, hW, hK, hL, hVW⟩ := generalized_tube_lemma K.isCompact L.isCompact hU hKL
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
U : Set (α × β)
hU : Membership.mem (γ := Set (Set (α × β))) {V : Set (α × β) | IsOpen[instTopologicalSpaceProd] V} U
⊢ IsOpen (X := Prod.{u_1, u_2} (Compacts α) (Compacts β))
    ((Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
        p.1 ×ˢ p.2) ⁻¹'
      (fun (V : Set (α × β)) ↦ ({s : Set (α × β) | (s ∩ V).Nonempty} : Set (Set (α × β)))) U)
have inr : ∀ (x : Prod.{u_1, u_2} (Compacts α) (Compacts β)),
  Membership.mem (γ := Set (Prod.{u_1, u_2} (Compacts α) (Compacts β)))
      ((Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
          p.1 ×ˢ p.2) ⁻¹'
        (fun (V : Set (α × β)) ↦ ({s : Set (α × β) | (s ∩ V).Nonempty} : Set (Set (α × β)))) U)
      x →
    ∃
      t ⊆
        (Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
            p.1 ×ˢ p.2) ⁻¹'
          (fun (V : Set (α × β)) ↦ ({s : Set (α × β) | (s ∩ V).Nonempty} : Set (Set (α × β)))) U,
      IsOpen t ∧ x ∈ t
Tactic: rw [isOpen_iff_forall_mem_open]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
U : Set (α × β)
hU : Membership.mem (γ := Set (Set (α × β))) {V : Set (α × β) | IsOpen[instTopologicalSpaceProd] V} U
K : Compacts α
L : Compacts β
⊢ Membership.mem (γ := Set (Prod.{u_1, u_2} (Compacts α) (Compacts β)))
      ((Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
          p.1 ×ˢ p.2) ⁻¹'
        (fun (V : Set (α × β)) ↦ ({s : Set (α × β) | (s ∩ V).Nonempty} : Set (Set (α × β)))) U)
      (K, L) →
    ∃
      t ⊆
        (Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
            p.1 ×ˢ p.2) ⁻¹'
          (fun (V : Set (α × β)) ↦ ({s : Set (α × β) | (s ∩ V).Nonempty} : Set (Set (α × β)))) U,
      IsOpen t ∧ (K, L) ∈ t
have inr : ∀ (x : α) (y : β) (hx : x ∈ K) (hy : y ∈ L) (hxy : (x, y) ∈ U),
  ∃
    t ⊆
      (Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
          p.1 ×ˢ p.2) ⁻¹'
        (fun (V : Set (α × β)) ↦ ({s : Set (α × β) | (s ∩ V).Nonempty} : Set (Set (α × β)))) U,
    IsOpen t ∧ (K, L) ∈ t
Tactic: ⟨⟨x, y⟩, ⟨(hx : x ∈ K), (hy : y ∈ L)⟩, hxy⟩
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
U : Set (α × β)
hU : Membership.mem (γ := Set (Set (α × β))) {V : Set (α × β) | IsOpen[instTopologicalSpaceProd] V} U
K : Compacts α
L : Compacts β
x : α
y : β
hx : x ∈ K
hy : y ∈ L
hxy : (x, y) ∈ U
⊢ ∃
    t ⊆
      (Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
          p.1 ×ˢ p.2) ⁻¹'
        (fun (V : Set (α × β)) ↦ ({s : Set (α × β) | (s ∩ V).Nonempty} : Set (Set (α × β)))) U,
    IsOpen t ∧ (K, L) ∈ t
have inr : ∀ (V : Set α) (W : Set β) (hV : IsOpen[inst] V) (hW : IsOpen[inst_1] W) (hxV : x ∈ V) (hyW : y ∈ W) (hVW : V ×ˢ W ⊆ U),
  ∃
    t ⊆
      (Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
          p.1 ×ˢ p.2) ⁻¹'
        (fun (V : Set (α × β)) ↦ ({s : Set (α × β) | (s ∩ V).Nonempty} : Set (Set (α × β)))) U,
    IsOpen t ∧ (K, L) ∈ t
Tactic: obtain ⟨V, W, hV, hW, hxV, hyW, hVW⟩ := isOpen_prod_iff.mp hU x y hxy
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
U : Set (α × β)
hU : Membership.mem (γ := Set (Set (α × β))) {V : Set (α × β) | IsOpen[instTopologicalSpaceProd] V} U
K : Compacts α
L : Compacts β
x : α
y : β
hx : x ∈ K
hy : y ∈ L
hxy : (x, y) ∈ U
V : Set α
W : Set β
hV : IsOpen[inst] V
hW : IsOpen[inst_1] W
hxV : x ∈ V
hyW : y ∈ W
hVW : V ×ˢ W ⊆ U
⊢ ∃
    t ⊆
      (Function.comp (β := Compacts (α × β)) SetLike.coe fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦
          p.1 ×ˢ p.2) ⁻¹'
        (fun (V : Set (α × β)) ↦ ({s : Set (α × β) | (s ∩ V).Nonempty} : Set (Set (α × β)))) U,
    IsOpen t ∧ (K, L) ∈ t
have inr : ∃
  t ⊆
    {a : Prod.{u_1, u_2} (Compacts α) (Compacts β) |
      (Function.comp (β := Compacts (α × β)) SetLike.coe
            (fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦ p.1 ×ˢ p.2) a ∩
          V ×ˢ W).Nonempty},
  IsOpen t ∧ (K, L) ∈ t
Tactic: grw [preimage_setOf_eq, ← hVW]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
U : Set (α × β)
hU : Membership.mem (γ := Set (Set (α × β))) {V : Set (α × β) | IsOpen[instTopologicalSpaceProd] V} U
K : Compacts α
L : Compacts β
x : α
y : β
hx : x ∈ K
hy : y ∈ L
hxy : (x, y) ∈ U
V : Set α
W : Set β
hV : IsOpen[inst] V
hW : IsOpen[inst_1] W
hxV : x ∈ V
hyW : y ∈ W
hVW : V ×ˢ W ⊆ U
⊢ ∃
    t ⊆
      {a : Prod.{u_1, u_2} (Compacts α) (Compacts β) |
        (Function.comp (β := Compacts (α × β)) SetLike.coe
              (fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦ p.1 ×ˢ p.2) a ∩
            V ×ˢ W).Nonempty},
    IsOpen t ∧ (K, L) ∈ t
have inr : ∃ t ⊆ {a : Prod.{u_1, u_2} (Compacts α) (Compacts β) | ((↑a.1 : Set α) ∩ V).Nonempty ∧ ((↑a.2 : Set β) ∩ W).Nonempty},
  IsOpen t ∧ (K, L) ∈ t
Tactic: simp_rw [Function.comp_apply, coe_prod, prod_inter_prod, prod_nonempty_iff]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : DiscreteTopology α
⊢ DiscreteTopology.{u_1} (Compacts α)
have rw : ∀ (a : Compacts α), IsOpen (X := Compacts α) {a}
Tactic: rw [discreteTopology_iff_isOpen_singleton]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : DiscreteTopology α
K : Compacts α
⊢ IsOpen (X := Compacts α) {K}
have h : Eq (α := Set (Compacts α)) {K}
  ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
    ⋂ i ∈ (↑K : Set α), {K : Compacts α | ((↑K : Set α) ∩ {i}).Nonempty})
Tactic: convert!
    (isOpen_subsets_of_isOpen (isOpen_discrete (K : Set α))).inter
      (K.isCompact.finite_of_discrete.isOpen_biInter fun x hx =>
        isOpen_inter_nonempty_of_isOpen (isOpen_discrete { x }))
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : DiscreteTopology α
K : Compacts α
⊢ Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      ⋂ i ∈ (↑K : Set α), {K : Compacts α | ((↑K : Set α) ∩ {i}).Nonempty})
have h : Eq (α := Set (Compacts α)) {K}
  ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
    {x : Compacts α | ∀ (i : α) (i_1 : i ∈ (↑K : Set α)), ((↑x : Set α) ∩ {i}).Nonempty})
Tactic: simp_rw [← setOf_forall, inter_singleton_nonempty, ← Set.subset_def, ← setOf_and,
    ← subset_antisymm_iff, SetLike.coe_set_eq, setOf_eq_eq_singleton]
-- Lean 4 proof step from Mathlib.Topology.Sets.VietorisTopology (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : DiscreteTopology α
K : Compacts α
h :
  Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      {x : Compacts α | ∀ (i : α) (i_1 : i ∈ (↑K : Set α)), ((↑x : Set α) ∩ {i}).Nonempty})
⊢ Eq (α := Set (Compacts α)) {K}
    ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
      ⋂ i ∈ (↑K : Set α), {K : Compacts α | ((↑K : Set α) ∩ {i}).Nonempty})
have h₁ : Eq (α := Set (Compacts α)) {K}
  ({K_1 : Compacts α | (↑K_1 : Set α) ⊆ (↑K : Set α)} ∩
    {x : Compacts α | ∀ (i : α) (i_1 : i ∈ (↑K : Set α)), i ∈ (↑x : Set α)})
Tactic: simp_rw [← setOf_forall, inter_singleton_nonempty, ← Set.subset_def, ← setOf_and,
    ← subset_antisymm_iff, SetLike.coe_set_eq, setOf_eq_eq_singleton]