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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
⊢ ∀ ⦃A B : Cᵒᵖ⦄ (f : A ⟶ op X) (g : B ⟶ op X) [inst : Mono f] [inst_1 : Mono g],
    Subobject.mk f ≤ Subobject.mk g →
      Subobject.lift (fun x f x_1 ↦ Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk f) ≤
        Subobject.lift (fun x f x_1 ↦ Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk g)

Tactic:
by
      intro A B f g hf hg h
      dsimp only [Subobject.lift_mk]
      refine Subobject.mk_le_mk_of_comm (kernel.lift g.unop (kernel.ι f.unop) ?_) ?_
      · rw [← Subobject.ofMkLEMk_comp h, unop_comp, kernel.condition_assoc, zero_comp]
      · exact Quiver.Hom.op_inj (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.desc prod.fst.op prod.snd.op ≫ (prod.lift coprod.inl.unop coprod.inr.unop).op = 𝟙 (op A ⨿ op B)

Tactic:
by
    ext <;>
    · simp only [colimit.ι_desc_assoc]
      apply Quiver.Hom.unop_inj
      simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ (prod.lift coprod.inl.unop coprod.inr.unop ≫ prod.snd).op = coprod.inr

Tactic:
prod.lift_snd,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inr.unop.op = coprod.inr
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
α : Type w
inst✝ : HasFiniteCoproducts C
I : Finset (Discrete α)
X✝ Y✝ : Discrete α ⥤ C
x✝ : X✝ ⟶ Y✝
⊢ (liftToFinset C α ⋙ (evaluation (Finset (Discrete α)) C).obj I).map x✝ ≫
      (HasColimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl ((Discrete.functor fun x ↦ Y✝.obj ↑x).obj x))).hom =
    (HasColimit.isoOfNatIso (Discrete.natIso fun x ↦ Iso.refl ((Discrete.functor fun x ↦ X✝.obj ↑x).obj x))).hom ≫
      ((Functor.whiskeringLeft (Discrete ↥I) (Discrete α) C).obj (Discrete.functor fun x ↦ ↑x) ⋙ colim).map x✝

Tactic:
by dsimp; ext; simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ (map₁ η p).yonedaEquivFst = p.yonedaEquivFst

Tactic:
by
  simp only [YonedaCollection.yonedaEquivFst_eq, map₁_fst]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Adjunction

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
⊢ (L.ranAdjunction H).counit = L.ranCounit

Tactic:
ext F : 2
  dsimp [ranAdjunction, homEquivOfIsRightKanExtension]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
y y' : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
f : y ⟶ y'
⊢ A.map f.left ≫ (uliftYonedaEquiv (y'.hom ≫ g)).down = (uliftYonedaEquiv (y.hom ≫ g)).down

Tactic:
← CostructuredArrow.w f,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
g : P ⟶ (restrictedULiftYoneda A).obj E
y y' : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
f : y ⟶ y'
⊢ A.map f.left ≫ (uliftYonedaEquiv (y'.hom ≫ g)).down =
    (uliftYonedaEquiv ((uliftYoneda.{max w v₂, v₁, u₁}.map f.left ≫ y'.hom) ≫ g)).down
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
⊢ g = h

Tactic:
refine hP _ _ fun G hG i => ?_

Goal state after:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
G : C
hG : P G
i : G ⟶ Y
⊢ i ≫ g = i ≫ h
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: case refine_2
M : Type u_1
inst✝² : AddCommGroup M
R : Type u
inst✝¹ : CommRing R
inst✝ : Module R M
h : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Ideal R
g : ↥I →ₗ[R] M
⊢ ∃ g', ∀ (x : R) (mem : x ∈ I), g' x = g ⟨x, mem⟩

Tactic:
· rcases h I g with ⟨g', hg'⟩
    use g'
    intro x hx
    simp [← hg']

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = Fintype.card { k // k < n ∧ p k }

Tactic:
rw [count_eq_card_filter_range, Fintype.card_of_subtype]

Goal state after:
case H
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ ∀ (x : ℕ), x ∈ {x ∈ range n | p x} ↔ x < n ∧ p x
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inr.i_inj
d : ℕ
hd0 : d > 0
x : ℕ
⊢ ∀ a₁ ∈ {a ∈ range x | x.Coprime a}, ∀ a₂ ∈ {a ∈ range x | x.Coprime a}, d * a₁ = d * a₂ → a₁ = a₂

Tactic:
simp [hd0.ne']

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

Goal state before:
pp: case inr.i_surj
d : ℕ
hd0 : d > 0
x b : ℕ
⊢ b < d * x → (d * x).gcd b = d → ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b

Tactic:
hb1

Goal state after:
case inr.i_surj
d : ℕ
hd0 : d > 0
x b : ℕ
hb1 : b < d * x
⊢ (d * x).gcd b = d → ∃ a, (a < x ∧ x.Coprime a) ∧ d * a = b
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: case refine_1
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirectedOrder α
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n ↦ List.foldl (fun x n ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
⊢ Monotone xs

Tactic:
refine monotone_nat_of_le_succ fun n ↦ ?_

Goal state after:
case refine_1
α : Type u_3
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : IsDirectedOrder α
inst✝ : atTop.IsCountablyGenerated
ys : ℕ → α
h : Tendsto ys atTop atTop
c : α → α → α
hleft : ∀ (a b : α), a ≤ c a b
hright : ∀ (a b : α), b ≤ c a b
xs : ℕ → α := fun n ↦ List.foldl (fun x n ↦ c x (ys n)) (ys 0) (List.range n)
hsucc : ∀ (n : ℕ), xs (n + 1) = c (xs n) (ys n)
n : ℕ
⊢ xs n ≤ xs (n + 1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inl
b : ℕ
h : 0 ∣ b
⊢ φ 0 ∣ φ b

Tactic:
simp [zero_dvd_iff.1 h]

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

Tactic:
toIcoDiv_add_right

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b + 1 = toIcoDiv hp a b + 1
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
f : Filter α
s : Set α
hs : s ∈ f
⊢ f ≤ 𝓟 s

Tactic:
by simp only [hs, le_principal_iff]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ (interior s)ᶜ ∩ interior s ∩ closure s = ∅

Tactic:
compl_inter_self,

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsOpen s
⊢ s ∩ frontier s = ∅

Tactic:
rw [hs.frontier_eq, inter_sdiff_self]

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

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

Tactic:
suffices hIoc₂₁ : toIocMod hp x₂' x₁ = x₁ + p from hIoc₂₁.trans_ge h₃₁
    apply (toIocMod_eq_iff hp).2
    exact ⟨⟨h₂₁, by simp [x₂', left_le_toIcoMod]⟩, -1, by simp⟩

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 : α
this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a) ≤ p
⊢ toIcoMod hp b a ≤ toIocMod hp b c ∨ toIcoMod hp b c ≤ toIocMod hp b a

Tactic:
rw [toIxxMod_iff, toIxxMod_iff]

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
this : toIcoMod hp 0 (a - b) + toIocMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIocMod hp 0 (b - a) ≤ p
⊢ toIcoMod hp 0 (a - b) + toIcoMod hp 0 (b - c) ≤ p ∨ toIcoMod hp 0 (c - b) + toIcoMod hp 0 (b - a) ≤ p
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s₁ s₂ t₁ t₂ : Set X
sc_st : HasSeparatingCover s₂ t₂
s_sub : s₁ ⊆ s₂
t_sub : t₁ ⊆ t₂
⊢ HasSeparatingCover s₁ t₁

Tactic:
by
  obtain ⟨u, u_cov, u_props⟩ := sc_st
  exact
    ⟨u,
     s_sub.trans u_cov,
     fun n ↦
       ⟨(u_props n).1,
        disjoint_of_subset (fun ⦃_⦄ a ↦ a) t_sub (u_props n).2⟩⟩

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
h₁ : Continuous[inst✝¹, inst✝] f
h₂ : Injective f
h₃ : IsOpenMap f
⊢ ∀ (x : X), 𝓝 x = comap f (𝓝 (f x))

Tactic:
exact fun x =>
    le_antisymm (h₁.tendsto _).le_comap (@comap_map _ _ (𝓝 x) _ h₂ ▸ comap_mono (h₃.nhds_le _))

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
h : Disjoint (𝓝 x) (𝓝 y)
U : Set X
hU : x ∈ U ∧ IsOpen[inst✝] U
V : Set X
hV : y ∈ V ∧ IsOpen[inst✝] V
hd : Disjoint U V
⊢ {p | Disjoint (𝓝 p.1) (𝓝 p.2)} ∈ 𝓝 (x, y)

Tactic:
exact mem_nhds_prod_iff'.mpr ⟨U, V, hU.2, hU.1, hV.2, hV.1, fun ⟨x', y'⟩ ⟨hx', hy'⟩ =>
    disjoint_of_disjoint_of_mem hd (hU.2.mem_nhds hx') (hV.2.mem_nhds hy')⟩

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

Goal state before:
pp: X : Type u_5
Y : Type u_6
s : Set (Set X)
t : Set (Set Y)
hs : ⋃₀ s = univ
ht : ⋃₀ t = univ
G : TopologicalSpace (X × Y) := generateFrom (image2 (fun x1 x2 ↦ x1 ×ˢ x2) s t)
v : Set Y
hv : v ∈ t
this : ⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v
⊢ TopologicalSpace.IsOpen (Prod.snd ⁻¹' v)

Tactic:
rw [← this]
            exact
              isOpen_iUnion fun u =>
                isOpen_iUnion fun hu => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
hs : s ∈ b
⊢ IsOpen[t] s

Tactic:
rw [hb.eq_generateFrom]

Goal state after:
α : Type u
t : TopologicalSpace α
s : Set α
b : Set (Set α)
hb : IsTopologicalBasis b
hs : s ∈ b
⊢ IsOpen[generateFrom b] s
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Set β)
hB : IsTopologicalBasis B
f : α → β
⊢ Continuous[t, inst✝] f ↔ ∀ s ∈ B, IsOpen[t] (f ⁻¹' s)

Tactic:
by
  rw [hB.eq_generateFrom, continuous_generateFrom_iff]

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : LE α
x : α
z : β
⊢ z ∈ accumulate s x ↔ ∃ y ≤ x, z ∈ s y

Tactic:
simp_rw [accumulate_def, mem_iUnion₂, exists_prop]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_9
g : (a : ι) → Set (Set (A a))
⊢ Pi.topologicalSpace = generateFrom {t | ∃ s i, (∀ a ∈ i, s a ∈ g a) ∧ t = (↑i).pi s}

Tactic:
by
  refine le_antisymm ?_ ?_
  · apply le_generateFrom
    rintro _ ⟨s, i, hi, rfl⟩
    let := fun a => generateFrom (g a)
    exact isOpen_set_pi i.finite_toSet (fun a ha => GenerateOpen.basic _ (hi a ha))
  · classical
    refine le_iInf fun i => coinduced_le_iff_le_induced.1 <| le_generateFrom fun s hs => ?_
    refine GenerateOpen.basic _ ⟨update (fun i => univ) i s, {i}, ?_⟩
    simp [hs]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
⊢ (∃ c, c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ s, s.Countable ∧ univ ⊆ closure[t] s

Tactic:
← hs.closure_eq,

Goal state after:
α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
⊢ (∃ c, c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ s_1, s_1.Countable ∧ closure[t] s ⊆ closure[t] s_1
Module: Mathlib.Topology.Bases

Goal state before:
pp: case a
α : Type u
t : TopologicalSpace α
inst✝¹ : Countable α
inst✝ : FirstCountableTopology α
b : α → ℕ → Set α
hxb : ∀ (x : α) (i : ℕ), x ∈ b x i ∧ IsOpen[t] (b x i)
hbb : ∀ (x : α), (𝓝 x).HasAntitoneBasis fun i ↦ b x i
x : α
n : ℕ
a✝ : True
⊢ IsOpen[generateFrom (range (uncurry b))] (b x n)

Tactic:
exact isOpen_generateFrom_of_mem ⟨⟨x, n⟩, rfl⟩

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
ι : Sort u_2
inst✝ : Countable ι
t : ι → TopologicalSpace α
ht : ∀ (i : ι), SecondCountableTopology α
⊢ SecondCountableTopology α

Tactic:
exact SecondCountableTopology.mk' <|
    countable_iUnion fun i => @countable_countableBasis _ (t i) (ht i)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2.h₁
α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
T : Set ↑u
T_count : T.Countable
hT : ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i
⊢ u ⊆ ⋃ i, a ↑i

Tactic:
intro x hx
    simp
    grind

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

Goal state before:
pp: case refine_1
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ s.pi n'' ∈ 𝓝 t

pp: case refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
x✝ : (i : ι) → X i
⊢ x✝ ∈ s.pi n'' → x✝ ∈ s.pi n'

pp: case refine_3
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ IsCompact (s.pi n'')

Tactic:
· exact (set_pi_mem_nhds_iff hs _).mpr fun i _ => hn'' i

Goal state after:
case refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
x✝ : (i : ι) → X i
⊢ x✝ ∈ s.pi n'' → x✝ ∈ s.pi n'

case refine_3
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s✝ t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
s : Set ι
hs : s.Finite
n' : (i : ι) → Set (X i)
hn' : ∀ (i : ι), n' i ∈ 𝓝 (t i)
hsub : s.pi n' ⊆ n
n'' : (i : ι) → Set (X i)
hn'' : ∀ (i : ι), n'' i ∈ 𝓝 (t i)
hsub' : ∀ (i : ι), n'' i ⊆ n' i
hc : ∀ (i : ι), IsCompact (n'' i)
⊢ IsCompact (s.pi n'')
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: case inr
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
h✝ : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
⊢ SigmaCompactSpace ((i : ι) × X i)

Tactic:
refine ⟨⟨fun n => ⋃ k ≤ n, Sigma.mk (f k) '' compactCovering (X (f k)) n, fun n => ?_, ?_⟩⟩

Goal state after:
case inr.refine_1
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
h✝ : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
n : ℕ
⊢ IsCompact ((fun n ↦ ⋃ k, ⋃ (_ : k ≤ n), Sigma.mk (f k) '' compactCovering (X (f k)) n) n)

case inr.refine_2
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁵ : TopologicalSpace X✝
inst✝⁴ : TopologicalSpace Y
s t : Set X✝
inst✝³ : SigmaCompactSpace X✝
inst✝² : Countable ι
X : ι → Type u_4
inst✝¹ : (i : ι) → TopologicalSpace (X i)
inst✝ : ∀ (i : ι), SigmaCompactSpace (X i)
h✝ : Nonempty ι
f : ℕ → ι
hf : Function.Surjective f
⊢ ⋃ n, (fun n ↦ ⋃ k, ⋃ (_ : k ≤ n), Sigma.mk (f k) '' compactCovering (X (f k)) n) n = univ
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝[s] x
⊢ ∃ t, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

Tactic:
choose! V V_nhds hV using fun x hx => mem_nhdsWithin_iff_exists_mem_nhds_inter.1 (hU x hx)

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝[s] x
V : X → Set X
V_nhds : ∀ x ∈ s, V x ∈ 𝓝 x
hV : ∀ x ∈ s, V x ∩ s ⊆ U x
⊢ ∃ t, (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
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
⊢ ∃ x ∈ s, ↑F ≤ 𝓝 x

Tactic:
by_contra hF

Goal state after:
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
⊢ False
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ Q ⊆ P, Q.Finite → ⋃₀ Q ≠ univ
⊢ ⋃₀ P ≠ univ

Tactic:
← Set.nonempty_compl,

Goal state after:
X : Type u
T : TopologicalSpace X
𝔅 : Set (Set X)
hT : T = generateFrom 𝔅
h𝔅 : ∀ s ∈ 𝔅, sᶜ ∈ 𝔅
h : ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty
P : Set (Set X)
hP𝔅 : P ⊆ 𝔅
hP : ∀ Q ⊆ P, Q.Finite → (⋃₀ Q)ᶜ.Nonempty
⊢ (⋃₀ P)ᶜ.Nonempty
Module: Mathlib.Topology.Inseparable

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x x✝ : X
⊢ x✝ ∈ (𝓝 x).ker ↔ x✝ ∈ {y | y ⤳ x}

Tactic:
simp [specializes_iff_pure, le_def]

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
S : Set Y
⊢ IsDiscrete S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥

Tactic:
isDiscrete_iff_discreteTopology,

Goal state after:
Y : Type u_2
inst✝ : TopologicalSpace Y
S : Set Y
⊢ DiscreteTopology ↑S ↔ ∀ x ∈ S, 𝓝[≠] x ⊓ 𝓟 S = ⊥
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set Y
⊢ IsDiscrete s ↔ ∀ y ∈ s, ∃ u, IsOpen[inst✝] u ∧ u ∩ s = {y}

Tactic:
isDiscrete_iff_discreteTopology,

Goal state after:
Y : Type u_2
inst✝ : TopologicalSpace Y
s : Set Y
⊢ DiscreteTopology ↑s ↔ ∀ y ∈ s, ∃ u, IsOpen[inst✝] u ∧ u ∩ s = {y}
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsDiscrete s ↔ ∀ t ⊆ s, ∃ u, IsOpen[inst✝] u ∧ u ∩ s = t

Tactic:
isDiscrete_iff_discreteTopology,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ DiscreteTopology ↑s ↔ ∀ t ⊆ s, ∃ u, IsOpen[inst✝] u ∧ u ∩ s = t
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
H : s ∈ irreducibleComponents X
⊢ s = closure[inst✝] s

Tactic:
exact subset_closure.antisymm (H.2 H.1.closure subset_closure)

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
⊢ p ∉ closure[inst✝] (S ∩ b)

Tactic:
simp only [closure, mem_sInter, mem_ofPred_eq, and_imp, not_forall, exists_prop]

Goal state after:
case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
⊢ ∃ x, IsClosed[inst✝] x ∧ S ∩ b ⊆ x ∧ p ∉ x
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst✝] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
⊢ IsPreirreducible S

Tactic:
rintro u v hu hv ⟨x, hx, hx'⟩ ⟨y, hy, hy'⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
t S U : Set X
hU' : IsOpen[inst✝] U
h₁ : U ⊆ S
h₂ : S ⊆ t
z : X
hz : z ∈ U
ht : IsIrreducible t
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
x : X
hx : x ∈ S
hx' : x ∈ u
y : X
hy : y ∈ S
hy' : y ∈ v
⊢ (S ∩ (u ∩ v)).Nonempty
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Set X
ht : t.Finite
⊢ Dense (s \ t)

Tactic:
convert! hs.sdiff_finset ht.toFinset

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : ∀ (x : X), (𝓝[≠] x).NeBot
s : Set X
hs : Dense s
t : Set X
ht : t.Finite
⊢ t = ↑ht.toFinset
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
x : X
s : Set X
hs : s ∈ 𝓝 x
hsf : s.Finite
⊢ {x} ⊆ s

Tactic:
simp only [singleton_subset_iff, mem_of_mem_nhds hs]

Goal state after: