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

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((const J).obj (colimit.cocone (curry.obj (swap K J ⋙ F) ⋙ lim)).1).map f ≫
        colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
          { pt := (colimit.cocone ((curry.obj F).obj Y)).1,
            ι :=
              { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) Y ≫ colimit.ι ((curry.obj F).obj Y) k,
                naturality := ⋯ } } =
      colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
          { pt := (colimit.cocone ((curry.obj F).obj X)).1,
            ι :=
              { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) X ≫ colimit.ι ((curry.obj F).obj X) k,
                naturality := ⋯ } } ≫
        (curry.obj F ⋙ colim).map f

Tactic:
intro j

Goal state after:
J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
⊢ ∀ ⦃Y : J⦄ (f : j ⟶ Y),
    ((const J).obj (colimit.cocone (curry.obj (swap K J ⋙ F) ⋙ lim)).1).map f ≫
        colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
          { pt := (colimit.cocone ((curry.obj F).obj Y)).1,
            ι :=
              { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) Y ≫ colimit.ι ((curry.obj F).obj Y) k,
                naturality := ⋯ } } =
      colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
          { pt := (colimit.cocone ((curry.obj F).obj j)).1,
            ι :=
              { app := fun k ↦ limit.π ((curry.obj (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
                naturality := ⋯ } } ≫
        (curry.obj F ⋙ colim).map f
Module: Mathlib.CategoryTheory.Limits.ColimitLimit

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
C : Type u
inst✝² : Category.{v, u} C
F : J × K ⥤ C
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasColimitsOfShape K C
j : J
k : K
⊢ colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) k ≫
      limit.lift (curry.obj F ⋙ colim)
          { pt := colimit (curry.obj (swap K J ⋙ F) ⋙ lim),
            π :=
              {
                app := fun j ↦
                  colimit.desc (curry.obj (swap K J ⋙ F) ⋙ lim)
                    { pt := colimit ((curry.obj F).obj j),
                      ι :=
                        {
                          app := fun k ↦
                            limit.π ((curry.obj (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k,
                          naturality := ⋯ } },
                naturality := ⋯ } } ≫
        limit.π (curry.obj F ⋙ colim) j =
    limit.π ((curry.obj (swap K J ⋙ F)).obj k) j ≫ colimit.ι ((curry.obj F).obj j) k

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
X : Cᵒᵖ
W : (J.Cover (unop X))ᵒᵖ
⊢ (colimit.cocone (J.diagram P (unop X) ⋙ F)).ι.app W ≫
      (HasColimit.isoOfNatIso
          (NatIso.ofComponents
            (fun W ↦
              (isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan)).conePointUniqueUpToIso
                  (limit.isLimit (((unop W).index P).multicospan ⋙ F)) ≪≫
                HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm)
            ⋯)).hom =
    (((isLimitOfPreserves F (limit.isLimit ((unop W).index P).multicospan)).conePointUniqueUpToIso
            (limit.isLimit (((unop W).index P).multicospan ⋙ F))).hom ≫
        (HasLimit.isoOfNatIso (Cover.multicospanComp F P (unop W)).symm).hom) ≫
      colimit.ι (J.diagram (P ⋙ F) (unop X)) W

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
K : Type z
inst✝¹ : Category.{z', z} K
inst✝ : HasWeakSheafify J D
F : K ⥤ Sheaf J D
h : ∀ (c : Cocone (F ⋙ sheafToPresheaf J D)) (x : IsColimit c), Presheaf.IsSheaf J c.pt
E : Cocone (F ⋙ sheafToPresheaf J D)
hE : IsColimit E
j : K
⊢ ((sheafToPresheaf J D).mapCocone
              { pt := { obj := E.pt, property := ⋯ },
                ι := { app := fun x ↦ { hom := E.ι.app x }, naturality := ⋯ } }).ι.app
        j ≫
      (eqToIso ⋯).hom =
    E.ι.app j

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CompatiblePlus

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type u_1
inst✝⁷ : Category.{v_1, u_1} D
E : Type u_2
inst✝⁶ : Category.{v_2, u_2} E
F : D ⥤ E
inst✝⁵ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) D
inst✝⁴ : ∀ (J : MulticospanShape), HasLimitsOfShape (WalkingMulticospan J) E
inst✝³ : ∀ (X : C) (W : J.Cover X) (P : Cᵒᵖ ⥤ D), PreservesLimit (W.index P).multicospan F
P : Cᵒᵖ ⥤ D
inst✝² : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ E
inst✝ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ F
hP : Presheaf.IsSheaf J (J.plusObj P ⋙ F)
⊢ J.toPlus (P ⋙ F) ≫ (J.plusCompIso F P).inv = whiskerRight (J.toPlus P) F

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Basic

Goal state before:
pp: X Y : TopCat
f : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom f.inv) ((ConcreteCategory.hom f.hom) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Basic

Goal state before:
pp: X Y : TopCat
f : X ≅ Y
y : ↑Y
⊢ (ConcreteCategory.hom f.hom) ((ConcreteCategory.hom f.inv) y) = y

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Basic

Goal state before:
pp: X Y : TopCat
f : X ≅ Y
x : ↑Y
⊢ (ConcreteCategory.hom f.hom) ((ConcreteCategory.hom f.inv) x) = x

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j j' : J
φ : j ⟶ j'
⊢ ((Functor.const J).obj (of (conePtOfConeForget c))).map φ ≫
      ofHom { toFun := ⇑(ConcreteCategory.hom (c.π.app j')), continuous_toFun := ⋯ } =
    ofHom { toFun := ⇑(ConcreteCategory.hom (c.π.app j)), continuous_toFun := ⋯ } ≫ F.map φ

Tactic:
ext
        apply ConcreteCategory.congr_hom (c.π.naturality φ)

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j j' : J
φ : j ⟶ j'
⊢ ((Functor.const J).obj (of (conePtOfConeForget c))).map φ ≫
      ofHom { toFun := ⇑(ConcreteCategory.hom (c.π.app j')), continuous_toFun := ⋯ } =
    ofHom { toFun := ⇑(ConcreteCategory.hom (c.π.app j)), continuous_toFun := ⋯ } ≫ F.map φ

Tactic:
by
        ext
        apply ConcreteCategory.congr_hom (c.π.naturality φ)

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
s : Cone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
rw [continuous_iff_coinduced_le]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
s : Cone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
s : Cone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
intro j

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsLimit c
s : Cone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : Cone F
hc : IsLimit (forget.mapCone c)
⊢ Nonempty (IsLimit c) ↔ c.pt.str = ⨅ j, induced (⇑(ConcreteCategory.hom (c.π.app j))) (F.obj j).str

Tactic:
by
  refine ⟨fun ⟨hc⟩ ↦ induced_of_isLimit _ hc, fun h ↦ ⟨?_⟩⟩
  refine .ofIsoLimit (isLimitConeOfForget _ hc) (Cone.ext ?_ ?_)
  · refine TopCat.isoOfHomeo
      { toEquiv := .refl _,
        continuous_toFun := h ▸ by fun_prop,
        continuous_invFun := h ▸ by fun_prop }
  · intro; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P : Cᵒᵖ ⥤ D
⊢ J.plusMap (J.plusMap (𝟙 P)) = 𝟙 (J.plusObj (J.plusObj P))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q R : Cᵒᵖ ⥤ D
η : P ⟶ Q
γ : Q ⟶ R
⊢ J.plusMap (J.plusMap (η ≫ γ)) = J.plusMap (J.plusMap η) ≫ J.plusMap (J.plusMap γ)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
⊢ η ≫ J.toPlus Q ≫ J.plusMap (J.toPlus Q) = (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ J.plusMap (J.plusMap η)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ J.plusLift (J.plusLift η hQ) hQ = η

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j : J
⊢ Continuous ⇑(ConcreteCategory.hom (c.ι.app j))

Tactic:
rw [continuous_iff_coinduced_le]

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
j : J
⊢ coinduced (⇑(ConcreteCategory.hom (c.ι.app j))) (F.1 j).str ≤ topologicalSpaceCoconePtOfCoconeForget c
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{w', w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η γ : J.sheafify P ⟶ Q
hQ : Presheaf.IsSheaf J Q
h : J.toSheafify P ≫ η = J.toSheafify P ≫ γ
⊢ η = γ

Tactic:
apply J.plus_hom_ext _ _ hQ
  apply J.plus_hom_ext _ _ hQ
  rw [← Category.assoc, ← Category.assoc, ← plusMap_toPlus]
  exact h

Goal state after:
Module: Mathlib.CategoryTheory.Sites.ConcreteSheafification

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁷ : Category.{w', w} D
FD : D → D → Type u_1
CD : D → Type t
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
instCC : ConcreteCategory D FD
inst✝⁵ : ∀ {X : C} (S : J.Cover X), PreservesLimitsOfShape (WalkingMulticospan S.shape) (forget D)
inst✝⁴ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝³ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝² : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
inst✝¹ : (forget D).ReflectsIsomorphisms
inst✝ : Preadditive D
F G : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
j : (J.Cover (unop x✝))ᵒᵖ
⊢ (J.diagramNatTrans (J.plusMap 0) (unop x✝)).app j ≫ colimit.ι (J.diagram (J.plusObj G) (unop x✝)) j = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsColimit c
s : Cocone F
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
intro j

Goal state after:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ TopCat
c✝ c : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hc : IsColimit c
s : Cocone F
j : J
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.Topology.Category.TopCat.Limits.Basic

Goal state before:
pp: X : TopCat
x✝ : Set PEmpty.{u_1 + 1}
⊢ IsOpen x✝ ↔ IsOpen x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: case property.refine_3
J : Type v
inst✝ : Category.{w, v} J
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
S : PullbackCone f g
⊢ ∀ {m : S.pt ⟶ (pullbackCone f g).pt},
    m ≫ (pullbackCone f g).fst = S.fst →
      m ≫ (pullbackCone f g).snd = S.snd →
        m =
          ofHom
            { toFun := fun x ↦ ⟨((ConcreteCategory.hom S.fst) x, (ConcreteCategory.hom S.snd) x), ⋯⟩,
              continuous_toFun := ⋯ }

Tactic:
intro m h₁ h₂
        ext x
        -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): used to be `ext x`.
        apply Subtype.ext
        apply Prod.ext
        · simpa using! ConcreteCategory.congr_hom h₁ x
        · simpa using! ConcreteCategory.congr_hom h₂ x

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Products

Goal state before:
pp: case h.left
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : ↑(Y ⨯ Z)
x₁ : ↑W
hx₁ : (ConcreteCategory.hom f) x₁ = (ConcreteCategory.hom prod.fst) x
x₂ : ↑X
hx₂ : (ConcreteCategory.hom g) x₂ = (ConcreteCategory.hom prod.snd) x
⊢ (ConcreteCategory.hom f) (x₁, x₂).1 = (ConcreteCategory.hom (limit.π (pair Y Z) { as := WalkingPair.left })) x

Tactic:
exact hx₁

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

Goal state before:
pp: J : Type v'
inst✝³ : Category.{u', v'} J
C : Type u
inst✝² : Category.{v, u} C
K : Type u_1
inst✝¹ : Category.{v_1, u_1} K
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F : J ⥤ C
c : Cocone F
h : IsUniversalColimit c
j : J
this : IsIso (𝟙 c.pt)
⊢ c.ι.app j ≫ 𝟙 c.pt = (𝟙 F).app j ≫ c.ι.app j

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
F' : Discrete PEmpty.{1} ⥤ C
c' : Cocone F'
α : F' ⟶ empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
⊢ α ≫ (asEmptyCocone X).ι = c'.ι ≫ (const (Discrete PEmpty.{1})).map f →
    NatTrans.Equifibered α →
      (Nonempty (IsColimit c') ↔
        ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j))

Tactic:
hf

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasStrictInitialObjects C
X : C
h : IsInitial X
F' : Discrete PEmpty.{1} ⥤ C
c' : Cocone F'
α : F' ⟶ empty C
f : c'.pt ⟶ (asEmptyCocone X).pt
hf : α ≫ (asEmptyCocone X).ι = c'.ι ≫ (const (Discrete PEmpty.{1})).map f
⊢ NatTrans.Equifibered α →
    (Nonempty (IsColimit c') ↔
      ∀ (j : Discrete PEmpty.{1}), IsPullback (c'.ι.app j) (α.app j) f ((asEmptyCocone X).ι.app j))
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
⊢ ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)

Tactic:
intro j

Goal state after:
J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
j : J
⊢ IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
hc : IsUniversalColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
H : ∀ (j : J), IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
j : J
⊢ c'.ι.app j ≫ e.inv.hom = 𝟙 (F.obj j) ≫ c.ι.app j

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsEmbedding ⇑(ConcreteCategory.hom g)
⊢ g ≫ 𝟙 S = g ≫ 𝟙 S

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
g : Y ⟶ S
⊢ g ≫ 𝟙 S = 𝟙 Y ≫ g

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Limits.Pullbacks

Goal state before:
pp: X Y S : TopCat
f : X ⟶ S
g : Y ⟶ S
H : IsOpenEmbedding ⇑(ConcreteCategory.hom g)
⊢ g ≫ 𝟙 S = g ≫ 𝟙 S

Tactic:
simp

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

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
⊢ ∀ (a : J),
    IsPullback (c''.ι.app a) (α.app a) (f ≫ e.inv.hom) (c.ι.app a) ↔ IsPullback (c''.ι.app a) (α.app a) f (c'.ι.app a)

Tactic:
intro j

Goal state after:
J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this : c'.ι ≫ (const J).map e.inv.hom = c.ι
j : J
⊢ IsPullback (c''.ι.app j) (α.app j) (f ≫ e.inv.hom) (c.ι.app j) ↔ IsPullback (c''.ι.app j) (α.app j) f (c'.ι.app j)
Module: Mathlib.CategoryTheory.Limits.VanKampen

Goal state before:
pp: J : Type v'
inst✝¹ : Category.{u', v'} J
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
c c' : Cocone F
H : IsVanKampenColimit c
e : c ≅ c'
F' : J ⥤ C
c'' : Cocone F'
α : F' ⟶ F
f : c''.pt ⟶ c'.pt
h : α ≫ c'.ι = c''.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
this✝ : c'.ι ≫ (const J).map e.inv.hom = c.ι
j : J
this : IsIso e.inv.hom
⊢ c'.ι.app j ≫ e.inv.hom = 𝟙 (F.obj j) ≫ c.ι.app j

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
kx : K
x : limit ((curry.obj (swap K J ⋙ F)).obj kx)
ky : K
y : limit ((curry.obj (swap K J ⋙ F)).obj ky)
h✝ :
  (ConcreteCategory.hom (colimitLimitToLimitColimit F))
      ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx)) x) =
    (ConcreteCategory.hom (colimitLimitToLimitColimit F))
      ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky)) y)
h :
  ∀ (j : J),
    ∃ k f g,
      (ConcreteCategory.hom (((curry.obj F).obj j).map f))
          ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j)) x) =
        (ConcreteCategory.hom (((curry.obj F).obj j).map g))
          ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j)) y)
k : J → K := fun j ↦ ⋯.choose
f : (j : J) → kx ⟶ k j := fun j ↦ ⋯.choose
g : (j : J) → ky ⟶ k j := fun j ↦ ⋯.choose
w :
  ∀ (j : J),
    (ConcreteCategory.hom (F.map (𝟙 j ×ₘ f j)))
        ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j)) x) =
      (ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j)))
        ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j)) y)
O : Finset K := Finset.image k Finset.univ ∪ {kx, ky}
⊢ kx ∈ {kx, ky}

Tactic:
simp

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

Goal state before:
pp: J : Type u₁
K : Type u₂
inst✝⁴ : Category.{v₁, u₁} J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
F : J × K ⥤ Type v
inst✝¹ : IsFiltered K
inst✝ : Finite J
val✝ : Fintype J
kx : K
x : limit ((curry.obj (swap K J ⋙ F)).obj kx)
ky : K
y : limit ((curry.obj (swap K J ⋙ F)).obj ky)
h✝ :
  (ConcreteCategory.hom (colimitLimitToLimitColimit F))
      ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) kx)) x) =
    (ConcreteCategory.hom (colimitLimitToLimitColimit F))
      ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) ky)) y)
h :
  ∀ (j : J),
    ∃ k f g,
      (ConcreteCategory.hom (((curry.obj F).obj j).map f))
          ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j)) x) =
        (ConcreteCategory.hom (((curry.obj F).obj j).map g))
          ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j)) y)
k : J → K := fun j ↦ ⋯.choose
f : (j : J) → kx ⟶ k j := fun j ↦ ⋯.choose
g : (j : J) → ky ⟶ k j := fun j ↦ ⋯.choose
w :
  ∀ (j : J),
    (ConcreteCategory.hom (F.map (𝟙 j ×ₘ f j)))
        ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj kx) j)) x) =
      (ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j)))
        ((ConcreteCategory.hom (limit.π ((curry.obj (swap K J ⋙ F)).obj ky) j)) y)
O : Finset K := Finset.image k Finset.univ ∪ {kx, ky}
kxO : kx ∈ O
⊢ ky ∈ {kx, ky}

Tactic:
simp

Goal state after: