mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.ToIntervalMod

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

Tactic:
toIcoMod_add_zsmul

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp a b = toIcoMod hp a b
Module: Mathlib.Algebra.Order.ToIntervalMod

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

Tactic:
by
  rw [add_comm, toIcoMod_add_zsmul]

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp a (b + -m • p) = toIcoMod hp a b

Tactic:
toIcoMod_add_zsmul

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp a b = toIcoMod hp a b
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ x, map g f ≤ 𝓝 x
⊢ f.limUnder g = Classical.choice hX

Tactic:
limUnder,

Goal state after:
X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ x, map g f ≤ 𝓝 x
⊢ (map g f).lim = Classical.choice hX
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
C : Set X
⊢ ClusterPt x (𝓟 C) ↔ x ∈ C ∨ AccPt x (𝓟 C)

Tactic:
constructor
  · intro h
    by_contra! hc
    rw [accPt_principal_iff_clusterPt] at hc
    simp_all only [not_false_eq_true, sdiff_singleton_eq_self, not_true_eq_false, hc.1]
  · rintro (h | h)
    · exact clusterPt_principal_iff.mpr fun _ mem ↦ ⟨x, ⟨mem_of_mem_nhds mem, h⟩⟩
    · exact h.clusterPt

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure[inst✝] s) t

Tactic:
rw [disjoint_principal_left, ← subset_interior_iff_mem_nhdsSet, interior_compl,
    subset_compl_iff_disjoint_left]

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 : IsEmbedding g
hgf : IsClosedEmbedding (g ∘ f)
⊢ IsClosed[inst✝¹] (range f)

Tactic:
by
    convert! hg.isClosed_preimage _ hgf.isClosed_range
    rw [range_comp, hg.injective.preimage_image]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
a : { x // x ∈ s }
t u : Set { x // x ∈ s }
⊢ t ∈ 𝓝[u] a ↔ t ∈ comap Subtype.val (𝓝[Subtype.val '' u] ↑a)

Tactic:
rw [nhdsWithin, nhds_subtype, principal_subtype, ← comap_inf, ← nhdsWithin]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s
hg : ∀ s ∈ 𝓝 y, ∃ᶠ (a : β) in lb, g a ∈ s
s : Set X
t : Set Y
hs : (s, t).1 ∈ 𝓝 x
ht : (s, t).2 ∈ 𝓝 y
⊢ ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, Prod.map f g (x, y) ∈ id (s, t).1 ×ˢ id (s, t).2

Tactic:
exact (hf s hs).mono fun x hx ↦ (hg t ht).mono fun y hy ↦ ⟨hx, hy⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
hs : s ∈ b
⊢ IsOpen[generateFrom b] s

Tactic:
exact .basic s hs

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝ : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → A i
⊢ (Filter.pi fun i ↦ 𝓝 (Pi.map f x i)) ≤ Filter.pi fun i ↦ map (f i) (𝓝 (x i))

Tactic:
exact Filter.pi_mono fun i ↦ (hfo i).nhds_le _

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s s' : Set α
t : Set β
hf : ContinuousOn f s'
hs' : s' ∈ 𝓝ˢ s
hst : MapsTo f s t
V : Set α
hV : IsOpen[inst✝¹] V
hsV : s ⊆ V
hVs' : V ⊆ s'
U : Set β
hU : IsOpen[inst✝] U ∧ t ⊆ U
x✝ : α
h : x✝ ∈ V ∩ f ⁻¹' U
⊢ x✝ ∈ f ⁻¹' U

Tactic:
exact mem_of_mem_inter_right h

Goal state after:
Module: Mathlib.Topology.Constructions

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

Tactic:
by
  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 ⟨I, fun a => eval a '' (I : Set ι).pi fun a => (h1 a).choose, fun i hi => ?_, ?_⟩
    · simp_rw [eval_image_pi (Finset.mem_coe.mpr hi)
          (pi_nonempty_iff.mpr fun i => ⟨_, fun _ => (h1 i).choose_spec.2.2⟩)]
      exact (h1 i).choose_spec.2
    · exact Subset.trans
        (pi_mono fun i hi => (eval_image_pi_subset hi).trans (h1 i).choose_spec.1) h2
  · rintro ⟨I, t, ⟨h1, h2⟩⟩
    classical
    refine ⟨I, fun a => ite (a ∈ I) (t a) univ, fun i => ?_, ?_⟩
    · by_cases hi : i ∈ I
      · use t i
        simp_rw [if_pos hi]
        exact ⟨Subset.rfl, (h1 i) hi⟩
      · use univ
        simp_rw [if_neg hi]
        exact ⟨Subset.rfl, isOpen_univ, mem_univ _⟩
    · rw [← univ_pi_ite]
      simp only [← ite_and, ← Finset.mem_coe, and_self_iff, univ_pi_ite, h2]

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)
val✝ : Fintype ι
a : (a : ι) → A a
x✝¹ : a ∈ s
x✝ : ∃ u, (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s
u : (a : ι) → Set (A a)
h1 : ∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1
right✝ : univ.pi u ⊆ s
⊢ (↑Finset.univ).pi u ⊆ s

Tactic:
Finset.coe_univ

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
a : (a : ι) → A a
x✝¹ : a ∈ s
x✝ : ∃ u, (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s
u : (a : ι) → Set (A a)
h1 : ∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1
right✝ : univ.pi u ⊆ s
⊢ univ.pi u ⊆ s
Module: Mathlib.Topology.Bases

Goal state before:
pp: β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
⊢ IsTopologicalBasis {S | ∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i}

Tactic:
convert! IsTopologicalBasis.iInf (fun i ↦ (cond i).induced (f i)) with S

Goal state after:
β : Type u_1
ι : Type u_2
X : ι → Type u_3
t : (i : ι) → TopologicalSpace (X i)
T : (i : ι) → Set (Set (X i))
cond : ∀ (i : ι), IsTopologicalBasis (T i)
f : (i : ι) → β → X i
S : Set β
⊢ (∃ U F, (∀ i ∈ F, U i ∈ T i) ∧ S = ⋂ i ∈ F, f i ⁻¹' U i) ↔
    ∃ U F, (∀ i ∈ F, U i ∈ preimage (f i) '' T i) ∧ S = ⋂ i ∈ F, U i
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
m : α → β
s : Set α
g : Ultrafilter β
h : m '' s ∈ g
f : Filter α := Filter.comap m ↑g ⊓ 𝓟 s
this : f.NeBot
⊢ Filter.map m (Filter.comap m ↑g) ⊓ Filter.map m (𝓟 s) = Filter.map m (Filter.comap m ↑g) ⊓ 𝓟 (m '' s)

Tactic:
by rw [map_principal]

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Basic

Goal state before:
pp: α : Type u
β : Type v
f : Ultrafilter α
is : Set β
s : β → Set α
his : is.Finite
⊢ ⋃ i ∈ is, s i ∈ f ↔ ∃ i ∈ is, s i ∈ f

Tactic:
simp only [← sUnion_image, finite_sUnion_mem_iff (his.image s), exists_mem_image]

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

Goal state before:
pp: α : Type u_1
l l' : Filter α
p : α → Prop
⊢ (∃ s ∈ l, ∀ᶠ (x : α) in l', x ∈ s → p x) ↔ ∃ s ∈ l, ∃ t ∈ l', ∀ x ∈ t, x ∈ s → p x

Tactic:
by simp only [eventually_iff_exists_mem]

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

Goal state before:
pp: 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✝² : Finite ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
⊢ ⋃ n, (fun n ↦ univ.pi fun i ↦ compactCovering (X i) n) n = univ

Tactic:
rw [iUnion_univ_pi_of_monotone]

Goal state after:
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✝² : Finite ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
⊢ (univ.pi fun i ↦ ⋃ j, compactCovering (X i) j) = univ

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✝² : Finite ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
⊢ ∀ (i : ι), Monotone (compactCovering (X i))
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 j k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
⊢ ∃ z, (fun x1 x2 ↦ x1 ⊇ x2) (V i ∩ Wᶜ) (V z ∩ Wᶜ) ∧ (fun x1 x2 ↦ x1 ⊇ x2) (V j ∩ Wᶜ) (V z ∩ Wᶜ)

Tactic:
refine ⟨k, ⟨fun x => ?_, fun x => ?_⟩⟩

Goal state after:
case refine_1
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 k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
⊢ x ∈ V k ∩ Wᶜ → x ∈ V i ∩ Wᶜ

case refine_2
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 k : ι
hki : V i ⊇ V k
hkj : V j ⊇ V k
x : X
⊢ x ∈ V k ∩ Wᶜ → x ∈ V j ∩ Wᶜ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ Disjoint (cocompact X) f ↔ ∃ K ∈ f, IsCompact K

Tactic:
simp_rw [hasBasis_cocompact.disjoint_iff_left, compl_compl]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
f : Filter X
⊢ (∃ i, IsCompact i ∧ i ∈ f) ↔ ∃ K ∈ f, IsCompact K
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case refine_2
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ Q ⊆ P, Q.Finite → (⋂₀ (compl '' Q)).Nonempty
Q : Set (Set X)
hQP : Q ⊆ compl '' P
hQ : Q.Finite
⊢ (⋂₀ Q).Nonempty

Tactic:
· replace hP : Q ⊆ compl '' P → (compl '' Q).Finite → (⋂₀ Q).Nonempty := by
      simpa [← compl_involutive.image_eq_preimage_symm] using hP (compl '' Q)
    exact hP hQP (hQ.image _)

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) → X i)
hs : IsClosed[topologicalSpace] s
⊢ IsCompact s ↔ ∀ (i : ι), IsCompact (eval i '' s)

Tactic:
constructor <;> intro H
  · exact fun i ↦ H.image <| continuous_apply i
  · exact IsCompact.of_isClosed_subset (isCompact_univ_pi H) hs (subset_pi_eval_image univ s)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
s : Set α
a : α
⊢ 𝓝[s ∩ Iic a] a ⊔ 𝓝[s ∩ Ici a] a = 𝓝[s] a

Tactic:
rw [← nhdsWithin_union, ← inter_union_distrib_left, Iic_union_Ici, inter_univ]

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

Goal state before:
pp: α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
a : α
⊢ 𝓝[≠] a ≤ cofinite

Tactic:
refine le_cofinite_iff_compl_singleton_mem.mpr fun x ↦ ?_
  rcases eq_or_ne a x with rfl | hx
  exacts [self_mem_nhdsWithin, eventually_ne_nhdsWithin hx]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsDiscrete s
ht✝ : IsDiscrete t
hsc : IsClosed[inst✝] s
ht : IsClosed[inst✝] t
⊢ ∀ (i : Bool), IsDiscrete (bif i then s else t)

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsDiscrete s
ht✝ : IsDiscrete t
hsc : IsClosed[inst✝] s
ht : IsClosed[inst✝] t
⊢ ∀ (i : Bool), IsClosed[inst✝] (bif i then s else t)

Tactic:
by simp [*]

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
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝¹] (U i)
hKU : closure[inst✝¹] K ⊆ ⋃ i, U i
⊢ ∃ t, closure[inst✝¹] K ⊆ ⋃ i ∈ t, U i

Tactic:
rcases hK.elim_finite_subcover U hUo (subset_closure.trans hKU) with ⟨t, ht⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen[inst✝¹] (U i)
hKU : closure[inst✝¹] K ⊆ ⋃ i, U i
t : Finset ι✝
ht : K ⊆ ⋃ i ∈ t, U i
⊢ ∃ t, closure[inst✝¹] K ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case inl
α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
z : α
zs : z ∈ s
zu : z ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
xs : x ∈ s
xu : x ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
| inl xu =>

Goal state after:
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 : Set (Set α)
hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l
hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l
S : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s | sᶜ ∈ l}
s : Set α
hs : ∃ x ∈ S, xᶜ = s
⊢ s ∈ l

Tactic:
rcases hs with ⟨t, ht, rfl⟩

Goal state after:
case refine_1
ι : 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 : Set (Set α)
hSc : S.Countable
hSp : S ⊆ {s | sᶜ ∈ l}
t : Set α
ht : t ∈ S
⊢ tᶜ ∈ l
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) × X i
hf : Continuous[inst✝², instTopologicalSpaceSigma] f
⊢ ∃ i g, Continuous[inst✝², inst✝ i] g ∧ f = Sigma.mk i ∘ g

Tactic:
obtain ⟨i, hi⟩ : ∃ i, range f ⊆ range (.mk i) := by
    rcases Sigma.isConnected_iff.1 (isConnected_range hf) with ⟨i, s, -, hs⟩
    exact ⟨i, hs.trans_subset (image_subset_range _ _)⟩

Goal state after:
α : Type u
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : ConnectedSpace α
inst✝ : (i : ι) → TopologicalSpace (X i)
f : α → (i : ι) × X i
hf : Continuous[inst✝², instTopologicalSpaceSigma] f
i : ι
hi : range f ⊆ range (Sigma.mk i)
⊢ ∃ i g, Continuous[inst✝², inst✝ i] g ∧ f = Sigma.mk i ∘ g
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : PreconnectedSpace α
P : α → α → Prop
inst✝ : Std.Symm P
h : ∀ (x : α), ∀ᶠ (y : α) in 𝓝 x, P x y
h' : IsTrans α P
x y : α
⊢ P x y

Tactic:
by
  refine PreconnectedSpace.induction₂' P (fun z ↦ ?_) h' x y
  filter_upwards [h z] with a ha
  exact ⟨ha, symm ha⟩

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

Goal state before:
pp: 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

Tactic:
intro u v hu hv hs huv

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: 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

Tactic:
intro u v hu hv hs huv

Goal state after:
case mp
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : IsPreconnected s
u v : Set α
hu : IsClosed[inst✝] u
hv : IsClosed[inst✝] v
hs : s ⊆ u ∪ v
huv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v
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
⊢ closure[inst✝¹] s ⊆ nhdsKer s

pp: case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set X
hs : IsCompact s
⊢ nhdsKer s ⊆ closure[inst✝¹] s

Tactic:
· rw [nhdsKer, ← hs.lift'_closure_nhdsSet]
    simp +contextual [Filter.lift', Filter.lift, closure_mono, subset_of_mem_nhdsSet]

Goal state after:
case a
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
s : Set X
hs : IsCompact s
⊢ nhdsKer s ⊆ closure[inst✝¹] s
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: 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
x : { x // x ∈ e }
hxs : x ∈ Subtype.val ⁻¹' closure[inst✝] s
hxt : x ∈ Subtype.val ⁻¹' closure[inst✝] t
⊢ False

Tactic:
exact x.2 ⟨hxs, hxt⟩

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
⊢ comap f (coLindelof Y) ≤ coLindelof X

Tactic:
by
  rw [(hasBasis_coLindelof.comap f).le_basis_iff hasBasis_coLindelof]
  intro t ht
  refine ⟨f '' t, ht.image hf, ?_⟩
  simpa using t.subset_preimage_image f

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ TotallyDisconnectedSpace ↑s ↔ IsTotallyDisconnected s

Tactic:
rw [← IsEmbedding.subtypeVal.isTotallyDisconnected_range, Subtype.range_val]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ ∀ t ∈ image f '' T, IsNowhereDense t

Tactic:
case =>

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsInducing f
s : Set X
T : Set (Set X)
isNowhereDense : ∀ t ∈ T, IsNowhereDense t
countable : T.Countable
cover : s ⊆ ⋃₀ T
⊢ f '' s ⊆ ⋃₀ (image f '' T)

Tactic:
case =>

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

Goal state before:
pp: case succ
α : Type ua
inst✝ : UniformSpace α
n✝ : ℕ
ihn : ∀ {s : SetRel α α}, s ∈ 𝓤 α → ∀ᶠ (t : SetRel α α) in (𝓤 α).smallSets, t ⊆ s ∧ (fun x ↦ t ○ x)^[n✝] t ⊆ s
s : SetRel α α
hs : s ∈ 𝓤 α
t : Set (α × α)
htU : t ∈ 𝓤 α
hts : t ○ t ⊆ s
U : SetRel α α
hU : U ⊆ t ∧ (fun x ↦ U ○ x)^[n✝] U ⊆ t
this : SetRel.IsRefl t
⊢ U ⊆ s ∧ U ○ (fun x ↦ U ○ x)^[n✝] U ⊆ s

Tactic:
exact ⟨hU.1.trans <| SetRel.left_subset_comp.trans hts,
     (SetRel.comp_subset_comp hU.1 hU.2).trans hts⟩

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf✝ :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (f x.2, F x.1 x.2) ∈ id i
hfg : ∀ x ∈ s, Inseparable (f x) (g x)
i : SetRel β β
hi : i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i
hf : ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (f x.2, F x.1 x.2) ∈ id i
⊢ ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (g x.2, F x.1 x.2) ∈ id i

Tactic:
rw [eventually_prod_principal_iff] at hf ⊢

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
g : α → β
hf✝ :
  ∀ (i : SetRel β β),
    i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i → ∀ᶠ (x : ι × α) in p ×ˢ 𝓟 s, (f x.2, F x.1 x.2) ∈ id i
hfg : ∀ x ∈ s, Inseparable (f x) (g x)
i : SetRel β β
hi : i ∈ 𝓤 β ∧ IsOpen[instTopologicalSpaceProd] i
hf : ∀ᶠ (x : ι) in p, ∀ y ∈ s, (f (x, y).2, F (x, y).1 (x, y).2) ∈ id i
⊢ ∀ᶠ (x : ι) in p, ∀ y ∈ s, (g (x, y).2, F (x, y).1 (x, y).2) ∈ id i
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
s : Set (UniformSpace α)
⊢ (sInf s).toTopologicalSpace = ⨅ i ∈ s, i.toTopologicalSpace

Tactic:
sInf_eq_iInf

Goal state after:
α : Type ua
s : Set (UniformSpace α)
⊢ (⨅ a ∈ s, a).toTopologicalSpace = ⨅ i ∈ s, i.toTopologicalSpace
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
U : (x : α) → x ∈ K → Set α
hK : IsCompact K
hU : ∀ (x : α) (hx : x ∈ K), U x hx ∈ 𝓝 x
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ y, ball x V ⊆ U ↑y ⋯

Tactic:
rcases lebesgue_number_lemma (U := fun x : K => interior (U x x.2)) hK (fun _ => isOpen_interior)
    (fun x hx => mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 (hU x hx)⟩) with ⟨V, V_uni, hV⟩
  exact ⟨V, V_uni, fun x hx => (hV x hx).imp fun _ hy => hy.trans interior_subset⟩

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

Goal state before:
pp: γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
this : CompactSpace γ
⊢ CompactSpace γ

Tactic:
h'

Goal state after:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
this : CompactSpace γ
⊢ CompactSpace γ
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
this✝ : CompactSpace γ
this : CompactSpace γ
⊢ ⨆ x, 𝓝 (x, x) = ⨆ x, 𝓝 (x, x)

Tactic:
h'

Goal state after:
γ : Type uc
t : TopologicalSpace γ
inst✝ : CompactSpace γ
u u' : UniformSpace γ
h : u.toTopologicalSpace = t
h' : u'.toTopologicalSpace = t
this✝ : CompactSpace γ
this : CompactSpace γ
⊢ ⨆ x, 𝓝 (x, x) = ⨆ x, 𝓝 (x, x)
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : TopologicalSpace β
K : Set β
h'f : HasCompactMulSupport f
hf : Continuous[inst✝², inst✝] f
hk : IsClosed[inst✝] K
h'k : 1 ∉ K
x : α
hx : x ∈ f ⁻¹' K
⊢ x ∈ mulTSupport f

Tactic:
apply subset_mulTSupport

Goal state after:
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : TopologicalSpace β
K : Set β
h'f : HasCompactMulSupport f
hf : Continuous[inst✝², inst✝] f
hk : IsClosed[inst✝] K
h'k : 1 ∉ K
x : α
hx : x ∈ f ⁻¹' K
⊢ x ∈ mulSupport f