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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Cotrident f
j : J
⊢ f j ≫ s.ι.app one = (parallelFamily f).map (line j) ≫ s.ι.app one

Tactic:
parallelFamily_map_left

Goal state after:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
s : Cotrident f
j : J
⊢ f j ≫ s.ι.app one = f j ≫ s.ι.app one
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj G).map f.op))
A : C
hA : P A
g : X ⟶ A
⊢ ∀ (y₁ y₂ : Y ⟶ A), f ≫ y₁ = g → f ≫ y₂ = g → y₁ = y₂

Tactic:
· intro l₁ l₂ h₁ h₂
      rw [← cancel_epi f, h₁, h₂]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Cotrident f
⊢ f j₁ ≫ t.π = f j₂ ≫ t.π

Tactic:
rw [t.app_one, t.app_one]

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

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

pp: case a
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).unop

Tactic:
← Quiver.Hom.unop_op g.unop.left

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

case a
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).unop
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Trident f
i : s.pt ≅ t.pt
w : i.hom ≫ t.ι = s.ι
⊢ i.inv ≫ s.ι = t.ι

Tactic:
rw [← w, Iso.inv_hom_id_assoc]

Goal state after:
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)
u : G.ColimitType
x : F.obj X
h : G.descColimitType c u = x
⊢ G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u

Tactic:
obtain ⟨⟨u⟩, v, rfl⟩ := Functor.ιColimitType_jointly_surjective _ u

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 : G.obj (op u)
h : G.descColimitType c (G.ιColimitType (op u) v) = x
⊢ G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = G.ιColimitType (op u) v
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 : G.obj (op u)
h : G.descColimitType c (G.ιColimitType (op u) v) = x
⊢ G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = G.ιColimitType (op u) v

Tactic:
obtain ⟨v, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective v

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 : 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)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommGroup α
h : Periodic f c
a x : α
⊢ (fun x ↦ f (a - x)) (x + c) = (fun x ↦ f (a - x)) x

Tactic:
simp only [← sub_sub, h.sub_eq]

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

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
r : R
x : ↥i.range
eq1 : r • i (Exists.choose ⋯) = ↑(r • x)
⊢ f (Exists.choose ⋯) = (RingHom.id R) r • f (Exists.choose ⋯)

Tactic:
rw [← map_smul, ← (r • x).2.choose_spec] at eq1

Goal state after:
R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
r : R
x : ↥i.range
eq1 : i (r • Exists.choose ⋯) = i (Exists.choose ⋯)
⊢ f (Exists.choose ⋯) = (RingHom.id R) r • f (Exists.choose ⋯)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddCommGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
a x : α
⊢ (fun x ↦ f (a - x)) (x + c) = -(fun x ↦ f (a - x)) x

Tactic:
simp only [← sub_sub, h.sub_eq]

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

Goal state before:
pp: α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y

Tactic:
rcases (hasBasis_iInf_principal_finite _).eventually_iff.1 h with ⟨S, hSf, hS⟩

Goal state after:
α : Type u_3
inst✝ : Preorder α
p : α → Prop
h : ∀ᶠ (x : α) in atTop, p x
S : Set α
hSf : S.Finite
hS : ∀ ⦃x : α⦄, x ∈ ⋂ i ∈ S, Ici i → p x
⊢ ∀ᶠ (x : α) in atTop, ∀ (y : α), x ≤ y → p y
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
⊢ Tendsto (fun p ↦ p.1 ×ˢ p.2) atTop atTop

Tactic:
classical
  apply Monotone.tendsto_atTop_atTop
  · intro p q hpq
    simpa using Finset.product_subset_product hpq.1 hpq.2
  · intro b
    use (Finset.image Prod.fst b, Finset.image Prod.snd b)
    exact Finset.subset_product

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

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : p ∈ n.factorization.support
⊢ p ^ (n.factorization p - 1) * (p - 1) * p = p ^ n.factorization p * (p - 1)

Tactic:
rw [Finsupp.mem_support_iff, ← zero_lt_iff] at hp

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
p : ℕ
hp : 0 < n.factorization p
⊢ p ^ (n.factorization p - 1) * (p - 1) * p = p ^ n.factorization p * (p - 1)
Module: Mathlib.Order.Filter.Curry

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
p : α × β → Prop
⊢ (∃ᶠ (x : α × β) in l.curry m, p x) ↔ ∃ᶠ (x : α) in l, ∃ᶠ (y : β) in m, p (x, y)

Tactic:
simp_rw [Filter.Frequently, not_iff_not, not_not, eventually_curry_iff]

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

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b

Tactic:
rw [hb, totient_zero, totient_eq_zero] at h'

Goal state after:
case pos
a b : ℕ
h : a ∣ b
h' : a = 0
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * 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 : α
⊢ a ≡ b [PMOD p] ↔ toIcoDiv hp a b = toIocDiv hp a b + 1

Tactic:
by
  rw [modEq_iff_toIcoMod_add_period_eq_toIocMod hp, toIcoMod, toIocMod, ← eq_sub_iff_add_eq,
    sub_sub, sub_right_inj, ← add_one_zsmul, zsmul_left_inj hp]

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
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
⊢ x₃' ≤ toIocMod hp x₂' x₁

Tactic:
rcases le_or_gt x₃' (x₁ + p) with h₃₁ | h₁₃

Goal state after:
case inl
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₃₁ : x₃' ≤ x₁ + p
⊢ x₃' ≤ toIocMod hp x₂' x₁

case inr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
⊢ x₃' ≤ toIocMod hp x₂' x₁
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
b : α
⊢ toIcoMod hp 0 b = Int.fract (b / p) * p

Tactic:
simp [toIcoMod_eq_add_fract_mul]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
b : α
⊢ toIcoMod ⋯ 0 b = Int.fract b

Tactic:
simp [toIcoMod_eq_add_fract_mul]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
hf : IsOpenMap (f ∘ ⇑h)
⊢ IsOpenMap ((f ∘ ⇑h) ∘ ⇑h.symm)

Tactic:
exact hf.comp h.symm.isOpenMap

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 : AccPt (f x) l
⊢ AccPt x (comap f l)

Tactic:
rw [accPt_iff_clusterPt] at h ⊢
  apply (hf.clusterPt_comap h).mono
  rw [comap_inf, comap_principal, preimage_compl]
  exact inf_le_inf_right (comap f l) (by simp)

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsOpen[instTopologicalSpaceSum] (range inr)

Tactic:
exact isOpen_range_inr

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
⊢ IsClosed[instTopologicalSpaceSum] (range inr)

Tactic:
by
  rw [← isOpen_compl_iff, compl_range_inr]
  exact isOpen_range_inl

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
⊢ IsOpen[t] s ↔ ∀ a ∈ s, ∃ t ∈ b, a ∈ t ∧ t ⊆ s

Tactic:
by simp [isOpen_iff_mem_nhds, hb.mem_nhds_iff]

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

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
s t : Set α
⊢ IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t

Tactic:
by
  simp only [← isCobounded_compl_iff, compl_union, isCobounded_inter]

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 : Set α
hf : ContinuousOn f s
t u t' : Set β
h : u ∈ 𝓝ˢ[t'] t
v : Set β
hv : IsOpen[inst✝] v ∧ t ⊆ v ∧ v ∩ t' ⊆ u
w : Set α
hw : IsOpen[inst✝¹] w ∧ f ⁻¹' v ∩ s = w ∩ s
⊢ w ∩ (s ∩ f ⁻¹' t') ⊆ f ⁻¹' u

Tactic:
rw [← inter_assoc, ← hw.2, inter_comm _ s, inter_assoc, ← preimage_inter]
    exact inter_subset_right.trans <| preimage_mono hv.2.2

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

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
s t : α → Set β
ht : ∀ t_1 ∈ lb, ∀ᶠ (x : α) in la, t x ⊆ t_1
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ ∀ t ∈ lb, ∀ᶠ (x : α) in la, s x ⊆ t

Tactic:
exact fun u hu => (ht u hu).mp (hst.mono fun _ hst ht => hst.trans ht)

Goal state after:
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 Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
x : X
⊢ (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)

Tactic:
have H : U ∈ 𝓝 (f x) := hU.mem_nhds (hUZ.subset <| mem_range_self _).1

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactSpace Y
f : X → Y
hf : IsInducing f
U Z : Set Y
hU : IsOpen[inst✝¹] U
hZ : IsClosed[inst✝¹] Z
hUZ : range f = U ∩ Z
x : X
H : U ∈ 𝓝 (f x)
⊢ (𝓝 x).HasBasis (fun s ↦ (s ∈ 𝓝 (f x) ∧ IsCompact s) ∧ s ⊆ U) fun s ↦ f ⁻¹' (s ∩ Z)
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: case inr
X : Type u_1
ι : Type u_3
inst✝ : TopologicalSpace X
hι : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsCompact (s i)
h✝ : Nonempty ι
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
· -- If ι is non-empty, choose a surjection f : ℕ → ι, this yields a map ℕ → Set X.
    obtain ⟨f, hf⟩ := countable_iff_exists_surjective.mp hι
    exact ⟨s ∘ f, fun n ↦ hcomp (f n), Function.Surjective.iUnion_comp hf _⟩

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

Goal state before:
pp: X : Type u_1
ι : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι
s : ι → Set X
hcomp : ∀ (i : ι), IsSigmaCompact (s i)
⊢ IsSigmaCompact (⋃ i, s i)

Tactic:
by
  -- Choose a decomposition s_i = ⋃ K_i,j for each i.
  choose K hcomp hcov using fun i ↦ hcomp i
  -- Then, we have a countable union of countable unions of compact sets, i.e. countably many.
  have := calc
    ⋃ i, s i
    _ = ⋃ i, ⋃ n, (K i n) := by simp_rw [hcov]
    _ = ⋃ (i) (n : ℕ), (K.uncurry ⟨i, n⟩) := by rw [Function.uncurry_def]
    _ = ⋃ x, K.uncurry x := by rw [← iUnion_prod']
  rw [this]
  exact isSigmaCompact_iUnion_of_isCompact K.uncurry fun x ↦ (hcomp x.1 x.2)

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
⊢ l ≤ 𝓟 (f '' s) → ∃ x ∈ f '' s, ClusterPt x l

Tactic:
ls

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
⊢ ∃ x ∈ f '' s, ClusterPt x l
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsCompact s
this : ∀ (x : X), {x} ∈ 𝓝 x
⊢ s.Finite

Tactic:
rcases hs.elim_nhds_subcover (fun x => {x}) fun x _ => this x with ⟨t, _, hst⟩

Goal state after:
X : Type u
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology X
hs : IsCompact s
this : ∀ (x : X), {x} ∈ 𝓝 x
t : Finset X
left✝ : ∀ x ∈ t, x ∈ s
hst : s ⊆ ⋃ x ∈ t, {x}
⊢ s.Finite
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
t : Set α
⊢ s.sdiff t = s ↔ Disjoint (↑s) t

Tactic:
simp [← SetLike.coe_set_eq]

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ IsCompact s ↔ IsCompact (f '' s)

Tactic:
by
  refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot F_le => ?_⟩
  obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)
  exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩

Goal state after:
Module: Mathlib.Topology.Inseparable

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

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

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
H : IsClosed[instTopologicalSpaceProd] {q | π q.1 = π q.2}
⊢ IsClosed[instTopologicalSpaceProd] (diagonal Y)

Tactic:
simp_rw [← isOpen_compl_iff] at H ⊢

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
π : X → Y
h : IsOpenQuotientMap (Prod.map π π)
H : IsOpen[instTopologicalSpaceProd] {q | π q.1 = π q.2}ᶜ
⊢ IsOpen[instTopologicalSpaceProd] (diagonal Y)ᶜ
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hU : U ∈ 𝓝[≠] x
hs : Finite ↑s
⊢ U \ s ∈ 𝓝[≠] x

Tactic:
mem_nhdsWithin

Goal state after:
X : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
U s : Set X
hU : ∃ u, IsOpen[inst✝¹] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U
hs : Finite ↑s
⊢ ∃ u, IsOpen[inst✝¹] u ∧ x ∈ u ∧ u ∩ {x}ᶜ ⊆ U \ s
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case insert
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
a✝¹ : X
s✝ : Finset X
a✝ : a✝¹ ∉ s✝
ih : Dense (s \ ↑s✝)
⊢ Dense (s \ (↑s✝ ∪ {a✝¹}))

Tactic:
← sdiff_sdiff

Goal state after:
case insert
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
a✝¹ : X
s✝ : Finset X
a✝ : a✝¹ ∉ s✝
ih : Dense (s \ ↑s✝)
⊢ Dense ((s \ ↑s✝) \ {a✝¹})
Module: Mathlib.Topology.Separation.Hausdorff

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : T2Space Y
x : X
f g : X → Y
hf : ContinuousAt f x
hg : ContinuousAt g x
inst✝ : (𝓝[≠] x).NeBot
⊢ f =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g

Tactic:
constructor <;> intro hfg
  · apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE hfg
    by_contra hCon
    obtain ⟨a, ha⟩ : {x | f x ≠ g x ∧ f x = g x}.Nonempty := by
      have h₁ := (eventually_nhdsWithin_of_eventually_nhds
        ((hf.ne_iff_eventually_ne hg).1 hCon)).and hfg
      have h₂ : ∅ ∉ 𝓝[≠] x := by exact empty_notMem (𝓝[≠] x)
      simp_all
    simp at ha
  · exact hfg.filter_mono nhdsWithin_le_nhds

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x : X
s t : Set X
f : X → Y
y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x

Tactic:
rw [← continuousWithinAt_insert_self (s := s), ← continuousWithinAt_insert_self (s := t)]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space X
x : X
s t : Set X
f : X → Y
y : X
h : s =ᶠ[𝓝[{y}ᶜ] x] t
⊢ ContinuousWithinAt f (insert x s) x ↔ ContinuousWithinAt f (insert x t) x
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
hf : IsEmbedding f
s t : Set X
⊢ f '' s ∈ codiscreteWithin (f '' t) ↔ s ∈ codiscreteWithin t

Tactic:
by
  simp only [mem_codiscreteWithin_accPt, forall_mem_image, accPt_principal_iff_clusterPt,
    ← hf.mapClusterPt_iff, MapClusterPt, map_principal, image_sdiff hf.injective, image_singleton]

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
x : α
H : ∀ y ∈ s, ∃ t ⊆ s, x ∈ t ∧ y ∈ t ∧ IsPreconnected t
⊢ IsPreconnected s

Tactic:
rintro u v hu hv hs ⟨z, zs, zu⟩ ⟨y, ys, yv⟩

Goal state after:
α : 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
⊢ (s ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
⊢ IsConnected s ↔ ∃ i t, IsConnected t ∧ s = mk i '' t

Tactic:
refine ⟨fun hs => ?_, ?_⟩

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

case refine_2
ι : Type u_1
X : ι → Type u_2
inst✝ : (i : ι) → TopologicalSpace (X i)
s : Set ((i : ι) × X i)
⊢ (∃ i t, IsConnected t ∧ s = mk i '' t) → IsConnected s
Module: Mathlib.Topology.Connected.Clopen

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

Tactic:
refine ⟨fun hs => ?_, ?_⟩

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

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

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

Tactic:
refine ⟨fun hs => ?_, ?_⟩

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

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

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

Tactic:
refine ⟨fun hs => ?_, ?_⟩

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

case refine_2
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set (α ⊕ β)
⊢ ((∃ t, IsPreconnected t ∧ s = inl '' t) ∨ ∃ t, IsPreconnected t ∧ s = inr '' t) → IsPreconnected s