mathlib-initiative/mathlib-tactics huggingface dataset:
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' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
x : ↑s.pt
val : ↑X'
h : (ConcreteCategory.hom s.fst) x = Sum.inl val
⊢ ∃! y, Sum.inl val = Sum.inr y

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' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
x : ↑s.pt
val : ↑Y'
h : (ConcreteCategory.hom s.fst) x = Sum.inr val
⊢ ∃! y, Sum.inr val = Sum.inr y

Tactic:
·

Goal state after:
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' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
x : ↑s.pt
val : ↑X'
h : (ConcreteCategory.hom s.fst) x = Sum.inl val
⊢ ∃! y, Sum.inl val = Sum.inr y
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr.uniq.h₁.h₂
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ c.inr ≫ H.cocone.inr ≫ m =
    c.inr ≫ (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯).ι.app WalkingSpan.right

Tactic:
·

Goal state after:
case mpr.uniq.h₁.h₂
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ c.inr ≫ H.cocone.inr ≫ m =
    c.inr ≫ (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯).ι.app WalkingSpan.right
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' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
x : ↑s.pt
val : ↑Y'
h : (ConcreteCategory.hom s.fst) x = Sum.inr val
⊢ ∃! y, Sum.inr val = Sum.inr y

Tactic:
·

Goal state after:
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' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f : (X'.binaryCofan Y').pt ⟶ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt
hαX : αX ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl = (X'.binaryCofan Y').inl ≫ f
hαY : αY ≫ ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr = (X'.binaryCofan Y').inr ≫ f
s : PullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr
x : ↑s.pt
val : ↑Y'
h : (ConcreteCategory.hom s.fst) x = Sum.inr val
⊢ ∃! y, Sum.inr val = Sum.inr y
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case mpr.uniq.h₁
C : Type u
inst✝ : Category.{v, u} C
X E Y YE : C
c : BinaryCofan X E
hc : IsColimit c
f : X ⟶ Y
iY : Y ⟶ YE
fE : c.pt ⟶ YE
H✝ : CommSq f c.inl iY fE
H : IsPushout f c.inl iY fE
s : BinaryCofan ((pair X E).obj { as := WalkingPair.right }) Y
m : YE ⟶ s.pt
e₁ : (c.inr ≫ fE) ≫ m = s.inl
e₂ : iY ≫ m = s.inr
⊢ H.cocone.inr ≫ m =
    H.cocone.inr ≫ H.isColimit.desc (PushoutCocone.mk s.inr (hc.desc (BinaryCofan.mk (f ≫ s.inr) s.inl)) ⋯)

Tactic:
· rw [H.isColimit.fac _ WalkingSpan.right]
        apply BinaryCofan.IsColimit.hom_ext hc
        · erw [hc.fac]
          erw [← H.w_assoc]
          rw [e₂]
          rfl
        · refine ((Category.assoc _ _ _).symm.trans e₁).trans ?_; symm; exact hc.fac _ _

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
⊢ pullback.snd αY c.inr ≫ (BinaryCofan.mk (c.inr ≫ i) h).inl =
    (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl ≫ αZ

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
⊢ IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inl ∧
      IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inr ↔
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
⊢ pullback.snd αY c.inr ≫ (BinaryCofan.mk (c.inr ≫ i) h).inl =
    (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl ≫ αZ
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h₂
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}).binaryCofan (TopCat.of PUnit.{u + 1})).pt) →
      IsColimit
        (BinaryCofan.mk
          (TopCat.pullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl).fst
          (TopCat.pullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr).fst)

Tactic:
·

Goal state after:
case h₂
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}).binaryCofan (TopCat.of PUnit.{u + 1})).pt) →
      IsColimit
        (BinaryCofan.mk
          (TopCat.pullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inl).fst
          (TopCat.pullbackCone f ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).inr).fst)
Module: Mathlib.CategoryTheory.Adhesive.Basic

Goal state before:
pp: case refine_2.mp
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
⊢ IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inl ∧
      IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inr →
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i

pp: case refine_2.mpr
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
⊢ IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i →
    IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inl ∧
      IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inr

Tactic:
·

Goal state after:
case refine_2.mp
C : Type u
inst✝² : Category.{v, u} C
W E X Z : C
c : BinaryCofan W E
inst✝¹ : FinitaryExtensive C
inst✝ : HasPullbacks C
hc : IsColimit c
f : W ⟶ X
h : X ⟶ Z
i : c.pt ⟶ Z
H : IsPushout f c.inl h i
hc₁ : IsColimit (BinaryCofan.mk (c.inr ≫ i) h)
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' ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := WalkingPair.left }
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX f
hg : IsPullback g' αW αY c.inl
hh : CommSq h' αX αZ h
hi : CommSq i' αY αZ i
w : CommSq f' g' h' i'
hc₂ : IsColimit (BinaryCofan.mk g' (pullback.fst αY c.inr))
⊢ IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inl (pullback.snd αY c.inr) αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inl ∧
      IsPullback (BinaryCofan.mk ((BinaryCofan.mk g' (pullback.fst αY c.inr)).inr ≫ i') h').inr αX αZ
        (BinaryCofan.mk (c.inr ≫ i) h).inr →
    IsPullback h' αX αZ h ∧ IsPullback i' αY αZ i
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: case w
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'
⊢ (fun X ↦ X) (colimit (curry.obj (swap K J ⋙ F) ⋙ lim))

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'
⊢ (ConcreteCategory.hom (colimitLimitToLimitColimit F)) ?w = x

Tactic:
·

Goal state after:
case w
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'
⊢ (fun X ↦ X) (colimit (curry.obj (swap K J ⋙ F) ⋙ lim))
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h_obj
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
⊢ ∀ (X_1 : Discrete WalkingPair), (pair X Y ⋙ Gr).obj X_1 = (pair (Gr.obj X) (Gr.obj Y)).obj X_1

pp: case h_map
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
⊢ ∀ (X_1 Y_1 : Discrete WalkingPair) (f : X_1 ⟶ Y_1), (pair X Y ⋙ Gr).map f ≍ (pair (Gr.obj X) (Gr.obj Y)).map f

Tactic:
·

Goal state after:
case h_obj
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
⊢ ∀ (X_1 : Discrete WalkingPair), (pair X Y ⋙ Gr).obj X_1 = (pair (Gr.obj X) (Gr.obj Y)).obj X_1
Module: Mathlib.CategoryTheory.Extensive

Goal state before:
pp: case h_map
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
⊢ ∀ (X_1 Y_1 : Discrete WalkingPair) (f : X_1 ⟶ Y_1), (pair X Y ⋙ Gr).map f ≍ (pair (Gr.obj X) (Gr.obj Y)).map f

Tactic:
·

Goal state after:
case h_map
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
⊢ ∀ (X_1 Y_1 : Discrete WalkingPair) (f : X_1 ⟶ Y_1), (pair X Y ⋙ Gr).map f ≍ (pair (Gr.obj X) (Gr.obj Y)).map f
Module: Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit

Goal state before:
pp: case x
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) → ((curry.obj (swap K J ⋙ F)).obj k'').obj j

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 (((curry.obj (swap K J ⋙ F)).obj k'').map f)) (?x j) = ?x j'

Tactic:
·

Goal state after:
case x
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) → ((curry.obj (swap K J ⋙ F)).obj k'').obj j
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 (((curry.obj (swap K J ⋙ F)).obj k'').map f))
        ((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:
·

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) (f : j ⟶ j'),
    (ConcreteCategory.hom (((curry.obj (swap K J ⋙ F)).obj k'').map f))
        ((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')