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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
w✝ : X
left✝ : w✝ ∈ s
⊢ IsClosed[inst✝] ((fun x ↦ closure[inst✝] {x}) w✝)

Tactic:
;

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : StableUnderSpecialization s
w✝ : X
left✝ : w✝ ∈ s
⊢ IsClosed[inst✝] ((fun x ↦ closure[inst✝] {x}) w✝)
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (∀ ⦃a : X⦄ ⦃b : Y⦄, b ∈ closure[inst✝] {f a} → ∃ a' ∈ closure[inst✝¹] {a}, f a' = b) ↔
    ∀ (x : X), closure[inst✝] {f x} ⊆ f '' closure[inst✝¹] {x}

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (∀ ⦃a : X⦄ ⦃b : Y⦄, b ∈ closure[inst✝] {f a} → ∃ a' ∈ closure[inst✝¹] {a}, f a' = b) ↔
    ∀ (x : X), closure[inst✝] {f x} ⊆ f '' closure[inst✝¹] {x}
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ SpecializingMap f ↔ ∀ (x : X), f '' closure[inst✝¹] {x} = closure[inst✝] {f x}

Tactic:
simpa only [closure_singleton_eq_Iic] using!
    Relation.fibration_iff_image_Iic hf.specialization_monotone

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsClosed univ

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsClosed univ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ↑f ≤ 𝓝 x ×ˢ 𝓝 y

Tactic:
;

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, ↑f ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, ↑f ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : ↑f ≤ comap Prod.fst (𝓝 x)
y : Y
ty : y ∈ t
hy : ↑f ≤ comap Prod.snd (𝓝 y)
⊢ ↑f ≤ 𝓝 x ×ˢ 𝓝 y
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact (univ ×ˢ univ)

Tactic:
;

Goal state after:
X : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
s t : Set X
f : X → Y
inst✝¹ : CompactSpace X
inst✝ : CompactSpace Y
⊢ IsCompact (univ ×ˢ univ)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X × Set Y
hK : IsCompact K.1 ∧ IsCompact K.2
⊢ K.1ᶜ ×ˢ univ ∪ univ ×ˢ K.2ᶜ ∈ cocompact (X × Y)

Tactic:
← compl_prod_eq_union

Goal state after:
case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
K : Set X × Set Y
hK : IsCompact K.1 ∧ IsCompact K.2
⊢ (K.1 ×ˢ K.2)ᶜ ∈ cocompact (X × Y)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι), IsCompact (s i)
⊢ IsCompact (univ.pi s)

Tactic:
convert! isCompact_pi_infinite h

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
h : ∀ (i : ι), IsCompact (s i)
⊢ univ.pi s = {x | ∀ (i : ι), x i ∈ s i}
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X✝ : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
s t : Set X✝
f : X✝ → Y
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ IsCompact (univ.pi fun i ↦ univ)

Tactic:
;

Goal state after:
X✝ : Type u
Y : Type v
ι : Type u_1
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y
s t : Set X✝
f : X✝ → Y
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ IsCompact (univ.pi fun i ↦ univ)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t
s : Set X
sS : s ⊆ S
U : Set X
Uo : IsOpen[inst✝] U
Us : U ∩ S = sᶜ ∩ S
⊢ Uᶜ ∩ S = s ∩ S

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ t ⊆ S, ∃ u, IsOpen[inst✝] u ∧ u ∩ S = t
s : Set X
sS : s ⊆ S
U : Set X
Uo : IsOpen[inst✝] U
Us : U ∩ S = sᶜ ∩ S
⊢ Uᶜ ∩ S = s ∩ S
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s✝ : Finset X
a✝ : ∀ t ⊂ s✝, (↑t).Nonempty → IsOpen[inst✝¹] ↑t → ∃ x ∈ ↑t, IsOpen[inst✝¹] {x}
hne : (↑s✝).Nonempty
ho : IsOpen[inst✝¹] ↑s✝
⊢ ∃ x ∈ ↑s✝, IsOpen[inst✝¹] {x}

Tactic:
rename_i s ihs

Goal state after:
case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T0Space X
s : Finset X
ihs : ∀ t ⊂ s, (↑t).Nonempty → IsOpen[inst✝¹] ↑t → ∃ x ∈ ↑t, IsOpen[inst✝¹] {x}
hne : (↑s).Nonempty
ho : IsOpen[inst✝¹] ↑s
⊢ ∃ x ∈ ↑s, IsOpen[inst✝¹] {x}
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s
s : Set X
sS : s ⊆ S
U : Set X
Uo : IsClosed[inst✝] U
Us : U ∩ S = sᶜ ∩ S
⊢ Uᶜ ∩ S = s ∩ S

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ s ⊆ S, ∃ U, IsClosed[inst✝] U ∧ U ∩ S = s
s : Set X
sS : s ⊆ S
U : Set X
Uo : IsClosed[inst✝] U
Us : U ∩ S = sᶜ ∩ S
⊢ Uᶜ ∩ S = s ∩ S
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
y : X
s : Set X
hys : y ∈ s
hs : T0Space ↑s
x : { x // x ∈ s }
hxy : Inseparable (↑x) y
⊢ ↑x = y

Tactic:
;

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ (x y : X), Inseparable x y → ∃ s, x ∈ s ∧ y ∈ s ∧ T0Space ↑s
y : X
s : Set X
hys : y ∈ s
hs : T0Space ↑s
x : { x // x ∈ s }
hxy : Inseparable (↑x) y
⊢ ↑x = y
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x x✝ : X
⊢ x✝ ∈ closure[inst✝¹] {x} ↔ x✝ ∈ (𝓝 x).ker

Tactic:
;

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R0Space X
x x✝ : X
⊢ x✝ ∈ closure[inst✝¹] {x} ↔ x✝ ∈ (𝓝 x).ker
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ⊆ Z
x : X
hx : x ∈ V
⊢ (f ⁻¹' Z).Nonempty

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ⊆ Z
x : X
hx : x ∈ V
⊢ (f ⁻¹' Z).Nonempty
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf₁ : Continuous[inst✝¹, inst✝] f
hf₂ : IsOpenMap f
hf₃ : ∀ (x : Y), IsPreirreducible (f ⁻¹' {x})
hf₄ : Function.Surjective f
V : Set X
hV : V ∈ irreducibleComponents X
Z : Set Y
hZ : IsIrreducible Z
hWZ : f '' V ⊆ Z
this : f ⁻¹' Z ⊆ V
⊢ f '' f ⁻¹' Z ⊆ f '' V

Tactic:
exact Set.image_mono this

Goal state after:
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: case inr
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
ι : Type u_4
X : ι → Type u_3
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (a : ι), T2Space (X a)
i : ι
x : X i
j : ι
y : X j
ne : ⟨i, x⟩ ≠ ⟨j, y⟩
h : i ≠ j
x✝ : TopologicalSpace ι := ⊥
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSigma] u ∧ IsOpen[instTopologicalSpaceSigma] v ∧ ⟨i, x⟩ ∈ u ∧ ⟨j, y⟩ ∈ v ∧ Disjoint u v

Tactic:
;

Goal state after:
case inr
X✝ : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X✝
ι : Type u_4
X : ι → Type u_3
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (a : ι), T2Space (X a)
i : ι
x : X i
j : ι
y : X j
ne : ⟨i, x⟩ ≠ ⟨j, y⟩
h : i ≠ j
x✝ : TopologicalSpace ι := ⊥
⊢ ∃ u v,
    IsOpen[instTopologicalSpaceSigma] u ∧ IsOpen[instTopologicalSpaceSigma] v ∧ ⟨i, x⟩ ∈ u ∧ ⟨j, y⟩ ∈ v ∧ Disjoint u v
Module: Mathlib.Order.SuccPred.Relation

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ (∀ i ∈ Ico n m, r i (succ i)) → ReflTransGen r n m

Tactic:
;

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hnm : n ≤ m
⊢ (∀ i ∈ Ico n m, r i (succ i)) → ReflTransGen r n m
Module: Mathlib.Order.SuccPred.Relation

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
r : α → α → Prop
m : α
inst✝ : Std.Refl r
h1 : ∀ i ∈ Ico m m, r i (succ i)
h2 : ∀ i ∈ Ico m m, r (succ i) i
⊢ TransGen r m m

pp: case inr
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
r : α → α → Prop
n m : α
inst✝ : Std.Refl r
h1 : ∀ i ∈ Ico n m, r i (succ i)
h2 : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≠ n
⊢ TransGen r n m

Tactic:
;

Goal state after:
case inl
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
r : α → α → Prop
m : α
inst✝ : Std.Refl r
h1 : ∀ i ∈ Ico m m, r i (succ i)
h2 : ∀ i ∈ Ico m m, r (succ i) i
⊢ TransGen r m m

case inr
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
r : α → α → Prop
n m : α
inst✝ : Std.Refl r
h1 : ∀ i ∈ Ico n m, r i (succ i)
h2 : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≠ n
⊢ TransGen r n m
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
H1 : IsClosed[inst✝¹] s
H2 : IsCompact (closure[inst✝¹] sᶜ)
H3 : IsClosed[inst✝¹] t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds s t

Tactic:
rw [← sdiff_union_of_subset (interior_subset (s := s))]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
s t : Set X
H1 : IsClosed[inst✝¹] s
H2 : IsCompact (closure[inst✝¹] sᶜ)
H3 : IsClosed[inst✝¹] t
H4 : Disjoint s t
ht : IsCompact t
⊢ SeparatedNhds (s \ interior s ∪ interior s) t
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ (∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s) → s ⊆ t

Tactic:
;

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
⊢ (∀ x ∈ 𝓝ˢ t, x ∈ 𝓝ˢ s) → s ⊆ t
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
⊢ cofinite ≤ codiscrete X

Tactic:
simpa using! isCompact_univ.cofinite_inf_le_codiscreteWithin

Goal state after:
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
x✝ : X
⊢ x✝ ∈ closure[inst✝¹] K ↔ x✝ ∈ ⋃ x ∈ K, {y | Inseparable x y}

Tactic:
;

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
x✝ : X
⊢ x✝ ∈ closure[inst✝¹] K ↔ x✝ ∈ ⋃ x ∈ K, {y | Inseparable x y}
Module: Mathlib.Topology.Clopen

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
U : Set X
⊢ Continuous[inst✝, _] U.boolIndicator ↔ IsClopen U

Tactic:
rw [continuous_bool_rng true, preimage_boolIndicator_true]

Goal state after:
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure[inst✝] {b | f b ≤ g b}ᶜ
⊢ {b | g b < f b} = {b | f b ≤ g b}ᶜ

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure[inst✝] {b | f b ≤ g b}ᶜ
⊢ {b | g b < f b} = {b | f b ≤ g b}ᶜ
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure[inst✝] {b | f b ≤ g b}ᶜ
⊢ {b | ¬f b ≤ g b} = {b | f b ≤ g b}ᶜ

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
b : β
hb₁ : b ∈ {b | f b ≤ g b}
hb₂ : b ∈ closure[inst✝] {b | f b ≤ g b}ᶜ
⊢ {b | ¬f b ≤ g b} = {b | f b ≤ g b}ᶜ
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₁

pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l : Filter α
inst✝² : CountableInterFilter l
l₁ l₂ : Filter α
inst✝¹ : CountableInterFilter l₁
inst✝ : CountableInterFilter l₂
S : Set (Set α)
hSc : S.Countable
hS : ∀ s ∈ S, s ∈ l₁ ⊔ l₂
s : Set α
hs : s ∈ S
⊢ s ∈ l₂

Tactic:
exacts [(hS s hs).1, (hS s hs).2]

Goal state after:
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty
i : β
hi : i ∈ t
j : β
hj : j ∈ t
k : β
hk : k ∈ Ico j i
⊢ (s k ∩ s (succ k)).Nonempty

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder β
inst✝¹ : SuccOrder β
inst✝ : IsSuccArchimedean β
s : β → Set α
t : Set β
ht : t.OrdConnected
H : ∀ n ∈ t, IsPreconnected (s n)
K : ∀ n ∈ t, succ n ∈ t → (s n ∩ s (succ n)).Nonempty
h1 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → k ∈ t
h2 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → succ k ∈ t
h3 : ∀ {i j k : β}, i ∈ t → j ∈ t → k ∈ Ico i j → (s k ∩ s (succ k)).Nonempty
i : β
hi : i ∈ t
j : β
hj : j ∈ t
k : β
hk : k ∈ Ico j i
⊢ (s k ∩ s (succ k)).Nonempty
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mp.superset
α : Type u_2
g : Set (Set α)
s s✝ t✝ : Set α
a✝¹ : CountableGenerateSets g s✝
a✝ : s✝ ⊆ t✝
ih : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s✝
S : Set (Set α)
⊢ S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ s✝ → S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ t✝

Tactic:
;

Goal state after:
case mp.superset
α : Type u_2
g : Set (Set α)
s s✝ t✝ : Set α
a✝¹ : CountableGenerateSets g s✝
a✝ : s✝ ⊆ t✝
ih : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s✝
S : Set (Set α)
⊢ S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ s✝ → S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ t✝
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inl
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
⊢ IsClopen ∅

pp: case inr
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
⊢ IsClopen univ

Tactic:
;

Goal state after:
case inl
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
⊢ IsClopen ∅

case inr
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
⊢ IsClopen univ
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
H : ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
a : X
s : Set X
hs : s ∈ 𝓝 a
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst✝] t ∧ t ⊆ s

Tactic:
rw [← H] at hs

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
tfae_1_iff_5 : RegularSpace X ↔ ∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x
tfae_5_to_6 : (∀ (x : X), (𝓝 x).lift' closure[inst✝] ≤ 𝓝 x) → ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
H : ∀ (x : X), (𝓝 x).lift' closure[inst✝] = 𝓝 x
a : X
s : Set X
hs : s ∈ (𝓝 a).lift' closure[inst✝]
⊢ ∃ t ∈ 𝓝 a, IsClosed[inst✝] t ∧ t ⊆ s
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsuv this : ¬(s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
;

Goal state after:
case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsuv this : ¬(s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
b : Y
⊢ (comap f (𝓝 (f b))).HasBasis (?m.10 b) (?m.11 b)

Tactic:
;

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
b : Y
⊢ (comap f (𝓝 (f b))).HasBasis (?m.10 b) (?m.11 b)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
⊢ ∀ (i : ι), IsClosed[inst✝] (t i)

Tactic:
;

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsLindelof s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
U : ι → Set X := tᶜ
⊢ ∀ (i : ι), IsClosed[inst✝] (t i)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ IsPreconnected (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅)

Tactic:
;

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ IsPreconnected (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Countable
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof (⋃ i ∈ S, i)

Tactic:
;

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Countable
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof (⋃ i ∈ S, i)
Module: Mathlib.Topology.Compactness.Lindelof

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

Tactic:
;

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
hf : S.Finite
hc : ∀ s ∈ S, IsLindelof s
⊢ IsLindelof (⋃ i ∈ S, i)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (⋃ b, bif b then s else t)

Tactic:
;

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsLindelof s
ht : IsLindelof t
⊢ IsLindelof (⋃ b, bif b then s else t)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
h : connectedComponent x = univ
⊢ IsPreconnected (connectedComponent x)

Tactic:
;

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x : α
h : connectedComponent x = univ
⊢ IsPreconnected (connectedComponent x)
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ IsPreconnected ∅

Tactic:
;

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : IsEmpty α
⊢ IsPreconnected ∅
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ IsPreconnected (connectedComponent (Classical.choice hα))

Tactic:
;

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), connectedComponent x = univ
hα : Nonempty α
⊢ IsPreconnected (connectedComponent (Classical.choice hα))
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), PreconnectedSpace (X i)
⊢ IsPreconnected (univ.pi fun i ↦ univ)

Tactic:
;

Goal state after:
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), PreconnectedSpace (X i)
⊢ IsPreconnected (univ.pi fun i ↦ univ)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LindelofSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsLindelof (f '' univ)

Tactic:
;

Goal state after:
X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LindelofSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsLindelof (f '' univ)
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
i : α → β
inst✝¹ : TopologicalSpace γ
inst✝ : T3Space γ
b : β
f : α → γ
di : IsDenseInducing i
hf : ∀ᶠ (x : β) in 𝓝 b, ∃ c, Tendsto f (comap i (𝓝 x)) (𝓝 c)
φ : β → γ := di.extend f
this : ∀ (b : β), (comap i (𝓝 b)).NeBot
V' : Set γ
V'_in : V' ∈ 𝓝 (φ b)
V'_closed : IsClosed[inst✝¹] V'
V₁ : Set β := {x | Tendsto f (comap i (𝓝 x)) (𝓝 (φ x))}
V₁_in : V₁ ∈ 𝓝 b
⊢ ∃ V₂ ∈ 𝓝 b, IsOpen[inst✝²] V₂ ∧ ∀ x ∈ i ⁻¹' V₂, f x ∈ V'

Tactic:
simpa [and_assoc] using!
      ((nhds_basis_opens' b).comap i).tendsto_left_iff.mp (mem_of_mem_nhds V₁_in : b ∈ V₁) V' V'_in

Goal state after:
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsLindelof (range f)

Tactic:
;

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsLindelof (range f)
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
ι : Type u_5
s : ι → Set α
p : ι → Prop
x : α
h : ∀ (t : Set α), t ∈ 𝓝 x ↔ ∃ i, p i ∧ s i ⊆ t
f : α → β
hf : IsDenseInducing f
T : Set β
hT : T ∈ 𝓝 (f x)
T' : Set β
hT₁ : T' ∈ 𝓝 (f x)
hT₂ : IsClosed[inst✝¹] T'
hT₃ : T' ⊆ T
⊢ f ⁻¹' T' ∈ Filter.comap f (𝓝 (f x))

Tactic:
exact ⟨T', hT₁, Subset.rfl⟩

Goal state after: