awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
h_open :
  ∀ (u : Set (α ⊕ β)),
    Membership.mem (γ := Set (Set (α ⊕ β)))
        ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) u →
      IsOpen[instTopologicalSpaceSum] u
h_nhds :
  ∀ (a : α ⊕ β) (u : Set (α ⊕ β)),
    a ∈ u →
      IsOpen[instTopologicalSpaceSum] u →
        ∃ (v : Set (α ⊕ β)),
          Membership.mem (γ := Set (Set (α ⊕ β)))
              ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) v ∧
            a ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis (α := α ⊕ β) ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t)

Tactic:
apply isTopologicalBasis_of_isOpen_of_nhds

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set α
hw : w ∈ s
⊢ IsOpen[instTopologicalSpaceSum] ((fun (u : Set α) ↦ (Sum.inl '' u : Set (α ⊕ β))) w)

Tactic:
IsOpenEmbedding.inl.isOpenMap w (hs.isOpen hw)

Premises used: Topology.IsOpenEmbedding.isOpenMap, TopologicalSpace.IsTopologicalBasis.isOpen, Topology.IsOpenEmbedding.inl
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set α
hw : w ∈ s
⊢ IsOpen[instTopologicalSpaceSum] ((fun (u : Set α) ↦ (Sum.inl '' u : Set (α ⊕ β))) w)

Tactic:
exact IsOpenEmbedding.inl.isOpenMap w (hs.isOpen hw)

Premises used: Topology.IsOpenEmbedding.isOpenMap, TopologicalSpace.IsTopologicalBasis.isOpen, Topology.IsOpenEmbedding.inl
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set β
hw : w ∈ t
⊢ IsOpen[instTopologicalSpaceSum] ((fun (u : Set β) ↦ (Sum.inr '' u : Set (α ⊕ β))) w)

Tactic:
IsOpenEmbedding.inr.isOpenMap w (ht.isOpen hw)

Premises used: Topology.IsOpenEmbedding.isOpenMap, TopologicalSpace.IsTopologicalBasis.isOpen, Topology.IsOpenEmbedding.inr
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
w : Set β
hw : w ∈ t
⊢ IsOpen[instTopologicalSpaceSum] ((fun (u : Set β) ↦ (Sum.inr '' u : Set (α ⊕ β))) w)

Tactic:
exact IsOpenEmbedding.inr.isOpenMap w (ht.isOpen hw)

Premises used: Topology.IsOpenEmbedding.isOpenMap, TopologicalSpace.IsTopologicalBasis.isOpen, Topology.IsOpenEmbedding.inr
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
⊢ ∃ v ∈ s, x ∈ v ∧ v ⊆ Sum.inl ⁻¹' u

Tactic:
hs.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).1

Premises used: isOpen_sum_iff, And.left, Iff.mp, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
h_nhds :
  ∀ (v : Set α) (vs : v ∈ s) (xv : x ∈ v) (vu : v ⊆ Sum.inl ⁻¹' u),
    ∃ (v : Set (α ⊕ β)),
      Membership.mem (γ := Set (Set (α ⊕ β)))
          ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) v ∧
        Sum.inl x ∈ v ∧ v ⊆ u
⊢ ∃ (v : Set (α ⊕ β)),
    Membership.mem (γ := Set (Set (α ⊕ β)))
        ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) v ∧
      Sum.inl x ∈ v ∧ v ⊆ u

Tactic:
obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ s, x ∈ v ∧ v ⊆ Sum.inl ⁻¹' u :=
        hs.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).1

Premises used: isOpen_sum_iff, Sum.inl, And.left, Iff.mp, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
v : Set α
vs : v ∈ s
xv : x ∈ v
vu : v ⊆ Sum.inl ⁻¹' u
⊢ ∃ (v : Set (α ⊕ β)),
    Membership.mem (γ := Set (Set (α ⊕ β)))
        ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) v ∧
      Sum.inl x ∈ v ∧ v ⊆ u

Tactic:
⟨Sum.inl '' v, mem_union_left _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
        image_subset_iff.2 vu⟩

Premises used: Iff.mpr, Sum.inl, Set.mem_image_of_mem, And.intro, Exists.intro, Set.image, Set.mem_union_left, Set.image_subset_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
v : Set α
vs : v ∈ s
xv : x ∈ v
vu : v ⊆ Sum.inl ⁻¹' u
⊢ ∃ (v : Set (α ⊕ β)),
    Membership.mem (γ := Set (Set (α ⊕ β)))
        ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) v ∧
      Sum.inl x ∈ v ∧ v ⊆ u

Tactic:
exact ⟨Sum.inl '' v, mem_union_left _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
        image_subset_iff.2 vu⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
⊢ ∃ v ∈ t, x ∈ v ∧ v ⊆ Sum.inr ⁻¹' u

Tactic:
ht.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).2

Premises used: isOpen_sum_iff, And.right, Iff.mp, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
h_nhds :
  ∀ (v : Set β) (vs : v ∈ t) (xv : x ∈ v) (vu : v ⊆ Sum.inr ⁻¹' u),
    ∃ (v : Set (α ⊕ β)),
      Membership.mem (γ := Set (Set (α ⊕ β)))
          ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) v ∧
        Sum.inr x ∈ v ∧ v ⊆ u
⊢ ∃ (v : Set (α ⊕ β)),
    Membership.mem (γ := Set (Set (α ⊕ β)))
        ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) v ∧
      Sum.inr x ∈ v ∧ v ⊆ u

Tactic:
obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ t, x ∈ v ∧ v ⊆ Sum.inr ⁻¹' u :=
        ht.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).2

Premises used: isOpen_sum_iff, And.right, Sum.inr, Iff.mp, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
v : Set β
vs : v ∈ t
xv : x ∈ v
vu : v ⊆ Sum.inr ⁻¹' u
⊢ ∃ (v : Set (α ⊕ β)),
    Membership.mem (γ := Set (Set (α ⊕ β)))
        ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) v ∧
      Sum.inr x ∈ v ∧ v ⊆ u

Tactic:
⟨Sum.inr '' v, mem_union_right _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
        image_subset_iff.2 vu⟩

Premises used: Iff.mpr, Set.mem_union_right, Sum.inr, Set.mem_image_of_mem, And.intro, Exists.intro, Set.image, Set.image_subset_iff
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t_1 : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : β
u : Set (α ⊕ β)
hxu : Sum.inr x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
v : Set β
vs : v ∈ t
xv : x ∈ v
vu : v ⊆ Sum.inr ⁻¹' u
⊢ ∃ (v : Set (α ⊕ β)),
    Membership.mem (γ := Set (Set (α ⊕ β)))
        ((fun (u : Set α) ↦ Sum.inl '' u) '' s ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' t) v ∧
      Sum.inr x ∈ v ∧ v ⊆ u

Tactic:
exact ⟨Sum.inr '' v, mem_union_right _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
        image_subset_iff.2 vu⟩
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : SecondCountableTopology α
inst_2 : SecondCountableTopology β
b : Set (Set (α ⊕ β)) :=
  (fun (u : Set α) ↦ Sum.inl '' u) '' countableBasis α ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' countableBasis β
⊢ IsTopologicalBasis b

Tactic:
have A : IsTopologicalBasis b := (isBasis_countableBasis α).sum (isBasis_countableBasis β)
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : SecondCountableTopology α
inst_2 : SecondCountableTopology β
b : Set (Set (α ⊕ β)) :=
  (fun (u : Set α) ↦ Sum.inl '' u) '' countableBasis α ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' countableBasis β
A : IsTopologicalBasis b
⊢ b.Countable

Tactic:
have B : b.Countable :=
    (Countable.image (countable_countableBasis _) _).union
      (Countable.image (countable_countableBasis _) _)
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : SecondCountableTopology α
inst_2 : SecondCountableTopology β
b : Set (Set (α ⊕ β)) :=
  (fun (u : Set α) ↦ Sum.inl '' u) '' countableBasis α ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' countableBasis β
A : IsTopologicalBasis b
B : b.Countable
⊢ SecondCountableTopology (α ⊕ β)

Tactic:
A.secondCountableTopology B

Premises used: TopologicalSpace.IsTopologicalBasis.secondCountableTopology
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u
t : TopologicalSpace α
β : Type u_1
inst : TopologicalSpace β
inst_1 : SecondCountableTopology α
inst_2 : SecondCountableTopology β
b : Set (Set (α ⊕ β)) :=
  (fun (u : Set α) ↦ Sum.inl '' u) '' countableBasis α ∪ (fun (u : Set β) ↦ Sum.inr '' u) '' countableBasis β
A : IsTopologicalBasis b
B : b.Countable
⊢ SecondCountableTopology (α ⊕ β)

Tactic:
exact A.secondCountableTopology B

Premises used: TopologicalSpace.IsTopologicalBasis.secondCountableTopology
-- Module: Mathlib.Topology.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
h_open : ∀ u ∈ image π '' V, IsOpen[inst_1] u
h_nhds : ∀ (a : Y) (u : Set Y), a ∈ u → IsOpen[inst_1] u → ∃ v ∈ image π '' V, a ∈ v ∧ v ⊆ u
⊢ IsTopologicalBasis (image π '' V)

Tactic:
apply isTopologicalBasis_of_isOpen_of_nhds

Premises used: TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
-- Module: Mathlib.Topology.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set X
U_in_V : U ∈ V
⊢ IsOpen[inst_1] (π '' U)

Tactic:
apply h U (hV.isOpen U_in_V)

Premises used: TopologicalSpace.IsTopologicalBasis.isOpen
-- Module: Mathlib.Topology.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
y : Y
U : Set Y
y_in_U : y ∈ U
U_open : IsOpen[inst_1] U
h_nhds : ∀ (x : X) (y_in_U : π x ∈ U), ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U
⊢ ∃ v ∈ image π '' V, y ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨x, rfl⟩ := h'.surjective y

Premises used: Topology.IsQuotientMap.surjective, rfl
-- Module: Mathlib.Topology.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen[inst_1] U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
⊢ x ∈ W

Tactic:
have x_in_W : x ∈ W := y_in_U
-- Module: Mathlib.Topology.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen[inst_1] U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
⊢ IsOpen[inst] W

Tactic:
have W_open : IsOpen W := U_open.preimage h'.continuous
-- Module: Mathlib.Topology.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen[inst_1] U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen[inst] W
h_nhds : ∀ (Z : Set X) (Z_in_V : Z ∈ V) (x_in_Z : x ∈ Z) (Z_in_W : Z ⊆ W), ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Tactic:
obtain ⟨Z, Z_in_V, x_in_Z, Z_in_W⟩ := hV.exists_subset_of_mem_open x_in_W W_open

Premises used: TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.Topology.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen[inst_1] U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen[inst] W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
⊢ π '' Z ⊆ U

Tactic:
have XZ_in_U : π '' Z ⊆ U := (Set.image_mono Z_in_W).trans (image_preimage_subset π U)
-- Module: Mathlib.Topology.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen[inst_1] U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen[inst] W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
XZ_in_U : π '' Z ⊆ U
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Tactic:
⟨π '' Z, ⟨Z, Z_in_V, rfl⟩, ⟨x, x_in_Z, rfl⟩, XZ_in_U⟩

Premises used: And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Topology.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
V : Set (Set X)
hV : IsTopologicalBasis V
h' : IsQuotientMap π
h : IsOpenMap π
U : Set Y
U_open : IsOpen[inst_1] U
x : X
y_in_U : π x ∈ U
W : Set X := π ⁻¹' U
x_in_W : x ∈ W
W_open : IsOpen[inst] W
Z : Set X
Z_in_V : Z ∈ V
x_in_Z : x ∈ Z
Z_in_W : Z ⊆ W
XZ_in_U : π '' Z ⊆ U
⊢ ∃ v ∈ image π '' V, π x ∈ v ∧ v ⊆ U

Tactic:
exact ⟨π '' Z, ⟨Z, Z_in_V, rfl⟩, ⟨x, x_in_Z, rfl⟩, XZ_in_U⟩
-- Module: Mathlib.Topology.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
inst_2 : SecondCountableTopology X
h' : IsQuotientMap π
h : IsOpenMap π
obtain :
  ∀ (V : Set (Set X)) (V_countable : V.Countable) (V_generates : IsTopologicalBasis V),
    ∃ (b : Set (Set Y)), b.Countable ∧ inst_1 = generateFrom b
⊢ ∃ (b : Set (Set Y)), b.Countable ∧ inst_1 = generateFrom b

Tactic:
obtain ⟨V, V_countable, -, V_generates⟩ := exists_countable_basis X

Premises used: TopologicalSpace.exists_countable_basis
-- Module: Mathlib.Topology.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
inst_2 : SecondCountableTopology X
h' : IsQuotientMap π
h : IsOpenMap π
V : Set (Set X)
V_countable : V.Countable
V_generates : IsTopologicalBasis V
⊢ ∃ (b : Set (Set Y)), b.Countable ∧ inst_1 = generateFrom b

Tactic:
⟨Set.image π '' V, V_countable.image (Set.image π),
      (V_generates.isQuotientMap h' h).eq_generateFrom⟩

Premises used: TopologicalSpace.IsTopologicalBasis.isQuotientMap, Set.Countable.image, TopologicalSpace.IsTopologicalBasis.eq_generateFrom, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Topology.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
Y : Type u_2
inst_1 : TopologicalSpace Y
π : X → Y
inst_2 : SecondCountableTopology X
h' : IsQuotientMap π
h : IsOpenMap π
V : Set (Set X)
V_countable : V.Countable
V_generates : IsTopologicalBasis V
⊢ ∃ (b : Set (Set Y)), b.Countable ∧ inst_1 = generateFrom b

Tactic:
exact ⟨Set.image π '' V, V_countable.image (Set.image π),
      (V_generates.isQuotientMap h' h).eq_generateFrom⟩
-- Module: Mathlib.Topology.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Setoid X
V : Set (Set X)
hV : IsTopologicalBasis V
h : IsOpenMap.{u_1, u_1} (X := X) (Y := Quotient S) Quotient.mk'
⊢ IsTopologicalBasis (α := Quotient S) (image Quotient.mk' '' V)

Tactic:
hV.isQuotientMap isQuotientMap_quotient_mk' h

Premises used: isQuotientMap_quotient_mk', TopologicalSpace.IsTopologicalBasis.isQuotientMap
-- Module: Mathlib.Topology.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
S : Setoid X
inst_1 : SecondCountableTopology X
h : IsOpenMap.{u_1, u_1} (X := X) (Y := Quotient S) Quotient.mk'
⊢ SecondCountableTopology.{u_1} (Quotient S)

Tactic:
isQuotientMap_quotient_mk'.secondCountableTopology h

Premises used: isQuotientMap_quotient_mk', Topology.IsQuotientMap.secondCountableTopology
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : TopologicalSpace β
inst_2 : SecondCountableTopology β
hf : IsInducing f
rw : SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
rw [hf.1]

Premises used: Topology.IsInducing.eq_induced
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : TopologicalSpace β
inst_2 : SecondCountableTopology β
hf : IsInducing f
⊢ SecondCountableTopology α

Tactic:
secondCountableTopology_induced α β f

Premises used: TopologicalSpace.secondCountableTopology_induced
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : TopologicalSpace β
inst_2 : SecondCountableTopology β
hf : IsInducing f
⊢ SecondCountableTopology α

Tactic:
exact secondCountableTopology_induced α β f

Premises used: TopologicalSpace.secondCountableTopology_induced
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
f : α → β
inst_1 : TopologicalSpace β
inst_2 : SecondCountableTopology β
hf : IsEmbedding f
⊢ SecondCountableTopology α

Tactic:
hf.1.secondCountableTopology

Premises used: Topology.IsInducing.secondCountableTopology, Topology.IsEmbedding.toIsInducing
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SecondCountableTopology β
f : α → β
hf : IsEmbedding f
⊢ SecondCountableTopology α

Tactic:
have := hf.secondCountableTopology
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SecondCountableTopology β
f : α → β
hf : IsEmbedding f
this : SecondCountableTopology α
⊢ SeparableSpace α

Tactic:
SecondCountableTopology.to_separableSpace

Premises used: TopologicalSpace.SecondCountableTopology.to_separableSpace
-- Module: Mathlib.Topology.Bases
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : SecondCountableTopology β
f : α → β
hf : IsEmbedding f
this : SecondCountableTopology α
⊢ SeparableSpace α

Tactic:
exact SecondCountableTopology.to_separableSpace

Premises used: TopologicalSpace.SecondCountableTopology.to_separableSpace
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
⊢ univᶜ ∈ T

Tactic:
simp [empty_mem]
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
s t : Set X
hs : sᶜ ∈ T
ht : tᶜ ∈ T
⊢ (s ∩ t)ᶜ ∈ T

Tactic:
simpa only [compl_inter] using union_mem sᶜ hs tᶜ ht

Premises used: Compl.compl, Set.compl_inter
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
s : Set (Set X)
hs : ∀ t ∈ s, tᶜ ∈ T
simp : ⋂₀ (compl '' s) ∈ T
⊢ (⋃₀ s)ᶜ ∈ T

Tactic:
simp only [Set.compl_sUnion]

Premises used: Set.compl_sUnion
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
s : Set (Set X)
hs : ∀ t ∈ s, tᶜ ∈ T
⊢ ⋂₀ (compl '' s) ∈ T

Tactic:
sInter_mem (compl '' s) fun z ⟨y, hy, hz⟩ => hz ▸ hs y hy

Premises used: Compl.compl, Membership.mem, Eq.rec, Set.image, _private.0.TopologicalSpace.ofClosed.match_2
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
s : Set (Set X)
hs : ∀ t ∈ s, tᶜ ∈ T
⊢ ⋂₀ (compl '' s) ∈ T

Tactic:
exact sInter_mem (compl '' s) fun z ⟨y, hy, hz⟩ => hz ▸ hs y hy

Premises used: Compl.compl, Membership.mem, Eq.rec, Set.image, _private.0.TopologicalSpace.ofClosed.match_2
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s : Set X
p : Set X → Prop
h₁ : p univ
h₂ : ∀ (s t : Set X), p s → p t → p (s ∩ t)
h₃ : ∀ (s : Set (Set X)), (∀ t ∈ s, p t) → p (⋃₀ s)
⊢ IsOpen[{ IsOpen := p, isOpen_univ := h₁, isOpen_inter := h₂, isOpen_sUnion := h₃ }] s ↔ p s

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsOpen
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
t t' : TopologicalSpace X
h a : ∀ (x : Set X), IsOpen[t] x ↔ IsOpen[t'] x
⊢ t = t'

Tactic:
ext
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
t t' : TopologicalSpace X
h : ∀ (s : Set X), IsOpen[t] s ↔ IsOpen[t'] s
x : Set X
⊢ IsOpen[t] x ↔ IsOpen[t'] x

Tactic:
h _
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
t t' : TopologicalSpace X
h : ∀ (s : Set X), IsOpen[t] s ↔ IsOpen[t'] s
x : Set X
⊢ IsOpen[t] x ↔ IsOpen[t'] x

Tactic:
exact h _
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s : Set X
t : TopologicalSpace X
⊢ TopologicalSpace.IsOpen s = IsOpen[t] s

Tactic:
rfl

Premises used: IsOpen, rfl
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
ι : Sort v
inst : TopologicalSpace X
f : ι → Set X
h : ∀ (i : ι), IsOpen[inst] (f i)
⊢ IsOpen[inst] (⋃ (i : ι), f i)

Tactic:
isOpen_sUnion (forall_mem_range.2 h)

Premises used: Iff.mpr, Set.forall_mem_range, iSup, isOpen_sUnion, Set.iUnion
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
inst : TopologicalSpace X
s : Set α
f : α → Set X
h : ∀ i ∈ s, IsOpen[inst] (f i)
⊢ IsOpen[inst] (⋃ i ∈ s, f i)

Tactic:
isOpen_iUnion fun i => isOpen_iUnion fun hi => h i hi

Premises used: isOpen_iUnion
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s₁ s₂ : Set X
inst : TopologicalSpace X
h₁ : IsOpen[inst] s₁
h₂ : IsOpen[inst] s₂
rw : IsOpen[inst] (⋃ (b : Bool), bif b then s₁ else s₂)
⊢ IsOpen[inst] (s₁ ∪ s₂)

Tactic:
rw [union_eq_iUnion]

Premises used: Set.union_eq_iUnion
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s₁ s₂ : Set X
inst : TopologicalSpace X
h₁ : IsOpen[inst] s₁
h₂ : IsOpen[inst] s₂
⊢ IsOpen[inst] (⋃ (b : Bool), bif b then s₁ else s₂)

Tactic:
isOpen_iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)

Premises used: Iff.mpr, Bool.forall_bool, isOpen_iUnion, And.intro
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
s₁ s₂ : Set X
inst : TopologicalSpace X
h₁ : IsOpen[inst] s₁
h₂ : IsOpen[inst] s₂
⊢ IsOpen[inst] (⋃ (b : Bool), bif b then s₁ else s₂)

Tactic:
exact isOpen_iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)

Premises used: Iff.mpr, Bool.forall_bool, isOpen_iUnion, And.intro
-- Module: Mathlib.Topology.Basic
Goal:
X : Type u
α : Type u_1
s : Set X
inst : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst] (f i)
hU : Eq.{u + 1} (α := Set X) (⋃ (i : α), f i) univ
⊢ IsOpen[inst] s ↔ ∀ (i : α), IsOpen[inst] (f i ∩ s)

Tactic:
⟨fun h i ↦ (ho i).inter h, fun h ↦ ?_⟩

Premises used: IsOpen.inter, Iff.intro