mathlib-initiative/mathlib-tactics huggingface dataset:
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
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝² : PreservesLimitsOfSize.{?u.146, ?u.145, v_2, v, u_2, u} Gr
this✝¹ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
⊢ ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j

Tactic:
intro j

Goal state after:
J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝³ : Gr.Full
inst✝² : Gr.Faithful
F : J ⥤ D
c : Cocone (F ⋙ Gr)
H : IsUniversalColimit c
inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst✝ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
this✝² : PreservesLimitsOfSize.{?u.146, ?u.145, v_2, v, u_2, u} Gr
this✝¹ : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : J ⥤ D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (const J).map f
hα : NatTrans.Equifibered α
hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)
this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.1 ((𝟭 C).obj X)))
this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))
j : J
⊢ Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case inl
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
hαY :
  αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
s : PullbackCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
x : s.pt
val : X'✝
h : (ConcreteCategory.hom s.fst) x = Sum.inl val
⊢ ∃! y, Sum.inl val = Sum.inl y

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case inr
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
X'✝ Y'✝ : Type u
αX✝ : X'✝ ⟶ PUnit.{u + 1}
αY✝ : Y'✝ ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X'✝ Y'✝).pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX✝ ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
hαY :
  αY✝ ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X'✝ Y'✝) ≫ f
s : PullbackCone f (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
x : s.pt
val : Y'✝
h : (ConcreteCategory.hom s.fst) x = Sum.inr val
⊢ ∃! y, Sum.inr val = Sum.inr y

Tactic:
simp

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

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
⊢ IsPullback f' αW αX f →
    IsPullback g' αW αY g →
      CommSq h' αX αZ h →
        CommSq i' αY αZ i → CommSq f' g' h' i' → (IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i)

Tactic:
hf

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
⊢ IsPullback g' αW αY g →
    CommSq h' αX αZ h →
      CommSq i' αY αZ i → CommSq f' g' h' i' → (IsPushout f' g' h' i' ↔ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
cs : CommSq f' g' h' i'
this : HasPullback αX f := IsPullback.hasPullback hf
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
W'' : C
f'' : W'' ⟶ X'
g'' : W'' ⟶ Y'
αW' : W'' ⟶ W
hf' : IsPullback f'' αW' αX f
hg' : IsPullback g'' αW' αY g
hP : IsPushout f'' g'' h' i'
⊢ f'' ≫ (Iso.refl X').hom = (IsPullback.isoIsPullback X' W hf' hf).hom ≫ f'

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
cs : CommSq f' g' h' i'
this : HasPullback αX f := IsPullback.hasPullback hf
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
W'' : C
f'' : W'' ⟶ X'
g'' : W'' ⟶ Y'
αW' : W'' ⟶ W
hf' : IsPullback f'' αW' αX f
hg' : IsPullback g'' αW' αY g
hP : IsPushout f'' g'' h' i'
⊢ h' ≫ (Iso.refl Z').hom = (Iso.refl X').hom ≫ h'

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' :
  ∀ ⦃X' Y' Z' : C⦄ (h' : X' ⟶ Z') (i' : Y' ⟶ Z') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (αZ : Z' ⟶ Z),
    CommSq h' αX αZ h →
      CommSq i' αY αZ i →
        ∀ [HasPullback αX f],
          IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i ↔
            ∃ W' f' g' αW, IsPullback f' αW αX f ∧ IsPullback g' αW αY g ∧ IsPushout f' g' h' i'
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ X
αY : Y' ⟶ Y
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY g
sq_h : CommSq h' αX αZ h
sq_i : CommSq i' αY αZ i
cs : CommSq f' g' h' i'
this : HasPullback αX f := IsPullback.hasPullback hf
hh : IsPullback h' αX αZ h
hi : IsPullback i' αY αZ i
W'' : C
f'' : W'' ⟶ X'
g'' : W'' ⟶ Y'
αW' : W'' ⟶ W
hf' : IsPullback f'' αW' αX f
hg' : IsPullback g'' αW' αY g
hP : IsPushout f'' g'' h' i'
⊢ i' ≫ (Iso.refl Z').hom = (Iso.refl Y').hom ≫ i'

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
Z : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
h₁ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
⊢ IsColimit
    (BinaryCofan.mk (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)
      (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr))

Tactic:
have h₂ : Set.range (TopCat.pullbackFst f (TopCat.binaryCofan (.of PUnit) (.of PUnit)).inr) =
      f ⁻¹' Set.range Sum.inr := by
    apply le_antisymm
    · rintro _ ⟨x, rfl⟩; exact ⟨PUnit.unit, x.2.symm⟩
    · rintro x ⟨⟨⟩, hx⟩; refine ⟨⟨⟨x, PUnit.unit⟩, hx.symm⟩, rfl⟩

Goal state after:
J : Type v'
inst✝² : Category.{u', v'} J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u''
inst✝ : Category.{v'', u''} D
X Y : C
Z : TopCat
f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})
h₁ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inl
h₂ :
  Set.range
      ⇑(ConcreteCategory.hom
          (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr)) =
    ⇑(ConcreteCategory.hom f) ⁻¹' Set.range Sum.inr
⊢ IsColimit
    (BinaryCofan.mk (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl)
      (TopCat.pullbackFst f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr))
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h_map.left
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{?u.122, ?u.121, v, v'', u, u''} Gl
X Y : D
c : BinaryCofan X Y
hc : IsColimit c
⊢ (pair X Y ⋙ Gr).map { down := { down := ⋯ } } ≍ (pair (Gr.obj X) (Gr.obj Y)).map { down := { down := ⋯ } }

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h_map.right
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
inst✝⁷ : HasFiniteCoproducts D
inst✝⁶ : HasPullbacksOfInclusions D
inst✝⁵ : FinitaryExtensive C
Gl : C ⥤ D
Gr : D ⥤ C
adj : Gl ⊣ Gr
inst✝⁴ : Gr.Full
inst✝³ : Gr.Faithful
inst✝² : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst✝¹ : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst✝ : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{?u.122, ?u.121, v, v'', u, u''} Gl
X Y : D
c : BinaryCofan X Y
hc : IsColimit c
⊢ (pair X Y ⋙ Gr).map { down := { down := ⋯ } } ≍ (pair (Gr.obj X) (Gr.obj Y)).map { down := { down := ⋯ } }

Tactic:
simp

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

Goal state before:
pp: case h
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
⊢ ∀ (j j' : J) (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (f ×ₘ 𝟙 k'')))
        ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j)))) (y j)) =
      (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j')))) (y j')

Tactic:
intro j

Goal state after:
case h
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j : J
⊢ ∀ (j' : J) (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (f ×ₘ 𝟙 k'')))
        ((ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j)))) (y j)) =
      (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf (𝟙 j') ≫ i (𝟙 j')))) (y j')
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁶ : FinitaryExtensive D
inst✝⁵ : HasFiniteCoproducts C
inst✝⁴ : HasPullbacksOfInclusions C
inst✝³ : PreservesPullbacksOfInclusions F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
i : Discrete WalkingPair
Z : C
f : Z ⟶ X ⨿ Y
⊢ PreservesLimit (cospan f ((BinaryCofan.mk coprod.inl coprod.inr).ι.app i)) F

Tactic:
rcases i with ⟨_ | _⟩

Goal state after:
case left
C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁶ : FinitaryExtensive D
inst✝⁵ : HasFiniteCoproducts C
inst✝⁴ : HasPullbacksOfInclusions C
inst✝³ : PreservesPullbacksOfInclusions F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
Z : C
f : Z ⟶ X ⨿ Y
⊢ PreservesLimit (cospan f ((BinaryCofan.mk coprod.inl coprod.inr).ι.app { as := WalkingPair.left })) F

case right
C : Type u
inst✝⁸ : Category.{v, u} C
D : Type u''
inst✝⁷ : Category.{v'', u''} D
F : C ⥤ D
inst✝⁶ : FinitaryExtensive D
inst✝⁵ : HasFiniteCoproducts C
inst✝⁴ : HasPullbacksOfInclusions C
inst✝³ : PreservesPullbacksOfInclusions F
inst✝² : ReflectsLimitsOfShape WalkingCospan F
inst✝¹ : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝ : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan X Y
hc : IsColimit c
Z : C
f : Z ⟶ X ⨿ Y
⊢ PreservesLimit (cospan f ((BinaryCofan.mk coprod.inl coprod.inr).ι.app { as := WalkingPair.right })) F
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
⊢ (coprod.inl ≫
      coprod.desc (Sigma.ι f i) (Sigma.desc fun j ↦ Sigma.ι f ↑j) ≫
        Sigma.desc fun j ↦ if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j ↦ f ↑j) ⟨j, h⟩ ≫ coprod.inr) =
    coprod.inl ≫ 𝟙 (f i ⨿ ∐ fun j ↦ f ↑j)

Tactic:
simp

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

Goal state before:
pp: case h
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
⊢ ∀ (j : J),
    (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j))
        ((ConcreteCategory.hom (colimitLimitToLimitColimit F))
          ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) k''))
            (id
              (Limit.mk ((curry.obj (swap K J ⋙ F)).obj k'')
                (fun j ↦ (ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j)))) (y j)) ⋯)))) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x

Tactic:
intro j

Goal state after:
case h
J : Type u₁
K : Type u₂
inst✝⁴ : SmallCategory J
inst✝³ : Category.{v₂, u₂} K
inst✝² : Small.{v, u₂} K
inst✝¹ : FinCategory J
F : J × K ⥤ Type v
inst✝ : IsFiltered K
x : limit (curry.obj F ⋙ colim)
k : J → K
y : (j : J) → F.obj (j, k j)
e :
  ∀ (j : J),
    (ConcreteCategory.hom (colimit.ι ((curry.obj F).obj j) (k j))) (y j) =
      (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
k' : K
g : (j : J) → k j ⟶ k'
kf : {j j' : J} → (j ⟶ j') → K
gf hf : {j j' : J} → (f : j ⟶ j') → k' ⟶ kf f
wf :
  ∀ {j j' : J} (f : j ⟶ j'),
    (ConcreteCategory.hom (F.map (𝟙 j' ×ₘ g j' ≫ gf f))) (y j') = (ConcreteCategory.hom (F.map (f ×ₘ g j ≫ hf f))) (y j)
k'' : K
i : {j j' : J} → (f : j ⟶ j') → kf f ⟶ k''
s : ∀ {j₁ j₂ j₃ j₄ : J} (f : j₁ ⟶ j₂) (f' : j₃ ⟶ j₄), gf f ≫ i f = hf f' ≫ i f'
j : J
⊢ (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j))
      ((ConcreteCategory.hom (colimitLimitToLimitColimit F))
        ((ConcreteCategory.hom (colimit.ι (curry.obj (swap K J ⋙ F) ⋙ lim) k''))
          (id
            (Limit.mk ((curry.obj (swap K J ⋙ F)).obj k'')
              (fun j ↦ (ConcreteCategory.hom (F.map (𝟙 j ×ₘ g j ≫ gf (𝟙 j) ≫ i (𝟙 j)))) (y j)) ⋯)))) =
    (ConcreteCategory.hom (limit.π (curry.obj F ⋙ colim) j)) x
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
ι : Type u_1
inst✝ : Finite ι
X : C
f : ι → C
c : Cofan f
hc : IsColimit c
i : ι
g : X ⟶ ((Functor.const (Discrete ι)).obj c.pt).obj { as := i }
e : ∐ f ≅ f i ⨿ ∐ fun j ↦ f ↑j :=
  { hom := Sigma.desc fun j ↦ if h : j = i then eqToHom ⋯ ≫ coprod.inl else Sigma.ι (fun j ↦ f ↑j) ⟨j, h⟩ ≫ coprod.inr,
    inv := coprod.desc (Sigma.ι f i) (Sigma.desc fun j ↦ Sigma.ι f ↑j), hom_inv_id := ⋯, inv_hom_id := ⋯ }
e' : c.pt ≅ f i ⨿ ∐ fun j ↦ f ↑j
this : coprod.inl ≫ e'.inv = c.ι.app { as := i }
⊢ 𝟙 X ≫ g = (g ≫ e'.hom) ≫ e'.inv

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
c : Cofan fun x ↦ pullback f (π x) := Cofan.mk Y fun x ↦ pullback.fst f (π x)
hau : IsUniversalColimit (Cofan.mk X π)
⊢ 𝟙 Y ≫ f = f ≫ 𝟙 (Cofan.mk X π).pt

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
X : C
Z : α → C
π : (a : α) → Z a ⟶ X
Y : C
f : Y ⟶ X
hπ : IsIso (Sigma.desc π)
c : Cofan fun x ↦ pullback f (π x) := Cofan.mk Y fun x ↦ pullback.fst f (π x)
hau : IsUniversalColimit (Cofan.mk X π)
⊢ ∀ (i : α), (Cofan.mk X π).inj i ≫ 𝟙 (Cofan.mk X π).pt = π i

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u''
inst✝⁴ : Category.{v'', u''} D
X✝ Y✝ : C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
p : ι × ι'
⊢ f p.1 ≫ 𝟙 S = Sigma.ι X p.1 ≫ Sigma.desc f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: J : Type v'
inst✝⁶ : Category.{u', v'} J
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u''
inst✝⁴ : Category.{v'', u''} D
X✝ Y✝ : C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
p : ι × ι'
⊢ g p.2 ≫ 𝟙 S = Sigma.ι Y p.2 ≫ Sigma.desc g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
H' : H.IsVanKampen
⊢ g ≫ 𝟙 Y = 𝟙 W ≫ g

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono f
H : IsPushout f g h i
H' : H.IsVanKampen
⊢ 𝟙 W ≫ g = g ≫ 𝟙 Y

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
inst✝ : Mono g
H : IsPushout f g h i
H' : H.IsVanKampen
⊢ f ≫ 𝟙 X = 𝟙 W ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case e'_7.e
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : FinitaryPreExtensive C
ι : Type u_1
ι' : Type u_2
inst✝¹ : Finite ι
inst✝ : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
e_3✝ :
  (∐ fun p ↦ pullback (f p.1) (g p.2)) =
    (Cofan.mk (∐ fun p ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun p ↦ pullback (f p.1) (g p.2))).pt
e_4✝ : ∐ X = (Cofan.mk (∐ X) fun i ↦ Sigma.ι X i).pt
x✝¹ : C
x✝ : (b : ι × ι') → pullback (f b.1) (g b.2) ⟶ x✝¹
b✝ : ι × ι'
⊢ Sigma.ι (fun p ↦ pullback (f p.1) (g p.2)) b✝ ≫ Sigma.desc x✝ =
    Sigma.ι (fun p ↦ pullback (f p.1) (g p.2)) b✝ ≫
      Cofan.IsColimit.desc (coproductIsCoproduct fun p ↦ pullback (f p.1) (g p.2)) x✝

Tactic:
simp [Cofan.IsColimit.desc, Sigma.ι, coproductIsCoproduct]

Goal state after: