awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
h :
  ∀ (K' : Compacts α) (h₁ : (↑K' : Set α) ⊆ interior L) (h₂ : ∀ i ∈ u, ((↑K' : Set α) ∩ interior (M i)).Nonempty),
    (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty
⊢ {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty} ∈ 𝓝 K

Tactic:
filter_upwards [
      (isOpen_subsets_of_isOpen isOpen_interior).mem_nhds hLK,
      (Filter.eventually_all_finite hu₁).mpr fun U hU =>
        (isOpen_inter_nonempty_of_isOpen isOpen_interior).mem_nhds (hMK U hU)] with K' h₁ h₂

Premises used: Iff.mpr, isOpen_interior, TopologicalSpace.Compacts.isOpen_inter_nonempty_of_isOpen, Filter.eventually_all_finite, IsOpen.mem_nhds, TopologicalSpace.Compacts.isOpen_subsets_of_isOpen
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
K' : Compacts α
h₁ : (↑K' : Set α) ⊆ interior L
h₂ : ∀ i ∈ u, ((↑K' : Set α) ∩ interior (M i)).Nonempty
⊢ (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty

Tactic:
⟨h₁.trans interior_subset,
      fun U hU => (h₂ U hU).mono (inter_subset_inter_right _ interior_subset)⟩

Premises used: Set.inter_subset_inter_right, interior_subset, HasSubset.Subset.trans, Set.Nonempty.mono, SetLike.coe, And.intro
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
K' : Compacts α
h₁ : (↑K' : Set α) ⊆ interior L
h₂ : ∀ i ∈ u, ((↑K' : Set α) ∩ interior (M i)).Nonempty
⊢ (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty

Tactic:
exact ⟨h₁.trans interior_subset,
      fun U hU => (h₂ U hU).mono (inter_subset_inter_right _ interior_subset)⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
refine_2 :
  IsCompact
    (image (α := Compacts α) SetLike.coe
      {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty})
⊢ IsCompact.{u_1} (X := Compacts α) {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty}

Tactic:
rw [isEmbedding_coe.isCompact_iff]

Premises used: TopologicalSpace.Compacts.isEmbedding_coe, Topology.IsEmbedding.isCompact_iff
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
⊢ M '' u ⊆ 𝒫 L

Tactic:
grind
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
⊢ ∀ L ∈ M '' u, IsCompact L

Tactic:
grind
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
⊢ image (α := Compacts α) SetLike.coe {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty} ⊆
    {t : Set α | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty}

Tactic:
grind
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
refine_2 :
  ∀ (s : Set α),
    Membership.mem (γ := Set (Set α)) {t : Set α | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty} s →
      ∀ (hsL : s ⊆ L) (hsu : ∀ L ∈ M '' u, (s ∩ L).Nonempty),
        ∃
          y ∈
            image (α := Compacts α) SetLike.coe
              {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty},
          s ⤳ y
⊢ IsCompact
    (image (α := Compacts α) SetLike.coe
      {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty})

Tactic:
refine vietoris.isCompact_aux hL (s := M '' u) (by grind) (by grind)
      |>.of_subset_of_specializes (by grind) (fun s ⟨hsL, hsu⟩ => ?_)

Premises used: Specializes, Membership.mem, Exists, IsCompact.of_subset_of_specializes, _private.0.TopologicalSpace.vietoris.isCompact_aux, And, _private.0.TopologicalSpace.Compacts.instLocallyCompactSpace.match_4
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
s : Set α
h : Membership.mem (γ := Set (Set α)) {t : Set α | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty} s
hsL : s ⊆ L
hsu : ∀ L ∈ M '' u, (s ∩ L).Nonempty
⊢ ∀ ⦃x : Set α⦄, x ∈ u → (s ∩ M x).Nonempty

Tactic:
rw [forall_mem_image] at hsu

Premises used: Set.forall_mem_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
s : Set α
h : Membership.mem (γ := Set (Set α)) {t : Set α | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty} s
hsL : s ⊆ L
hsu : ∀ ⦃x : Set α⦄, x ∈ u → (s ∩ M x).Nonempty
s' : Compacts α := { carrier := L ∩ closure[inst] s, isCompact' := ⋯ }
⊢ ∃
    y ∈
      image (α := Compacts α) SetLike.coe
        {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty},
    s ⤳ y

Tactic:
⟨s', mem_image_of_mem _ ⟨inter_subset_left, fun U hU => (hsu hU).mono ?_⟩,
      vietoris.specializes_of_subset_closure ?_ ?_⟩

Premises used: TopologicalSpace.vietoris.specializes_of_subset_closure, Set.inter_subset_left, Set.Nonempty.mono, SetLike.coe, Set.mem_image_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
s : Set α
h : Membership.mem (γ := Set (Set α)) {t : Set α | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty} s
hsL : s ⊆ L
hsu : ∀ ⦃x : Set α⦄, x ∈ u → (s ∩ M x).Nonempty
s' : Compacts α := { carrier := L ∩ closure[inst] s, isCompact' := ⋯ }
refine_2 : ∀ (U : Set α) (hU : U ∈ u), s ∩ M U ⊆ (↑s' : Set α) ∩ M U
refine_2₁ : s ⊆ (↑s' : Set α)
refine_2₂ : (↑s' : Set α) ⊆ closure[inst] s
⊢ ∃
    y ∈
      image (α := Compacts α) SetLike.coe
        {K' : Compacts α | (↑K' : Set α) ⊆ L ∧ ∀ U ∈ u, ((↑K' : Set α) ∩ M U).Nonempty},
    s ⤳ y

Tactic:
refine ⟨s', mem_image_of_mem _ ⟨inter_subset_left, fun U hU => (hsu hU).mono ?_⟩,
      vietoris.specializes_of_subset_closure ?_ ?_⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
s : Set α
h : Membership.mem (γ := Set (Set α)) {t : Set α | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty} s
hsL : s ⊆ L
hsu : ∀ ⦃x : Set α⦄, x ∈ u → (s ∩ M x).Nonempty
s' : Compacts α := { carrier := L ∩ closure[inst] s, isCompact' := ⋯ }
U : Set α
hU : U ∈ u
⊢ s ∩ M U ⊆ (↑s' : Set α) ∩ M U

Tactic:
grind [coe_mk, subset_closure]

Premises used: subset_closure, TopologicalSpace.Compacts.coe_mk
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
s : Set α
h : Membership.mem (γ := Set (Set α)) {t : Set α | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty} s
hsL : s ⊆ L
hsu : ∀ ⦃x : Set α⦄, x ∈ u → (s ∩ M x).Nonempty
s' : Compacts α := { carrier := L ∩ closure[inst] s, isCompact' := ⋯ }
⊢ s ⊆ (↑s' : Set α)

Tactic:
grind [coe_mk, subset_closure]

Premises used: subset_closure, TopologicalSpace.Compacts.coe_mk
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α → β
inst_2 : LocallyCompactSpace α
K : Compacts α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
hKu₁ : (↑K : Set α) ⊆ ⋃₀ u
hKu₂ : ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty
L : Set α
hL : IsCompact L
hLK : (↑K : Set α) ⊆ interior L
hLu : L ⊆ ⋃₀ u
M : (U : Set α) → Set α
hM : ∀ (U : Set α) (hU : U ∈ u), IsCompact (M U)
hML : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ L
hMU : ∀ (U : Set α) (hU : U ∈ u), M U ⊆ U
hMK : ∀ (U : Set α) (hU : U ∈ u), ((↑K : Set α) ∩ interior (M U)).Nonempty
s : Set α
h : Membership.mem (γ := Set (Set α)) {t : Set α | t ⊆ L ∧ ∀ L ∈ M '' u, (t ∩ L).Nonempty} s
hsL : s ⊆ L
hsu : ∀ ⦃x : Set α⦄, x ∈ u → (s ∩ M x).Nonempty
s' : Compacts α := { carrier := L ∩ closure[inst] s, isCompact' := ⋯ }
⊢ (↑s' : Set α) ⊆ closure[inst] s

Tactic:
grind [coe_mk, subset_closure]

Premises used: subset_closure, TopologicalSpace.Compacts.coe_mk
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Continuous[_, TopologicalSpace.vietoris α] SetLike.coe

Tactic:
isEmbedding_coe.continuous

Premises used: TopologicalSpace.NonemptyCompacts.isEmbedding_coe, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ Continuous.{u_1, u_1} (X := NonemptyCompacts α) toCompacts

Tactic:
isEmbedding_toCompacts.continuous

Premises used: TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts, Topology.IsEmbedding.continuous
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
rw : IsClosed (X := Compacts α) {⊥}ᶜ
⊢ IsClosed.{u_1} (X := Compacts α) (range toCompacts)

Tactic:
rw [range_toCompacts]

Premises used: TopologicalSpace.NonemptyCompacts.range_toCompacts
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsClosed (X := Compacts α) {⊥}ᶜ

Tactic:
Compacts.isClopen_singleton_bot.compl.isClosed

Premises used: TopologicalSpace.Compacts.isClopen_singleton_bot, IsClopen.compl, IsClopen.isClosed
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsClosed (X := Compacts α) {⊥}ᶜ

Tactic:
exact Compacts.isClopen_singleton_bot.compl.isClosed

Premises used: TopologicalSpace.Compacts.isClopen_singleton_bot, IsClopen.compl, IsClopen.isClosed
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
rw : IsOpen (X := Compacts α) {⊥}ᶜ
⊢ IsOpen.{u_1} (X := Compacts α) (range toCompacts)

Tactic:
rw [range_toCompacts]

Premises used: TopologicalSpace.NonemptyCompacts.range_toCompacts
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsOpen (X := Compacts α) {⊥}ᶜ

Tactic:
Compacts.isClopen_singleton_bot.compl.isOpen

Premises used: TopologicalSpace.Compacts.isClopen_singleton_bot, IsClopen.compl, IsClopen.isOpen
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsOpen (X := Compacts α) {⊥}ᶜ

Tactic:
exact Compacts.isClopen_singleton_bot.compl.isOpen

Premises used: TopologicalSpace.Compacts.isClopen_singleton_bot, IsClopen.compl, IsClopen.isOpen
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
U : Set α
h : IsOpen[inst] U
⊢ IsOpen.{u_1} (X := NonemptyCompacts α) {K : NonemptyCompacts α | (↑K : Set α) ⊆ U}

Tactic:
h.powerset_vietoris.preimage continuous_coe

Premises used: Set.Mem, setOf, Set.powerset, Set.preimage, IsOpen.powerset_vietoris, TopologicalSpace.NonemptyCompacts.continuous_coe, IsOpen.preimage
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
U : Set α
h : IsOpen[inst] U
⊢ IsOpen.{u_1} (X := NonemptyCompacts α) {K : NonemptyCompacts α | ((↑K : Set α) ∩ U).Nonempty}

Tactic:
(vietoris.isOpen_inter_nonempty_of_isOpen h).preimage continuous_coe

Premises used: Set.Mem, setOf, Set.Nonempty, TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen, Set.preimage, TopologicalSpace.NonemptyCompacts.continuous_coe, IsOpen.preimage
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
⊢ IsClosed.{u_1} (X := NonemptyCompacts α) {K : NonemptyCompacts α | (↑K : Set α) ⊆ F}

Tactic:
h.powerset_vietoris.preimage continuous_coe

Premises used: Set.Mem, setOf, Set.powerset, Set.preimage, IsClosed.powerset_vietoris, IsClosed.preimage, TopologicalSpace.NonemptyCompacts.continuous_coe
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
⊢ IsClosed.{u_1} (X := NonemptyCompacts α) {K : NonemptyCompacts α | ((↑K : Set α) ∩ F).Nonempty}

Tactic:
(vietoris.isClosed_inter_nonempty_of_isClosed h).preimage continuous_coe

Premises used: Set.Mem, TopologicalSpace.vietoris.isClosed_inter_nonempty_of_isClosed, setOf, Set.Nonempty, Set.preimage, IsClosed.preimage, TopologicalSpace.NonemptyCompacts.continuous_coe
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
⊢ IsTopologicalBasis.{u_1} (α := NonemptyCompacts α)
    ((fun (u : Set (Set α)) ↦ {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
      {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})

Tactic:
hB.compacts.isInducing isEmbedding_toCompacts.isInducing
    |>.isTopologicalBasis_of_exists_subset ?_ ?_

Premises used: TopologicalSpace.IsTopologicalBasis.compacts, Topology.IsEmbedding.isInducing, TopologicalSpace.IsTopologicalBasis.isInducing, TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts, TopologicalSpace.IsTopologicalBasis.isTopologicalBasis_of_exists_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
refine_1 :
  ∀ (u : Set (NonemptyCompacts α)),
    Membership.mem (γ := Set (Set (NonemptyCompacts α)))
        ((fun (u : Set (Set α)) ↦
            {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
        u →
      IsOpen u
refine_2 :
  ∀ (u : Set (NonemptyCompacts α)),
    Membership.mem (γ := Set (Set (NonemptyCompacts α)))
        (preimage toCompacts ''
          (fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        u →
      ∀ x ∈ u,
        ∃ (v : Set (NonemptyCompacts α)),
          Membership.mem (γ := Set (Set (NonemptyCompacts α)))
              ((fun (u : Set (Set α)) ↦
                  {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
              v ∧
            x ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis.{u_1} (α := NonemptyCompacts α)
    ((fun (u : Set (Set α)) ↦ {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
      {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})

Tactic:
refine hB.compacts.isInducing isEmbedding_toCompacts.isInducing
    |>.isTopologicalBasis_of_exists_subset ?_ ?_

Premises used: TopologicalSpace.IsTopologicalBasis.compacts, Topology.IsEmbedding.isInducing, TopologicalSpace.IsTopologicalBasis.isInducing, TopologicalSpace.NonemptyCompacts.isEmbedding_toCompacts, TopologicalSpace.IsTopologicalBasis.isTopologicalBasis_of_exists_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
refine_1 :
  ∀ ⦃x : Set (Set α)⦄,
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B} x →
      IsOpen.{u_1} (X := NonemptyCompacts α)
        {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}
⊢ ∀ (u : Set (NonemptyCompacts α)),
    Membership.mem (γ := Set (Set (NonemptyCompacts α)))
        ((fun (u : Set (Set α)) ↦
            {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
        u →
      IsOpen u

Tactic:
simp_rw [forall_mem_image]

Premises used: Set.forall_mem_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
refine_2 :
  ∀ ⦃x : Set (Set α)⦄,
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ u ⊆ B} x →
      ∀ (x_1 : NonemptyCompacts α),
        Membership.mem (γ := Set (NonemptyCompacts α))
            (toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}) x_1 →
          ∃ (v : Set (NonemptyCompacts α)),
            Membership.mem (γ := Set (Set (NonemptyCompacts α)))
                ((fun (u : Set (Set α)) ↦
                    {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
                  {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
                v ∧
              x_1 ∈ v ∧ v ⊆ toCompacts ⁻¹' {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ x ∧ ∀ U ∈ x, ((↑K : Set α) ∩ U).Nonempty}
⊢ ∀ (u : Set (NonemptyCompacts α)),
    Membership.mem (γ := Set (Set (NonemptyCompacts α)))
        (preimage toCompacts ''
          (fun (u : Set (Set α)) ↦ {K : Compacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
            {u : Set (Set α) | u.Finite ∧ u ⊆ B})
        u →
      ∀ x ∈ u,
        ∃ (v : Set (NonemptyCompacts α)),
          Membership.mem (γ := Set (Set (NonemptyCompacts α)))
              ((fun (u : Set (Set α)) ↦
                  {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ u.Nonempty ∧ u ⊆ B})
              v ∧
            x ∈ v ∧ v ⊆ u

Tactic:
simp_rw [forall_mem_image]

Premises used: Set.forall_mem_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
B : Set (Set α)
hB : IsTopologicalBasis B
u : Set (Set α)
hu : u.Finite
huB : u ⊆ B
refine_1 :
  IsOpen.{u_1} (X := NonemptyCompacts α)
    ({a : NonemptyCompacts α | (↑a : Set α) ⊆ ⋃₀ u} ∩ ⋂ i ∈ u, {x : NonemptyCompacts α | ((↑x : Set α) ∩ i).Nonempty})
⊢ IsOpen.{u_1} (X := NonemptyCompacts α)
    {K : NonemptyCompacts α | (↑K : Set α) ⊆ ⋃₀ u ∧ ∀ U ∈ u, ((↑K : Set α) ∩ U).Nonempty}

Tactic:
simp_rw [setOf_and, setOf_forall]

Premises used: Set.setOf_and, Set.setOf_forall