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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ IsCofiltered C ↔
    ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))

Tactic:
IsCofiltered.iff_cone_nonempty.{v}

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
⊢ (∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)) ↔
    ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
inst✝ : L.HasPointwiseRightKanExtensionAt F Y₁
⊢ L.HasPointwiseRightKanExtensionAt F Y₂

Tactic:
change HasLimit ((StructuredArrow.mapIso e.symm).functor ⋙ StructuredArrow.proj Y₁ L ⋙ F)

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
inst✝ : L.HasPointwiseRightKanExtensionAt F Y₁
⊢ HasLimit ((StructuredArrow.mapIso e.symm).functor ⋙ StructuredArrow.proj Y₁ L ⋙ F)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E E' : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
⊢ ((whiskeringLeft C D H).obj L).map { app := fun Y ↦ (h Y).lift (G.coneAt Y), naturality := ⋯ } ≫
      CostructuredArrow.hom E =
    CostructuredArrow.hom G

Tactic:
ext X
      simpa using (h (L.obj X)).fac (RightExtension.coneAt G _) (StructuredArrow.mk (𝟙 _))

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
x : F.obj (op X)
⊢ (unitForward η X ∘ unitBackward η X) x = id x

Tactic:
simp [unitForward, unitBackward]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ OverArrows.val ((ConcreteCategory.hom ((restrictedYonedaObj η).map (eqToHom ⋯))) (id p).snd) =
    OverArrows.val ((unitBackward η X ∘ unitForward η X) p).snd

Tactic:
simp [unitForward, unitBackward]

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

Goal state before:
pp: case refine_2.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel.lift (cokernel.π f) f ⋯ ≫ monoLift f (kernel.ι (cokernel.π f)) ⋯ = 𝟙 A

pp: case refine_2.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ { hom := monoLift f (kernel.ι (cokernel.π f)) ⋯, inv := kernel.lift (cokernel.π f) f ⋯, hom_inv_id := ⋯,
          inv_hom_id := ?refine_2.refine_4 }.hom ≫
      f =
    kernel.ι (cokernel.π f)

Tactic:
· simp only [← cancel_mono f, Category.assoc, monoLift_comp, image.fac, Category.id_comp]

Goal state after:
case refine_2.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ { hom := monoLift f (kernel.ι (cokernel.π f)) ⋯, inv := kernel.lift (cokernel.π f) f ⋯, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      f =
    kernel.ι (cokernel.π f)
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : Cofan F
⊢ Nonempty (IsColimit c) ↔ Function.Bijective (CofanTypes.fromSigma F c.cofanTypes)

Tactic:
by
  rw [← isColimit_cofanTypes_iff, CofanTypes.isColimit_iff_bijective_fromSigma]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : CategoryTheory.Injective (ModuleCat.of R M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
⊢ ∃ h, ∀ (x : X), h (f x) = g x

Tactic:
by
    have : CategoryTheory.Mono (ModuleCat.ofHom f) := (ModuleCat.mono_iff_injective _).mpr hf
    obtain ⟨l, h⟩ := inj.factors (ModuleCat.ofHom g) (ModuleCat.ofHom f)
    obtain rfl := ModuleCat.hom_ext_iff.mp h
    exact ⟨l.hom, fun _ => rfl⟩

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul au ^ (z₁ * z₂).val = Additive.toMul au ^ (z₂.val * z₁.val)

Tactic:
ZMod.val_mul,

Goal state after:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul au ^ (z₁.val * z₂.val % 2) = Additive.toMul au ^ (z₂.val * z₁.val)
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case inl
n : ℤ
h : |n| = n
⊢ |n|.negOnePow = n.negOnePow

Tactic:
simp only [h, negOnePow_neg]

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

Goal state before:
pp: case inr
n : ℤ
h : |n| = -n
⊢ |n|.negOnePow = n.negOnePow

Tactic:
simp only [h, negOnePow_neg]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddCommMonoid α
hf : Periodic f c
x : α
m : ℕ
⊢ f (⟨(fun i ↦ i • c) m, ⋯⟩ +ᵥ x) = f x

Tactic:
simp [AddSubmonoid.vadd_def, add_comm _ x, hf.nsmul m x]

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

Goal state before:
pp: case h
ι : Type u_1
ι' : Type u_2
b : Finset (ι × ι')
⊢ b ⊆ (Finset.image Prod.fst b, Finset.image Prod.snd b).1 ×ˢ (Finset.image Prod.fst b, Finset.image Prod.snd b).2

Tactic:
exact Finset.subset_product

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

Goal state before:
pp: β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ m < n, N ≤ m → u m ≤ u k
⊢ ∃ n ≥ N, ∀ k < n, u k < u n

Tactic:
use n, hnN

Goal state after:
case right
β : Type u_4
inst✝¹ : LinearOrder β
inst✝ : NoMaxOrder β
u : ℕ → β
hu : Tendsto u atTop atTop
N k : ℕ
hku : ∀ l ≤ N, u l ≤ u k
ex : ∃ n ≥ N, u k < u n
n : ℕ
hnN : n ≥ N
hnk : u k < u n
hn_min : ∀ m < n, N ≤ m → u m ≤ u k
⊢ ∀ k < n, u k < u n
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: c d : ℕ
⊢ ∀ (b : ℕ), 2 * (c ^ 2 + d + 1) ≤ b → c ^ b < (b - d)!

Tactic:
intro n hn

Goal state after:
c d n : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ n
⊢ c ^ n < (n - d)!
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: case e'_4
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ (2 * (c ^ 2 + d + 1) + d' - d)! = (c ^ 2 + (c ^ 2 + d' + d + 1) + 1)!

Tactic:
congr 1
    lia

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 : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
ho : -b - toIcoDiv hp a (-b) • p < a + p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)

Tactic:
rw [← neg_lt_neg_iff, neg_sub' (-b), neg_neg, ← neg_smul] at ho

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
hc : a ≤ -b - toIcoDiv hp a (-b) • p
ho : -(a + p) < b - -toIcoDiv hp a (-b) • p
⊢ b - -toIcoDiv hp a (-b) • p ∈ Set.Ioc (-(a + p)) (-(a + p) + p)
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 - p) b = toIcoMod hp a b - p

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

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
h : Disjoint (closure s) (closure t)
⊢ interior sᶜ ∪ interior tᶜ = univ

Tactic:
simpa [disjoint_iff, ← compl_inter] using h

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s \ closure s ∪ s ∩ interior s = interior s

Tactic:
sdiff_eq_empty.2 subset_closure,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ ∅ ∪ s ∩ interior s = interior s
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed[inst✝] s ↔ ∀ (a : X), AccPt a (𝓟 s) → a ∈ s

Tactic:
by
  simp [isClosed_iff_clusterPt, clusterPt_principal, or_imp]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : 𝓝 x ⊓ (𝓟 s₁ ⊔ 𝓟 s₂) ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥

Tactic:
inf_sup_left,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s₁ s₂ : Set X
h : 𝓝 x ⊓ 𝓟 s₁ ⊔ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
h₁ : s₁ᶜ ∈ 𝓝 x
⊢ 𝓝 x ⊓ 𝓟 s₂ ≠ ⊥
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
s : Set (Set α)
hs : {u | GenerateOpen s u} = s
⊢ IsOpen[TopologicalSpace.mkOfClosure s hs] = IsOpen[generateFrom s]

Tactic:
by ext U; exact Set.ext_iff.mp hs.symm U

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
t₂ : TopologicalSpace α
inst✝ : IndiscreteTopology α
U : Set α
⊢ IsOpen[t₂] U ↔ U = ∅ ∨ U = univ

Tactic:
cases IndiscreteTopology.eq_top α

Goal state after:
case refl
α : Type u_1
U : Set α
inst✝ : IndiscreteTopology α
⊢ IsOpen[⊤] U ↔ U = ∅ ∨ U = univ
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : IndiscreteTopology α
a : α
⊢ 𝓝 a = ⊤

Tactic:
cases IndiscreteTopology.eq_top α

Goal state after:
case refl
α : Type u
a : α
inst✝ : IndiscreteTopology α
⊢ 𝓝 a = ⊤
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
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
hfg : IsClosedMap (g ∘ f)
⊢ IsClosedMap g

Tactic:
intro K

Goal state after:
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
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
hfg : IsClosedMap (g ∘ f)
K : Set Y
⊢ IsClosed[inst✝¹] K → IsClosed[inst✝] (g '' K)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
⊢ (∃ t_1, IsOpen[inst✝¹] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t) → ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s

Tactic:
rintro ⟨u, ou, useq⟩

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen[inst✝¹] u
useq : s ∩ u = s ∩ f ⁻¹' t
⊢ ∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
⊢ (∃ u, IsOpen[inst✝¹] u ∧ f ⁻¹' t ∩ s = u ∩ s) → ∃ t_1, IsOpen[inst✝¹] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t

Tactic:
rintro ⟨u, ou, useq⟩

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
t : Set β
u : Set α
ou : IsOpen[inst✝¹] u
useq : f ⁻¹' t ∩ s = u ∩ s
⊢ ∃ t_1, IsOpen[inst✝¹] t_1 ∧ s ∩ t_1 = s ∩ f ⁻¹' t
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen[inst✝¹] t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x

Tactic:
rcases h x xs with ⟨t, open_t, xt, ct⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ∀ x ∈ s, ∃ t, IsOpen[inst✝¹] t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
t : Set α
open_t : IsOpen[inst✝¹] t
xt : x ∈ t
ct : ContinuousOn f (s ∩ t)
⊢ ContinuousWithinAt f s x
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
h : ContinuousOn f univ
⊢ ContinuousOn f s

Tactic:
exact h.mono (subset_univ _)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set (Set α)
h : IsTopologicalBasis s
⊢ ∀ u ∈ insert ∅ s, IsOpen[t] u

Tactic:
by rintro _ (rfl | hu); exacts [isOpen_empty, h.isOpen hu]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
a : (a : ι) → A a
x✝ : a ∈ s
⊢ (∃ u, (∀ (a_1 : ι), IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ univ.pi u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s

Tactic:
exact fun ⟨u, ⟨h1, _⟩⟩ =>
      ⟨Finset.univ, u, ⟨fun i => ⟨u i, ⟨rfl.subset, h1 i⟩⟩, by rwa [Finset.coe_univ]⟩⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_2
ι : Type u_5
X : ι → Type u_9
g : (a : ι) → Set (Set (X a))
inst✝ : Finite ι
hg : ∀ (a : ι), ⋃₀ g a = univ
val✝ : Fintype ι
t : (a : ι) → Set (X a)
i : Finset ι
ht : ∀ a ∈ i, t a ∈ g a
this : TopologicalSpace ((i : ι) → X i) := generateFrom {t | ∃ s, (∀ (a : ι), s a ∈ g a) ∧ t = univ.pi s}
f : (i : ι) → X i
hf : f ∈ (↑i).pi t
c : (a : ι) → Set (X a)
hcg : ∀ (a : ι), c a ∈ g a
hfc : ∀ (a : ι), f a ∈ c a
a : ι
⊢ (↑i).piecewise t c a ∈ g a

Tactic:
by_cases a ∈ i <;> simp [*]

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
K : Set X
hK : IsCompact K
⊢ ∀ (i : Set X), IsOpen[inst✝¹] i ∧ K ⊆ i → ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ i

Tactic:
intro U ⟨hU, h_KU⟩

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : LocallyCompactSpace X
K : Set X
hK : IsCompact K
U : Set X
hU : IsOpen[inst✝¹] U
h_KU : K ⊆ U
⊢ ∃ r ∈ 𝓝ˢ K, IsCompact r ∧ r ⊆ U
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
⊢ 𝓝[⋃ i, f i] a = ⨆ i, 𝓝[f i] a

Tactic:
rcases hf a with ⟨U, haU, hfin⟩
  refine le_antisymm ?_ (Monotone.le_map_iSup fun _ _ ↦ nhdsWithin_mono _)
  calc
    𝓝[⋃ i, f i] a = 𝓝[⋃ i, f i ∩ U] a := by
      rw [← iUnion_inter, ← nhdsWithin_inter_of_mem' (nhdsWithin_le_nhds haU)]
    _ = 𝓝[⋃ i ∈ {j | (f j ∩ U).Nonempty}, (f i ∩ U)] a := by
      simp only [mem_ofPred_eq, iUnion_nonempty_self]
    _ = ⨆ i ∈ {j | (f j ∩ U).Nonempty}, 𝓝[f i ∩ U] a := nhdsWithin_biUnion hfin _ _
    _ ≤ ⨆ i, 𝓝[f i ∩ U] a := iSup₂_le_iSup _ _
    _ ≤ ⨆ i, 𝓝[f i] a := iSup_mono fun i ↦ nhdsWithin_mono _ inter_subset_left

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

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) (interior ∘ ⇑K)

Tactic:
exact Monotone.directed_le fun _ _ h ↦ interior_mono <| K.subset h

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
⊢ IsCompact (insert y (range f))

Tactic:
intro l hne hle

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
y : Y
hf : Tendsto f (cocompact X) (𝓝 y)
hfc : Continuous[inst✝¹, inst✝] f
l : Filter Y
hne : l.NeBot
hle : l ≤ 𝓟 (insert y (range f))
⊢ ∃ x ∈ insert y (range f), ClusterPt x l
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs₁ : IsClosed[inst✝] s
hs₂ : IsCompact s
t : Set X
ht₁ : IsClosed[inst✝] t
ht₂ : IsCompact t
⊢ ∃ k, (IsClosed[inst✝] k ∧ IsCompact k) ∧ kᶜ ⊆ sᶜ ∧ kᶜ ⊆ tᶜ

Tactic:
exact ⟨s ∪ t, ⟨⟨hs₁.union ht₁, hs₂.union ht₂⟩, compl_subset_compl.2 subset_union_left,
    compl_subset_compl.2 subset_union_right⟩⟩

Goal state after:
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
s : Set X
f g : X → Y
inst✝ : DecidablePred fun x ↦ x ∈ s
hs : IsOpen[inst✝²] s
hf : Continuous[inst✝², inst✝¹] f
hg : Continuous[inst✝², inst✝¹] g
hspec : ∀ (x : X), f x ⤳ g x
⊢ Continuous[inst✝², inst✝¹] (s.piecewise f g)

Tactic:
have : ∀ U, IsOpen U → g ⁻¹' U ⊆ f ⁻¹' U := fun U hU x hx ↦ (hspec x).mem_open hU hx
  rw [continuous_def]
  intro U hU
  rw [piecewise_preimage, ite_eq_of_subset_right _ (this U hU)]
  exact hU.preimage hf |>.inter hs |>.union (hU.preimage hg)

Goal state after:
Module: Mathlib.Topology.Piecewise

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s s' t : Set α
hs : IsOpen[inst✝] s
hs' : IsOpen[inst✝] s'
ht : ∀ x ∈ frontier t, x ∈ s ↔ x ∈ s'
⊢ IsOpen[inst✝] (t.ite s s')

Tactic:
by
  classical
    simp only [isOpen_iff_continuous_mem, Set.ite] at *
    convert!
      continuous_piecewise (fun x hx => propext (ht x hx)) hs.continuousOn hs'.continuousOn using 2
    rename_i x
    by_cases hx : x ∈ t <;> simp [hx]

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

Goal state before:
pp: ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
⊢ (Filter.coprodᵢ fun d ↦ cocompact (X d)) = cocompact ((d : ι) → X d)

Tactic:
refine le_antisymm (iSup_le fun i => Filter.comap_cocompact_le (continuous_apply i)) ?_

Goal state after:
ι : Type u_1
X : ι → Type u_3
inst✝ : (d : ι) → TopologicalSpace (X d)
⊢ cocompact ((d : ι) → X d) ≤ Filter.coprodᵢ fun d ↦ cocompact (X d)
Module: Mathlib.Topology.DiscreteSubset

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

Tactic:
obtain ⟨t, h₁t, h₂t⟩ := 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
t : Set X
h₁t : t ∈ 𝓝[≠] z
h₂t : t ∩ (U \ s) = ∅
⊢ ∃ t ∈ 𝓝[≠] z, t ⊆ (U \ s)ᶜ
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h₂
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ Z ⊆ closure[inst✝] (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ)

Tactic:
apply subset_closure_inter_of_isPreirreducible_of_isOpen hZ.1.2

Goal state after:
case h₂.hU
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ IsOpen[inst✝] (⋃₀ (irreducibleComponents X \ {Z}))ᶜ

case h₂.h
X : Type u_1
inst✝ : TopologicalSpace X
hX : (irreducibleComponents X).Finite
Z : Set X
hZ : Z ∈ irreducibleComponents X
h : (⋃₀ (irreducibleComponents X \ {Z}))ᶜ ⊆ Z
⊢ (Z ∩ (⋃₀ (irreducibleComponents X \ {Z}))ᶜ).Nonempty
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

Goal state after:
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 ∉ U \ s
h₂a : ¬a = x
⊢ a ∈ (U \ s)ᶜ
Module: Mathlib.Topology.Separation.Hausdorff

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

Tactic:
by
  constructor
  rintro (x | x) (y | y) h
  · exact separated_by_isOpenEmbedding .inl <| ne_of_apply_ne _ h
  · exact separated_by_continuous continuous_isLeft <| by simp
  · exact separated_by_continuous continuous_isLeft <| by simp
  · exact separated_by_isOpenEmbedding .inr <| ne_of_apply_ne _ h

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
i✝ : T2Quotient X
x : X
j✝ : T2Quotient X
y : X
h : ¬mk x = mk y
⊢ ∃ s, T2Space (Quotient s) ∧ ⟦x⟧ ≠ ⟦y⟧

Tactic:
by
    simpa [T2Quotient.mk_eq, Quotient.eq] using h

Goal state after:
Module: Mathlib.Order.SuccPred.Relation

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

Tactic:
· intro m hnm ih h
    have : ReflTransGen r n m := ih fun i hi => h i ⟨hi.1, hi.2.trans_le <| le_succ m⟩
    rcases (le_succ m).eq_or_lt with hm | hm
    · rwa [← hm]
    exact this.tail (h m ⟨hnm, hm⟩)

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

Goal state before:
pp: case insert.refine_2.inl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
ι : Type u_3
t : Finset ι
ih :
  ∀ {s : Set X},
    IsCompact s →
      ∀ (U : ι → Set X),
        (∀ i ∈ t, IsOpen[inst✝¹] (U i)) →
          s ⊆ ⋃ i ∈ t, U i → ∃ K, (∀ (i : ι), IsCompact (K i)) ∧ (∀ (i : ι), K i ⊆ U i) ∧ s = ⋃ i ∈ t, K i
s : Set X
hs : IsCompact s
U : ι → Set X
hU' : ∀ i ∈ t, IsOpen[inst✝¹] (U i)
K₁ K₂ : Set X
h1K₁ : IsCompact K₁
h1K₂ : IsCompact K₂
h2K₂ : K₂ ⊆ ⋃ i ∈ ↑t, U i
hK : s = K₁ ∪ K₂
K : ι → Set X
h1K : ∀ (i : ι), IsCompact (K i)
h2K : ∀ (i : ι), K i ⊆ U i
h3K : K₂ = ⋃ i ∈ t, K i
i : ι
hx : i ∉ t
hsC : s ⊆ U i ∪ ⋃ x ∈ t, U x
hU : IsOpen[inst✝¹] (U i) ∧ ∀ x ∈ t, IsOpen[inst✝¹] (U x)
h2K₁ : K₁ ⊆ U i
⊢ update K i K₁ i ⊆ U i

Tactic:
simp only [update_self, h2K₁]

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

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

Tactic:
exact this.imp fun z hz => ⟨ts hz.1, hz.2⟩

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
⊢ ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s

Tactic:
have hc : IsCompact (f '' K \ interior s) := (hKc.image hf).diff isOpen_interior

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)
⊢ ∃ L ∈ 𝓝 x, IsCompact L ∧ MapsTo f L s
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
S : Set (Set α)
K : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) S
H : ∀ s ∈ S, IsPreconnected s
⊢ IsPreconnected (⋃₀ S)

Tactic:
by
  rintro u v hu hv Huv ⟨a, ⟨s, hsS, has⟩, hau⟩ ⟨b, ⟨t, htS, hbt⟩, hbv⟩
  obtain ⟨r, hrS, hsr, htr⟩ : ∃ r ∈ S, s ⊆ r ∧ t ⊆ r := K s hsS t htS
  have Hnuv : (r ∩ (u ∩ v)).Nonempty :=
    H _ hrS u v hu hv ((subset_sUnion_of_mem hrS).trans Huv) ⟨a, hsr has, hau⟩ ⟨b, htr hbt, hbv⟩
  have Kruv : r ∩ (u ∩ v) ⊆ ⋃₀ S ∩ (u ∩ v) := inter_subset_inter_left _ (subset_sUnion_of_mem hrS)
  exact Hnuv.mono Kruv

Goal state after: