mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: case inr
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this✝ : Nonempty (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
this :
  ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : IsCofiltered J] (d : J) (n : ℕ),
    (sequentialFunctor J).obj (op n) ≤ d →
      Nonempty (CostructuredArrow (sequentialFunctor J) d) →
        ∀ (i j : CostructuredArrow (sequentialFunctor J) d),
          unop i.left ≤ unop j.left → Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
h : unop j.left < unop i.left
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

pp: J✝ : Type u_2
inst✝⁵ : Countable J✝
inst✝⁴ : Preorder J✝
inst✝³ : IsCofiltered J✝
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this : Nonempty (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h : unop i.left ≤ unop j.left
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)

Tactic:
· exact or_comm.1 (this J d n g inferInstance j i (le_of_lt h))

Goal state after:
J✝ : Type u_2
inst✝⁵ : Countable J✝
inst✝⁴ : Preorder J✝
inst✝³ : IsCofiltered J✝
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsCofiltered J
d : J
n : ℕ
g : (sequentialFunctor J).obj (op n) ≤ d
this : Nonempty (CostructuredArrow (sequentialFunctor J) d)
i j : CostructuredArrow (sequentialFunctor J) d
h : unop i.left ≤ unop j.left
⊢ Nonempty (i ⟶ j) ∨ Nonempty (j ⟶ i)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCofilteredLimitsOfSize.{w₂, w₂', v, u} C
inst✝² : UnivLE.{w, w₂}
inst✝¹ : UnivLE.{w', w₂'}
inst✝ : AB5StarOfSize.{w₂, w₂', v, u} C
⊢ AB5StarOfSize.{w, w', v, u} C

Tactic:
have : HasCofilteredLimitsOfSize.{w, w'} C := hasCofilteredLimitsOfSize_of_univLE.{w}
  constructor
  intro J _ _
  have := IsCofiltered.of_equivalence ((ShrinkHoms.equivalence.{w₂} J).trans <|
    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J))
  exact HasExactLimitsOfShape.of_domain_equivalence _ ((ShrinkHoms.equivalence.{w₂} J).trans <|
    Shrink.equivalence.{w₂', w₂} (ShrinkHoms.{w'} J)).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
this : (X : C) → Unique (wideEqualizer id ⟶ X)
⊢ HasInitial C

Tactic:
exact hasInitial_of_unique (wideEqualizer (id : endos → endos))

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ g.unop.left.op.unop ≫ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left

Tactic:
rw [← unop_comp]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
inst✝¹ : Mono f.unop.left.op
inst✝ : Mono g.unop.left.op
h : Subobject.mk f.unop.left.op ≤ Subobject.mk g.unop.left.op
⊢ (Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h ≫ g.unop.left.op).unop = f.unop.left
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
h : IsCoseparator G
α : C ≌ D
⊢ IsCoseparator (α.functor.obj G)

Tactic:
by
  simpa using! ObjectProperty.IsCoseparating.of_equivalence h α

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ IsDetector (op G) ↔ IsCodetector G

Tactic:
IsDetector,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ (ObjectProperty.singleton (op G)).IsDetecting ↔ IsCodetector G
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ IsCodetector (op G) ↔ IsDetector G

Tactic:
IsDetector,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ IsCodetector (op G) ↔ (ObjectProperty.singleton G).IsDetecting
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ IsCodetector (unop G) ↔ IsDetector G

Tactic:
IsDetector,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ IsCodetector (unop G) ↔ (ObjectProperty.singleton G).IsDetecting
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ IsDetector (unop G) ↔ IsCodetector G

Tactic:
IsDetector,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ (ObjectProperty.singleton (unop G)).IsDetecting ↔ IsCodetector G
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
X : C
⊢ (compULiftYonedaIsoULiftYonedaCompLan F).hom.app X ≫
      (natTrans (StructuredArrow.hom Φ)).app (uliftYoneda.{max w v₂, v₁, u₁}.obj X) =
    (StructuredArrow.hom Φ).app X

Tactic:
rw [natTrans_app_uliftYoneda_obj, Iso.hom_inv_id_app_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasProduct fun x ↦ G
h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g
A Z✝ : C
u v : Z✝ ⟶ A
huv : (u ≫ Pi.lift fun f ↦ f) = v ≫ Pi.lift fun f ↦ f
i : A ⟶ G
⊢ u ≫ i = v ≫ i

pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasProduct fun x ↦ G
h : ∀ (A : C), Mono (Pi.lift fun f ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

Tactic:
· simpa using huv =≫ Pi.π _ i

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
G : C
inst✝ : ∀ (A : C), HasProduct fun x ↦ G
h : ∀ (A : C), Mono (Pi.lift fun f ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: case pos
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : IsEmpty X
Z✝ : AddCommGrpCat
g✝ h✝ : Z✝ ⟶ free.obj X
a✝ : g✝ ≫ free.map f = h✝ ≫ free.map f
⊢ g✝ = h✝

Tactic:
apply (IsInitial.isInitialObj free _
        ((Types.initial_iff_empty X).2 hX).some).isZero.eq_of_tgt

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Injective

Goal state before:
pp: case inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
n : ℤ
hn✝ : n ∈ ℤ ∙ 0
hn : n ∈ ⊥
⊢ 0 n = g ⟨n, hn✝⟩

Tactic:
subst hn

Goal state after:
case inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
hn : 0 ∈ ℤ ∙ 0
⊢ 0 0 = g ⟨0, hn⟩
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = #({x ∈ range n | p x})

Tactic:
by
  rw [count, List.countP_eq_length_filter]
  rfl

Goal state after:
Module: Mathlib.Data.Nat.Periodic

Goal state before:
pp: α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f (n % a + (n / a) • a)

Tactic:
hf.nsmul

Goal state after:
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f (n % a)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case a
hp : 0 < 1
h : 1 = 0
⊢ False

Tactic:
exact one_ne_zero h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ ⨅ i, (bif i then f else g).lift' s = ⨅ b, bif b then f.lift' s else g.lift' s

Tactic:
refine iInf_congr ?_

Goal state after:
α : Type u_1
β : Type u_2
f g : Filter α
s : Set α → Set β
hs : ∀ (t₁ t₂ : Set α), s (t₁ ∩ t₂) = s t₁ ∩ s t₂
⊢ ∀ (i : Bool), (bif i then f else g).lift' s = bif i then f.lift' s else g.lift' s
Module: Mathlib.Topology.Closure

Goal state before:
pp: case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
hd : Dense {x}ᶜ
⊢ ¬IsOpen {x}

Tactic:
ho

Goal state after:
case mp
X : Type u
inst✝ : TopologicalSpace X
x : X
hd : Dense {x}ᶜ
ho : IsOpen {x}
⊢ False
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : IsClosed s
A : frontier s = s \ interior s
B : interior (frontier s) ⊆ interior s
C : interior (frontier s) ⊆ frontier s
⊢ interior (frontier s) ⊆ s \ interior s

Tactic:
simpa [A] using C

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
x : X
y : Y
g : Y → Z
hg : ContinuousAt g y
hf : ContinuousAt f x
hy : f x = y
⊢ ContinuousAt (g ∘ f) x

Tactic:
subst hy; exact hg.comp hf

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
β : Type v
f : α → β
ι : Sort u_2
t₁ : TopologicalSpace α
t₂ : ι → TopologicalSpace β
⊢ Continuous[t₁, iInf t₂] f ↔ ∀ (i : ι), Continuous[t₁, t₂ i] f

Tactic:
simp only [continuous_iff_coinduced_le, le_iInf_iff]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ comap f (𝓟 {f x}ᶜ ⊓ l) ≤ 𝓟 {x}ᶜ ⊓ comap f l

Tactic:
rw [comap_inf, comap_principal, preimage_compl]

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenMap f
x : X
l : Filter Y
h : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ 𝓟 (f ⁻¹' {f x})ᶜ ⊓ comap f l ≤ 𝓟 {x}ᶜ ⊓ comap f l
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : s ∈ 𝓝 x
⊢ f '' s ∈ 𝓝 (f x)

Tactic:
contrapose hs

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : f '' s ∉ 𝓝 (f x)
⊢ s ∉ 𝓝 x
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 : IsOpenEmbedding g
⊢ (∀ (x : X), 𝓝 (f x) ≤ map f (𝓝 x)) ↔ ∀ (x : X), map g (𝓝 (f x)) ≤ map g (map f (𝓝 x))

Tactic:
map_le_map_iff hg.injective

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
⊢ IsOpen[instTopologicalSpaceProd] {p | Disjoint (𝓝 p.1) (𝓝 p.2)}

Tactic:
by
  simp only [isOpen_iff_mem_nhds, Prod.forall, mem_ofPred_eq]
  intro x y h
  obtain ⟨U, hU, V, hV, hd⟩ := ((nhds_basis_opens x).disjoint_iff (nhds_basis_opens y)).mp h
  exact mem_nhds_prod_iff'.mpr ⟨U, V, hU.2, hU.1, hV.2, hV.1, fun ⟨x', y'⟩ ⟨hx', hy'⟩ =>
    disjoint_of_disjoint_of_mem hd (hU.2.mem_nhds hx') (hV.2.mem_nhds hy')⟩

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 : MapClusterPt x la f
hg : MapClusterPt y lb g
⊢ MapClusterPt (x, y) (la.curry lb) (Prod.map f g)

Tactic:
mapClusterPt_iff_frequently

Goal state after:
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
⊢ MapClusterPt (x, y) (la.curry lb) (Prod.map f g)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y → Z
x : X
y : Y
s : Set X
t : Set Y
u : Set Z
hf₁ : ∀ (x : X), Continuous[inst✝¹, inst✝] (f x)
hf₂ : ∀ (y : Y), Continuous[inst✝², inst✝] fun x ↦ f x y
hx : x ∈ closure[inst✝²] s
hy : y ∈ closure[inst✝¹] t
h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u
⊢ f x y ∈ closure[inst✝] u

Tactic:
by
  rw [← isClosed_closure.closure_eq]
  apply map_mem_closure (hf₁ x) hy fun b hb ↦ ?_
  apply map_mem_closure (hf₂ b) hx fun a ha ↦ h a ha b hb

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
x : α
h : t ∈ 𝓝[s] x
⊢ ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x

Tactic:
simp [ContinuousWithinAt, nhdsWithin_restrict'' s h]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ⋃₀ ∅ = univ

Tactic:
simp [Set.univ_eq_empty_iff.2]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
h : IsEmpty α
⊢ ⋃₀ {∅} = univ

Tactic:
simp [Set.univ_eq_empty_iff.2]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
x✝ : Bornology α
inst✝ : Bornology β
f : α → β
h : comap f (cobounded β) ≤ cobounded α
s : Set α
hs : IsBounded s
t : Set β
ht : t ∈ cobounded β
hts : s ⊆ f ⁻¹' tᶜ
⊢ IsBounded (f '' s)

Tactic:
exact (IsCobounded.compl ht).subset ((image_mono hts).trans <| image_preimage_subset _ _)

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

Goal state before:
pp: α : Type u
β : Type v
m : α → β
a : α
inj : Injective m
large : range m ∈ pure (m a)
⊢ 𝓟 (m ⁻¹' {m a}) = ↑(pure a)

Tactic:
coe_pure,

Goal state after:
α : Type u
β : Type v
m : α → β
a : α
inj : Injective m
large : range m ∈ pure (m a)
⊢ 𝓟 (m ⁻¹' {m a}) = pure a
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ts ≤ generateFrom (⋃ u ∈ s', f u)

Tactic:
apply le_generateFrom_iff_subset_isOpen.2

Goal state after:
case refine_2.a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ ⋃ u ∈ s', f u ⊆ {s | IsOpen[ts] s}
Module: Mathlib.Topology.Bases

Goal state before:
pp: case a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ t}
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ generateFrom (⋃ u ∈ s', f u) ≤ generateFrom s'

Tactic:
apply le_generateFrom_iff_subset_isOpen.2

Goal state after:
case a
α : Type u_1
ts : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : ts = generateFrom t
t' : Set (Set α) := ⋯
this : IsTopologicalBasis t'
s' : Set (Set α)
s't' : s' ⊆ t'
s'_count : s'.Countable
hs' : IsTopologicalBasis s'
f : Set α → Set (Set α)
f_fin : ∀ u ∈ s', (f u).Finite
ft : ∀ u ∈ s', f u ⊆ t
hf : ∀ u ∈ s', ⋂₀ f u = u
⊢ s' ⊆ {s | IsOpen[generateFrom (⋃ u ∈ s', f u)] s}
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : {i | (f i ∩ s).Nonempty}.Finite
⊢ ∃ t ∈ 𝓝 x, {i | ((fun i ↦ closure[inst✝] (f i)) i ∩ t).Nonempty}.Finite

Tactic:
refine ⟨interior s, interior_mem_nhds.2 hsx, hsf.subset fun i hi => ?_⟩

Goal state after:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
x : X
s : Set X
hsx : s ∈ 𝓝 x
hsf : {i | (f i ∩ s).Nonempty}.Finite
i : ι
hi : i ∈ {i | ((fun i ↦ closure[inst✝] (f i)) i ∩ interior s).Nonempty}
⊢ i ∈ {i | (f i ∩ s).Nonempty}
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
h : LocallyFinite f
x : X
⊢ x ∈ closure[inst✝] (⋃ i, f i) ↔ x ∈ ⋃ i, closure[inst✝] (f i)

Tactic:
simp only [mem_closure_iff_nhdsWithin_neBot, h.nhdsWithin_iUnion, iSup_neBot, mem_iUnion]

Goal state after:
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | ((fun n ↦ {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite
N : X → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
x : X
⊢ ∀ a ∈ {x_1 | N x < x_1} ×ˢ U x, f a.1 a.2 = f (N a.2 + 1) a.2

Tactic:
rintro ⟨n, y⟩ ⟨hn : N x < n, hy : y ∈ U x⟩

Goal state after:
X : Type u_4
inst✝ : TopologicalSpace X
π : X → Sort u_6
f : ℕ → (x : X) → π x
U : X → Set X
hUx : ∀ (x : X), U x ∈ 𝓝 x
hU : ∀ (x : X), {i | ((fun n ↦ {x | f (n + 1) x ≠ f n x}) i ∩ U x).Nonempty}.Finite
N : X → ℕ
hN : ∀ (x : X), ∀ n ≥ N x + 1, ∀ y ∈ U x, f n y = f (N x + 1) y
x : X
n : ℕ
y : X
hn : N x < n
hy : y ∈ U x
⊢ f (n, y).1 (n, y).2 = f (N (n, y).2 + 1) (n, y).2
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
⊢ ⋃ n, accumulate ⋯.choose n = univ

Tactic:
iUnion_accumulate

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : SigmaCompactSpace X
⊢ ⋃ x, ⋯.choose x = univ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : X → Set X
hUl : ∀ x ∈ s, (U x)ᶜ ∈ l
hxU : ∀ x ∈ s, x ∈ U x
hUo : ∀ x ∈ s, IsOpen[inst✝] (U x)
t : Finset X
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
⊢ Disjoint (𝓝ˢ s) l

Tactic:
refine (hasBasis_nhdsSet _).disjoint_iff_left.2
    ⟨⋃ x ∈ t, U x, ⟨isOpen_biUnion fun x hx => hUo x (hts x hx), hst⟩, ?_⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
U : X → Set X
hUl : ∀ x ∈ s, (U x)ᶜ ∈ l
hxU : ∀ x ∈ s, x ∈ U x
hUo : ∀ x ∈ s, IsOpen[inst✝] (U x)
t : Finset X
hts : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, U x
⊢ (⋃ x ∈ t, U x)ᶜ ∈ l
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✝ : NoncompactSpace X
i✝ : Set X
hs : IsCompact i✝
⊢ i✝ᶜ.Nonempty

Tactic:
contrapose hs

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✝ : NoncompactSpace X
i✝ : Set X
hs : ¬i✝ᶜ.Nonempty
⊢ ¬IsCompact 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
⊢ (cocompact ℤ).NeBot

Tactic:
by simp only [Filter.cocompact_eq_cofinite, Filter.cofinite_neBot]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
⊢ (∀ x ∈ U, (U \ s)ᶜ ∈ 𝓝[≠] x) ↔ ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅

Tactic:
refine ⟨fun h z hz ↦ ⟨(U \ s)ᶜ, h z hz, by simp⟩, fun h z hz ↦ ?_⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
h : ∀ z ∈ U, ∃ t ∈ 𝓝[≠] z, t ∩ (U \ s) = ∅
z : X
hz : z ∈ U
⊢ (U \ s)ᶜ ∈ 𝓝[≠] z
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T2Space Y
f : X → Y
s : Set X
inj : InjOn f s
sc : IsCompact s
fc : ∀ x ∈ s, ContinuousAt f x
loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u
⊢ ∃ t ∈ 𝓝ˢ s, InjOn f t

Tactic:
by
  have : ∀ x ∈ s ×ˢ s, ∀ᶠ y in 𝓝 x, f y.1 = f y.2 → y.1 = y.2 := fun (x, y) ⟨hx, hy⟩ ↦ by
    rcases eq_or_ne x y with rfl | hne
    · rcases loc x hx with ⟨u, hu, hf⟩
      exact Filter.mem_of_superset (prod_mem_nhds hu hu) <| forall_prod_set.2 hf
    · suffices ∀ᶠ z in 𝓝 (x, y), f z.1 ≠ f z.2 from this.mono fun _ hne h ↦ absurd h hne
      refine (fc x hx).prodMap' (fc y hy) <| isClosed_diagonal.isOpen_compl.mem_nhds ?_
      exact inj.ne hx hy hne
  rw [← eventually_nhdsSet_iff_forall, sc.nhdsSet_prod_eq sc] at this
  exact eventually_prod_self_iff.1 this

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a : α
⊢ IsOpen[inst✝²] (Ioi a)

Tactic:
← compl_Iic

Goal state after:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : ClosedIicTopology α
a : α
⊢ IsOpen[inst✝²] (Iic a)ᶜ
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s t : Set α
H : (s ∩ t).Nonempty
Hs : IsConnected s
Ht : IsConnected t
⊢ IsConnected (s ∪ t)

Tactic:
rcases H with ⟨x, hx⟩
  refine ⟨⟨x, mem_union_left t (mem_of_mem_inter_left hx)⟩, ?_⟩
  exact Hs.isPreconnected.union x (mem_of_mem_inter_left hx) (mem_of_mem_inter_right hx)
    Ht.isPreconnected

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

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : LocallyConnectedSpace α
⊢ DiscreteTopology (ConnectedComponents α)

Tactic:
by
  refine discreteTopology_iff_isOpen_singleton.mpr fun c ↦ ?_
  obtain ⟨x, rfl⟩ := ConnectedComponents.surjective_coe c
  simp [← ConnectedComponents.isQuotientMap_coe.isOpen_preimage,
    connectedComponents_preimage_singleton, isOpen_connectedComponent]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
⊢ (∀ (t t' : Set α),
      IsClosed[inst✝] t →
        IsClosed[inst✝] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty) →
    IsPreconnected s

Tactic:
rintro h u v hu hv huv ⟨x, xs, xu⟩ ⟨y, ys, yv⟩

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (t t' : Set α),
    IsClosed[inst✝] t → IsClosed[inst✝] t' → s ⊆ t ∪ t' → (s ∩ t).Nonempty → (s ∩ t').Nonempty → (s ∩ (t ∩ t')).Nonempty
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
huv : s ⊆ u ∪ v
x : α
xs : x ∈ s
xu : x ∈ u
y : α
ys : y ∈ s
yv : y ∈ v
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case mpr.inr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
· rcases hsu with ⟨x, hxs, hxu⟩
      exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩

Goal state after: