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
inr :
  ∀
    (this :
      ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
        (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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})
    (hw : ¬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}
wlog :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
⊢ ∃ (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:
wlog hw : w.Finite generalizing w

Premises used: Set.Finite
-- 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
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
hw : ¬w.Finite
⊢ (↑K : Set α) ⊆ ⋃ i ∈ w, i

Tactic:
rw [sUnion_eq_biUnion] at hKV

Premises used: Set.sUnion_eq_biUnion
-- 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
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
hw : ¬w.Finite
hKV₁ : (↑K : Set α) ⊆ ⋃ i ∈ w, i
⊢ w ⊆ B

Tactic:
rw [sUnion_eq_biUnion] at hKV

Premises used: Set.sUnion_eq_biUnion
-- 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
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
hw : ¬w.Finite
hKV₁ : (↑K : Set α) ⊆ ⋃ i ∈ w, i
hwB₁ : w ⊆ B
⊢ ⋃₀ w ⊆ V

Tactic:
rw [sUnion_eq_biUnion] at hKV

Premises used: Set.sUnion_eq_biUnion
-- 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
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
hw : ¬w.Finite
hKV₁ : (↑K : Set α) ⊆ ⋃ i ∈ w, i
hwB₁ : w ⊆ B
hwV₁ : ⋃₀ w ⊆ V
⊢ ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty

Tactic:
rw [sUnion_eq_biUnion] at hKV

Premises used: Set.sUnion_eq_biUnion
-- 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
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
hw : ¬w.Finite
hKV₁ : (↑K : Set α) ⊆ ⋃ i ∈ w, i
hwB₁ : w ⊆ B
hwV₁ : ⋃₀ w ⊆ V
hwK₁ : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
⊢ ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}

Tactic:
rw [sUnion_eq_biUnion] at hKV

Premises used: Set.sUnion_eq_biUnion
-- 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
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
hw : ¬w.Finite
hKV₁ : (↑K : Set α) ⊆ ⋃ i ∈ w, i
hwB₁ : w ⊆ B
hwV₁ : ⋃₀ w ⊆ V
hwK₁ : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this₁ :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
⊢ ¬w.Finite

Tactic:
rw [sUnion_eq_biUnion] at hKV

Premises used: Set.sUnion_eq_biUnion
-- 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 α) ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
hw : ¬w.Finite
inr :
  ∀ (w' : Set (Set α)),
    w' ⊆ w ∧ w'.Finite ∧ (↑K : Set α) ⊆ ⋃ i ∈ w', i →
      ∃ (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}
⊢ ∃ (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:
obtain ⟨w', _⟩ := K.isCompact.elim_finite_subcover_image (fun W hW => hB.isOpen (hwB hW)) hKV

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen, TopologicalSpace.Compacts.isCompact, IsCompact.elim_finite_subcover_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 α) ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
hw : ¬w.Finite
w' : Set (Set α)
h : w' ⊆ w ∧ w'.Finite ∧ (↑K : Set α) ⊆ ⋃ i ∈ w', i
inr : (↑K : Set α) ⊆ ⋃₀ w'
inr₁ : w' ⊆ B
inr₂ : ⋃₀ w' ⊆ V
inr₃ : ∀ W ∈ w', ((↑K : Set α) ∩ W).Nonempty
inr₄ : 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}

Tactic:
apply this 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 α) ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
hw : ¬w.Finite
w' : Set (Set α)
h : w' ⊆ w ∧ w'.Finite ∧ (↑K : Set α) ⊆ ⋃ i ∈ w', i
⊢ (↑K : Set α) ⊆ ⋃₀ w'

Tactic:
grind [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- 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 α) ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
hw : ¬w.Finite
w' : Set (Set α)
h : w' ⊆ w ∧ w'.Finite ∧ (↑K : Set α) ⊆ ⋃ i ∈ w', i
⊢ w' ⊆ B

Tactic:
grind [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- 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 α) ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
hw : ¬w.Finite
w' : Set (Set α)
h : w' ⊆ w ∧ w'.Finite ∧ (↑K : Set α) ⊆ ⋃ i ∈ w', i
⊢ ⋃₀ w' ⊆ V

Tactic:
grind [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- 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 α) ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
hw : ¬w.Finite
w' : Set (Set α)
h : w' ⊆ w ∧ w'.Finite ∧ (↑K : Set α) ⊆ ⋃ i ∈ w', i
⊢ ∀ W ∈ w', ((↑K : Set α) ∩ W).Nonempty

Tactic:
grind [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- 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 α) ⊆ ⋃ i ∈ w, i
hwB : w ⊆ B
hwV : ⋃₀ w ⊆ V
hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty
this :
  ∀ (w : Set (Set α)) (hKV : (↑K : Set α) ⊆ ⋃₀ w) (hwB : w ⊆ B) (hwV : ⋃₀ w ⊆ V)
    (hwK : ∀ W ∈ w, ((↑K : Set α) ∩ W).Nonempty) (hw : 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}
hw : ¬w.Finite
w' : Set (Set α)
h : w' ⊆ w ∧ w'.Finite ∧ (↑K : Set α) ⊆ ⋃ i ∈ w', i
⊢ w'.Finite

Tactic:
grind [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- 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
inr :
  ∀
    (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}
wlog :
  ∀ (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}
⊢ ∃ (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:
wlog huw : u ⊆ w generalizing 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
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
inr₅ : u ⊆ 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}

Tactic:
apply this (u ∪ w)

Premises used: Union.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
⊢ (↑K : Set α) ⊆ ⋃₀ (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
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 ⊆ B

Tactic:
grind [sUnion_union, Finite.union]

Premises used: Set.Finite.union, Set.sUnion_union