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

Goal state before:
pp: case neg
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
i : ι
h : i ∉ s
⊢ IsCompact (if i ∈ s then n'' i else univ)

Tactic:
if_neg h

Goal state after:
case neg
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
i : ι
h : i ∉ s
⊢ IsCompact univ
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst✝] (s i)
x y : X
⊢ y ∈ ⋂ i, ⋂ (_ : x ∉ s i), (s i)ᶜ → {i | y ∈ s i} ⊆ {i | x ∈ s i}

Tactic:
hy

Goal state after:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
s : ι → Set X
hs : LocallyFinite s
hs' : ∀ (i : ι), IsClosed[inst✝] (s i)
x y : X
hy : y ∈ ⋂ i, ⋂ (_ : x ∉ s i), (s i)ᶜ
⊢ {i | y ∈ s i} ⊆ {i | x ∈ s i}
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: case inr.refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
h✝ : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
⊢ ⋃ n, (fun n ↦ ⋃ k, ⋃ (_ : k ≤ n), Sigma.mk (f k) '' compactCovering (X (f k)) n) n = univ

Tactic:
simp only [iUnion_eq_univ_iff, Sigma.forall, mem_iUnion, hf.forall]
      intro k y
      rcases exists_mem_compactCovering y with ⟨n, hn⟩
      refine ⟨max k n, k, le_max_left _ _, mem_image_of_mem _ ?_⟩
      exact compactCovering_subset _ (le_max_right _ _) hn

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

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
⊢ (⋂ i, V i ∩ Wᶜ).Nonempty

Tactic:
refine
      IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed _ (fun i j => ?_) H
        (fun i => (hV_cpct i).inter_right W_op.isClosed_compl) fun i =>
        (hV_closed i).inter W_op.isClosed_compl

Goal state after:
X : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : Nonempty ι
V : ι → Set X
hV : Directed (fun x1 x2 ↦ x1 ⊇ x2) V
hV_cpct : ∀ (i : ι), IsCompact (V i)
hV_closed : ∀ (i : ι), IsClosed[inst✝¹] (V i)
U : Set X
hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x
W : Set X
hsubW : ⋂ i, V i ⊆ W
W_op : IsOpen[inst✝¹] W
hWU : W ⊆ U
H : ∀ (i : ι), (V i ∩ Wᶜ).Nonempty
i j : ι
⊢ ∃ z, (fun x1 x2 ↦ x1 ⊇ x2) (V i ∩ Wᶜ) (V z ∩ Wᶜ) ∧ (fun x1 x2 ↦ x1 ⊇ x2) (V j ∩ Wᶜ) (V z ∩ Wᶜ)
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
h : Minimal (fun x ↦ x ∈ { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }) x
a : α
has : a ∈ s
hax : a ≤ x
⊢ x ∈ s

Tactic:
h.eq_of_ge ⟨a, has, rfl.le⟩ hax

Goal state after:
case refine_1
α : Type u_1
inst✝ : PartialOrder α
s : Set α
x : α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
h : Minimal (fun x ↦ x ∈ { carrier := {x | ∃ a ∈ s, a ≤ x}, upper' := ⋯ }) x
a : α
has : a ∈ s
hax : a ≤ x
⊢ a ∈ s
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
hf : ∀ (x : X), ∃ t ∈ 𝓝 x, IsBounded (f '' t)
⊢ IsBounded (f '' s)

Tactic:
choose U hU using hf

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Bornology Y
s : Set X
hs : IsCompact s
f : X → Y
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x ∧ IsBounded (f '' U x)
⊢ IsBounded (f '' s)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case a
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ (cocompact X).coprod (cocompact Y) ≤ cocompact (X × Y)

Tactic:
exact sup_le (comap_cocompact_le continuous_fst) (comap_cocompact_le continuous_snd)

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
⊢ IsPreirreducible (f '' s)

Tactic:
rintro u v hu hv ⟨_, ⟨⟨x, hx, rfl⟩, hxu⟩⟩ ⟨_, ⟨⟨y, hy, rfl⟩, hyv⟩⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
H : IsPreirreducible s
f : X → Y
hf : ContinuousOn f s
u v : Set Y
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ s
hxu : f x ∈ u
y : X
hy : y ∈ s
hyv : f y ∈ v
⊢ (f '' s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y

Tactic:
rcases eq_or_ne a b with rfl | h

Goal state after:
case inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
hb : ∀ᶠ (x : X) in 𝓝[≠] a, p x
⊢ ∀ᶠ (y : X) in 𝓝[≠] a, p y

case inr
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
p : X → Prop
a : X
ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
b : X
hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x
h : a ≠ b
⊢ ∀ᶠ (y : X) in 𝓝[≠] b, p y
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case h.refine_3
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
S : Set X
hS : IsClosed[inst✝¹] S
hne : S.Nonempty
opens : Set (Set X) := {U | Sᶜ ⊆ U ∧ IsOpen[inst✝¹] U ∧ Uᶜ.Nonempty}
c : Set (Set X)
hc : c ⊆ opens
hz : IsChain (fun x1 x2 ↦ x1 ⊆ x2) c
U₀ : Set X
hU₀ : U₀ ∈ c
this : Nonempty { U // U ∈ c }
U₀compl : Sᶜ ⊆ U₀
⊢ (⋃₀ c)ᶜ.Nonempty

Tactic:
· convert_to (⋂ U : { U // U ∈ c }, U.1ᶜ).Nonempty
          · ext
            simp only [not_exists, not_and, Set.mem_iInter, Subtype.forall,
              mem_compl_iff, mem_sUnion]
          apply IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed
          · rintro ⟨U, hU⟩ ⟨U', hU'⟩
            obtain ⟨V, hVc, hVU, hVU'⟩ := hz.directedOn U hU U' hU'
            exact ⟨⟨V, hVc⟩, Set.compl_subset_compl.mpr hVU, Set.compl_subset_compl.mpr hVU'⟩
          · exact fun U => (hc U.2).2.2
          · exact fun U => (hc U.2).2.1.isClosed_compl.isCompact
          · exact fun U => (hc U.2).2.1.isClosed_compl

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case right
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
y : X
⊢ y ∈ Uᶜ → y ∈ (U \ s)ᶜ

Tactic:
hy

Goal state after:
case right
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : s ∈ codiscreteWithin U
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∉ U
y : X
hy : y ∈ Uᶜ
⊢ y ∈ (U \ s)ᶜ
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
hs : s.Subsingleton
⊢ (closure[inst✝¹] s).Subsingleton

Tactic:
by
  rwa [hs.closure_eq]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
x✝ : X
f g : X → Y
hf : ContinuousAt f x✝
hg : ContinuousAt g x✝
hfg : f x✝ ≠ g x✝
Uf Ug : Set Y
h₁U : IsOpen[inst✝¹] Uf
h₂U : IsOpen[inst✝¹] Ug
h₃U : f x✝ ∈ Uf
h₄U : g x✝ ∈ Ug
h₅U : Uf ∩ Ug = ∅
x : X
hx : g x ∈ Uf ∧ g x ∈ Ug
H : f x = g x
this : g x ∈ Uf ∩ Ug
⊢ False

Tactic:
simp [h₅U] at this

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

Goal state before:
pp: case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
⊢ y ∈ S → y ∈ closure[inst✝¹] {x}

Tactic:
hy

Goal state after:
case mp
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
⊢ y ∈ closure[inst✝¹] {x}
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x
a✝ : X
⊢ (∀ᶠ (x : X) in 𝓝 a✝, p x) → ∀ᶠ (x : X) in 𝓝[s] a✝, p x

Tactic:
hy

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
a : X
p : X → Prop
hs : IsOpen[inst✝] s
h : ∀ᶠ (y : X) in 𝓝[s] a, ∀ᶠ (x : X) in 𝓝 y, p x
a✝ : X
hy : ∀ᶠ (x : X) in 𝓝 a✝, p x
⊢ ∀ᶠ (x : X) in 𝓝[s] a✝, p x
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Finite
⊢ tᶜ ∈ codiscreteWithin s

Tactic:
by
  apply h.induction_on (motive := fun t _ ↦ tᶜ ∈ codiscreteWithin s)
  · simp
  · intro τ t hτ h₁t h₂t
    have : (insert τ t)ᶜ = {τ}ᶜ ∩ tᶜ := by aesop
    simp_all

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
s : Set α
a : α
⊢ 𝓝[univ ∩ (s \ {a})] a = 𝓝[s \ {a}] a

Tactic:
univ_inter

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
s : Set α
a : α
⊢ 𝓝[s \ {a}] a = 𝓝[s \ {a}] a
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst✝¹] L
hd : Disjoint K L
⊢ SeparatedNhds K L

Tactic:
simp_rw [separatedNhds_iff_disjoint, hK.disjoint_nhdsSet_left, hL.disjoint_nhdsSet_right,
    disjoint_nhds_nhds_iff_not_inseparable]

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst✝¹] L
hd : Disjoint K L
⊢ ∀ x ∈ K, ∀ x_1 ∈ L, ¬Inseparable x x_1
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst✝¹] L
hd : Disjoint K L
x : X
hx : x ∈ K
y : X
⊢ y ∈ L → ¬Inseparable x y

Tactic:
hy

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K L : Set X
hK : IsCompact K
hL : IsCompact L
h'L : IsClosed[inst✝¹] L
hd : Disjoint K L
x : X
hx : x ∈ K
y : X
hy : y ∈ L
⊢ ¬Inseparable x y
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α✝ : Type u
β : Type v
γ : Type w
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), OrderClosedTopology (α i)
⊢ OrderClosedTopology ((i : ι) → α i)

Tactic:
by
  constructor
  simp only [Pi.le_def, ofPred_forall]
  exact isClosed_iInter fun i => isClosed_le (continuous_apply i).fst' (continuous_apply i).snd'

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

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst✝¹] F
y : α
⊢ y ∈ connectedComponentIn F x → connectedComponentIn F x ∈ 𝓝 y

Tactic:
hy

Goal state after:
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : LocallyConnectedSpace α
F : Set α
x : α
hF : IsOpen[inst✝¹] F
y : α
hy : y ∈ connectedComponentIn F x
⊢ connectedComponentIn F x ∈ 𝓝 y
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
x : α
hx : x ∈ ⋃ n ∈ t, s n
y : α
⊢ y ∈ ⋃ n ∈ t, s n → ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1

Tactic:
hy

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
ι : Type u_3
t : Set ι
s : ι → Set α
H : ∀ i ∈ t, IsPreconnected (s i)
K : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen (fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t) i j
R : ι → ι → Prop := fun i j ↦ (s i ∩ s j).Nonempty ∧ i ∈ t
P : ∀ i ∈ t, ∀ j ∈ t, ReflTransGen R i j → ∃ p ⊆ t, i ∈ p ∧ j ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)
x : α
hx : x ∈ ⋃ n ∈ t, s n
y : α
hy : y ∈ ⋃ n ∈ t, s n
⊢ ∃ t_1 ⊆ ⋃ n ∈ t, s n, x ∈ t_1 ∧ y ∈ t_1 ∧ IsPreconnected t_1
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)
⊢ LocallyConnectedSpace α

Tactic:
rw [locallyConnectedSpace_iff_subsets_isOpen_isConnected]

Goal state after:
case mpr
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (F : Set α), IsOpen[inst✝] F → ∀ x ∈ F, IsOpen[inst✝] (connectedComponentIn F x)
⊢ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ LocallyConnectedSpace α → ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
rw [locallyConnectedSpace_iff_subsets_isOpen_isConnected]

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ (∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V) →
    ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U
Module: Mathlib.Topology.Connected.LocallyConnected

Goal state before:
pp: case neg
ι : Type u_1
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), LocallyConnectedSpace (X i)
hfinite : {i | ¬PreconnectedSpace (X i)}.Finite
x : (i : ι) → X i
U : Set ((i : ι) → X i)
J : Set ι
hJ : J.Finite
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), t i ∈ 𝓝 (x i)
htU : J.pi t ⊆ U
K : Set ι := J ∪ {i | ¬PreconnectedSpace (X i)}
i : ι
hi : i ∉ K
this : PreconnectedSpace (X i)
⊢ IsPreconnected univ

Tactic:
exact isPreconnected_univ

Goal state after:
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: α : Type u_2
g : Set (Set α)
s : Set α
⊢ s ∈ countableGenerate g ↔ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s

Tactic:
constructor <;> intro h

Goal state after:
case mp
α : Type u_2
g : Set (Set α)
s : Set α
h : s ∈ countableGenerate g
⊢ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s

case mpr
α : Type u_2
g : Set (Set α)
s : Set α
h : ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s
⊢ s ∈ countableGenerate g
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
⊢ f ≤ countableGenerate g ↔ g ⊆ f.sets

Tactic:
constructor <;> intro h

Goal state after:
case mp
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : f ≤ countableGenerate g
⊢ g ⊆ f.sets

case mpr
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
⊢ f ≤ countableGenerate g
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inr
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : univ ∩ s j = ∅
hi : s i = univ
⊢ False

Tactic:
univ_inter

Goal state after:
case inr
α : Type u
ι : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PreconnectedSpace α
s : ι → Set α
h_nonempty : ∀ (i : ι), (s i).Nonempty
h_disj : Pairwise (Disjoint on s)
h_clopen : ∀ (i : ι), IsClopen (s i)
i j : ι
h_ne : s j = ∅
hi : s i = univ
⊢ False
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ IsPreconnected s ↔ ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Tactic:
constructor <;> intro h

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
⊢ ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen[inst✝] u → IsOpen[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ IsPreconnected s ↔
    ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Tactic:
constructor <;> intro h

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
⊢ ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsClosed[inst✝] u → IsClosed[inst✝] v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
⊢ IsPreconnected s
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set X
hs : IsCompact s
y : X
⊢ y ∈ nhdsKer s → y ∈ closure[inst✝¹] s

Tactic:
hy

Goal state after:
case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set X
hs : IsCompact s
y : X
hy : y ∈ nhdsKer s
⊢ y ∈ closure[inst✝¹] s
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
F : Set β
hf : ContinuousOn f (f ⁻¹' F)
y : β
x : α
hx : x ∈ f ⁻¹' connectedComponentIn F y
z : α
hz : z ∈ connectedComponentIn (f ⁻¹' F) x
⊢ f z ∈ connectedComponentIn F (f x)

Tactic:
exact connectedComponentIn_mono _ (image_preimage_subset f F)
      (hf.mapsTo_connectedComponentIn (connectedComponentIn_subset F y hx) hz)

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
hst : Disjoint (Subtype.val ⁻¹' closure[inst✝] s) (Subtype.val ⁻¹' closure[inst✝] t)
U : Set X
hU : IsOpen[inst✝] U
hsU : closure[inst✝] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst✝] V
htV : closure[inst✝] t ∩ e ⊆ V ∩ e
hUV : Disjoint (Subtype.val ⁻¹' U) (Subtype.val ⁻¹' V)
⊢ s ⊆ U ∩ e

pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
hst : Disjoint (Subtype.val ⁻¹' closure[inst✝] s) (Subtype.val ⁻¹' closure[inst✝] t)
U : Set X
hU : IsOpen[inst✝] U
hsU : closure[inst✝] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst✝] V
htV : closure[inst✝] t ∩ e ⊆ V ∩ e
hUV : Disjoint (Subtype.val ⁻¹' U) (Subtype.val ⁻¹' V)
⊢ t ⊆ V ∩ e

pp: case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
hst : Disjoint (Subtype.val ⁻¹' closure[inst✝] s) (Subtype.val ⁻¹' closure[inst✝] t)
U : Set X
hU : IsOpen[inst✝] U
hsU : closure[inst✝] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst✝] V
htV : closure[inst✝] t ∩ e ⊆ V ∩ e
hUV : Disjoint (Subtype.val ⁻¹' U) (Subtype.val ⁻¹' V)
⊢ Disjoint (U ∩ e) (V ∩ e)

Tactic:
· intro x hx
    exact hsU ⟨subset_closure hx, fun h => hsT.notMem_of_mem_left hx h.2⟩

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
hst : Disjoint (Subtype.val ⁻¹' closure[inst✝] s) (Subtype.val ⁻¹' closure[inst✝] t)
U : Set X
hU : IsOpen[inst✝] U
hsU : closure[inst✝] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst✝] V
htV : closure[inst✝] t ∩ e ⊆ V ∩ e
hUV : Disjoint (Subtype.val ⁻¹' U) (Subtype.val ⁻¹' V)
⊢ t ⊆ V ∩ e

case refine_3
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hSt : Disjoint (closure[inst✝] s) t
hsT : Disjoint s (closure[inst✝] t)
e : Set X := (closure[inst✝] s ∩ closure[inst✝] t)ᶜ
h : NormalSpace ↑e
he : IsOpen[inst✝] e
hst : Disjoint (Subtype.val ⁻¹' closure[inst✝] s) (Subtype.val ⁻¹' closure[inst✝] t)
U : Set X
hU : IsOpen[inst✝] U
hsU : closure[inst✝] s ∩ e ⊆ U ∩ e
V : Set X
hV : IsOpen[inst✝] V
htV : closure[inst✝] t ∩ e ⊆ V ∩ e
hUV : Disjoint (Subtype.val ⁻¹' U) (Subtype.val ⁻¹' V)
⊢ Disjoint (U ∩ e) (V ∩ e)
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
H : ∀ (s : Set X), IsOpen[inst✝] s → IsLindelof s
⊢ HereditarilyLindelofSpace X

Tactic:
by
  refine ⟨fun s _ ↦ isLindelof_of_countable_subcover fun U U_open hU ↦ ?_⟩
  obtain ⟨t, t_count, ht⟩ := H (⋃ i, U i) (isOpen_iUnion U_open)
    |>.elim_countable_subcover U U_open subset_rfl
  exact ⟨t, t_count, hU.trans ht⟩

Goal state after:
Module: Mathlib.Topology.DenseEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
e : α → β
de : IsDenseEmbedding e
p : α → Prop
⊢ closure[instTopologicalSpaceSubtype] (range (subtypeEmb p e)) = univ

Tactic:
ext ⟨x, hx⟩
      rw [image_eq_range] at hx
      simpa [closure_subtype, ← range_comp, (· ∘ ·)]

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
I : Set ι
hI : I.Countable
f : ι → Set X
hf : ∀ i ∈ I, IsOpen[inst✝] (f i)
⊢ ∀ t ∈ f '' I, IsOpen[inst✝] t

Tactic:
rwa [forall_mem_image]

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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
x✝ : ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
S : Set (Set X)
hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst✝] x ∧ IsNowhereDense x
hc : (compl '' S).Countable
hsub : s ⊆ ⋃₀ S
⊢ S.Countable

Tactic:
← compl_compl_image S

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
x✝ : ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
S : Set (Set X)
hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst✝] x ∧ IsNowhereDense x
hc : (compl '' S).Countable
hsub : s ⊆ ⋃₀ S
⊢ (compl '' compl '' S).Countable
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: case refine_1
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst✝¹] (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
⊢ ∀ s ∈ f '' S, IsOpen[inst✝¹] s

Tactic:
rwa [forall_mem_image]

Goal state after:
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: case refine_2
X : Type u_1
α : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
S : Set α
f : α → Set X
ho : ∀ s ∈ S, IsOpen[inst✝¹] (f s)
hS : S.Countable
hd : ∀ s ∈ S, Dense (f s)
⊢ ∀ s ∈ f '' S, Dense s

Tactic:
rwa [forall_mem_image]

Goal state after: