mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
f : Filter α
h : Set α → Set β
ι : Sort u_5
p : ι → Prop
s : ι → Set α
hf : f.HasBasis p s
hh : Monotone h
t : Set β
⊢ (∃ i, p i ∧ ∃ x, True ∧ h (s i) ⊆ t) ↔ ∃ i, p i ∧ (h ∘ s) i ⊆ t

Tactic:
simp only [exists_const, true_and, comp]

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
h : toIocMod hp a b = a + p
⊢ b = a + (toIocDiv hp a b • p + p)

Tactic:
add_left_comm,

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
h : toIocMod hp a b = a + p
⊢ b = toIocDiv hp a b • p + (a + p)
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : Dense s
ht : IsOpen[inst✝] t
⊢ t = t ∩ closure[inst✝] s

Tactic:
hs.closure_eq,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : Dense s
ht : IsOpen[inst✝] t
⊢ t = t ∩ univ
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
hs : Dense s
⊢ range f ⊆ closure[inst✝] (f '' s)

Tactic:
by
  rw [← image_univ, ← hs.closure_eq]
  exact image_closure_subset_closure_image hf

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hU : IsOpen[inst✝] s
⊢ t ⊆ interior s ↔ t ⊆ s

Tactic:
hU.interior_eq

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
hU : IsOpen[inst✝] s
⊢ t ⊆ s ↔ t ⊆ s
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
T : TopologicalSpace α
f : β → α
a : β
s : Set β
⊢ s ∈ 𝓝 a ↔ ∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s

Tactic:
let := T.induced f
  simp_rw [mem_nhds_iff, isOpen_induced_iff]
  constructor
  · rintro ⟨u, usub, ⟨v, openv, rfl⟩, au⟩
    exact ⟨v, ⟨v, Subset.rfl, openv, au⟩, usub⟩
  · rintro ⟨u, ⟨v, vsubu, openv, amem⟩, finvsub⟩
    exact ⟨f ⁻¹' v, (Set.preimage_mono vsubu).trans finvsub, ⟨⟨v, openv, rfl⟩, amem⟩⟩

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedEmbedding g
⊢ IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f

Tactic:
simp_rw [isClosedEmbedding_iff, hg.isEmbedding.of_comp_iff, Set.range_comp,
    ← hg.isClosed_iff_image_isClosed]

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case refine_1
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
h : IsOpenMap (Prod.map f g)
⊢ IsOpenMap f

pp: case refine_2
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
h : IsOpenMap (Prod.map f g)
⊢ IsOpenMap g

Tactic:
· rw [(isOpenQuotientMap_fst (Y := Z)).isOpenMap_iff]
    exact isOpenMap_fst.comp h

Goal state after:
case refine_2
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace Y
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace W
inst✝¹ : Nonempty X
inst✝ : Nonempty Z
f : X → Y
g : Z → W
h : IsOpenMap (Prod.map f g)
⊢ IsOpenMap g
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u_5
Y : Type u_6
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set Y
inst✝ : DiscreteTopology ↑s
f : X → Y
hc : Continuous[inst✝², inst✝¹] f
hinj : Injective f
⊢ MapsTo f (f ⁻¹' s) s

Tactic:
exact fun _ x ↦ x

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
g : β → α
x : β
s : Set β
h : LeftInvOn f g s
hx : f (g x) = x
hf : ContinuousWithinAt f (g '' s) (g x)
hg : ContinuousWithinAt g s x
⊢ map g (𝓝[s] x) = 𝓝[g '' s] g x

Tactic:
by
  apply le_antisymm
  · exact hg.tendsto_nhdsWithin (mapsTo_image _ _)
  · have A : g ∘ f =ᶠ[𝓝[g '' s] g x] id :=
      h.rightInvOn_image.eqOn.eventuallyEq_of_mem self_mem_nhdsWithin
    refine le_map_of_right_inverse A ?_
    simpa only [hx] using hf.tendsto_nhdsWithin (h.mapsTo (surjOn_image _ _))

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
s : Set β
x : α
⊢ map f (𝓝[f ⁻¹' s] x) = 𝓝[s] f x

Tactic:
rw [hf.isEmbedding.map_nhdsWithin_eq, image_preimage_eq_inter_range]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
hf : IsOpenEmbedding f
s : Set β
x : α
⊢ 𝓝[s ∩ range f] f x = 𝓝[s] f x
Module: Mathlib.Order.ZornAtoms

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
⊢ IsCoatomic α

Tactic:
refine ⟨fun x => le_top.eq_or_lt.imp_right fun hx => ?_⟩

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
⊢ ∃ a, IsCoatom a ∧ x ≤ a
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
s t : Set α
⊢ IsSeparable (s ∪ t) ↔ IsSeparable s ∧ IsSeparable t

Tactic:
simp [union_eq_iUnion, and_comm]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
⊢ IsOpen[Pi.topologicalSpace] s ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s

Tactic:
cases nonempty_fintype ι
  rw [isOpen_iff_nhds]
  simp_rw [le_principal_iff, nhds_pi, Filter.mem_pi', mem_nhds_iff]
  refine forall₂_congr fun a _ => ⟨?_, ?_⟩
  · rintro ⟨I, t, ⟨h1, h2⟩⟩
    refine
      ⟨fun i => (h1 i).choose,
        ⟨fun i => (h1 i).choose_spec.2,
          (pi_mono fun i _ => (h1 i).choose_spec.1).trans (Subset.trans ?_ h2)⟩⟩
    rw [← pi_inter_compl (I : Set ι)]
    exact inter_subset_left
  · exact fun ⟨u, ⟨h1, _⟩⟩ =>
      ⟨Finset.univ, u, ⟨fun i => ⟨u i, ⟨rfl.subset, h1 i⟩⟩, by rwa [Finset.coe_univ]⟩⟩

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:

Tactic:
𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a := by
      rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
    _ = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, (f i ∩ U)] a := by
      simp only [mem_ofPred_eq, iUnion_nonempty_self]
    _ = ⨆ i ∈ {j | (f j ∩ U).Nonempty}, 𝓝[f i ∩ U] a := nhdsWithin_biUnion hfin _ _
    _ ≤ ⨆ i, 𝓝[f i ∩ U] a := iSup₂_le_iSup _ _
    _ ≤ ⨆ i, 𝓝[f i] a := iSup_mono fun i ↦ nhdsWithin_mono _ inter_subset_left

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: case pos
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∈ closure[inst✝¹] (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

pp: case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∉ closure[inst✝¹] (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))

Tactic:
· exact hc i _ hx

Goal state after:
case neg
ι : Type u_1
X : Type u_4
Y : Type u_5
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : ι → Set X
g : X → Y
hf : LocallyFinite f
hc : ∀ (i : ι), ∀ x ∈ closure[inst✝¹] (f i), ContinuousWithinAt g (f i) x
x : X
i : ι
hx : x ∉ closure[inst✝¹] (f i)
⊢ Tendsto g (𝓝[f i] x) (𝓝 (g x))
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case refine_3
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs✝ : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx✝ : x ∈ K
u : Set X
v : Set Y
hs : (u, v).1 ×ˢ id (u, v).2 ⊆ s
hv : (u, v).2 ∈ l
hx : x ∈ (u, v).1
huo : IsOpen[inst✝] (u, v).1
⊢ ∃ t ∈ 𝓝[K] x, s ∈ 𝓝ˢ t ×ˢ l

Tactic:
refine ⟨u, nhdsWithin_le_nhds (huo.mem_nhds hx), mem_of_superset ?_ hs⟩

Goal state after:
case refine_3
X : Type u
inst✝ : TopologicalSpace X
K : Set X
Y : Type u_2
l : Filter Y
s : Set (X × Y)
hK : IsCompact K
hs✝ : ∀ x ∈ K, s ∈ 𝓝 x ×ˢ l
x : X
hx✝ : x ∈ K
u : Set X
v : Set Y
hs : (u, v).1 ×ˢ id (u, v).2 ⊆ s
hv : (u, v).2 ∈ l
hx : x ∈ (u, v).1
huo : IsOpen[inst✝] (u, v).1
⊢ (u, v).1 ×ˢ id (u, v).2 ∈ 𝓝ˢ u ×ˢ l
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ : X
K : Set Y
hK : IsCompact K
P : X → Y → Prop
hP : ∀ y ∈ K, ∀ᶠ (z : X × Y) in 𝓝 (x₀, y), P z.1 z.2
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∀ y ∈ K, P x y

Tactic:
simp only [nhds_prod_eq, ← eventually_iSup, ← hK.prod_nhdsSet_eq_biSup] at hP
  exact hP.curry.mono fun _ h ↦ h.self_of_nhdsSet

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

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Finite
hf : ∀ i ∈ s, IsCompact (f i)
l : Ultrafilter X
i : ι
his : i ∈ s
hi : f i ∈ l
x : X
hxi : x ∈ f i
hlx : ↑l ≤ 𝓝 x
⊢ ∃ x ∈ ⋃ i ∈ s, f i, ↑l ≤ 𝓝 x

Tactic:
exact ⟨x, mem_iUnion₂.2 ⟨i, his, hxi⟩, hlx⟩

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
⊢ ∃ i, V i ⊆ U

Tactic:
obtain ⟨W, hsubW, W_op, hWU⟩ := exists_open_set_nhds hU

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
⊢ ∃ i, V i ⊆ U
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
α : Type u_4
inst✝ : TopologicalSpace X
x : X
f : X → α
hf : ∀ (x y : X), (x ~ᵢ y) → f x = f y
s : Set (SeparationQuotient X)
l : Filter α
⊢ Tendsto (lift f hf) (𝓝[s] mk x) l ↔ Tendsto f (𝓝[mk ⁻¹' s] x) l

Tactic:
by
  simp only [← map_mk_nhdsWithin_preimage, tendsto_map'_iff, lift_comp_mk]

Goal state after:
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
r : X → X → Prop
inst✝ : CompactSpace X
⊢ IsCompact univ

Tactic:
by
    rw [← range_quot_mk]
    exact isCompact_range continuous_quot_mk

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsDiscrete s ↔ ∀ x ∈ s, 𝓝[s] x = pure x

Tactic:
simp [isDiscrete_iff_discreteTopology, discreteTopology_iff_isOpen_singleton,
    isOpen_singleton_iff_nhds_eq_pure, nhds_induced,
    ← (Filter.map_injective Subtype.val_injective).eq_iff,
    Filter.map_comap, nhdsWithin]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h₂.h
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ).Nonempty

Tactic:
· rw [Set.inter_compl_nonempty_iff]
      exact mt (mem_of_subset_sUnion_irreducibleComponents Z hZ _ hX.sdiff Set.sdiff_subset)
        (Set.notMem_sdiff_of_mem (Set.mem_singleton Z))

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
i✝ : T2Quotient X
x : X
j✝ : T2Quotient X
y : X
h : ¬mk x = mk y
s : Setoid X
hs : T2Space (Quotient s)
hsxy : ⟦x⟧ ≠ ⟦y⟧
⊢ s ∈ {s | T2Space (Quotient s)}

Tactic:
by exact hs

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
⊢ s ∈ codiscreteWithin U ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite

Tactic:
codiscreteWithin_iff_locallyEmptyComplementWithin

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s U : Set X
⊢ (∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ (U \ s)).Finite
Module: Mathlib.Topology.DiscreteSubset

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

Tactic:
codiscreteWithin_iff_locallyEmptyComplementWithin

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s t : Set X
h : t.Subsingleton
⊢ ∀ z ∈ t, ∃ t_1 ∈ 𝓝[≠] z, t_1 ∩ (t \ s) = ∅
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x : X
⊢ {x}ᶜ ∈ codiscreteWithin s

Tactic:
codiscreteWithin_iff_locallyEmptyComplementWithin

Goal state after:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
x : X
⊢ ∀ z ∈ s, ∃ t ∈ 𝓝[≠] z, t ∩ (s \ {x}ᶜ) = ∅
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ T1Space (SeparationQuotient X) ↔ R0Space X

Tactic:
rw [r0Space_iff, ((t1Space_TFAE (SeparationQuotient X)).out 0 9 :)]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ (∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y) ↔ Std.Symm Specializes
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
ι : Type u_1
F : Filter ι
inst✝³ : F.NeBot
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
a : α
f : ι → α
hlt : ∀ (i : ι), f i < a
hlim : Tendsto f F (𝓝 a)
⊢ ⋃ i, Iic (f i) = Iio a

Tactic:
have obs : a ∉ range f := by
    rw [mem_range]
    rintro ⟨i, rfl⟩
    exact (hlt i).false
  rw [← biUnion_range, (IsLUB.range_of_tendsto (le_of_lt <| hlt ·) hlim).biUnion_Iic_eq_Iio obs]

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

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : PredOrder α
a : α
⊢ 𝓝[≥] a = 𝓝 a

Tactic:
rw [← nhdsLT_sup_nhdsGE, PredOrder.nhdsLT, bot_sup_eq]

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

Goal state before:
pp: case refl
α : 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
i : ι
hi : i ∈ t
j : ι
hj : i ∈ t
⊢ ∃ p ⊆ t, i ∈ p ∧ i ∈ p ∧ IsPreconnected (⋃ j ∈ p, s j)

Tactic:
| refl =>

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

Goal state before:
pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝ : CountableInterFilter l✝
l : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
s t : Set α
ht : s ∈ {s | sᶜ ∈ l}
hsub : s ⊆ t
⊢ t ∈ {s | sᶜ ∈ l}

Tactic:
rw [mem_ofPred_eq]
    rw [← compl_subset_compl] at hsub
    exact hmono sᶜ ht tᶜ hsub

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

Goal state before:
pp: ι : 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
s t : (s : Set α) → s ∈ S → Set α
hst : ∀ (s_1 : Set α) (a : s_1 ∈ S), s_1 = s s_1 a ∩ t s_1 a
hs : ⋂ i, ⋂ (h : i ∈ S), s i h ∈ l₁
ht : ⋂ i, ⋂ (h : i ∈ S), t i h ∈ l₂
i : Set α
hi : i ∈ S
⊢ (⋂ i, ⋂ (h : i ∈ S), s i h) ∩ ⋂ i, ⋂ (h : i ∈ S), t i h ⊆ s i hi ∩ t i hi

Tactic:
apply inter_subset_inter <;> exact iInter_subset_of_subset i (iInter_subset _ _)

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

Goal state before:
pp: case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : ¬(s ∩ (u ∩ v)).Nonempty → ¬(s ∩ v).Nonempty
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
simp_rw [Set.not_nonempty_iff_eq_empty, ← Set.disjoint_iff_inter_eq_empty,
      disjoint_iff_inter_eq_empty.1 huv] at hs

Goal state after:
case inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : Disjoint u v
hsuv : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hs : Disjoint s ∅ → Disjoint s v
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst✝] (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
⊢ ∃ t, t.Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ t, U i_1

Tactic:
have hiU : ∀ i ∈ s, f i ⊆ ⋃ i, U i :=
    fun _ is ↦ _root_.subset_trans (subset_biUnion_of_mem is) hUcover

Goal state after:
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
s : Set ι
f : ι → Set X
hs : s.Countable
hf : ∀ i ∈ s, IsLindelof (f i)
i : Type u
U : i → Set X
hU : ∀ (i : i), IsOpen[inst✝] (U i)
hUcover : ⋃ i ∈ s, f i ⊆ ⋃ i, U i
hiU : ∀ i_1 ∈ s, f i_1 ⊆ ⋃ i, U i
⊢ ∃ t, t.Countable ∧ ⋃ i ∈ s, f i ⊆ ⋃ i_1 ∈ t, U i_1
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set (SeparationQuotient X)
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ Disjoint (comap mk (𝓝ˢ s)) (comap mk (𝓝ˢ t))

Tactic:
comap_mk_nhdsSet,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set (SeparationQuotient X)
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ Disjoint (𝓝ˢ (mk ⁻¹' s)) (comap mk (𝓝ˢ t))
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (comap SeparationQuotient.mk (𝓝ˢ s)) (comap SeparationQuotient.mk (𝓝ˢ t))

Tactic:
comap_mk_nhdsSet,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : CompletelyNormalSpace X
inst✝ : R0Space X
s t : Set (SeparationQuotient X)
hd₁ : Disjoint (closure s) t
hd₂ : Disjoint s (closure t)
⊢ Disjoint (𝓝ˢ (SeparationQuotient.mk ⁻¹' s)) (comap SeparationQuotient.mk (𝓝ˢ t))
Module: Mathlib.Topology.Compactness.Lindelof

Goal state before:
pp: case inr
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : HereditarilyLindelofSpace X
ι : Type u_2
inst✝ : Nonempty ι
U : ι → Set X
h : ∀ (i : ι), IsOpen[inst✝²] (U i)
t : Set ι
htc : t.Countable
htu : ⋃ i ∈ t, U i = ⋃ i, U i
t_ne : t.Nonempty
⊢ ∃ k, ⋃ n, U (k n) = ⋃ i, U i

Tactic:
obtain ⟨k, rfl⟩ := htc.exists_eq_range t_ne
    use k
    rwa [biUnion_range] at htu

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

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

Tactic:
refine ⟨fun ⟨S, hS, hc, hsub⟩ ↦ ⟨S, fun s hs ↦ (hS hs).2, ?_, hsub⟩, ?_⟩

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
⊢ S.Countable

case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (∃ S, (∀ t ∈ S, IsNowhereDense t) ∧ S.Countable ∧ s ⊆ ⋃₀ S) →
    ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ u ∪ v
⊢ ⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b

Tactic:
· have H1 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hu hv huv
    rw [union_comm] at H
    have H2 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hv hu huv.symm
    by_cases hxu : x ∈ u <;> [left; right]
    -- The x ∈ u case.
    · suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ u
        from Disjoint.left_le_of_le_sup_right hab (huv.mono this hbv)
      · apply Subset.trans _ s.inter_subset_right
        exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ u, H1, mem_inter H.2.1 hxu⟩
    -- If x ∉ u, we get x ∈ v since x ∈ u ∪ v. The rest is then like the x ∈ u case.
    · have h1 : x ∈ v :=
        (hab.trans (union_subset_union hau hbv) (mem_iInter.2 fun i => i.2.2)).resolve_left hxu
      suffices ⋂ s : { s : Set X // IsClopen s ∧ x ∈ s }, ↑s ⊆ v
        from (huv.symm.mono this hau).left_le_of_le_sup_left hab
      · refine Subset.trans ?_ s.inter_subset_right
        exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ v, H2, mem_inter H.2.1 h1⟩

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

Goal state before:
pp: case pos
X : Type u_1
Y✝ : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y✝
inst✝⁵ : TopologicalSpace W
inst✝⁴ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
ι : Type u_7
inst✝¹ : DecidableEq ι
i : ι
Y : ι → Type u_8
inst✝ : (j : ι) → TopologicalSpace (Y j)
j : ι
h : j = i
⊢ Continuous[instTopologicalSpaceProd, inst✝ j] fun a ↦ ⋯ ▸ a.1

pp: case neg
X : Type u_1
Y✝ : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y✝
inst✝⁵ : TopologicalSpace W
inst✝⁴ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
ι : Type u_7
inst✝¹ : DecidableEq ι
i : ι
Y : ι → Type u_8
inst✝ : (j : ι) → TopologicalSpace (Y j)
j : ι
h : ¬j = i
⊢ Continuous[instTopologicalSpaceProd, inst✝ j] fun a ↦ a.2 ⟨j, h⟩

Tactic:
· subst h
        exact continuous_fst

Goal state after:
case neg
X : Type u_1
Y✝ : Type u_2
W : Type u_3
Z : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y✝
inst✝⁵ : TopologicalSpace W
inst✝⁴ : TopologicalSpace Z
X' : Type u_5
Y' : Type u_6
inst✝³ : TopologicalSpace X'
inst✝² : TopologicalSpace Y'
ι : Type u_7
inst✝¹ : DecidableEq ι
i : ι
Y : ι → Type u_8
inst✝ : (j : ι) → TopologicalSpace (Y j)
j : ι
h : ¬j = i
⊢ Continuous[instTopologicalSpaceProd, inst✝ j] fun a ↦ a.2 ⟨j, h⟩
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
N : β
hN : U N ⊆ s
mn : β × β
hmn : (N, N) ≤ mn
⊢ mn ∈ Prod.map f f ⁻¹' s

Tactic:
obtain ⟨m, n⟩ := mn

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : SemilatticeSup β
inst✝ : Nonempty β
U : β → SetRel α α
hU : ∀ s ∈ 𝓤 α, ∃ n, U n ⊆ s
f : β → α
hf : ∀ ⦃N m n : β⦄, N ≤ m → N ≤ n → (f m, f n) ∈ U N
s : Set (α × α)
hs : s ∈ 𝓤 α
N : β
hN : U N ⊆ s
m n : β
hmn : (N, N) ≤ (m, n)
⊢ (m, n) ∈ Prod.map f f ⁻¹' s