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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
⊢ Over.mk (𝟙 c.pt) ≅
    colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt)

Tactic:
let isc : IsColimit ((Over.forget _).mapCocone _) := isColimitOfPreserves _
    (colimit.isColimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙
      CostructuredArrow.toOver yoneda c.pt))

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
I : Type v₁
inst✝ : SmallCategory I
F : I ⥤ C
c : Cocone (F ⋙ yoneda)
hc : IsColimit c
isc : IsColimit
  ((Over.forget c.pt).mapCocone
    (colimit.cocone
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))) :=
  isColimitOfPreserves (Over.forget c.pt)
    (colimit.isColimit
      ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt))
⊢ Over.mk (𝟙 c.pt) ≅
    colimit ((c.toCostructuredArrow ⋙ CostructuredArrow.pre F yoneda c.pt) ⋙ CostructuredArrow.toOver yoneda c.pt)
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
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)
x : F.obj X
u : F.Elements
v : unop ((CategoryOfElements.π F).op.obj (op u)) ⟶ X
h : G.descColimitType c (G.ιColimitType (op u) (shrinkYonedaObjObjEquiv.symm v)) = x
⊢ G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) =
    G.ιColimitType (op u) (shrinkYonedaObjObjEquiv.symm v)

Tactic:
dsimp [c] at v h

Goal state after:
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)
x : F.obj X
u : F.Elements
v : u.fst ⟶ X
h : (ConcreteCategory.hom (F.map (shrinkYonedaObjObjEquiv (shrinkYonedaObjObjEquiv.symm v)))) u.snd = x
⊢ G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) =
    G.ιColimitType (op u) (shrinkYonedaObjObjEquiv.symm v)
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
⊢ Mono (free.map f)

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

Goal state after:
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₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
⊢ c.inj i₁ y₁ = c.inj i₂ y₂ ↔ ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨h₁, h₂⟩ ↦ by subst h₁ h₂; rfl⟩

Goal state after:
C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
h : c.inj i₁ y₁ = c.inj i₂ y₂
⊢ ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
n : ℤ
⊢ Periodic f ((2 * n) • c)

Tactic:
by
  rw [mul_comm, mul_zsmul, two_zsmul, ← two_nsmul]
  exact h.periodic.zsmul n

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : NonAssocRing α
inst✝ : NonAssocRing β
h : Antiperiodic f c
n : ℤ
⊢ f (↑n * c - x) = ↑↑n.negOnePow * f (-x)

Tactic:
by
  simpa only [zsmul_eq_mul] using h.zsmul_sub_eq n

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: case succ
motive : ℕ → Prop
zero : motive 0
one : motive 1
prime_mul : ∀ (p a : ℕ), Prime p → motive a → motive (p * a)
a p : ℕ
hp : Prime p
ha : motive a
n : ℕ
ih : motive (p ^ n * a)
⊢ motive (p ^ (n + 1) * a)

Tactic:
rw [pow_succ', mul_assoc]
    exact prime_mul _ _ hp ih

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

Goal state before:
pp: case mpr
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ (∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)) → ¬p ∣ a

Tactic:
rintro h ⟨b, rfl⟩
            rw [pow_succ'] at ha
            exact h b ⟨lt_of_mul_lt_mul_left ha (zero_le _), mul_comm _ _⟩

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

Goal state before:
pp: a b a1 : ℕ
⊢ ∀ (a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)

Tactic:
a2

Goal state after:
a b a1 a2 : ℕ
⊢ ∀ (b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
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 : ℤ
⊢ toIocDiv hp (a - m • p) b = toIocDiv hp a b + m

Tactic:
by
  rw [sub_eq_add_neg, ← neg_smul, toIocDiv_add_zsmul', sub_neg_eq_add]

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 : α
⊢ toIocDiv hp (a + p) b = toIocDiv hp a b - 1

Tactic:
simpa only [one_zsmul] using toIocDiv_add_zsmul' hp a b 1

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 c : α
⊢ toIcoDiv hp (a - c) b = toIcoDiv hp a (b + c)

Tactic:
rw [← sub_neg_eq_add, toIcoDiv_sub_eq_toIcoDiv_add, sub_eq_add_neg]

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 c : α
⊢ toIcoMod hp a (b + c) = toIcoMod hp (a - c) b + c

Tactic:
simp_rw [toIcoMod, toIcoDiv_sub_eq_toIcoDiv_add', sub_add_eq_add_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) = p - toIocMod hp (-a) b

Tactic:
simp_rw [toIcoMod, toIocMod, toIcoDiv_neg, neg_smul, add_smul]
  abel

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ Y
⊢ IsOpenMap ⇑e.symm ↔ Continuous[inst✝¹, inst✝] ⇑e

Tactic:
by
  simp_rw [← Equiv.continuous_symm_iff, Equiv.symm_symm]

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

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
⊢ toIocMod hp a b + ↑(toIocDiv hp a b) * p = b

Tactic:
toIocMod_add_toIocDiv_mul

Goal state after:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
⊢ b = b
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
⊢ IsClosed[inst✝] s ↔ ∃ t, IsClosed[inst✝¹] t ∧ f ⁻¹' t = s

Tactic:
rw [hf.eq_induced, isClosed_induced_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
s : Set Y
⊢ f ⁻¹' frontier s ⊆ frontier (f ⁻¹' s)

Tactic:
by
  simpa only [frontier_eq_closure_inter_closure, preimage_inter] using!
    inter_subset_inter hf.preimage_closure_subset_closure_preimage
      hf.preimage_closure_subset_closure_preimage

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
ι : Type u_5
I : Set ι
hI : I.Finite
s : ι → Set α
a : α
⊢ 𝓝[⋃ i ∈ I, s i] a = ⨆ i ∈ I, 𝓝[s i] a

Tactic:
by
  induction I, hI using Set.Finite.induction_on with
  | empty => simp
  | insert _ _ hT => simp only [hT, nhdsWithin_union, iSup_insert, biUnion_insert]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝² : TopologicalSpace α
ι : Type u_5
X : ι → Type u_6
inst✝¹ : (i : ι) → TopologicalSpace (X i)
s : (i : ι) → Set (X i)
x : (i : ι) → X i
inst✝ : ∀ (i : ι), (𝓝[s i] x i).NeBot
⊢ (𝓝[univ.pi s] x).NeBot

Tactic:
simpa [nhdsWithin_pi_neBot]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t u : Set α
⊢ u ∈ 𝓝ˢ[t] s ↔ ∃ v, IsOpen[inst✝] v ∧ s ⊆ v ∧ v ∩ t ⊆ u

Tactic:
by
  simpa [and_assoc] using (nhdsSetWithin_basis_open s t).mem_iff

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
x : X
hx : p x
h : ∀ᶠ (x : X) in 𝓝 x, p x
⊢ range Subtype.val ∈ 𝓝 ↑⟨x, hx⟩

Tactic:
rw [Subtype.range_val]; exact h

Goal state after:
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 → Z
g : Y → Z
hf : IsClosedEmbedding f
hg : IsClosedEmbedding g
h : Injective (Sum.elim f g)
⊢ IsClosedEmbedding (Sum.elim f g)

Tactic:
rw [IsClosedEmbedding.isClosedEmbedding_iff_continuous_injective_isClosedMap] at hf hg ⊢
  exact ⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
h_nhds : ∀ (a : α), (𝓝 a).HasBasis (fun t ↦ t ∈ s ∧ a ∈ t) id
x : α
⊢ 𝓝 x = 𝓝 x

Tactic:
by
    simpa only [nhds_generateFrom, and_comm] using! (h_nhds x).eq_biInf

Goal state after:
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 → Z
g : Y → Z
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
⊢ IsInducing (Sum.elim f g)

Tactic:
isInducing_iff_nhds

Goal state after:
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
⊢ ∀ (x : X ⊕ Y), 𝓝 x = comap (Sum.elim f g) (𝓝 (Sum.elim f g x))
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
ht : IsOpen[inst✝] t
⊢ frontier (s ∩ t) ∩ t = frontier s ∩ t

Tactic:
by
  simp only [Set.inter_comm _ t, ← Subtype.preimage_coe_eq_preimage_coe_iff,
    ht.isOpenMap_subtype_val.preimage_frontier_eq_frontier_preimage continuous_subtype_val,
    Subtype.preimage_coe_self_inter]

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

Goal state before:
pp: case mpr
X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf₁ : IsInducing f
hf₂ : Injective f
hg₁ : IsInducing g
hg₂ : Injective g
hFg : Disjoint (closure[inst✝] (range f)) (range g)
hfG : Disjoint (range f) (closure[inst✝] (range g))
⊢ ∀ (a : X) (b : Y), f a ≠ g b

Tactic:
exact fun a b ↦ hfG.ne_of_mem (mem_range_self a) (subset_closure (mem_range_self b))

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case h
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ (t i ⊆ if i ∈ I then t i else univ) ∧ IsOpen[T i] (t i) ∧ a i ∈ t i

Tactic:
if_pos hi

Goal state after:
case h
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
I : Finset ι
t : (a : ι) → Set (A a)
h1 : ∀ a_1 ∈ I, IsOpen[T a_1] (t a_1) ∧ a a_1 ∈ t a_1
h2 : (↑I).pi t ⊆ s
i : ι
hi : i ∈ I
⊢ t i ⊆ t i ∧ IsOpen[T i] (t i) ∧ a i ∈ t i
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
b : β
f : α → β
h : Continuous[inst✝¹, inst✝] f
h' : EqOn f (fun x ↦ b) s
⊢ Tendsto f (𝓝ˢ s) (𝓝 b)

Tactic:
rw [← nhdsSet_singleton]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
b : β
f : α → β
h : Continuous[inst✝¹, inst✝] f
h' : EqOn f (fun x ↦ b) s
⊢ Tendsto f (𝓝ˢ s) (𝓝ˢ {b})
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
a : (i : ι) → A i
⊢ I.pi s ∈ 𝓝 a ↔ ∀ i ∈ I, s i ∈ 𝓝 (a i)

Tactic:
rw [nhds_pi, pi_mem_pi_iff hI]

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

Goal state before:
pp: α : Type u_1
L : Filter (Set α)
l : Filter α
⊢ L.bind 𝓟 ≤ l ↔ L ≤ l.smallSets

Tactic:
smallSets_eq_generate,

Goal state after:
α : Type u_1
L : Filter (Set α)
l : Filter α
⊢ L.bind 𝓟 ≤ l ↔ L ≤ generate (powerset '' l.sets)
Module: Mathlib.Topology.LocallyFinite

Goal state before:
pp: ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : {i | (f i ∩ U).Nonempty}.Finite
⊢ 𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a

Tactic:
← iUnion_inter,

Goal state after:
ι : Type u_1
X : Type u_4
inst✝ : TopologicalSpace X
f : ι → Set X
hf : LocallyFinite f
a : X
U : Set X
haU : U ∈ 𝓝 a
hfin : {i | (f i ∩ U).Nonempty}.Finite
⊢ 𝓝[⋃ i, f i] a = 𝓝[(⋃ i, f i) ∩ U] a
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
⊢ ∀ (x : Y), ∀ n ∈ 𝓝 x, ∃ s ∈ 𝓝 x, s ⊆ n ∧ IsCompact s

Tactic:
refine hf.surjective.forall.2 fun x U hU ↦ ?_
    rcases local_compact_nhds (hf.continuous.continuousAt hU) with ⟨K, hKx, hKU, hKc⟩
    exact ⟨f '' K, hf.isOpenMap.image_mem_nhds hKx, image_subset_iff.2 hKU, hKc.image hf.continuous⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
⊢ l ≤ 𝓝 y

Tactic:
rw [← nhdsSet_singleton]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
⊢ l ≤ 𝓝ˢ {y}
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
Y : Type u_2
l : Filter Y
y : X
f : Y → X
hs : IsCompact s
hmem : ∀ᶠ (x : Y) in l, f x ∈ s
h : ∀ x ∈ s, MapClusterPt x l f → x = y
⊢ Tendsto f l (𝓝 y)

Tactic:
rw [← nhdsSet_singleton]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
Y : Type u_2
l : Filter Y
y : X
f : Y → X
hs : IsCompact s
hmem : ∀ᶠ (x : Y) in l, f x ∈ s
h : ∀ x ∈ s, MapClusterPt x l f → x = y
⊢ Tendsto f l (𝓝ˢ {y})
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
X : ι → Type u_2
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
⊢ IsCompact univ

Tactic:
by rw [← pi_univ univ]; exact isCompact_univ_pi fun i => isCompact_univ

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

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

Tactic:
exact fun U => (hc U.2).2.1.isClosed_compl.isCompact

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst✝] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ z ∈ (Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t, IsClosed[inst✝] z) →
      s ⊆ ⋃₀ ↑((Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t) →
        ∃ z ∈ (Equiv.finsetCongr (Function.Involutive.toPerm compl ⋯)) t, s ⊆ z

Tactic:
simp_rw [Equiv.finsetCongr_apply, Finset.forall_mem_map, Finset.mem_map, Finset.coe_map,
    sUnion_image, Equiv.coe_toEmbedding, Function.Involutive.coe_toPerm, isClosed_compl_iff,
    exists_exists_and_eq_and]

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
t : Finset (Set X)
⊢ (∀ u ∈ t, IsOpen[inst✝] u) → (∀ u ∈ t, (s ∩ u).Nonempty) → (s ∩ ⋂₀ ↑t).Nonempty ↔
    (∀ u ∈ t, IsOpen[inst✝] u) → s ⊆ ⋃ a ∈ ↑t, aᶜ → ∃ a ∈ t, s ⊆ aᶜ
Module: Mathlib.Order.SuccPred.Relation

Goal state before:
pp: case refine_2.inr
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m✝ : α
hnm✝ : n ≤ m✝
m : α
hnm : n ≤ m
ih : (∀ i ∈ Ico n m, r i (succ i)) → ReflTransGen r n m
h : ∀ i ∈ Ico n (succ m), r i (succ i)
this : ReflTransGen r n m
hm : m < succ m
⊢ ReflTransGen r n (succ m)

Tactic:
exact this.tail (h m ⟨hnm, hm⟩)

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ coclosedCompact X ≤ cocompact X

Tactic:
hasBasis_coclosedCompact.le_basis_iff hasBasis_cocompact

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
⊢ ∀ (i' : Set X), IsCompact i' → ∃ i, (IsClosed[inst✝¹] i ∧ IsCompact i) ∧ iᶜ ⊆ i'ᶜ
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
inst✝ : DenselyOrdered α
s : Set α
hs : Dense s
x : α
⊢ Ioi x = ⋃ y ∈ s ∩ Ioi x, Ioi y

Tactic:
refine Subset.antisymm (fun z hz ↦ ?_) (iUnion₂_subset fun y hy ↦ Ioi_subset_Ioi (le_of_lt hy.2))
  rcases hs.exists_between hz with ⟨y, hys, hy⟩
  exact mem_iUnion₂.2 ⟨y, ⟨hys, hy.1⟩, hy.2⟩

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

Goal state before:
pp: case refine_1
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsPreconnected s
⊢ ∃ i t, IsPreconnected t ∧ s = mk i '' t

Tactic:
obtain rfl | h := s.eq_empty_or_nonempty

Goal state after:
case refine_1.inl
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (X i)
hs : IsPreconnected ∅
⊢ ∃ i t, IsPreconnected t ∧ ∅ = mk i '' t

case refine_1.inr
ι : Type u_1
X : ι → Type u_2
hι : Nonempty ι
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
hs : IsPreconnected s
h : s.Nonempty
⊢ ∃ i t, IsPreconnected t ∧ s = mk i '' t
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsPreconnected s
⊢ (∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t

Tactic:
obtain rfl | h := s.eq_empty_or_nonempty

Goal state after:
case refine_1.inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
hs : IsPreconnected ∅
⊢ (∃ t, IsPreconnected t ∧ ∅ = inl '' t) ∨ ∃ t, IsPreconnected t ∧ ∅ = inr '' t

case refine_1.inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
hs : IsPreconnected s
h : s.Nonempty
⊢ (∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsuv : s ∩ (u ∩ v) = ∅
⊢ s ⊆ u ∨ s ⊆ v

Tactic:
← not_nonempty_iff_eq_empty

Goal state after:
case refine_3
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h :
  ∀ (U : Finset (Set α)),
    (∀ (u v : Set α), u ∈ U → v ∈ U → (s ∩ (u ∩ v)).Nonempty → u = v) →
      (∀ u ∈ U, IsOpen[inst✝] u) → s ⊆ ⋃₀ ↑U → ∃ u ∈ U, s ⊆ u
u v : Set α
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hs : s ⊆ u ∪ v
hsuv : ¬(s ∩ (u ∩ v)).Nonempty
⊢ s ⊆ u ∨ s ⊆ v
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
⊢ PreconnectedSpace α → ∀ (x : α), connectedComponent x = univ

Tactic:
intro h x
    exact eq_univ_of_univ_subset <| isPreconnected_univ.subset_connectedComponent (mem_univ x)

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

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s✝ t u v : Set α
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
s : Set ((i : ι) × X i)
x✝ : s ⊆ univ
hs : IsPreconnected s
⊢ s.Subsingleton

Tactic:
obtain rfl | h := s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s t u v : Set α
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
x✝ : ∅ ⊆ univ
hs : IsPreconnected ∅
⊢ ∅.Subsingleton

case inr
α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝² : TopologicalSpace α
s✝ t u v : Set α
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
s : Set ((i : ι) × X i)
x✝ : s ⊆ univ
hs : IsPreconnected s
h : s.Nonempty
⊢ s.Subsingleton
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (⋂ b, bif b then s else t)

Tactic:
exact .iInter (Bool.forall_bool.2 ⟨ht, hs⟩)

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

Goal state before:
pp: case refine_3
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
H1 : Disjoint (u ∪ v)ᶜ (⋂ i, ↑i) → ∃ x_1, ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, ↑i).Nonempty
si : Finset { s // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, ↑i).Nonempty
⊢ (u ∪ v)ᶜ ∩ ⋂ U ∈ si, ↑U = ∅

Tactic:
← not_nonempty_iff_eq_empty

Goal state after:
case refine_3
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
H1 : Disjoint (u ∪ v)ᶜ (⋂ i, ↑i) → ∃ x_1, ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ x_1, ↑i).Nonempty
si : Finset { s // IsClopen s ∧ x ∈ s }
H2 : ¬((u ∪ v)ᶜ ∩ ⋂ i ∈ si, ↑i).Nonempty
⊢ ¬((u ∪ v)ᶜ ∩ ⋂ U ∈ si, ↑U).Nonempty
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
⊢ T2Space (ConnectedComponents X)

Tactic:
refine ⟨ConnectedComponents.surjective_coe.forall₂.2 fun a b ne => ?_⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
a b : X
ne : mk a ≠ mk b
⊢ (fun x y ↦ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v) (mk a) (mk b)