mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
J : (m : ℕ) → Finset (cell C m)
hJ : cellFrontier n ↑i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ J m, openCell m j
⊢ ↑(map n ↑i) '' sphere 0 1 ⊆
    D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ (fun m ↦ (J m).preimage Subtype.val ⋯) m, ↑(map m ↑j) '' closedBall 0 1

Tactic:
]

Goal state after:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
J : (m : ℕ) → Finset (cell C m)
hJ : cellFrontier n ↑i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ J m, openCell m j
⊢ ↑(map n ↑i) '' sphere 0 1 ⊆
    D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ (fun m ↦ (J m).preimage Subtype.val ⋯) m, ↑(map m ↑j) '' closedBall 0 1
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (o : Ordinal.{u}), gfpApprox relDerivedSet s o = s) ↔ ∀ (a : Ordinal.{u}), sᵈ[a] = s

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (∀ (o : Ordinal.{u}), gfpApprox relDerivedSet s o = s) ↔ ∀ (a : Ordinal.{u}), sᵈ[a] = s
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
a : Ordinal.{u}
ha : sᵈ[a + 1] = sᵈ[a]
⊢ relDerivedSet sᵈ[a] = sᵈ[a]

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
a : Ordinal.{u}
ha : sᵈ[a + 1] = sᵈ[a]
⊢ relDerivedSet sᵈ[a] = sᵈ[a]
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
a : Ordinal.{u}
ha : sᵈ[a] ∈ fixedPoints ⇑relDerivedSet
⊢ Perfect sᵈ[a]

Tactic:
]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
a : Ordinal.{u}
ha : sᵈ[a] ∈ fixedPoints ⇑relDerivedSet
⊢ Perfect sᵈ[a]
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : Finite C
x✝ : ∀ (n : ℕ), _root_.Finite (cell C n)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty (cell C b)
this : ∀ (m : ℕ) (j : cell C m), m < n
f : (m : { m // m < n }) × cell C ↑m ≃ (m : ℕ) × cell C m :=
  {
    toFun := fun x ↦
      match x with
      | ⟨m, j⟩ => ⟨↑m, j⟩,
    invFun := fun x ↦
      match x with
      | ⟨m, j⟩ => ⟨⟨m, ⋯⟩, j⟩,
    left_inv := ⋯, right_inv := ⋯ }
⊢ _root_.Finite ((m : { m // m < n }) × cell C ↑m)

Tactic:
]

Goal state after:
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : Finite C
x✝ : ∀ (n : ℕ), _root_.Finite (cell C n)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty (cell C b)
this : ∀ (m : ℕ) (j : cell C m), m < n
f : (m : { m // m < n }) × cell C ↑m ≃ (m : ℕ) × cell C m :=
  {
    toFun := fun x ↦
      match x with
      | ⟨m, j⟩ => ⟨↑m, j⟩,
    invFun := fun x ↦
      match x with
      | ⟨m, j⟩ => ⟨⟨m, ⋯⟩, j⟩,
    left_inv := ⋯, right_inv := ⋯ }
⊢ _root_.Finite ((m : { m // m < n }) × cell C ↑m)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
x : X.A
⊢ (ConcreteCategory.hom (𝟙 X.A)) x = x

Tactic:
]

Goal state after:
X : Compactum
x : X.A
⊢ (ConcreteCategory.hom (𝟙 X.A)) x = x
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (ConcreteCategory.hom (β.map f.f ≫ Y.a)) xs = Y.str (Ultrafilter.map (⇑(ConcreteCategory.hom f)) xs)

Tactic:
]

Goal state after:
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (ConcreteCategory.hom (β.map f.f ≫ Y.a)) xs = Y.str (Ultrafilter.map (⇑(ConcreteCategory.hom f)) xs)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ (ConcreteCategory.hom (β.map X.a ≫ X.a)) uux = X.str (Ultrafilter.map X.str uux)

Tactic:
]

Goal state after:
X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ (ConcreteCategory.hom (β.map X.a ≫ X.a)) uux = X.str (Ultrafilter.map X.str uux)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
S : Set X.A
⊢ IsOpen Sᶜ ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

Tactic:
]

Goal state after:
X : Compactum
S : Set X.A
⊢ IsOpen Sᶜ ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case mp
X : Compactum
S : Set X.A
F : Ultrafilter X.A
cond : S ∉ F
h : S ∈ F
c : X.str F ∉ S
⊢ False

Tactic:
]

Goal state after:
case mp
X : Compactum
S : Set X.A
F : Ultrafilter X.A
cond : S ∉ F
h : S ∈ F
c : X.str F ∉ S
⊢ False
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case mp
X : Compactum
S : Set X.A
F : Ultrafilter X.A
cond : Sᶜ ∈ F
h : S ∈ F
c : X.str F ∉ S
⊢ False

Tactic:
rw [compl_mem_iff_notMem] at cond

Goal state after:
case mp
X : Compactum
S : Set X.A
F : Ultrafilter X.A
cond : S ∉ F
h : S ∈ F
c : X.str F ∉ S
⊢ False
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
⊢ ∀ (f : Ultrafilter X.A), ↑f ≤ 𝓟 Set.univ → ∃ x ∈ Set.univ, ↑f ≤ 𝓝 x

Tactic:
]

Goal state after:
X : Compactum
⊢ ∀ (f : Ultrafilter X.A), ↑f ≤ 𝓟 Set.univ → ∃ x ∈ Set.univ, ↑f ≤ 𝓝 x
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
a✝ : ↑F ≤ 𝓟 Set.univ
⊢ ∀ (s : Set X.A), X.str F ∈ s → IsOpen s → s ∈ ↑F

Tactic:
]

Goal state after:
X : Compactum
F : Ultrafilter X.A
a✝ : ↑F ≤ 𝓟 Set.univ
⊢ ∀ (s : Set X.A), X.str F ∈ s → IsOpen s → s ∈ ↑F
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
⊢ ⨆ i, ⨆ f, coinduced (⇑f) inferInstance =
    ⨆ i, ⨆ j, coinduced (fun x ↦ x.fst.snd x.snd) (coinduced (Sigma.mk ⟨i, j⟩) (inst✝ ⟨i, j⟩.fst))

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
⊢ ⨆ i, ⨆ f, coinduced (⇑f) inferInstance =
    ⨆ i, ⨆ j, coinduced (fun x ↦ x.fst.snd x.snd) (coinduced (Sigma.mk ⟨i, j⟩) (inst✝ ⟨i, j⟩.fst))
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : WithGeneratedByTopology X Y → Z
i : ι
f : C(X i, Y)
⊢ Continuous[inferInstance, inst✝] (g ∘ ⇑f) ↔ Continuous[inst✝¹ i, inst✝] (g ∘ ⇑equiv.symm ∘ ⇑f)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : WithGeneratedByTopology X Y → Z
i : ι
f : C(X i, Y)
⊢ Continuous[inferInstance, inst✝] (g ∘ ⇑f) ↔ Continuous[inst✝¹ i, inst✝] (g ∘ ⇑equiv.symm ∘ ⇑f)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
⊢ ∀ (s : Set Y), IsOpen[tY] s → IsOpen (⇑equiv ⁻¹' s)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
⊢ ∀ (s : Set Y), IsOpen[tY] s → IsOpen (⇑equiv ⁻¹' s)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
U : Set Y
hU : IsOpen[tY] U
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen[inst✝ i] (⇑f ⁻¹' ⇑equiv.symm ⁻¹' ⇑equiv ⁻¹' U)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
U : Set Y
hU : IsOpen[tY] U
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen[inst✝ i] (⇑f ⁻¹' ⇑equiv.symm ⁻¹' ⇑equiv ⁻¹' U)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
h : tY ≤ TopologicalSpace.generatedBy X
⊢ ∀ (s : Set (WithGeneratedByTopology X Y)), IsOpen s → IsOpen[tY] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' s)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
h : tY ≤ TopologicalSpace.generatedBy X
⊢ ∀ (s : Set (WithGeneratedByTopology X Y)), IsOpen s → IsOpen[tY] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' s)
Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
⊢ LocallyPathConnectedSpace X

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
⊢ LocallyPathConnectedSpace X
Module: Mathlib.Topology.Compactness.DeltaGeneratedSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
⊢ SequentialSpace X

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : DeltaGeneratedSpace X
⊢ SequentialSpace X
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
⊢ (∀ ⦃i : ι⦄ (f : C(X i, Y)),
      Continuous[inst✝² i, inst✝¹] ((g ∘ ⇑homeomorph) ∘ ⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f)) ↔
    ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, inst✝¹] (g ∘ ⇑f)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
⊢ (∀ ⦃i : ι⦄ (f : C(X i, Y)),
      Continuous[inst✝² i, inst✝¹] ((g ∘ ⇑homeomorph) ∘ ⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f)) ↔
    ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, inst✝¹] (g ∘ ⇑f)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
i : ι
f : C(X i, Y)
⊢ ∀ (s : Set (WithGeneratedByTopology X Z)),
    IsOpen s → IsOpen[inst✝² i] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f ⁻¹' s)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
i : ι
f : C(X i, Y)
⊢ ∀ (s : Set (WithGeneratedByTopology X Z)),
    IsOpen s → IsOpen[inst✝² i] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f ⁻¹' s)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
i : ι
f : C(X i, Y)
U : Set (WithGeneratedByTopology X Z)
hU : ∀ ⦃i : ι⦄ (f : C(X i, Z)), IsOpen[inst✝² i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
⊢ IsOpen[inst✝² i] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f ⁻¹' U)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
i : ι
f : C(X i, Y)
U : Set (WithGeneratedByTopology X Z)
hU : ∀ ⦃i : ι⦄ (f : C(X i, Z)), IsOpen[inst✝² i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
⊢ IsOpen[inst✝² i] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f ⁻¹' U)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
i : ι
⊢ ∀ (s : Set (WithGeneratedByTopology X (X i))), IsOpen s → IsOpen[inst✝¹ i] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' s)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
i : ι
⊢ ∀ (s : Set (WithGeneratedByTopology X (X i))), IsOpen s → IsOpen[inst✝¹ i] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' s)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
i : ι
U : Set (WithGeneratedByTopology X (X i))
hU : ∀ ⦃i_1 : ι⦄ (f : C(X i_1, X i)), IsOpen[inst✝¹ i_1] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
⊢ IsOpen[inst✝¹ i] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
i : ι
U : Set (WithGeneratedByTopology X (X i))
hU : ∀ ⦃i_1 : ι⦄ (f : C(X i_1, X i)), IsOpen[inst✝¹ i_1] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
⊢ IsOpen[inst✝¹ i] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
q : X.A
P : Ultrafilter X.A
hq1 : X.str P ∈ Q
hq2 : P ∈ basic A
hq3 : X.str P = q
⊢ P ∈ X.str ⁻¹' Q

Tactic:
]

Goal state after:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
Q : Set X.A
hQ : Q ∈ F
q : X.A
P : Ultrafilter X.A
hq1 : X.str P ∈ Q
hq2 : P ∈ basic A
hq3 : X.str P = q
⊢ P ∈ X.str ⁻¹' Q
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
⊢ ∀ (s : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))),
    IsOpen s → IsOpen (⇑WithGeneratedByTopology.equiv.symm ⁻¹' s)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
⊢ ∀ (s : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))),
    IsOpen s → IsOpen (⇑WithGeneratedByTopology.equiv.symm ⁻¹' s)
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
⊢ ContinuousGeneratedBy X g ↔
    ∀ ⦃i : ι⦄ (f : C(X i, Y)),
      Continuous[inst✝² i, inst✝] ((g ∘ ⇑WithGeneratedByTopology.equiv) ∘ ⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
⊢ ContinuousGeneratedBy X g ↔
    ∀ ⦃i : ι⦄ (f : C(X i, Y)),
      Continuous[inst✝² i, inst✝] ((g ∘ ⇑WithGeneratedByTopology.equiv) ∘ ⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f)
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
hg : ContinuousGeneratedBy X g
⊢ ContinuousGeneratedBy X g

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
hg : ContinuousGeneratedBy X g
⊢ ContinuousGeneratedBy X g
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝² : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
g : Y → Z
hg : ContinuousGeneratedBy X g
T : Type u_1
inst✝ : TopologicalSpace T
f : T → Y
hf : ContinuousGeneratedBy X f
⊢ Continuous (⇑WithGeneratedByTopology.equiv.symm ∘ (g ∘ f) ∘ ⇑WithGeneratedByTopology.equiv)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝² : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
g : Y → Z
hg : ContinuousGeneratedBy X g
T : Type u_1
inst✝ : TopologicalSpace T
f : T → Y
hf : ContinuousGeneratedBy X f
⊢ Continuous (⇑WithGeneratedByTopology.equiv.symm ∘ (g ∘ f) ∘ ⇑WithGeneratedByTopology.equiv)
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
hg : Continuous[inst✝¹, inst✝] g
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, inst✝] (g ∘ ⇑f)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
g : Y → Z
hg : Continuous[inst✝¹, inst✝] g
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, inst✝] (g ∘ ⇑f)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
⊢ ∀ ⦃i_1 : ι⦄ (f_1 : C(X i_1, X i)), Continuous[inst✝¹ i_1, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f) ∘ ⇑f_1)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
⊢ ∀ ⦃i_1 : ι⦄ (f_1 : C(X i_1, X i)), Continuous[inst✝¹ i_1, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f) ∘ ⇑f_1)
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, _] (⇑equiv.symm ∘ ⇑f)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, _] (⇑equiv.symm ∘ ⇑f)
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
i : ι
f : C(X i, Y)
⊢ Continuous[inst✝² i, inst✝¹] ⇑f

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
i : ι
f : C(X i, Y)
⊢ Continuous[inst✝² i, inst✝¹] ⇑f
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
j : ι
g : C(X j, X i)
⊢ Continuous[inst✝¹ j, tY] (⇑f ∘ ⇑g)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
j : ι
g : C(X j, X i)
⊢ Continuous[inst✝¹ j, tY] (⇑f ∘ ⇑g)
Module: Mathlib.Topology.Convenient.Category

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y Z : ContinuousGeneratedByCat X
g : (toTopCat X).obj Y ⟶ (toTopCat X).obj Z
⊢ Continuous
    (⇑WithGeneratedByTopology.equiv.symm ∘
      (⇑WithGeneratedByTopology.equiv ∘ ⇑(TopCat.Hom.hom g) ∘ ⇑WithGeneratedByTopology.equiv.symm) ∘
        ⇑WithGeneratedByTopology.equiv)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y Z : ContinuousGeneratedByCat X
g : (toTopCat X).obj Y ⟶ (toTopCat X).obj Z
⊢ Continuous
    (⇑WithGeneratedByTopology.equiv.symm ∘
      (⇑WithGeneratedByTopology.equiv ∘ ⇑(TopCat.Hom.hom g) ∘ ⇑WithGeneratedByTopology.equiv.symm) ∘
        ⇑WithGeneratedByTopology.equiv)
Module: Mathlib.Topology.Convenient.Category

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : ContinuousGeneratedByCat X
⊢ IsGeneratedBy X ↑((toTopCat X).obj Y)

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : ContinuousGeneratedByCat X
⊢ IsGeneratedBy X ↑((toTopCat X).obj Y)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
⊢ instTopologicalSpacePUnit ≤ TopologicalSpace.generatedBy X

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
⊢ instTopologicalSpacePUnit ≤ TopologicalSpace.generatedBy X