mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ ∀ ⦃x : X⦄, x ∈ ↑s → MapsTo (⇑f) (L x) (⋃₀ t)

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ ∀ ⦃x : X⦄, x ∈ ↑s → MapsTo (⇑f) (L x) (⋃₀ t)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
m n : ↑(MaxProducts C ho)
h : (↑m).Tail = (↑n).Tail
⊢ term I ho :: ↑(↑n).Tail = term I ho :: ↑(↑n).Tail

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
⊢ LinearIndependent ℤ (eval (C' C ho)) →
    LinearIndependent ℤ fun (l : ↑(MaxProducts C ho)) ↦ Products.eval (C' C ho) (↑l).Tail

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
⊢ LinearIndependent ℤ (eval (C' C ho)) →
    LinearIndependent ℤ fun (l : ↑(MaxProducts C ho)) ↦ Products.eval (C' C ho) (↑l).Tail
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
hB : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → B ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ B ⊆ ⋃ i ∈ t, U i
⊢ ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ∪ B ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i

Tactic:
]

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
hB : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → B ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ B ⊆ ⋃ i ∈ t, U i
⊢ ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ∪ B ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
h : LinearIndependent ℤ (eval (C' C ho))
f : ↑(MaxProducts C ho) → ↑(GoodProducts (C' C ho)) := MaxToGood C hC hsC ho h₁
hf : Function.Injective f
hh : (fun l ↦ Products.eval (C' C ho) (↑l).Tail) = eval (C' C ho) ∘ f
⊢ LinearIndependent (ι := ↑(MaxProducts C ho)) ℤ (eval (C' C ho) ∘ f)

Tactic:
]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
h : LinearIndependent ℤ (eval (C' C ho))
f : ↑(MaxProducts C ho) → ↑(GoodProducts (C' C ho)) := MaxToGood C hC hsC ho h₁
hf : Function.Injective f
hh : (fun l ↦ Products.eval (C' C ho) (↑l).Tail) = eval (C' C ho) ∘ f
⊢ LinearIndependent (ι := ↑(MaxProducts C ho)) ℤ (eval (C' C ho) ∘ f)
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: case neg
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg✝ : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf✝ :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg✝ :
  ∀ (K : Set ↑(Icc b c)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen[inst✝] U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' Subtype.val '' (K ∩ Iic ⟨b, h⟩)
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' Subtype.val '' (K ∩ Ici ⟨b, h⟩)
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f) K₁ U
hgU : MapsTo (⇑g) K₂ U
i : ι
hf : MapsTo (⇑(F i)) K₁ U
hg : MapsTo (⇑(G i)) K₂ U
hfg : (F i) ⊤ = (G i) ⊥
x : ↑(Icc a c)
hx : x ∈ K
hxb : b ≤ ↑x
⊢ (G i) ⟨↑x, ⋯⟩ ∈ U

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg✝ : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf✝ :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg✝ :
  ∀ (K : Set ↑(Icc b c)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen[inst✝] U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' Subtype.val '' (K ∩ Iic ⟨b, h⟩)
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' Subtype.val '' (K ∩ Ici ⟨b, h⟩)
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f) K₁ U
hgU : MapsTo (⇑g) K₂ U
i : ι
hf : MapsTo (⇑(F i)) K₁ U
hg : MapsTo (⇑(G i)) K₂ U
hfg : (F i) ⊤ = (G i) ⊥
x : ↑(Icc a c)
hx : x ∈ K
hxb : b ≤ ↑x
⊢ (G i) ⟨↑x, ⋯⟩ ∈ U
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
S : Set (Set E)
hf : S.Finite
hc : ∀ s ∈ S, IsCountablyCompact s
⊢ IsCountablyCompact (⋃ i ∈ S, i)

Tactic:
]

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
S : Set (Set E)
hf : S.Finite
hc : ∀ s ∈ S, IsCountablyCompact s
⊢ IsCountablyCompact (⋃ i ∈ S, i)
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
x : X
hxV : x ∈ ⇑f ⁻¹' V
⊢ ⇑f ⁻¹' V ∈ 𝓝 x

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
x : X
hxV : x ∈ ⇑f ⁻¹' V
⊢ ⇑f ⁻¹' V ∈ 𝓝 x
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case h.refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ Subtype.val '' (K U) n ∈ map Subtype.val (𝓝 ⟨↑x, ⋯⟩)

pp: case h.refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ ∀ᶠ (x : X) in 𝓝 ↑x, x ∈ ↑U

Tactic:
]

Goal state after:
case h.refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ Subtype.val '' (K U) n ∈ map Subtype.val (𝓝 ⟨↑x, ⋯⟩)

case h.refine_2.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ ∀ᶠ (x : X) in 𝓝 ↑x, x ∈ ↑U
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case h.refine_2.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ MapsTo (⇑f ∘ Subtype.val) ((K U) n) V

Tactic:
]

Goal state after:
case h.refine_2.refine_2
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
f : C(X, Y)
V : Set Y
hVo : IsOpen[inst✝³] V
U : { x // x ∈ countableBasis X }
hUV : ↑U ⊆ ⇑f ⁻¹' V
x : { x // x ∈ ↑U }
hxV : ↑x ∈ ⇑f ⁻¹' V
n : ℕ
hn : (K U) n ∈ 𝓝 x
⊢ MapsTo (⇑f ∘ Subtype.val) ((K U) n) V
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Z : Type v'
inst✝¹ : TopologicalSpace Z
T : Type v''
inst✝ : TopologicalSpace T
i : ι
f : C(X i, Z)
⊢ instTopologicalSpace ≤ TopologicalSpace.induced (precomp f) ContinuousMap.compactOpen

Tactic:
]

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Z : Type v'
inst✝¹ : TopologicalSpace Z
T : Type v''
inst✝ : TopologicalSpace T
i : ι
f : C(X i, Z)
⊢ instTopologicalSpace ≤ TopologicalSpace.induced (precomp f) ContinuousMap.compactOpen
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: case refine_1
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : C(X i₁, Z)
i₂ : ι
f₂ : C(X i₂, Y)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, X i₁ × X i₂)),
    Continuous[inst✝⁴ i, inst✝¹]
      ((fun x ↦
          match x with
          | (x₁, x₂) => g (f₂ x₂, f₁ x₁)) ∘
        ⇑f)

Tactic:
]

Goal state after:
case refine_1
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : C(X i₁, Z)
i₂ : ι
f₂ : C(X i₂, Y)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, X i₁ × X i₂)),
    Continuous[inst✝⁴ i, inst✝¹]
      ((fun x ↦
          match x with
          | (x₁, x₂) => g (f₂ x₂, f₁ x₁)) ∘
        ⇑f)
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
⊢ ∀ (i : Opens X), t ≤ induced (fun x ↦ x ∈ i) sierpinskiSpace

Tactic:
]

Goal state after:
case a
X : Type u_1
t : TopologicalSpace X
⊢ ∀ (i : Opens X), t ≤ induced (fun x ↦ x ∈ i) sierpinskiSpace
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen[t] u
⊢ IsOpen[generateFrom (⋃ i, {s | IsOpen[induced (fun x ↦ x ∈ i) sierpinskiSpace] s})] u

Tactic:
]

Goal state after:
case a
X : Type u_1
t : TopologicalSpace X
u : Set X
h : IsOpen[t] u
⊢ IsOpen[generateFrom (⋃ i, {s | IsOpen[induced (fun x ↦ x ∈ i) sierpinskiSpace] s})] u
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: case refine_1
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
i₁ : ι
f₁ : C(X i₁, Z)
i₂ : ι
f₂ : C(X i₂, Y)
j : ι
p : C(X j, X i₁ × X i₂)
φ : X i₁ × X i₂ → Y × Z :=
  fun x ↦
    match x with
    | (x₁, x₂) => (f₂ x₂, f₁ x₁)
h : ∀ ⦃i : ι⦄ (f : C(X i, X i₁ × X i₂)), Continuous[inst✝⁴ i, inst✝¹] ((g ∘ φ) ∘ ⇑f)
⊢ Continuous[inst✝⁴ j, inst✝¹]
    ((fun x ↦
        match x with
        | (x₁, x₂) => g (f₂ x₂, f₁ x₁)) ∘
      ⇑p)

Tactic:
]

Goal state after:
case refine_1
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
i₁ : ι
f₁ : C(X i₁, Z)
i₂ : ι
f₂ : C(X i₂, Y)
j : ι
p : C(X j, X i₁ × X i₂)
φ : X i₁ × X i₂ → Y × Z :=
  fun x ↦
    match x with
    | (x₁, x₂) => (f₂ x₂, f₁ x₁)
h : ∀ ⦃i : ι⦄ (f : C(X i, X i₁ × X i₂)), Continuous[inst✝⁴ i, inst✝¹] ((g ∘ φ) ∘ ⇑f)
⊢ Continuous[inst✝⁴ j, inst✝¹]
    ((fun x ↦
        match x with
        | (x₁, x₂) => g (f₂ x₂, f₁ x₁)) ∘
      ⇑p)
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: case refine_2
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h :
  ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
    Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
      match x with
      | (x₁, x₂) => g (f₂ x₂, f₁ x₁)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y × Z)), Continuous[inst✝⁴ i, inst✝¹] (g ∘ ⇑f)

Tactic:
]

Goal state after:
case refine_2
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h :
  ∀ (i₁ : ι) (f₁ : C(X i₁, Z)) (i₂ : ι) (f₂ : C(X i₂, Y)),
    Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
      match x with
      | (x₁, x₂) => g (f₂ x₂, f₁ x₁)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y × Z)), Continuous[inst✝⁴ i, inst✝¹] (g ∘ ⇑f)
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
x1 x2 : X
h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2
⊢ Inseparable ((productOfMemOpens X) x2) ((productOfMemOpens X) x2)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (l.lift' (Iic ∘ 𝓟)).HasBasis p fun i ↦ Iic (𝓟 (s i))

Tactic:
]

Goal state after:
ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (l.lift' (Iic ∘ 𝓟)).HasBasis p fun i ↦ Iic (𝓟 (s i))
Module: Mathlib.Topology.Filter

Goal state before:
pp: X : Type u_4
l : Filter X
⊢ ∀ s ∈ l, ∀ᶠ (a : X) in l, s ∈ pure a

Tactic:
]

Goal state after:
X : Type u_4
l : Filter X
⊢ ∀ s ∈ l, ∀ᶠ (a : X) in l, s ∈ pure a
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
x : α
⊢ 𝓟 {⊥, pure x} = 𝓟 {⊥, pure x}

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ ⋂₀ {s | s ∈ 𝓝 l₁} ⊆ ⋂₀ {s | s ∈ 𝓝 l₂}

Tactic:
]

Goal state after:
α : Type u_2
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ ⋂₀ {s | s ∈ 𝓝 l₁} ⊆ ⋂₀ {s | s ∈ 𝓝 l₂}
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
s : Set (Filter α)
l : Filter α
⊢ (∃ t ∈ l, Iic (𝓟 t) ⊆ s) ↔ ∃ t ∈ l, Iic (𝓟 t) ⊆ s

Tactic:
]

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case mp
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
y : α
yh : y ∈ Metric.eball a r
yx : some y = x
⊢ some y ∈ Metric.eball (some a) r

Tactic:
]

Goal state after:
case mp
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
y : α
yh : y ∈ Metric.eball a r
yx : some y = x
⊢ some y ∈ Metric.eball (some a) r
Module: Mathlib.Topology.Germ

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X✝
f✝ g✝ : X✝ → Y
A : Set X✝
x✝ : X✝
X : Type u_4
α : Type u_5
inst✝ : TopologicalSpace X
x : X
φ : (𝓝 x).Germ α
f g : X → α
h : ((𝓝 x).germSetoid α) f g
⊢ g x = g x

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝ : TopologicalSpace X
f✝ g : X → Y
A✝ : Set X
x✝ : X
P : (x : X) → (𝓝 x).Germ Y → Prop
A : Set X
x : X
φ : (𝓝 x).Germ Y
f f' : X → Y
hff' : f =ᶠ[𝓝 x] f'
hf : ∀ᶠ (y : X) in 𝓝 x, P y ↑f
y : X
hy : P y ↑f
hy' : ∀ᶠ (x : X) in 𝓝 y, f x = f' x
⊢ P y ↑f

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝ : TopologicalSpace X
f✝ g : X → Y
A✝ : Set X
x✝ : X
P : (x : X) → (𝓝 x).Germ Y → Prop
A : Set X
x : X
φ : (𝓝 x).Germ Y
f f' : X → Y
hff' : f =ᶠ[𝓝 x] f'
hf : ∀ᶠ (y : X) in 𝓝 x, P y ↑f
y : X
hy : P y ↑f
hy' : ∀ᶠ (x : X) in 𝓝 y, f x = f' x
⊢ P y ↑f
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x : Option α
xs : x ∈ s
this : ∃ ε > 0, Metric.eball x ε ⊆ s
⊢ ∃ ε > 0, Metric.eball x ε ⊆ s

Tactic:
]

Goal state after:
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x : Option α
xs : x ∈ s
this : ∃ ε > 0, Metric.eball x ε ⊆ s
⊢ ∃ ε > 0, Metric.eball x ε ⊆ s
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f
h : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, g y = f y
⊢ ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑g

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f
h : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, g y = f y
⊢ ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑g
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x : Option α
r : ℝ≥0∞
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' Metric.eball x r)

Tactic:
]

Goal state after:
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x : Option α
r : ℝ≥0∞
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' Metric.eball x r)
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
hx : x ∈ A
y : X
hy : P y ↑f
h'y : ∀ᶠ (x : X) in 𝓝 y, g x = f x
⊢ P y ↑f

Tactic:
]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
hx : x ∈ A
y : X
hy : P y ↑f
h'y : ∀ᶠ (x : X) in 𝓝 y, g x = f x
⊢ P y ↑f