mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : CostructuredArrow yoneda A
x : F.obj (op s)
⊢ op s = op (CostructuredArrow.mk (YonedaCollection.fst (counitForward F s x).val))

Tactic:
by simp [← CostructuredArrow.eq_mk]

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
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ s = op (CostructuredArrow.mk (yoneda.map f.unop.left ≫ (unop t).hom))

Tactic:
by simp [← CostructuredArrow.eq_mk]

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
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s : CostructuredArrow yoneda A
p : OverArrows (yonedaCollectionPresheafToA F) s.hom
⊢ op (CostructuredArrow.mk (YonedaCollection.fst p.val)) = op s

Tactic:
by simp [← CostructuredArrow.eq_mk]

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
x : C
hb_fac_app :
  (StructuredArrow.hom b ≫ ((whiskeringLeft D D' H).obj L').map (hb.desc u)).app (L.obj x) =
    (StructuredArrow.hom u).app (L.obj x)
hα_fac_app :
  (StructuredArrow.hom (mk F₁ α) ≫
          ((whiskeringLeft C D H).obj L).map
            (hα.desc
              (mk (L' ⋙ StructuredArrow.right y)
                (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))).app
      x =
    (StructuredArrow.hom
          (mk (L' ⋙ StructuredArrow.right y)
            (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom))).app
      x
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫ ((whiskeringLeft C D' H).obj (L ⋙ L')).map (hb.desc u)).app x =
    (StructuredArrow.hom y).app x

Tactic:
dsimp at hα_fac_app hb_fac_app

Goal state after:
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
y : (L ⋙ L').LeftExtension F₀
u : L'.LeftExtension F₁ :=
  mk (StructuredArrow.right y)
    (hα.desc
      (mk (L' ⋙ StructuredArrow.right y) (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)))
x : C
hb_fac_app :
  (StructuredArrow.hom b).app (L.obj x) ≫ (hb.desc u).app (L'.obj (L.obj x)) = (StructuredArrow.hom u).app (L.obj x)
hα_fac_app :
  α.app x ≫
      (hα.desc
            (mk (L' ⋙ StructuredArrow.right y)
              (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom))).app
        (L.obj x) =
    (StructuredArrow.hom y).app x ≫ 𝟙 ((StructuredArrow.right y).obj (L'.obj (L.obj x)))
⊢ (StructuredArrow.hom ((precomp₂ L' α).obj b) ≫ ((whiskeringLeft C D' H).obj (L ⋙ L')).map (hb.desc u)).app x =
    (StructuredArrow.hom y).app x
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case refine_2
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := ⋯
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension γ
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)
⊢ StructuredArrow.IsUniversal ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β))

Tactic:
apply IsInitial.isInitialIffObj Ψ.functor _ |>.invFun

Goal state after:
case refine_2
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
α : F₀ ⟶ L ⋙ F₁
inst✝ : F₁.IsLeftKanExtension α
F₂ : D' ⥤ H
L'' : C ⥤ D'
e : L ⋙ L' ≅ L''
β : F₁ ⟶ L' ⋙ F₂
γ : F₀ ⟶ L'' ⋙ F₂
hγ : α ≫ L.whiskerLeft β ≫ (L.associator L' F₂).inv ≫ whiskerRight e.hom F₂ = γ
Ψ : (L ⋙ L').LeftExtension F₀ ≌ L''.LeftExtension F₀ := ⋯
hα : StructuredArrow.IsUniversal (LeftExtension.mk F₁ α)
x✝ : F₂.IsLeftKanExtension γ
h : StructuredArrow.IsUniversal (LeftExtension.mk F₂ γ)
⊢ IsInitial (Ψ.functor.obj ((LeftExtension.precomp₂ L' α).obj (LeftExtension.mk F₂ β)))
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_1.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op ≫ (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op).unop =
    (𝟙 (op (cokernel (kernel.ι f.unop)))).unop

pp: case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((cokernel.desc (kernel.ι f.unop) f.unop ⋯).op ≫ (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op).unop =
    (𝟙 A).unop

pp: case refine_1.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ { hom := (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op, inv := (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op,
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      f =
    (cokernel.π (kernel.ι f.unop)).op

Tactic:
· rw [← cancel_epi (cokernel.π (kernel.ι f.unop))]
      simp only [unop_comp, Quiver.Hom.unop_op, unop_id_op, cokernel.π_desc_assoc,
        comp_epiDesc, Category.comp_id]

Goal state after:
case refine_1.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ ((cokernel.desc (kernel.ι f.unop) f.unop ⋯).op ≫ (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op).unop =
    (𝟙 A).unop

case refine_1.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ { hom := (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯).op, inv := (cokernel.desc (kernel.ι f.unop) f.unop ⋯).op,
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      f =
    (cokernel.π (kernel.ι f.unop)).op
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasColimitsOfShape J C
inst✝³ : HasColimitsOfShape J D
inst✝² : HasExactColimitsOfShape J C
inst✝¹ : HasFiniteLimits D
inst✝ : PreservesFiniteLimits F
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ D
this✝ : PreservesLimitsOfSize.{0, 0, v'', v, u'', u} G
this : PreservesColimitsOfSize.{v', u', v, v'', u, u''} F
e : (whiskeringRight J D C).obj G ⋙ colim ⋙ F ≅ colim :=
  ((whiskeringRight J D C).obj G).isoWhiskerLeft (preservesColimitNatIso F) ≪≫
    (((whiskeringRight J D C).obj G).associator ((whiskeringRight J C D).obj F) colim).symm ≪≫
      isoWhiskerRight (G.whiskeringRightObjCompIso F) colim ≪≫
        isoWhiskerRight ((whiskeringRight J D D).mapIso (asIso adj.counit)) colim ≪≫
          isoWhiskerRight whiskeringRightObjIdIso colim ≪≫ colim.leftUnitor
⊢ PreservesLimit H colim

Tactic:
exact preservesLimit_of_natIso _ e

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 : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
X : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
⊢ uliftYoneda.{max w v₂, v₁, u₁}.map
        (Iso.refl
            (CostructuredArrow.mk
                (uliftYonedaEquiv.symm ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left }))).left).hom ≫
      X.hom =
    (CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left }))).hom

Tactic:
ext Y x

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 : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
X : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
Y : Cᵒᵖ
x :
  (uliftYoneda.{max w v₂, v₁, u₁}.obj
        (CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left }))).left).obj
    Y
⊢ (hom
          ((uliftYoneda.{max w v₂, v₁, u₁}.map
                  (Iso.refl
                      (CostructuredArrow.mk
                          (uliftYonedaEquiv.symm ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left }))).left).hom ≫
                X.hom).app
            Y)).toFun
      x =
    (hom
          ((CostructuredArrow.mk (uliftYonedaEquiv.symm ((hom (X.hom.app (op X.left))) { down := 𝟙 X.left }))).hom.app
            Y)).toFun
      x
Module: Mathlib.CategoryTheory.Abelian.Transfer

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X Y : C
f : X ⟶ Y
this✝¹ : PreservesColimits G
this✝ : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
this : HasCokernel (G.map (F.map f) ≫ i.hom.app Y)
⊢ HasCokernel (i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y)

Tactic:
apply Limits.hasCokernel_epi_comp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice ⋯)
⊢ a = default

Tactic:
let h : T ⟶ E := Classical.choice (hT E)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
⊢ a = default
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ autoParam ((mk q).hom ≫ T.map (Subobject.underlyingIso (Hom.right (MonoOver.mk f).arrow)).hom = P.hom) isoMk._auto_1

Tactic:
· exact (cancel_mono (T.map f.right)).1 (by dsimp; simpa [← T.map_comp] using hq)

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
P : ObjectProperty C
hP : P.IsCoseparating
⊢ (P.inverseImage (proj S T)).IsCoseparating

Tactic:
by
  refine fun X Y f g hfg => ext _ _ (hP _ _ fun G hG h => ?_)
  exact congr_arg CommaMorphism.right (hfg (mk (Y.hom ≫ T.map h)) hG (homMk h rfl))

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: X : Type u
Y : AddCommGrpCat
⊢ (free.obj X ⟶ Y) ≃ (X ⟶ (forget AddCommGrpCat).obj Y)

Tactic:
by
        refine ConcreteCategory.homEquiv.trans (Equiv.trans ?_ TypeCat.homEquiv.symm)
        exact FreeAbelianGroup.lift.symm

Goal state after:
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
B : Type u_2
α : Type u_3
inst✝⁵ : Zero α
inst✝⁴ : Monoid A
inst✝³ : Monoid B
inst✝² : Pow A α
inst✝¹ : Pow B α
inst✝ : RootableBy A α
f : A → B
hf : Surjective f
hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n
n : α
hn : n ≠ 0
x : B
y : A
hy : f y = x
⊢ f (RootableBy.root y n) ^ n = x

Tactic:
← hpow (RootableBy.root y n) n,

Goal state after:
A : Type u_1
B : Type u_2
α : Type u_3
inst✝⁵ : Zero α
inst✝⁴ : Monoid A
inst✝³ : Monoid B
inst✝² : Pow A α
inst✝¹ : Pow B α
inst✝ : RootableBy A α
f : A → B
hf : Surjective f
hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n
n : α
hn : n ≠ 0
x : B
y : A
hy : f y = x
⊢ f (RootableBy.root y n ^ n) = x
Module: Mathlib.Order.Circular

Goal state before:
pp: α : Type u_1
inst✝ : CircularOrder α
a b : α
⊢ (cIoo a b)ᶜ = cIcc b a

Tactic:
ext
  rw [Set.mem_cIcc, btw_iff_not_sbtw, cIoo, mem_compl_iff, mem_ofPred]

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
hca : c ≤ a
⊢ btw a b c ∨ btw c b a

Tactic:
exact Or.inl (Or.inr <| Or.inr ⟨hca, hab⟩)

Goal state after:
Module: Mathlib.Order.Circular

Goal state before:
pp: case inl.inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c : α
hab : a ≤ b
hcb : c ≤ b
hac : a ≤ c
⊢ btw a b c ∨ btw c b a

Tactic:
exact Or.inr (Or.inr <| Or.inr ⟨hac, hcb⟩)

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 ↔ c ∈ Set.Ico a (a + p) ∧ ∃ z, b = c + z • p

Tactic:
refine
    ⟨fun h =>
      ⟨h ▸ toIcoMod_mem_Ico hp a b, toIcoDiv hp a b, h ▸ (toIcoMod_add_toIcoDiv_zsmul _ _ _).symm⟩,
      ?_⟩

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ (c ∈ Set.Ico a (a + p) ∧ ∃ z, b = c + z • p) → toIcoMod hp a b = c
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_sub_zsmul' hp a b 1

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst✝] s ↔ {x | x ∉ s} ∉ 𝓝 x

Tactic:
← mem_interior_iff_mem_nhds,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x : X
s : Set X
⊢ x ∈ closure[inst✝] s ↔ x ∉ interior {x | x ∉ s}
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous[inst✝¹, inst✝] f
l : Filter X
l' : Filter Y
h : Tendsto f l l'
s : Set Y
hs : s ∈ l'
⊢ ∀ᶠ (a : X) in l.lift' closure[inst✝¹], f a ∈ closure[inst✝] s

Tactic:
filter_upwards [mem_lift' (h hs)] using (mapsTo_preimage _ _).closure hf

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
x : X
inst✝ : (𝓝[≠] x).NeBot
y : X
⊢ y ∈ closure[inst✝¹] {x}ᶜ

Tactic:
rcases eq_or_ne y x with (rfl | hne)

Goal state after:
case inl
X : Type u
inst✝¹ : TopologicalSpace X
y : X
inst✝ : (𝓝[≠] y).NeBot
⊢ y ∈ closure[inst✝¹] {y}ᶜ

case inr
X : Type u
inst✝¹ : TopologicalSpace X
x : X
inst✝ : (𝓝[≠] x).NeBot
y : X
hne : y ≠ x
⊢ y ∈ closure[inst✝¹] {x}ᶜ
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
p : X → Prop
⊢ (∀ᶠ (x : X) in 𝓝ˢ s ⊔ 𝓝ˢ t, p x) ↔ (∀ᶠ (x : X) in 𝓝ˢ s, p x) ∧ ∀ᶠ (x : X) in 𝓝ˢ t, p x

Tactic:
eventually_sup

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
p : X → Prop
⊢ ((∀ᶠ (x : X) in 𝓝ˢ s, p x) ∧ ∀ᶠ (x : X) in 𝓝ˢ t, p x) ↔ (∀ᶠ (x : X) in 𝓝ˢ s, p x) ∧ ∀ᶠ (x : X) in 𝓝ˢ t, p x
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : X ≃ₜ Y
s : Set Y
⊢ IsClosed[inst✝¹] (⇑h ⁻¹' s) ↔ IsClosed[inst✝] s

Tactic:
simp only [← isOpen_compl_iff, ← preimage_compl, isOpen_preimage]

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 ⊢

Goal state after:
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 : ClusterPt (f x) (𝓟 {f x}ᶜ ⊓ l)
⊢ ClusterPt x (𝓟 {x}ᶜ ⊓ comap f l)
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 : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : f '' s ∉ 𝓝 (f x)
⊢ s ∉ 𝓝 x

Tactic:
← mem_interior_iff_mem_nhds,

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : f x ∉ interior (f '' s)
⊢ x ∉ interior s
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₃ : IsClosedMap f
⊢ IsClosedEmbedding f

Tactic:
by
  refine .of_isEmbedding_isClosedMap ⟨⟨?_⟩, h₂⟩ h₃
  refine h₁.le_induced.antisymm fun s hs => ?_
  refine ⟨(f '' sᶜ)ᶜ, (h₃ _ hs.isClosed_compl).isOpen_compl, ?_⟩
  rw [preimage_compl, preimage_image_eq _ h₂, compl_compl]

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

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace ε
inst✝² : TopologicalSpace ζ
inst✝¹ : Preorder X
inst✝ : Preorder Y
x : X × Y
hx₁ : (𝓝[<] x.1).NeBot
hx₂ : (𝓝[<] x.2).NeBot
⊢ (𝓝[<] x).NeBot

Tactic:
by
  refine (hx₁.prod hx₂).mono ?_
  rw [← nhdsWithin_prod_eq]
  exact nhdsWithin_mono _ fun _ ⟨h₁, h₂⟩ ↦ Prod.lt_iff.2 <| .inl ⟨h₁, h₂.le⟩

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

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
ε : Type u_3
ζ : Type u_4
inst✝⁷ : TopologicalSpace X
inst✝⁶ : TopologicalSpace Y
inst✝⁵ : TopologicalSpace Z
inst✝⁴ : TopologicalSpace W
inst✝³ : TopologicalSpace ε
inst✝² : TopologicalSpace ζ
inst✝¹ : Preorder X
inst✝ : Preorder Y
x : X × Y
hx₁ : (𝓝[>] x.1).NeBot
hx₂ : (𝓝[>] x.2).NeBot
⊢ (𝓝[>] x).NeBot

Tactic:
by
  refine (hx₁.prod hx₂).mono ?_
  rw [← nhdsWithin_prod_eq]
  exact nhdsWithin_mono _ fun _ ⟨h₁, h₂⟩ ↦ Prod.lt_iff.2 <| .inl ⟨h₁, h₂.le⟩

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
x : X
y : Y
u : Set X
hu : u ∈ 𝓝 x
v : Set Y
hv : v ∈ 𝓝 y
H : ∀ x_1 ∈ u, ∀ y ∈ v, x_1 = x → y ∈ s
⊢ s ∈ 𝓝 (x, y).2

Tactic:
exact mem_of_superset hv fun z hz => H _ (mem_of_mem_nhds hu) _ hz rfl

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
h : s ∈ 𝓝 x
⊢ ContinuousWithinAt f s x ↔ ContinuousAt f x

Tactic:
← univ_inter s,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
h : s ∈ 𝓝 x
⊢ ContinuousWithinAt f (univ ∩ s) x ↔ ContinuousAt f x
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology β
f : α × β → γ
s : Set (α × β)
x : α × β
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt (fun x_1 ↦ f (x_1, x.2)) {a | (a, x.2) ∈ s} x.1

Tactic:
rw [← x.eta]; simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, prod_pure,
    ← map_inf_principal_preimage]; rfl

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
f : Y → (i : ι) → A i
g : (i : ι) → A i
u : Filter Y
⊢ Tendsto f u (Filter.pi fun i ↦ 𝓝 (g i)) ↔ ∀ (x : ι), Tendsto (fun i ↦ f i x) u (𝓝 (g x))

Tactic:
Filter.tendsto_pi

Goal state after:
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
f : Y → (i : ι) → A i
g : (i : ι) → A i
u : Filter Y
⊢ (∀ (i : ι), Tendsto (fun x ↦ f x i) u (𝓝 (g i))) ↔ ∀ (x : ι), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
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:
by
    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.Bases

Goal state before:
pp: case h_nhds.inl
α : Type u
t✝ : TopologicalSpace α
β : Type u_1
inst✝ : TopologicalSpace β
s : Set (Set α)
hs : IsTopologicalBasis s
t : Set (Set β)
ht : IsTopologicalBasis t
x : α
u : Set (α ⊕ β)
hxu : Sum.inl x ∈ u
u_open : IsOpen[instTopologicalSpaceSum] u
⊢ ∃ v ∈ (fun u ↦ Sum.inl '' u) '' s ∪ (fun u ↦ Sum.inr '' u) '' t, Sum.inl x ∈ v ∧ v ⊆ u

Tactic:
obtain ⟨v, vs, xv, vu⟩ : ∃ v ∈ s, x ∈ v ∧ v ⊆ Sum.inl ⁻¹' u :=
        hs.exists_subset_of_mem_open hxu (isOpen_sum_iff.1 u_open).1
      exact ⟨Sum.inl '' v, mem_union_left _ (mem_image_of_mem _ vs), mem_image_of_mem _ xv,
        image_subset_iff.2 vu⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
⊢ Disjoint (𝓝ˢ s) l ↔ ∀ x ∈ s, Disjoint (𝓝 x) l

Tactic:
refine ⟨fun h x hx => h.mono_left <| nhds_le_nhdsSet hx, fun H => ?_⟩

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
H : ∀ x ∈ s, Disjoint (𝓝 x) l
⊢ Disjoint (𝓝ˢ s) l
Module: Mathlib.Order.UpperLower.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : UpperSet α
a : α
ha : a ∈ s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ s.erase a ⊓ Ici a = s

Tactic:
by
  rw [← upperClosure_singleton, ← sdiff_singleton, sdiff_inf_upperClosure] <;> simpa

Goal state after: