awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
⊢ ⋃₀ (u ∪ w) ⊆ V

Tactic:
grind [sUnion_union, Finite.union]

Premises used: Set.Finite.union, Set.sUnion_union
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
⊢ ∀ W ∈ u ∪ w, ((↑K : Set α) ∩ W).Nonempty

Tactic:
grind [sUnion_union, Finite.union]

Premises used: Set.Finite.union, Set.sUnion_union
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
⊢ (u ∪ w).Finite

Tactic:
grind [sUnion_union, Finite.union]

Premises used: Set.Finite.union, Set.sUnion_union
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
⊢ u ⊆ u ∪ w

Tactic:
grind [sUnion_union, Finite.union]

Premises used: Set.Finite.union, Set.sUnion_union
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
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})
⊢ ∃ (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}

Tactic:
rw [exists_mem_image]

Premises used: Set.exists_mem_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
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})
⊢ ∃ (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:
exists w
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
⊢ 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:
grind (splits := 12)
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsTopologicalBasis.{u_1} (α := Compacts α)
    ((fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
      {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})

Tactic:
isTopologicalBasis_opens.compacts

Premises used: Set.Mem, TopologicalSpace.IsTopologicalBasis.compacts, setOf, TopologicalSpace.isTopologicalBasis_opens, Set.Subset, IsOpen
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsEmbedding (Y := Compacts α) fun (x : α) ↦ {x}

Tactic:
isEmbedding_coe.of_comp_iff.mp vietoris.isEmbedding_singleton

Premises used: TopologicalSpace.Compacts.isEmbedding_coe, TopologicalSpace.vietoris.isEmbedding_singleton, Iff.mp, Topology.IsEmbedding.of_comp_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Continuous[inst, _] fun (x : α) ↦ {x}

Tactic:
isEmbedding_singleton.continuous

Premises used: TopologicalSpace.Compacts.isEmbedding_singleton, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : T2Space α
⊢ IsClosedEmbedding (Y := Compacts α) fun (x : α) ↦ {x}

Tactic:
.of_comp isEmbedding_coe vietoris.isClosedEmbedding_singleton

Premises used: TopologicalSpace.Compacts.isEmbedding_coe, TopologicalSpace.vietoris.isClosedEmbedding_singleton, Topology.IsClosedEmbedding.of_comp
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
continuous_sup : Continuous (Y := Compacts α) fun (p : Compacts α × Compacts α) ↦ p.1 ⊔ p.2
⊢ ContinuousSup.{u_1} (Compacts α)

Tactic:
constructor
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
continuous_sup :
  Continuous[_, TopologicalSpace.vietoris α] fun (x : Compacts α × Compacts α) ↦ (↑x.1 : Set α) ∪ (↑x.2 : Set α)
⊢ Continuous (Y := Compacts α) fun (p : Compacts α × Compacts α) ↦ p.1 ⊔ p.2

Tactic:
simp_rw [isEmbedding_coe.continuous_iff, Function.comp_def, coe_sup]

Premises used: TopologicalSpace.Compacts.isEmbedding_coe, TopologicalSpace.Compacts.coe_sup, Function.comp_def, Topology.IsEmbedding.continuous_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
⊢ Continuous[_, TopologicalSpace.vietoris α] fun (x : Compacts α × Compacts α) ↦ (↑x.1 : Set α) ∪ (↑x.2 : Set α)

Tactic:
fun_prop
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
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)
⊢ Continuous (Y := Compacts (α × β)) fun (p : Prod.{u_1, u_2} (Compacts α) (Compacts β)) ↦ p.1 ×ˢ p.2

Tactic:
rw [continuous_induced_rng, continuous_generateFrom_iff]

Premises used: continuous_generateFrom_iff, continuous_induced_rng
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
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
⊢ 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)

Tactic:
rw [isOpen_iff_forall_mem_open]

Premises used: isOpen_iff_forall_mem_open
-- Module: Mathlib.Topology.Sets.VietorisTopology
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 β
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
⊢ 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

Tactic:
(hKL : (K : Set α) ×ˢ (L : Set β) ⊆ U)
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
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
⊢ ∃
    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

Premises used: TopologicalSpace.Compacts.isCompact, generalized_tube_lemma
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
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:
⟨_, fun ⟨K', L'⟩ ⟨hK', hL'⟩ => (Set.prod_mono hK' hL').trans hVW,
      (isOpen_subsets_of_isOpen hV).prod (isOpen_subsets_of_isOpen hW), hK, hL⟩

Premises used: And.intro, Exists.intro, TopologicalSpace.Compacts.isOpen_subsets_of_isOpen, IsOpen.prod
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
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:
exact ⟨_, fun ⟨K', L'⟩ ⟨hK', hL'⟩ => (Set.prod_mono hK' hL').trans hVW,
      (isOpen_subsets_of_isOpen hV).prod (isOpen_subsets_of_isOpen hW), hK, hL⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
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
⊢ 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)

Tactic:
rw [isOpen_iff_forall_mem_open]

Premises used: isOpen_iff_forall_mem_open
-- Module: Mathlib.Topology.Sets.VietorisTopology
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 β
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
⊢ 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

Tactic:
⟨⟨x, y⟩, ⟨(hx : x ∈ K), (hy : y ∈ L)⟩, hxy⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
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
⊢ ∃
    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

Premises used: isOpen_prod_iff, Iff.mp
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
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
⊢ ∃
    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:
grw [preimage_setOf_eq, ← hVW]

Premises used: Set.preimage_setOf_eq
-- Module: Mathlib.Topology.Sets.VietorisTopology
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
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
⊢ ∃
    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:
simp_rw [Function.comp_apply, coe_prod, prod_inter_prod, prod_nonempty_iff]

Premises used: Set.prod_nonempty_iff, TopologicalSpace.Compacts.coe_prod, Function.comp_apply, Set.prod_inter_prod
-- Module: Mathlib.Topology.Sets.VietorisTopology
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 β) | ((↑a.1 : Set α) ∩ V).Nonempty ∧ ((↑a.2 : Set β) ∩ W).Nonempty},
    IsOpen t ∧ (K, L) ∈ t

Tactic:
⟨_, .rfl,
      (isOpen_inter_nonempty_of_isOpen hV).prod (isOpen_inter_nonempty_of_isOpen hW),
      ⟨x, hx, hxV⟩, ⟨y, hy, hyW⟩⟩

Premises used: TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen, Set.Subset.rfl, And.intro, Exists.intro, IsOpen.prod
-- Module: Mathlib.Topology.Sets.VietorisTopology
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 β) | ((↑a.1 : Set α) ∩ V).Nonempty ∧ ((↑a.2 : Set β) ∩ W).Nonempty},
    IsOpen t ∧ (K, L) ∈ t

Tactic:
exact ⟨_, .rfl,
      (isOpen_inter_nonempty_of_isOpen hV).prod (isOpen_inter_nonempty_of_isOpen hW),
      ⟨x, hx, hxV⟩, ⟨y, hy, hyW⟩⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
hf : Continuous[inst, inst_1] f
⊢ Continuous (Compacts.map f hf)

Tactic:
isEmbedding_coe.continuous_iff.mpr <| hf.image_vietoris.comp continuous_coe

Premises used: Iff.mpr, TopologicalSpace.Compacts.isEmbedding_coe, Continuous.comp, TopologicalSpace.Compacts.continuous_coe, Continuous.image_vietoris, Topology.IsEmbedding.continuous_iff