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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
this :
  ∀ (u : G.ColimitType) (x : F.obj X),
    G.descColimitType c u = x → G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).ColimitType
hu :
  ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₁ =
    ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₂
⊢ u₁ = u₂

Tactic:
generalize hx₁ : G.descColimitType c u₁ = x

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
this :
  ∀ (u : G.ColimitType) (x : F.obj X),
    G.descColimitType c u = x → G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).ColimitType
hu :
  ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₁ =
    ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₂
x : c.pt
hx₁ : G.descColimitType c u₁ = x
⊢ u₁ = u₂
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i : C
y₁ : F i
⊢ ∀ ⦃a₂ : F i⦄, c.inj i y₁ = c.inj i a₂ → y₁ = a₂

Tactic:
y₂

Goal state after:
C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i : C
y₁ y₂ : F i
⊢ c.inj i y₁ = c.inj i y₂ → y₁ = y₂
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
u v : F.Elementsᵒᵖ
g : u ⟶ v
⊢ ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).map g ≫
      { app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app v, naturality := ⋯ } =
    { app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app u, naturality := ⋯ } ≫ ((const F.Elementsᵒᵖ).obj F).map g

Tactic:
ext X x
    obtain ⟨x, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective x
    simp [← shrinkYonedaObjObjEquiv_symm_comp.{w}]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) ''
      Set.range ⇑(ConcreteCategory.hom (↾Sum.inl)) =
    (Set.range ⇑(ConcreteCategory.hom (↾Sum.inr ≫ (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv)))ᶜ

Tactic:
types_comp

Goal state after:
case mp
X Y : Type u
c : BinaryCofan X Y
h : IsColimit c
⊢ ⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) ''
      Set.range ⇑(ConcreteCategory.hom (↾Sum.inl)) =
    (Set.range
        (⇑(ConcreteCategory.hom (h.coconePointUniqueUpToIso (binaryCoproductColimit X Y)).inv) ∘
          ⇑(ConcreteCategory.hom (↾Sum.inr))))ᶜ
Module: Mathlib.GroupTheory.QuotientGroup.ModEq

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
a b p : G
⊢ b ≡ a [PMOD p] ↔ ↑a = ↑b

Tactic:
modEq_iff_eq_add_zsmul,

Goal state after:
G : Type u_1
inst✝ : AddCommGroup G
a b p : G
⊢ (∃ z, a = b + z • p) ↔ ↑a = ↑b
Module: Mathlib.Data.Nat.Cast.Field

Goal state before:
pp: K : Type u_1
inst✝ : DivisionSemiring K
k : ℕ
hn : ↑0 ≠ 0
⊢ False

Tactic:
simp at hn

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

Goal state before:
pp: m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ Fintype.card { x // x.val.Coprime (m + 1) } = φ (m + 1)

Tactic:
simp only [totient, Finset.card_eq_sum_ones, Fintype.card_subtype, Finset.sum_filter, ←
        Fin.sum_univ_eq_sum_range, @Nat.coprime_comm (m + 1)]

Goal state after:
m : ℕ
inst✝¹ : NeZero (m + 1)
inst✝ : Fintype (ZMod (m + 1))ˣ
⊢ (∑ a, if a.val.Coprime (m + 1) then 1 else 0) = ∑ i, if (↑i).Coprime (m + 1) then 1 else 0
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P s✝ : Set α
h✝ : s✝ ∈ S
⊢ s✝ ∈ S

Tactic:
by assumption

Goal state after:
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case univ
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P : Set α
⊢ Set.univ ∈ S ∨ ∃ Q ∈ S, Set.univ = A ∩ Q

Tactic:
| univ =>

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

Goal state before:
pp: n : ℕ
⊢ n.divisors.sum φ = n

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn)
  · simp
  rw [← sum_div_divisors n φ]
  have : n = ∑ d ∈ n.divisors, #{k ∈ range n | n.gcd k = d} := by
    nth_rw 1 [← card_range n]
    refine card_eq_sum_card_fiberwise fun x _ => mem_divisors.2 ⟨?_, hn.ne'⟩
    apply gcd_dvd_left
  nth_rw 3 [this]
  exact sum_congr rfl fun x hx => totient_div_of_dvd (dvd_of_mem_divisors hx)

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst✝ : l.IsCountablyGenerated
hxy : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, x n ∉ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), x (y n) ∉ s
ms : ℕ → ℕ
hms_tendsto : Tendsto (fun n ↦ x (y (ms n))) atTop f
⊢ False

Tactic:
rcases (hms_tendsto.eventually_mem hs).exists with ⟨n, hn⟩

Goal state after:
α : Type u_1
ι : Type u_3
x : ι → α
f : Filter α
l : Filter ι
inst✝ : l.IsCountablyGenerated
hxy : ¬Tendsto x l f
s : Set α
hs : s ∈ f
hfreq : ∃ᶠ (n : ι) in l, x n ∉ s
y : ℕ → ι
hy_tendsto : Tendsto y atTop l
hy_freq : ∀ (n : ℕ), x (y n) ∉ s
ms : ℕ → ℕ
hms_tendsto : Tendsto (fun n ↦ x (y (ms n))) atTop f
n : ℕ
hn : x (y (ms n)) ∈ s
⊢ False
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 : α
⊢ toIocDiv hp a b • p - b = -toIocMod hp a b

Tactic:
by
  rw [toIocMod, neg_sub]

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 : α
⊢ toIcoMod hp a b + toIcoDiv hp a b • p = b

Tactic:
rw [toIcoMod, sub_add_cancel]

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 : α
⊢ a < a + p ∧ ∃ z, a + p = a + z • p

Tactic:
exact ⟨lt_add_of_pos_right _ hp, 1, by simp⟩

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
t : Set α
ht : t ∈ iInf f
inhabited_h : Inhabited ι
⊢ ⨅ i, (f i).lift g ≤ g univ

Tactic:
exact iInf₂_le_of_le default univ (iInf_le _ univ_mem)

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
⊢ frontier (s ∪ t) ⊆ frontier s ∩ closure tᶜ ∪ closure sᶜ ∩ frontier t

Tactic:
by
  simpa only [frontier_compl, ← compl_union] using frontier_inter_subset sᶜ tᶜ

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b = -⌊(a + p - b) / p⌋

Tactic:
refine toIocDiv_eq_of_sub_zsmul_mem_Ioc hp ?_

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - -⌊(a + p - b) / p⌋ • p ∈ Set.Ioc a (a + p)
Module: Mathlib.Topology.Order

Goal state before:
pp: case univ
α : Type u
g : Set (Set α)
a : α
this : TopologicalSpace α := generateFrom g
s : Set α
ha : a ∈ univ
⊢ ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s ≤ 𝓟 univ

Tactic:
| univ =>

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: case refl.refine_1.univ
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
⊢ univ = ∅ ∨ univ = univ

Tactic:
| univ =>

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ generateFrom (insert t s) = generateFrom s

Tactic:
refine le_antisymm (generateFrom_anti <| subset_insert t s) (le_generateFrom ?_)

Goal state after:
α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ ∀ s_1 ∈ insert t s, IsOpen[generateFrom s] s_1
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ IsOpen[inst✝] s ↔ ∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = s

Tactic:
rw [hf.eq_induced, isOpen_induced_iff]

Goal state after:
Module: Mathlib.Topology.Order

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

Tactic:
by
  simp only [continuous_iff_le_induced, iSup_le_iff]

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 : IsClosedMap g
hf : IsClosedMap f
⊢ IsClosedMap (g ∘ f)

Tactic:
intro s hs
  rw [image_comp]
  exact hg _ (hf _ hs)

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
⊢ ContinuousWithinAt f {x}ᶜ x ↔ ContinuousAt f x

Tactic:
rw [compl_eq_univ_sdiff, continuousWithinAt_sdiff_self, continuousWithinAt_univ]

Goal state after:
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:
map_principal

Goal state after:
α : 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) ⊓ 𝓟 (m '' s) = Filter.map m (Filter.comap m ↑g) ⊓ 𝓟 (m '' s)
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ s ∈ S, IsCompact s
⊢ IsSigmaCompact (⋃₀ S)

Tactic:
have : Countable S := countable_coe_iff.mpr hc

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ s ∈ S, IsCompact s
this : Countable ↑S
⊢ IsSigmaCompact (⋃₀ S)
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ (s : ↑S), IsSigmaCompact ↑s
⊢ IsSigmaCompact (⋃₀ S)

Tactic:
have : Countable S := countable_coe_iff.mpr hc

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
hc : S.Countable
hcomp : ∀ (s : ↑S), IsSigmaCompact ↑s
this : Countable ↑S
⊢ IsSigmaCompact (⋃₀ S)
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f

Tactic:
simpa [f] using hnhds

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst✝] t
⊢ IsCompact (s ∩ t)

Tactic:
intro f hnf hstf
  obtain ⟨x, hsx, hx⟩ : ∃ x ∈ s, ClusterPt x f :=
    hs (le_trans hstf (le_principal_iff.2 inter_subset_left))
  have : x ∈ t := ht.mem_of_nhdsWithin_neBot <|
    hx.mono <| le_trans hstf (le_principal_iff.2 inter_subset_right)
  exact ⟨x, ⟨hsx, this⟩, hx⟩

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ ¬K.shiftr.find x ≤ K.find x

Tactic:
simp only [find_shiftr, not_le, Nat.lt_succ_self]

Goal state after:
Module: Mathlib.Data.Set.Subset

Goal state before:
pp: α : Type u_2
A : Set α
D : Set ↑A
⊢ range Subtype.val \ Subtype.val '' D = A \ Subtype.val '' D

Tactic:
Subtype.range_coe_subtype,

Goal state after:
α : Type u_2
A : Set α
D : Set ↑A
⊢ {x | x ∈ A} \ Subtype.val '' D = A \ Subtype.val '' D
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
S : Set (Set X)
hTS : T = generateFrom S
s : Set X
h : ∀ P ⊆ S, s ⊆ ⋃₀ P → ∃ Q ⊆ P, Q.Finite ∧ s ⊆ ⋃₀ Q
F : Ultrafilter X
hsF : s ∈ F
hF : ¬∃ x ∈ s, ↑F ≤ 𝓝 x
U : X → Set X
hxU : ∀ x ∈ s, x ∈ U x
hSU : ∀ x ∈ s, U x ∈ S
hUF : ∀ x ∈ s, U x ∉ F
⊢ U '' s ⊆ S

Tactic:
simpa [Set.subset_def]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsCompact (range f)

Tactic:
rw [← image_univ]; exact isCompact_univ.image hf

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : CompactSpace X
f : X → Y
hf : Continuous[inst✝², inst✝¹] f
⊢ IsCompact (range f)

Tactic:
by
  rw [← image_univ]; exact isCompact_univ.image hf

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x y : X
⊢ (x ~ᵢ y) ↔ ∀ (s : Set X), IsClosed[inst✝] s → (x ∈ s ↔ y ∈ s)

Tactic:
simp only [inseparable_iff_specializes_and, specializes_iff_forall_closed, ← forall_and, ←
    iff_def]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
x : X
hx : x ∈ s
⊢ 𝓝 (f x) ⊓ 𝓟 (f '' s) ≤ map f (𝓝 x) ⊓ map f (𝓟 s)

Tactic:
map_principal

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
hs : IsDiscrete s
hf : IsOpenMap f
hf' : Injective f
x : X
hx : x ∈ s
⊢ 𝓝 (f x) ⊓ 𝓟 (f '' s) ≤ map f (𝓝 x) ⊓ 𝓟 (f '' s)
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst✝³, inst✝²] f
hf : Tendsto f cofinite (cocompact Y)
x : X
⊢ IsOpen[inst✝³] {x}

Tactic:
obtain ⟨K : Set Y, hK : IsCompact K, hK' : K ∈ 𝓝 (f x)⟩ := exists_compact_mem_nhds (f x)

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
f : X → Y
inst✝¹ : T1Space X
inst✝ : WeaklyLocallyCompactSpace Y
hf' : Continuous[inst✝³, inst✝²] f
hf : Tendsto f cofinite (cocompact Y)
x : X
K : Set Y
hK : IsCompact K
hK' : K ∈ 𝓝 (f x)
⊢ IsOpen[inst✝³] {x}
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: case h
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
hcne : ¬c.Nonempty
⊢ S.Nonempty

Tactic:
exact hne

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: case neg
X : Type u_1
inst✝ : TopologicalSpace X
s U : Set X
hs : ∀ x ∈ U, Disjoint (𝓝[≠] x) (𝓟 (U \ s))
hU : IsClosed[inst✝] U
x : X
hx : x ∈ (U \ s)ᶜ
h₁x : x ∈ U
a : X
ha : a ∈ {x}ᶜ → a ∉ U \ s
h₂a : ¬a = x
⊢ a ∈ (U \ s)ᶜ

Tactic:
specialize ha h₂a
      tauto_set

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

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[≤] a ⊔ 𝓝[≥] a = 𝓝 a

Tactic:
rw [← nhdsWithin_union, Iic_union_Ici, nhdsWithin_univ]

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
⊢ IsCompact (closure[inst✝¹] K)

Tactic:
by
  refine isCompact_of_finite_subcover fun U hUo hKU ↦ ?_
  rcases hK.elim_finite_subcover U hUo (subset_closure.trans hKU) with ⟨t, ht⟩
  exact ⟨t, hK.closure_subset_of_isOpen (isOpen_biUnion fun _ _ ↦ hUo _) ht⟩

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

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
inst✝ : TopologicalSpace β
a b : α
f : α → β
h : a < b
⊢ ContinuousWithinAt f (Ico a b) b ↔ ContinuousWithinAt f (Iio b) b

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_Ico_eq_nhdsLT h]

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

Goal state before:
pp: X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
⊢ Disjoint (𝓝 (f x)) (𝓝ˢ (f '' K \ interior s))

Tactic:
hc.disjoint_nhdsSet_right,

Goal state after:
X : Type u_3
Y : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : R1Space Y
f : X → Y
x : X
K : Set X
s : Set Y
hf : Continuous[inst✝², inst✝¹] f
hs : s ∈ 𝓝 (f x)
hKc : IsCompact K
hKx : K ∈ 𝓝 x
hc : IsCompact (f '' K \ interior s)
⊢ ∀ x_1 ∈ f '' K \ interior s, Disjoint (𝓝 (f x)) (𝓝 x_1)
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 α
x : α
⊢ IsOpen {ConnectedComponents.mk x}

Tactic:
simp [← ConnectedComponents.isQuotientMap_coe.isOpen_preimage,
    connectedComponents_preimage_singleton, isOpen_connectedComponent]

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.Topology.Connected.LocallyConnected

Goal state before:
pp: case pos
ι : 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
⊢ IsPreconnected (K.piecewise (fun i ↦ connectedComponentIn (t i) (x i)) (fun x ↦ univ) i)

Tactic:
rw [piecewise_eq_of_mem _ _ _ hi]
    exact isPreconnected_connectedComponentIn

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 ⊆ i

Tactic:
hst i hi

Goal state after:
ι : 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
Module: Mathlib.Order.Filter.CountableInter

Goal state before:
pp: case mp.univ
α : Type u_2
g : Set (Set α)
s : Set α
⊢ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ univ

Tactic:
| univ =>

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

Goal state before:
pp: case mpr.univ
α : Type u_2
g : Set (Set α)
f : Filter α
inst✝ : CountableInterFilter f
h : g ⊆ f.sets
s : Set α
⊢ univ ∈ f

Tactic:
| univ =>

Goal state after:
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
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ v
x : α
hxs : x ∈ s
hxu : x ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩

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

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hsU : s ⊆ ⋃ i, U i
⊢ ∃ f, s ⊆ ⋃ n, U (f n)

Tactic:
obtain ⟨c, ⟨c_count, c_cov⟩⟩ := hs.elim_countable_subcover U hUo hsU

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
ι : Type v
inst✝ : Nonempty ι
hs : IsLindelof s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst✝¹] (U i)
hsU : s ⊆ ⋃ i, U i
c : Set ι
c_count : c.Countable
c_cov : s ⊆ ⋃ i ∈ c, U i
⊢ ∃ f, s ⊆ ⋃ n, U (f n)
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case univ
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (Set X)
h : inst✝ = generateFrom s
h' : ∀ t ∈ s, ∀ a ∈ t, Disjoint (𝓝ˢ tᶜ) (𝓝 a)
a : X
t : Set X
ha : a ∈ univ
⊢ Disjoint (𝓝ˢ univᶜ) (𝓝 a)

Tactic:
| univ =>

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

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

Tactic:
exact ⟨x, hxs, ⟨hxu, h hxs⟩⟩

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

Goal state before:
pp: case mp
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
U : Set X
⊢ IsLindelof U ∧ IsOpen[inst✝] U → ∃ s, s.Countable ∧ U = ⋃ i ∈ s, b i

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
case mp
X : Type u
ι : Type u_1
inst✝ : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsLindelof (b i)
U : Set X
h₁ : IsLindelof U
h₂ : IsOpen[inst✝] U
⊢ ∃ s, s.Countable ∧ U = ⋃ i ∈ s, b i
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ ConnectedSpace α → ∃ x, connectedComponent x = univ

Tactic:
rintro ⟨⟨x⟩⟩
    exact
      ⟨x, eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)⟩

Goal state after: