awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x_1 : X
hx : x_1 ∈ s
i : ι
hi : x_1 ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ (↑(U j) : Set X)
hji : j ≠ i
x : X
hx₁ : x ∈ (↑(U i) : Set X)
hx₂ : x ∈ uᶜ
⊢ False

Tactic:
hx₂ <| hUu hx₁
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible (↑(U i) : Set X)
s : Set X
hs : IsOpen[inst] s
hsU : s ⊆ ⋃ (i : ι), (↑(U i) : Set X)
x_1 : X
hx : x_1 ∈ s
i : ι
hi : x_1 ∈ (↑(U i) : Set X)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ (↑(U j) : Set X)
hji : j ≠ i
x : X
hx₁ : x ∈ (↑(U i) : Set X)
hx₂ : x ∈ uᶜ
⊢ False

Tactic:
exact hx₂ <| hUu hx₁
-- Module: Mathlib.Topology.Sets.OpenCover
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun (x1 x2 : Opens X) ↦ ¬Disjoint x1 x2) on U)
hU : IsOpenCover U
h : ∀ (i : ι), PreirreducibleSpace.{u_1} ↥(U i)
h' : ∀ (i : ι), IsPreirreducible (U i).carrier
⊢ Subset.{u_1} (α := Set X) univ (⋃ (i : ι), (↑(U i) : Set X))

Tactic:
simpa using hU.iSup_set_eq_univ

Premises used: TopologicalSpace.IsOpenCover.iSup_set_eq_univ
-- 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 x_1 : Opens α
carrier : Set α
is_open' : IsOpen[inst] carrier
carrier_1 : Set α
is_open'_1 : IsOpen[inst] carrier_1
h :
  { carrier := carrier, is_open' := is_open' : Opens α }.carrier =
    { carrier := carrier_1, is_open' := is_open'_1 : Opens α }.carrier
⊢ { carrier := carrier, is_open' := is_open' : Opens α } = { carrier := carrier_1, is_open' := is_open'_1 }

Tactic:
congr
-- 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 γ
⊢ CanLift (Set α) (Opens α) SetLike.coe IsOpen[inst]

Tactic:
⟨fun s h => ⟨⟨s, h⟩, rfl⟩⟩

Premises used: TopologicalSpace.Opens.mk, Exists.intro, CanLift.mk, 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 : SecondCountableTopology α
U : Opens α
⊢ SecondCountableTopology.{u_2} ↥U

Tactic:
inferInstanceAs (SecondCountableTopology U.1)

Premises used: _private.0.TopologicalSpace.Opens.instSecondCountableOpens._proof_1
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
p : Opens α → Prop
⊢ (∀ (U : Opens α), p U) ↔ ∀ (U : Set α) (hU : IsOpen[inst] U), p { carrier := U, is_open' := hU }

Tactic:
⟨fun h _ _ => h _, fun h _ => h _ _⟩

Premises used: TopologicalSpace.Opens.carrier, TopologicalSpace.Opens.mk, Iff.intro, TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
⊢ U.carrier = (↑U : Set α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Set α
hU : IsOpen[inst] U
⊢ (↑{ carrier := U, is_open' := hU : Opens α } : Set α) = U

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
x : α
U : Set α
h : IsOpen[inst] U
⊢ x ∈ { carrier := U, is_open' := h : Opens α } ↔ x ∈ U

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
⊢ Nonempty.{u_2 + 1} ↥U ↔ (↑U : Set α).Nonempty

Tactic:
Set.nonempty_coe_sort

Premises used: Set.nonempty_coe_sort
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
⊢ (↑U : Set α).Nonempty ↔ ∃ (x : α), x ∈ U

Tactic:
Iff.rfl

Premises used: Iff.rfl, Set.Nonempty
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U V : Opens α
h : (↑U : Set α) = (↑V : Set α)
⊢ U = V

Tactic:
SetLike.coe_injective h

Premises used: SetLike.coe_injective
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U V : Opens α
⊢ (↑U : Set α) = (↑V : Set α) ↔ U = V

Tactic:
SetLike.ext'_iff.symm

Premises used: SetLike.ext'_iff, Iff.symm
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
⊢ IsOpen[inst] (↑U : Set α)

Tactic:
U.is_open'

Premises used: TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
⊢ { carrier := (↑U : Set α), is_open' := ⋯ : Opens α } = U

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s : Set α
x : α
⊢ Membership.mem (γ := Opens α) (Opens.interior s) x ↔ x ∈ interior s

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.sUnion, interior
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ GaloisConnection (α := Opens α) SetLike.coe Opens.interior

Tactic:
fun U _ =>
  ⟨fun h => interior_maximal h U.isOpen, fun h => le_trans h interior_subset⟩

Premises used: interior_subset, interior_maximal, TopologicalSpace.Opens.isOpen, Iff.intro, le_trans, GaloisConnection
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U V : Set α
hU : IsOpen[inst] U
hV : IsOpen[inst] V
⊢ { carrier := U, is_open' := hU : Opens α } ⊓ { carrier := V, is_open' := hV : Opens α } =
    { carrier := U ⊓ V, is_open' := ⋯ }

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : Opens α
⊢ (↑(s ⊓ t) : Set α) = (↑s : Set α) ∩ (↑t : Set α)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : Opens α
x : α
⊢ x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : Opens α
⊢ (↑(s ⊔ t) : Set α) = (↑s : Set α) ∪ (↑t : Set α)

Tactic:
rfl

Premises used: Set.union, setOf, rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : Opens α
x : α
⊢ x ∈ s ⊔ t ↔ x ∈ s ∨ x ∈ t

Tactic:
.rfl

Premises used: Set.union, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ (↑⊥ : Set α) = ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
x : α
⊢ Membership.mem (γ := Opens α) ⊥ x ↔ False

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ Eq.{u_2 + 1} (α := Opens α) { carrier := ∅, is_open' := ⋯ } ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
⊢ (↑U : Set α) = ∅ ↔ U = ⊥

Tactic:
SetLike.coe_injective.eq_iff' rfl

Premises used: Function.Injective.eq_iff', SetLike.coe_injective, rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
x : α
⊢ Membership.mem (γ := Opens α) ⊤ x

Tactic:
trivial

Premises used: trivial, Set.Mem, Set.univ, setOf
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ (↑⊤ : Set α) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
⊢ Eq.{u_2 + 1} (α := Opens α) { carrier := univ, is_open' := ⋯ } ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
⊢ (↑U : Set α) = univ ↔ U = ⊤

Tactic:
SetLike.coe_injective.eq_iff' rfl

Premises used: Function.Injective.eq_iff', SetLike.coe_injective, rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
S : Set (Opens α)
⊢ (↑(sSup S) : Set α) = ⋃ i ∈ S, (↑i : Set α)

Tactic:
rfl

Premises used: iSup, setOf, Set.iUnion, rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
ι : Type u_1
α : Type u_2
inst : TopologicalSpace α
f : ι → Opens α
s : Finset ι
⊢ (↑(s.sup f) : Set α) = s.sup (SetLike.coe ∘ f)

Tactic:
map_finset_sup (⟨⟨(↑), coe_sup⟩, coe_bot⟩ : SupBotHom (Opens α) (Set α)) _ _

Premises used: SetLike.coe, TopologicalSpace.Opens.coe_bot, TopologicalSpace.Opens.coe_sup, SupHom.mk, map_finset_sup, SupBotHom.mk
-- Module: Mathlib.Topology.Sets.Opens
Goal:
ι : Type u_1
α : Type u_2
inst : TopologicalSpace α
f : ι → Opens α
s : Finset ι
⊢ (↑(s.inf f) : Set α) = s.inf (SetLike.coe ∘ f)

Tactic:
map_finset_inf (⟨⟨(↑), coe_inf⟩, coe_top⟩ : InfTopHom (Opens α) (Set α)) _ _

Premises used: map_finset_inf, InfTopHom.mk, SetLike.coe, InfHom.mk, TopologicalSpace.Opens.coe_inf, TopologicalSpace.Opens.coe_top
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
s t : Opens α
⊢ Disjoint (↑s : Set α) (↑t : Set α) ↔ Disjoint s t

Tactic:
simp [disjoint_iff, ← SetLike.coe_set_eq]

Premises used: disjoint_iff, SetLike.coe_set_eq
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Sort u_5
s : ι → Opens α
⊢ (↑(⨆ (i : ι), s i) : Set α) = ⋃ (i : ι), (↑(s i) : Set α)

Tactic:
simp [iSup]

Premises used: iSup
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Sort u_5
s : ι → Opens α
⊢ Eq.{u_2 + 1} (α := Opens α) (⨆ (i : ι), s i) { carrier := ⋃ (i : ι), (↑(s i) : Set α), is_open' := ⋯ }

Tactic:
ext <| coe_iSup s

Premises used: TopologicalSpace.Opens.coe_iSup, TopologicalSpace.Opens.ext
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Sort u_5
s : ι → Set α
h : ∀ (i : ι), IsOpen[inst] (s i)
⊢ ⨆ (i : ι), { carrier := s i, is_open' := ⋯ } = { carrier := ⋃ (i : ι), s i, is_open' := ⋯ : Opens α }

Tactic:
iSup_def _

Premises used: TopologicalSpace.Opens.iSup_def
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
ι : Sort u_5
x : α
s : ι → Opens α
⊢ x ∈ (↑(iSup s) : Set α) ↔ ∃ (i : ι), x ∈ s i

Tactic:
simp
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
Us : Set (Opens α)
x : α
simp_rw : Membership.mem (γ := Opens α) (⨆ a ∈ Us, a) x ↔ ∃ u ∈ Us, x ∈ u
simp_rw₁ : (∃ (i : Opens α) (_ : i ∈ Us), x ∈ i) ↔ ∃ u ∈ Us, x ∈ u
⊢ x ∈ sSup Us ↔ ∃ u ∈ Us, x ∈ u

Tactic:
simp_rw [sSup_eq_iSup, mem_iSup, exists_prop]

Premises used: exists_prop, TopologicalSpace.Opens.mem_iSup, sSup_eq_iSup
-- 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 γ
a : Opens α
s : Set (Opens α)
⊢ (↑(a ⊓ sSup s) : Set α) = (↑(⨆ b ∈ s, a ⊓ b) : Set α)

Tactic:
simp only [coe_inf, coe_iSup, coe_sSup, Set.inter_iUnion₂]

Premises used: TopologicalSpace.Opens.coe_iSup, Set.inter_iUnion₂, TopologicalSpace.Opens.coe_sSup, TopologicalSpace.Opens.coe_inf
-- 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 : Set (Opens α)
⊢ (↑(sSup x) : Set α) = sSup ((fun (x : Opens α) ↦ (↑x : Set α)) '' x)

Tactic:
simp
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
⊢ IsOpenEmbedding.{u_2, u_2} (X := ↥U) (Subtype.val (p := fun (x : α) ↦ x ∈ U))

Tactic:
U.isOpen.isOpenEmbedding_subtypeVal

Premises used: IsOpen.isOpenEmbedding_subtypeVal, TopologicalSpace.Opens.isOpen
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U V : Opens α
i : U ≤ V
rw : IsOpen[instTopologicalSpaceSubtype] {x : (↑(↑V : Set α) : Type u_2) | (↑x : α) ∈ (↑U : Set α)}
⊢ IsOpen[instTopologicalSpaceSubtype] (range (Set.inclusion (s := (↑U : Set α)) (t := (↑V : Set α)) ⋯))

Tactic:
rw [Set.range_inclusion i]

Premises used: Set.range_inclusion
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U V : Opens α
i : U ≤ V
⊢ IsOpen[instTopologicalSpaceSubtype] {x : (↑(↑V : Set α) : Type u_2) | (↑x : α) ∈ (↑U : Set α)}

Tactic:
U.isOpen.preimage continuous_subtype_val

Premises used: continuous_subtype_val, setOf, TopologicalSpace.Opens.isOpen, Set.preimage, IsOpen.preimage
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U V : Opens α
i : U ≤ V
⊢ IsOpen[instTopologicalSpaceSubtype] {x : (↑(↑V : Set α) : Type u_2) | (↑x : α) ∈ (↑U : Set α)}

Tactic:
exact U.isOpen.preimage continuous_subtype_val

Premises used: continuous_subtype_val, TopologicalSpace.Opens.isOpen, IsOpen.preimage
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
rw : ¬(↑U : Set α).Nonempty ↔ (↑U : Set α) = (↑⊥ : Set α)
rw₁ : ¬(↑U : Set α).Nonempty ↔ (↑U : Set α) = ∅
rw₂ rw₃ : ¬(↑U : Set α).Nonempty ↔ ¬(↑U : Set α).Nonempty
⊢ ¬(↑U : Set α).Nonempty ↔ U = ⊥

Tactic:
rw [← coe_inj, coe_bot, ← Set.not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty, TopologicalSpace.Opens.coe_bot, TopologicalSpace.Opens.coe_inj
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
U : Opens α
rw : ¬U = ⊥ ↔ (↑U : Set α).Nonempty
rw₁ : ¬¬(↑U : Set α).Nonempty ↔ (↑U : Set α).Nonempty
rw₂ rw₃ : (↑U : Set α).Nonempty ↔ (↑U : Set α).Nonempty
⊢ U ≠ ⊥ ↔ (↑U : Set α).Nonempty

Tactic:
rw [Ne, ← not_nonempty_iff_eq_bot, not_not]

Premises used: Classical.not_not, Ne, TopologicalSpace.Opens.not_nonempty_iff_eq_bot
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : IndiscreteTopology α
U : Opens α
rw : IsOpen[inst] (↑U : Set α)
⊢ U = ⊥ ∨ U = ⊤

Tactic:
rw [← coe_eq_empty, ← coe_eq_univ, ← IndiscreteTopology.isOpen_iff]

Premises used: IndiscreteTopology.isOpen_iff, TopologicalSpace.Opens.coe_eq_empty, TopologicalSpace.Opens.coe_eq_univ
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : IndiscreteTopology α
U : Opens α
⊢ IsOpen[inst] (↑U : Set α)

Tactic:
U.2

Premises used: TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
inst_1 : IndiscreteTopology α
U : Opens α
⊢ IsOpen[inst] (↑U : Set α)

Tactic:
exact U.2

Premises used: TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
mp : IsBasis B → ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
mpr : (∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U) → IsBasis B
⊢ IsBasis B ↔ ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

Tactic:
constructor
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU : Opens α }
mp :
  ∀ (sV : Set α) (hsV : x ∈ sV ∧ sV ⊆ sU) (V : Opens α) (H₁ : V ∈ B) (H₂ : (↑V : Set α) = sV),
    ∃ U' ∈ B, x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }

Tactic:
rcases h.mem_nhds_iff.mp (IsOpen.mem_nhds hU hx) with ⟨sV, ⟨⟨V, H₁, H₂⟩, hsV⟩⟩

Premises used: IsOpen.mem_nhds, Iff.mp, TopologicalSpace.IsTopologicalBasis.mem_nhds_iff
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU : Opens α }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : (↑V : Set α) = sV
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }

Tactic:
⟨V, H₁, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU : Opens α }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : (↑V : Set α) = sV
mp : x ∈ V ∧ V ≤ { carrier := sU, is_open' := hU }
⊢ ∃ U' ∈ B, x ∈ U' ∧ U' ≤ { carrier := sU, is_open' := hU }

Tactic:
refine ⟨V, H₁, ?_⟩
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU : Opens α }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
V : Opens α
H₁ : V ∈ B
H₂ : (↑V : Set α) = sV
mp :
  ∀ (carrier : Set α) (is_open' : IsOpen[inst] carrier)
    (H₁ : { carrier := carrier, is_open' := is_open' : Opens α } ∈ B)
    (H₂ : (↑{ carrier := carrier, is_open' := is_open' : Opens α } : Set α) = sV),
    x ∈ { carrier := carrier, is_open' := is_open' : Opens α } ∧
      { carrier := carrier, is_open' := is_open' : Opens α } ≤ { carrier := sU, is_open' := hU }
⊢ x ∈ V ∧ V ≤ { carrier := sU, is_open' := hU }

Tactic:
cases V
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU : Opens α }
sV : Set α
hsV : x ∈ sV ∧ sV ⊆ sU
carrier : Set α
is_open' : IsOpen[inst] carrier
H₁ : { carrier := carrier, is_open' := is_open' : Opens α } ∈ B
H₂ : carrier = sV
⊢ x ∈ carrier ∧ carrier ⊆ sU

Tactic:
subst H₂
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU : Opens α }
carrier : Set α
is_open' : IsOpen[inst] carrier
H₁ : { carrier := carrier, is_open' := is_open' : Opens α } ∈ B
hsV : x ∈ carrier ∧ carrier ⊆ sU
⊢ x ∈ { carrier := carrier, is_open' := is_open' : Opens α } ∧
    { carrier := carrier, is_open' := is_open' : Opens α } ≤ { carrier := sU, is_open' := hU }

Tactic:
hsV

Premises used: Set.Mem, Set.Subset
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : IsBasis B
sU : Set α
hU : IsOpen[inst] sU
x : α
hx : x ∈ { carrier := sU, is_open' := hU : Opens α }
carrier : Set α
is_open' : IsOpen[inst] carrier
H₁ : { carrier := carrier, is_open' := is_open' : Opens α } ∈ B
hsV : x ∈ carrier ∧ carrier ⊆ sU
⊢ x ∈ { carrier := carrier, is_open' := is_open' : Opens α } ∧
    { carrier := carrier, is_open' := is_open' : Opens α } ≤ { carrier := sU, is_open' := hU }

Tactic:
exact hsV
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
⊢ IsBasis B

Tactic:
isTopologicalBasis_of_isOpen_of_nhds ?_ ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds, TopologicalSpace.Opens.IsBasis
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
mpr : ∀ u ∈ SetLike.coe '' B, IsOpen[inst] u
mpr₁ : ∀ (a : α) (u : Set α), a ∈ u → IsOpen[inst] u → ∃ v ∈ SetLike.coe '' B, a ∈ v ∧ v ⊆ u
⊢ IsBasis B

Tactic:
refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
U : Opens α
⊢ IsOpen[inst] (↑U : Set α)

Tactic:
U.2

Premises used: TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
U : Opens α
⊢ IsOpen[inst] (↑U : Set α)

Tactic:
exact U.2

Premises used: TopologicalSpace.Opens.is_open'
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen[inst] sU
mpr :
  ∀ (V : Opens α) (hV : V ∈ B) (H : x ∈ V ∧ V ≤ { carrier := sU, is_open' := hsU }),
    ∃ v ∈ SetLike.coe '' B, x ∈ v ∧ v ⊆ sU
⊢ ∃ v ∈ SetLike.coe '' B, x ∈ v ∧ v ⊆ sU

Tactic:
rcases @h ⟨sU, hsU⟩ x hx with ⟨V, hV, H⟩
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen[inst] sU
V : Opens α
hV : V ∈ B
H : x ∈ V ∧ V ≤ { carrier := sU, is_open' := hsU }
⊢ ∃ v ∈ SetLike.coe '' B, x ∈ v ∧ v ⊆ sU

Tactic:
⟨V, ⟨V, hV, rfl⟩, H⟩

Premises used: SetLike.coe, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
x : α
sU : Set α
hx : x ∈ sU
hsU : IsOpen[inst] sU
V : Opens α
hV : V ∈ B
H : x ∈ V ∧ V ≤ { carrier := sU, is_open' := hsU }
⊢ ∃ v ∈ SetLike.coe '' B, x ∈ v ∧ v ⊆ sU

Tactic:
exact ⟨V, ⟨V, hV, rfl⟩, H⟩
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
mp : IsBasis B → ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
mpr : (∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us) → IsBasis B
⊢ IsBasis B ↔ ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us

Tactic:
constructor
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ ∃ Us ⊆ B, U = sSup Us

Tactic:
⟨{ V : Opens α | V ∈ B ∧ V ≤ U }, fun U hU => hU.left, ext ?_⟩

Premises used: setOf, Membership.mem, TopologicalSpace.Opens.ext, LE.le, And, And.left, And.intro, Exists.intro
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
mp : (↑U : Set α) = (↑(sSup {V : Opens α | V ∈ B ∧ V ≤ U}) : Set α)
⊢ ∃ Us ⊆ B, U = sSup Us

Tactic:
refine ⟨{ V : Opens α | V ∈ B ∧ V ≤ U }, fun U hU => hU.left, ext ?_⟩
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
mp :
  Eq.{u_2 + 1} (α := Set α) (⋃₀ {s : Set α | s ∈ SetLike.coe '' B ∧ s ⊆ (↑U : Set α)})
    (⋃ (i : Opens α), ⋃ (_ : Membership.mem (γ := Set (Opens α)) {V : Opens α | V ∈ B ∧ V ≤ U} i), (↑i : Set α))
⊢ (↑U : Set α) = (↑(sSup {V : Opens α | V ∈ B ∧ V ≤ U}) : Set α)

Tactic:
rw [coe_sSup, hB.open_eq_sUnion' U.isOpen]

Premises used: TopologicalSpace.Opens.isOpen, TopologicalSpace.Opens.coe_sSup, TopologicalSpace.IsTopologicalBasis.open_eq_sUnion'
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
mp :
  Eq.{u_2 + 1} (α := Set α) (⨆ b ∈ B, ⨆ (_ : (↑b : Set α) ⊆ (↑U : Set α)), (↑b : Set α))
    (⨆ i ∈ B, ⨆ (_ : i ≤ U), (↑i : Set α))
⊢ Eq.{u_2 + 1} (α := Set α) (⋃₀ {s : Set α | s ∈ SetLike.coe '' B ∧ s ⊆ (↑U : Set α)})
    (⋃ (i : Opens α), ⋃ (_ : Membership.mem (γ := Set (Opens α)) {V : Opens α | V ∈ B ∧ V ≤ U} i), (↑i : Set α))

Tactic:
simp_rw [sUnion_eq_biUnion, iUnion, mem_setOf_eq, iSup_and, iSup_image]

Premises used: iSup_image, Set.mem_setOf_eq, Set.sUnion_eq_biUnion, Set.iUnion, iSup_and
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
hB : IsBasis B
U : Opens α
⊢ Eq.{u_2 + 1} (α := Set α) (⨆ b ∈ B, ⨆ (_ : (↑b : Set α) ⊆ (↑U : Set α)), (↑b : Set α))
    (⨆ i ∈ B, ⨆ (_ : i ≤ U), (↑i : Set α))

Tactic:
rfl
-- Module: Mathlib.Topology.Sets.Opens
Goal:
α : Type u_2
inst : TopologicalSpace α
B : Set (Opens α)
h : ∀ (U : Opens α), ∃ Us ⊆ B, U = sSup Us
mpr : ∀ {U : Opens α} {x : α}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U
⊢ IsBasis B

Tactic:
rw [isBasis_iff_nbhd]

Premises used: TopologicalSpace.Opens.isBasis_iff_nbhd