awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : C(α, β)
s t : Opens β
h : s ≤ t
⊢ LE.le.{u_2} (α := Opens α) ((comap f : (a : Opens β) → Opens α) s : Opens α)
    ((comap f : (a : Opens β) → Opens α) t : Opens α)

Tactic:
OrderHomClass.mono (comap f) h

Premises used: Set.Mem, OrderHomClass.mono, TopologicalSpace.Opens.comap
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : C(α, β)
U : Opens β
⊢ (↑((comap f : (a : Opens β) → Opens α) U : Opens α) : Set α) = (⇑f : (a : α) → β) ⁻¹' (↑U : Set β)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : C(α, β)
U : Opens β
x : α
⊢ Membership.mem (γ := Opens α) ((comap f : (a : Opens β) → Opens α) U : Opens α) x ↔
    Membership.mem (α := β) U ((f : (a : α) → β) x : β)

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
⊢ comap (g.comp f) = (comap f).comp (comap g)

Tactic:
rfl

Premises used: Set.Mem, setOf, FrameHom.comp, TopologicalSpace.Opens.comap, Set.preimage, InfTopHom.comp, InfHom.comp, rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
g : C(β, γ)
f : C(α, β)
U : Opens γ
⊢ Eq.{u_2 + 1} (α := Opens α) ((comap f : (a : Opens β) → Opens α) ((comap g : (a : Opens γ) → Opens β) U) : Opens α)
    ((comap (g.comp f) : (a : Opens γ) → Opens α) U : Opens α)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : T0Space β
⊢ Injective (α := C(α, β)) comap

Tactic:
fun f g h =>
  ContinuousMap.ext fun a =>
    Inseparable.eq <|
      inseparable_iff_forall_isOpen.2 fun s hs =>
        have : comap f ⟨s, hs⟩ = comap g ⟨s, hs⟩ := DFunLike.congr_fun h ⟨_, hs⟩
        show a ∈ f ⁻¹' s ↔ a ∈ g ⁻¹' s from Set.ext_iff.1 (coe_inj.2 this) a

Premises used: Iff.mpr, Inseparable.eq, inseparable_iff_forall_isOpen, ContinuousMap.ext, Iff.mp, Set.ext_iff, Function.Injective, TopologicalSpace.Opens.coe_inj
-- Module: Mathlib.Topology.Sets.Opens
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α ≃ₜ β
a b : Opens α
⊢ (↑(({ toFun := (⇑(comap (↑f.symm : C(β, α))) : (a : Opens α) → Opens β),
                  invFun := (⇑(comap (↑f : C(α, β))) : (a : Opens β) → Opens α), left_inv := ⋯, right_inv := ⋯ :
                  Equiv.{u_2 + 1, u_3 + 1} (Opens α) (Opens β) } :
                (a : Opens α) → Opens β)
              a :
            Opens β) :
        Set β) ⊆
      (↑(({ toFun := (⇑(comap (↑f.symm : C(β, α))) : (a : Opens α) → Opens β),
                  invFun := (⇑(comap (↑f : C(α, β))) : (a : Opens β) → Opens α), left_inv := ⋯, right_inv := ⋯ } :
                (a : Opens α) → Opens β)
              b :
            Opens β) :
        Set β) ↔
    (↑a : Set α) ⊆ (↑b : Set α)

Tactic:
f.symm.surjective.preimage_subset_preimage_iff

Premises used: Function.Surjective.preimage_subset_preimage_iff, Set.Mem, setOf, Set.preimage, Homeomorph.symm, Homeomorph.surjective
-- Module: Mathlib.Topology.Sets.Opens
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
f : α ≃ₜ β
⊢ ∀ {a b : Opens α},
    (↑(({ toFun := (⇑(comap (↑f.symm : C(β, α))) : (a : Opens α) → Opens β),
                    invFun := (⇑(comap (↑f : C(α, β))) : (a : Opens β) → Opens α), left_inv := ⋯, right_inv := ⋯ :
                    Equiv.{u_2 + 1, u_3 + 1} (Opens α) (Opens β) } :
                  (a : Opens α) → Opens β)
                a :
              Opens β) :
          Set β) ⊆
        (↑(({ toFun := (⇑(comap (↑f.symm : C(β, α))) : (a : Opens α) → Opens β),
                    invFun := (⇑(comap (↑f : C(α, β))) : (a : Opens β) → Opens α), left_inv := ⋯, right_inv := ⋯ } :
                  (a : Opens α) → Opens β)
                b :
              Opens β) :
          Set β) ↔
      (↑a : Set α) ⊆ (↑b : Set α)

Tactic:
exact f.symm.surjective.preimage_subset_preimage_iff

Premises used: Function.Surjective.preimage_subset_preimage_iff, Homeomorph.symm, Homeomorph.surjective
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
β : Type u_3
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
⊢ f.opensCongr.symm = f.symm.opensCongr

Tactic:
rfl

Premises used: RelIso.symm, Homeomorph.opensCongr, OrderIso.symm, Homeomorph.symm, Equiv.symm, rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : Finite α
⊢ Finite.{u_2 + 1} (Opens α)

Tactic:
Finite.of_injective _ SetLike.coe_injective

Premises used: SetLike.coe_injective, Finite.of_injective
-- Module: Mathlib.Topology.Sets.Opens
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
x : α
⊢ CanLift (Set α) (OpenNhdsOf x) SetLike.coe fun (s : Set α) ↦ IsOpen[inst] s ∧ x ∈ s

Tactic:
⟨fun s hs => ⟨⟨⟨s, hs.1⟩, hs.2⟩, rfl⟩⟩

Premises used: TopologicalSpace.OpenNhdsOf.mk, And.right, TopologicalSpace.Opens.mk, And.left, Exists.intro, CanLift.mk, rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
x : α
U : OpenNhdsOf x
⊢ x ∈ U

Tactic:
U.mem'

Premises used: Set.Mem, TopologicalSpace.OpenNhdsOf.mem'
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
x : α
U : OpenNhdsOf x
⊢ IsOpen[inst] (↑U : Set α)

Tactic:
U.is_open'

Premises used: TopologicalSpace.OpenNhdsOf.toOpens, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
x : α
⊢ (𝓝 x).HasBasis (fun (x : OpenNhdsOf x) ↦ True) SetLike.coe

Tactic:
(nhds_basis_opens x).to_hasBasis (fun U hU => ⟨⟨⟨U, hU.2⟩, hU.1⟩, trivial, Subset.rfl⟩) fun U _ =>
    ⟨U, ⟨⟨U.mem, U.isOpen⟩, Subset.rfl⟩⟩

Premises used: trivial, TopologicalSpace.OpenNhdsOf.mem, TopologicalSpace.OpenNhdsOf.mk, TopologicalSpace.OpenNhdsOf.isOpen, Set.Subset.rfl, SetLike.coe, And.right, TopologicalSpace.Opens.mk, And.left, And.intro, Exists.intro, nhds_basis_opens, Filter.HasBasis.to_hasBasis
-- Module: Mathlib.Topology.Sets.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LE α
s t : ClopenUpperSet α
h : Eq.{u_1 + 1} (α := Set α) ((fun (s : ClopenUpperSet α) ↦ s.carrier) s) ((fun (s : ClopenUpperSet α) ↦ s.carrier) t)
obtain :
  ∀ (carrier : Set α) (isClopen' : IsClopen carrier)
    (upper' : IsUpperSet { carrier := carrier, isClopen' := isClopen' : Clopens α }.carrier)
    (h :
      Eq.{u_1 + 1} (α := Set α)
        ((fun (s : ClopenUpperSet α) ↦ s.carrier) { carrier := carrier, isClopen' := isClopen', upper' := upper' })
        ((fun (s : ClopenUpperSet α) ↦ s.carrier) t)),
    { carrier := carrier, isClopen' := isClopen', upper' := upper' : ClopenUpperSet α } = t
⊢ s = t

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := s
-- Module: Mathlib.Topology.Sets.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LE α
t : ClopenUpperSet α
carrier : Set α
isClopen' : IsClopen carrier
upper' : IsUpperSet { carrier := carrier, isClopen' := isClopen' : Clopens α }.carrier
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (s : ClopenUpperSet α) ↦ s.carrier) { carrier := carrier, isClopen' := isClopen', upper' := upper' })
    ((fun (s : ClopenUpperSet α) ↦ s.carrier) t)
obtain :
  ∀ (carrier_1 : Set α) (isClopen'_1 : IsClopen carrier_1)
    (upper'_1 : IsUpperSet { carrier := carrier_1, isClopen' := isClopen'_1 : Clopens α }.carrier)
    (h :
      Eq.{u_1 + 1} (α := Set α)
        ((fun (s : ClopenUpperSet α) ↦ s.carrier) { carrier := carrier, isClopen' := isClopen', upper' := upper' })
        ((fun (s : ClopenUpperSet α) ↦ s.carrier)
          { carrier := carrier_1, isClopen' := isClopen'_1, upper' := upper'_1 })),
    { carrier := carrier, isClopen' := isClopen', upper' := upper' : ClopenUpperSet α } =
      { carrier := carrier_1, isClopen' := isClopen'_1, upper' := upper'_1 }
⊢ { carrier := carrier, isClopen' := isClopen', upper' := upper' : ClopenUpperSet α } = t

Tactic:
obtain ⟨⟨_, _⟩, _⟩ := t
-- Module: Mathlib.Topology.Sets.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LE α
carrier : Set α
isClopen' : IsClopen carrier
upper' : IsUpperSet { carrier := carrier, isClopen' := isClopen' : Clopens α }.carrier
carrier_1 : Set α
isClopen'_1 : IsClopen carrier_1
upper'_1 : IsUpperSet { carrier := carrier_1, isClopen' := isClopen'_1 : Clopens α }.carrier
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (s : ClopenUpperSet α) ↦ s.carrier) { carrier := carrier, isClopen' := isClopen', upper' := upper' })
    ((fun (s : ClopenUpperSet α) ↦ s.carrier) { carrier := carrier_1, isClopen' := isClopen'_1, upper' := upper'_1 })
⊢ { carrier := carrier, isClopen' := isClopen', upper' := upper' : ClopenUpperSet α } =
    { carrier := carrier_1, isClopen' := isClopen'_1, upper' := upper'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Sets.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LE α
s : ClopenUpperSet α
⊢ IsUpperSet (↑s : Set α)

Tactic:
s.upper'

Premises used: ClopenUpperSet.upper'
-- Module: Mathlib.Topology.Sets.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LE α
s : ClopenUpperSet α
⊢ IsClopen (↑s : Set α)

Tactic:
s.isClopen'

Premises used: ClopenUpperSet.toClopens, TopologicalSpace.Clopens.isClopen'
-- Module: Mathlib.Topology.Sets.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LE α
s t : ClopenUpperSet α
h : (↑s : Set α) = (↑t : Set α)
⊢ s = t

Tactic:
SetLike.ext' h

Premises used: SetLike.ext'
-- Module: Mathlib.Topology.Sets.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LE α
s : Clopens α
h : IsUpperSet s.carrier
⊢ (↑{ toClopens := s, upper' := h : ClopenUpperSet α } : Set α) = (↑s : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LE α
s t : ClopenUpperSet α
⊢ (↑(s ⊔ t) : Set α) = (↑s : Set α) ∪ (↑t : Set α)

Tactic:
rfl

Premises used: Set.union, Set.Mem, setOf, rfl
-- Module: Mathlib.Topology.Sets.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LE α
s t : ClopenUpperSet α
⊢ (↑(s ⊓ t) : Set α) = (↑s : Set α) ∩ (↑t : Set α)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, rfl
-- Module: Mathlib.Topology.Sets.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LE α
⊢ (↑⊤ : Set α) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Topology.Sets.Order
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : LE α
⊢ (↑⊥ : Set α) = ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
U : Set α
h : IsOpen[inst] U
⊢ IsOpen[TopologicalSpace.vietoris α] (𝒫 U)

Tactic:
isOpen_generateFrom_of_mem <| .inl ⟨U, h, rfl⟩

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem, And.intro, Exists.intro, Or.inl, rfl
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
U : Set α
h : IsOpen[inst] U
⊢ IsOpen[TopologicalSpace.vietoris α] {s : Set α | (s ∩ U).Nonempty}

Tactic:
isOpen_generateFrom_of_mem <| .inr ⟨U, h, rfl⟩

Premises used: TopologicalSpace.isOpen_generateFrom_of_mem, And.intro, Exists.intro, Or.inr, rfl
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
simp_rw : IsOpen[TopologicalSpace.vietoris α] {a : Set α | (a ∩ Fᶜ).Nonempty}
⊢ IsClosed[TopologicalSpace.vietoris α] (𝒫 F)

Tactic:
simp_rw [powerset, ← isOpen_compl_iff, compl_setOf, ← inter_compl_nonempty_iff]

Premises used: Set.powerset, Set.inter_compl_nonempty_iff, isOpen_compl_iff, Set.compl_setOf
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
⊢ IsOpen[TopologicalSpace.vietoris α] {a : Set α | (a ∩ Fᶜ).Nonempty}

Tactic:
isOpen_inter_nonempty_of_isOpen h.isOpen_compl

Premises used: IsClosed.isOpen_compl, TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
⊢ IsOpen[TopologicalSpace.vietoris α] {a : Set α | (a ∩ Fᶜ).Nonempty}

Tactic:
exact isOpen_inter_nonempty_of_isOpen h.isOpen_compl

Premises used: IsClosed.isOpen_compl, TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
simp_rw : IsClosed[TopologicalSpace.vietoris α] {a : Set α | a ⊆ Fᶜ}ᶜ
⊢ IsClosed[TopologicalSpace.vietoris α] {s : Set α | (s ∩ F).Nonempty}

Tactic:
simp_rw +singlePass [← compl_compl F, inter_compl_nonempty_iff, ← compl_setOf]

Premises used: compl_compl, Set.inter_compl_nonempty_iff, Set.compl_setOf
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
⊢ IsClosed[TopologicalSpace.vietoris α] {a : Set α | a ⊆ Fᶜ}ᶜ

Tactic:
h.isOpen_compl.powerset_vietoris.isClosed_compl

Premises used: IsClosed.isOpen_compl, Set.Mem, setOf, Set.powerset, IsOpen.isClosed_compl, IsOpen.powerset_vietoris
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
F : Set α
h : IsClosed[inst] F
⊢ IsClosed[TopologicalSpace.vietoris α] {a : Set α | a ⊆ Fᶜ}ᶜ

Tactic:
exact h.isOpen_compl.powerset_vietoris.isClosed_compl

Premises used: IsClosed.isOpen_compl, IsOpen.isClosed_compl, IsOpen.powerset_vietoris
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
rw : IsClopen.{u_1} (X := Set α) (𝒫 ∅)
⊢ IsClopen (X := Set α) {∅}

Tactic:
rw [← powerset_empty]

Premises used: Set.powerset_empty
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsClopen.{u_1} (X := Set α) (𝒫 ∅)

Tactic:
⟨isClosed_empty.powerset_vietoris, isOpen_empty.powerset_vietoris⟩

Premises used: isClosed_empty, IsOpen.powerset_vietoris, And.intro, IsClosed.powerset_vietoris, IsClopen, isOpen_empty
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsClopen.{u_1} (X := Set α) (𝒫 ∅)

Tactic:
exact ⟨isClosed_empty.powerset_vietoris, isOpen_empty.powerset_vietoris⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
⊢ IsTopologicalBasis.{u_1} (α := Set α)
    ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
      {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})

Tactic:
isTopologicalBasis_of_subbasis rfl |>.isTopologicalBasis_of_exists_subset ?_ ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_subbasis, rfl, TopologicalSpace.IsTopologicalBasis.isTopologicalBasis_of_exists_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
refine_1 :
  ∀ (u : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
        u →
      IsOpen[generateFrom
            (powerset '' {U : Set α | IsOpen[inst] U} ∪
              (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
        u
refine_2 :
  ∀ (u : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (f : Set (Set (Set α))) ↦ ⋂₀ f) ''
          {f : Set (Set (Set α)) |
            f.Finite ∧
              f ⊆
                powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}})
        u →
      ∀ x ∈ u,
        ∃ (v : Set (Set α)),
          Membership.mem (γ := Set (Set (Set α)))
              ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
              v ∧
            x ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis.{u_1} (α := Set α)
    ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
      {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})

Tactic:
refine isTopologicalBasis_of_subbasis rfl |>.isTopologicalBasis_of_exists_subset ?_ ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_subbasis, rfl, TopologicalSpace.IsTopologicalBasis.isTopologicalBasis_of_exists_subset
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
refine_1 :
  ∀ ⦃x : Set (Set α)⦄,
    Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} x →
      IsOpen[generateFrom
            (powerset '' {U : Set α | IsOpen[inst] U} ∪
              (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
        {s : Set α | s ⊆ ⋃₀ x ∧ ∀ U ∈ x, (s ∩ U).Nonempty}
⊢ ∀ (u : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
          {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
        u →
      IsOpen[generateFrom
            (powerset '' {U : Set α | IsOpen[inst] U} ∪
              (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
        u

Tactic:
rw [forall_mem_image]

Premises used: Set.forall_mem_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
refine_2 :
  ∀ ⦃x : Set (Set (Set α))⦄,
    Membership.mem (γ := Set (Set (Set (Set α))))
        {f : Set (Set (Set α)) |
          f.Finite ∧
            f ⊆
              powerset '' {U : Set α | IsOpen[inst] U} ∪
                (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}}
        x →
      ∀ x_1 ∈ ⋂₀ x,
        ∃ (v : Set (Set α)),
          Membership.mem (γ := Set (Set (Set α)))
              ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
              v ∧
            x_1 ∈ v ∧ v ⊆ ⋂₀ x
⊢ ∀ (u : Set (Set α)),
    Membership.mem (γ := Set (Set (Set α)))
        ((fun (f : Set (Set (Set α))) ↦ ⋂₀ f) ''
          {f : Set (Set (Set α)) |
            f.Finite ∧
              f ⊆
                powerset '' {U : Set α | IsOpen[inst] U} ∪
                  (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}})
        u →
      ∀ x ∈ u,
        ∃ (v : Set (Set α)),
          Membership.mem (γ := Set (Set (Set α)))
              ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
                {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
              v ∧
            x ∈ v ∧ v ⊆ u

Tactic:
rw [forall_mem_image]

Premises used: Set.forall_mem_image
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
u : Set (Set α)
refine_1 :
  ∀ (hu₁ : u.Finite) (hu₂ : ∀ U ∈ u, IsOpen[inst] U),
    IsOpen[generateFrom
          (powerset '' {U : Set α | IsOpen[inst] U} ∪
            (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
      {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}
⊢ Membership.mem (γ := Set (Set (Set α))) {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U} u →
    IsOpen[generateFrom
          (powerset '' {U : Set α | IsOpen[inst] U} ∪
            (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
      {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
⟨hu₁, hu₂⟩
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
refine_1 :
  IsOpen[generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
    ({a : Set α | a ⊆ ⋃₀ u} ∩ ⋂ i ∈ u, {x : Set α | (x ∩ i).Nonempty})
⊢ IsOpen[generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
    {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}

Tactic:
simp_rw [setOf_and, setOf_forall]

Premises used: Set.setOf_and, Set.setOf_forall
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
⊢ IsOpen[generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
    ({a : Set α | a ⊆ ⋃₀ u} ∩ ⋂ i ∈ u, {x : Set α | (x ∩ i).Nonempty})

Tactic:
(isOpen_sUnion hu₂).powerset_vietoris.inter <|
      hu₁.isOpen_biInter fun U hU => isOpen_inter_nonempty_of_isOpen (hu₂ U hU)

Premises used: Set.powerset, TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen, IsOpen.powerset_vietoris, IsOpen.inter, Set.Finite.isOpen_biInter, isOpen_sUnion
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
u : Set (Set α)
hu₁ : u.Finite
hu₂ : ∀ U ∈ u, IsOpen[inst] U
⊢ IsOpen[generateFrom
        (powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V})]
    ({a : Set α | a ⊆ ⋃₀ u} ∩ ⋂ i ∈ u, {x : Set α | (x ∩ i).Nonempty})

Tactic:
exact (isOpen_sUnion hu₂).powerset_vietoris.inter <|
      hu₁.isOpen_biInter fun U hU => isOpen_inter_nonempty_of_isOpen (hu₂ U hU)

Premises used: TopologicalSpace.vietoris.isOpen_inter_nonempty_of_isOpen, IsOpen.powerset_vietoris, IsOpen.inter, Set.Finite.isOpen_biInter, isOpen_sUnion
-- Module: Mathlib.Topology.Sets.VietorisTopology
Goal:
α : Type u_1
inst : TopologicalSpace α
t : Set (Set (Set α))
refine_2 :
  ∀ (ht₁ : t.Finite)
    (ht₂ :
      t ⊆
        powerset '' {U : Set α | IsOpen[inst] U} ∪
          (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}),
    ∀ x ∈ ⋂₀ t,
      ∃ (v : Set (Set α)),
        Membership.mem (γ := Set (Set (Set α)))
            ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
              {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
            v ∧
          x ∈ v ∧ v ⊆ ⋂₀ t
⊢ Membership.mem (γ := Set (Set (Set (Set α))))
      {f : Set (Set (Set α)) |
        f.Finite ∧
          f ⊆
            powerset '' {U : Set α | IsOpen[inst] U} ∪
              (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {V : Set α | IsOpen[inst] V}}
      t →
    ∀ x ∈ ⋂₀ t,
      ∃ (v : Set (Set α)),
        Membership.mem (γ := Set (Set (Set α)))
            ((fun (u : Set (Set α)) ↦ {s : Set α | s ⊆ ⋃₀ u ∧ ∀ U ∈ u, (s ∩ U).Nonempty}) ''
              {u : Set (Set α) | u.Finite ∧ ∀ U ∈ u, IsOpen[inst] U})
            v ∧
          x ∈ v ∧ v ⊆ ⋂₀ t

Tactic:
⟨ht₁, ht₂⟩