awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
cofans : (X Y : C) → BinaryCofan.{v, u} X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
H₁ : IsPullback c'.inl αX f c.inl
H₂ : IsPullback c'.inr αY f c.inr
e₁ : X' ≅ (cones f c.inl).pt := H₁.isLimit.conePointUniqueUpToIso (limits f c.inl)
e₂ : Y' ≅ (cones f c.inr).pt := H₂.isLimit.conePointUniqueUpToIso (limits f c.inr)
he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst
⊢ c'.inr = e₂.hom ≫ (cones f c.inr).fst

Tactic:
simp [e₂]
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
cofans : (X Y : C) → BinaryCofan.{v, u} X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
H₁ : IsPullback c'.inl αX f c.inl
H₂ : IsPullback c'.inr αY f c.inr
e₁ : X' ≅ (cones f c.inl).pt := H₁.isLimit.conePointUniqueUpToIso (limits f c.inl)
e₂ : Y' ≅ (cones f c.inr).pt := H₂.isLimit.conePointUniqueUpToIso (limits f c.inr)
he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst
⊢ c'.inr = e₂.hom ≫ (cones f c.inr).fst

Tactic:
have he₂ : c'.inr = e₂.hom ≫ (cones f c.inr).fst := by simp [e₂]
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
cofans : (X Y : C) → BinaryCofan.{v, u} X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
H₁ : IsPullback c'.inl αX f c.inl
H₂ : IsPullback c'.inr αY f c.inr
e₁ : X' ≅ (cones f c.inl).pt := H₁.isLimit.conePointUniqueUpToIso (limits f c.inl)
e₂ : Y' ≅ (cones f c.inr).pt := H₂.isLimit.conePointUniqueUpToIso (limits f c.inr)
he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst
he₂ : c'.inr = e₂.hom ≫ (cones f c.inr).fst
mpr : IsColimit (BinaryCofan.mk (e₁.hom ≫ (cones f c.inl).fst) (e₂.hom ≫ (cones f c.inr).fst))
⊢ IsColimit (BinaryCofan.mk c'.inl c'.inr)

Tactic:
rw [he₁, he₂]
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
cofans : (X Y : C) → BinaryCofan.{v, u} X Y
colimits : (X Y : C) → IsColimit (cofans X Y)
cones : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → PullbackCone f g
limits : {X Y Z : C} → (f : X ⟶ Z) → (g : Y ⟶ Z) → IsLimit (cones f g)
h₁ :
  ∀ {X' Y' : C} (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : (cofans X' Y').pt ⟶ c.pt),
    αX ≫ c.inl = (cofans X' Y').inl ≫ f →
      αY ≫ c.inr = (cofans X' Y').inr ≫ f →
        IsPullback (cofans X' Y').inl αX f c.inl ∧ IsPullback (cofans X' Y').inr αY f c.inr
h₂ : {Z : C} → (f : Z ⟶ c.pt) → IsColimit (BinaryCofan.mk (cones f c.inl).fst (cones f c.inr).fst)
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hX : αX ≫ c.inl = c'.inl ≫ f
hY : αY ≫ c.inr = c'.inr ≫ f
H₁ : IsPullback c'.inl αX f c.inl
H₂ : IsPullback c'.inr αY f c.inr
e₁ : X' ≅ (cones f c.inl).pt := H₁.isLimit.conePointUniqueUpToIso (limits f c.inl)
e₂ : Y' ≅ (cones f c.inr).pt := H₂.isLimit.conePointUniqueUpToIso (limits f c.inr)
he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst
he₂ : c'.inr = e₂.hom ≫ (cones f c.inr).fst
⊢ IsColimit (BinaryCofan.mk (e₁.hom ≫ (cones f c.inl).fst) (e₂.hom ≫ (cones f c.inr).fst))

Tactic:
exact (BinaryCofan.mk _ _).isColimitCompRightIso e₂.hom
      ((BinaryCofan.mk _ _).isColimitCompLeftIso e₁.hom (h₂ f))

Premises used: CategoryTheory.Limits.BinaryCofan.isColimitCompRightIso, CategoryTheory.Limits.BinaryCofan.mk, CategoryTheory.Limits.BinaryCofan.isColimitCompLeftIso, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
⊢ Mono c.inr

Tactic:
PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)

Premises used: CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
refine :
  IsPullback (𝟙 (obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
    (𝟙 (obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })) c.inr c.inr
⊢ Mono c.inr

Tactic:
refine PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)

Premises used: CategoryTheory.Limits.PullbackCone.mono_of_isLimitMkIdId, CategoryTheory.IsPullback.isLimit
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
⊢ IsPullback (𝟙 (obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
    (𝟙 (obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })) c.inr c.inr

Tactic:
(h (BinaryCofan.mk (initial.to Y) (𝟙 Y)) (mapPair (initial.to X) (𝟙 Y)) c.inr ?_
      (.of_discrete _)).mp ⟨?_⟩ ⟨WalkingPair.right⟩

Premises used: CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.initial.to, CategoryTheory.NatTrans.Equifibered.of_discrete, Nonempty.intro, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryCofan.mk, CategoryTheory.Limits.mapPair, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
refine_1 :
  Eq (α :=
    Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair (initial.{v, u} C) Y)
      (obj (const (Discrete WalkingPair)) c.pt))
    (mapPair (initial.to X) (𝟙 Y) ≫ c.ι)
    (CategoryStruct.comp (Y :=
      obj (const (Discrete WalkingPair))
        (Cocone.pt.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))))
      (Cocone.ι (BinaryCofan.mk (initial.to Y) (𝟙 Y))) (map (const (Discrete WalkingPair)) c.inr))
refine_2 : IsColimit.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))
⊢ IsPullback (𝟙 (obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }))
    (𝟙 (obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })) c.inr c.inr

Tactic:
refine (h (BinaryCofan.mk (initial.to Y) (𝟙 Y)) (mapPair (initial.to X) (𝟙 Y)) c.inr ?_
      (.of_discrete _)).mp ⟨?_⟩ ⟨WalkingPair.right⟩

Premises used: CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Limits.initial.to, CategoryTheory.NatTrans.Equifibered.of_discrete, Nonempty.intro, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryCofan.mk, CategoryTheory.Limits.mapPair, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
refine_1 :
  Eq (α :=
    obj.{0, v, 0, u} (pair (initial.{v, u} C) Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c.pt) { as := WalkingPair.left : Discrete WalkingPair })
    (NatTrans.app (mapPair (initial.to X) (𝟙 Y) ≫ c.ι) { as := WalkingPair.left })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))))
        (Cocone.ι (BinaryCofan.mk (initial.to Y) (𝟙 Y))) (map (const (Discrete WalkingPair)) c.inr))
      { as := WalkingPair.left })
refine_1₁ :
  Eq (α :=
    obj.{0, v, 0, u} (pair (initial.{v, u} C) Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c.pt) { as := WalkingPair.right : Discrete WalkingPair })
    (NatTrans.app (mapPair (initial.to X) (𝟙 Y) ≫ c.ι) { as := WalkingPair.right })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))))
        (Cocone.ι (BinaryCofan.mk (initial.to Y) (𝟙 Y))) (map (const (Discrete WalkingPair)) c.inr))
      { as := WalkingPair.right })
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair (initial.{v, u} C) Y)
      (obj (const (Discrete WalkingPair)) c.pt))
    (mapPair (initial.to X) (𝟙 Y) ≫ c.ι)
    (CategoryStruct.comp (Y :=
      obj (const (Discrete WalkingPair))
        (Cocone.pt.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))))
      (Cocone.ι (BinaryCofan.mk (initial.to Y) (𝟙 Y))) (map (const (Discrete WalkingPair)) c.inr))

Tactic:
ext ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair (initial.{v, u} C) Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c.pt) { as := WalkingPair.left : Discrete WalkingPair })
    (NatTrans.app (mapPair (initial.to X) (𝟙 Y) ≫ c.ι) { as := WalkingPair.left })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))))
        (Cocone.ι (BinaryCofan.mk (initial.to Y) (𝟙 Y))) (map (const (Discrete WalkingPair)) c.inr))
      { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair (initial.{v, u} C) Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c.pt) { as := WalkingPair.right : Discrete WalkingPair })
    (NatTrans.app (mapPair (initial.to X) (𝟙 Y) ≫ c.ι) { as := WalkingPair.right })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))))
        (Cocone.ι (BinaryCofan.mk (initial.to Y) (𝟙 Y))) (map (const (Discrete WalkingPair)) c.inr))
      { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
dsimp : IsIso.{v, u} (𝟙 Y)
⊢ IsIso.{v, u} (X := obj.{0, v, 0, u} (pair (initial.{v, u} C) Y) { as := WalkingPair.right : Discrete WalkingPair })
    (Y :=
    obj.{0, v, 0, u}
      (obj (const (Discrete WalkingPair))
        (Cocone.pt.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))))
      { as := WalkingPair.right : Discrete WalkingPair })
    (BinaryCofan.inr (BinaryCofan.mk (initial.to Y) (𝟙 Y)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
⊢ IsIso.{v, u} (𝟙 Y)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
⊢ IsColimit.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))

Tactic:
exact ((BinaryCofan.isColimit_iff_isIso_inr initialIsInitial _).mpr (by
      dsimp
      infer_instance)).some

Premises used: Iff.mpr, CategoryTheory.Limits.initialIsInitial, Nonempty.some, CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasInitial.{v, u} C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
⊢ IsPullback (P := initial.{v, u} C)
    (initial.to (obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
    (initial.to (obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })) c.inl c.inr

Tactic:
((h (BinaryCofan.mk (initial.to Y) (𝟙 Y)) (mapPair (initial.to X) (𝟙 Y)) c.inr ?_
      (.of_discrete _)).mp ⟨?_⟩ ⟨WalkingPair.left⟩).flip

Premises used: CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.initial.to, CategoryTheory.NatTrans.Equifibered.of_discrete, Nonempty.intro, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryCofan.mk, CategoryTheory.Limits.colimit.desc, CategoryTheory.IsPullback.flip, CategoryTheory.Limits.mapPair, Iff.mp, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasInitial.{v, u} C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
refine_1 :
  Eq (α :=
    Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair (initial.{v, u} C) Y)
      (obj (const (Discrete WalkingPair)) c.pt))
    (mapPair (initial.to X) (𝟙 Y) ≫ c.ι)
    (CategoryStruct.comp (Y :=
      obj (const (Discrete WalkingPair))
        (Cocone.pt.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))))
      (Cocone.ι (BinaryCofan.mk (initial.to Y) (𝟙 Y))) (map (const (Discrete WalkingPair)) c.inr))
refine_2 : IsColimit.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))
⊢ IsPullback (P := initial.{v, u} C)
    (initial.to (obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }))
    (initial.to (obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })) c.inl c.inr

Tactic:
refine ((h (BinaryCofan.mk (initial.to Y) (𝟙 Y)) (mapPair (initial.to X) (𝟙 Y)) c.inr ?_
      (.of_discrete _)).mp ⟨?_⟩ ⟨WalkingPair.left⟩).flip

Premises used: CategoryTheory.Limits.BinaryCofan.inr, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.initial.to, CategoryTheory.NatTrans.Equifibered.of_discrete, Nonempty.intro, CategoryTheory.Discrete.mk, CategoryTheory.Limits.BinaryCofan.mk, CategoryTheory.IsPullback.flip, CategoryTheory.Limits.mapPair, Iff.mp, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasInitial.{v, u} C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
refine_1 :
  Eq (α :=
    obj.{0, v, 0, u} (pair (initial.{v, u} C) Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c.pt) { as := WalkingPair.left : Discrete WalkingPair })
    (NatTrans.app (mapPair (initial.to X) (𝟙 Y) ≫ c.ι) { as := WalkingPair.left })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))))
        (Cocone.ι (BinaryCofan.mk (initial.to Y) (𝟙 Y))) (map (const (Discrete WalkingPair)) c.inr))
      { as := WalkingPair.left })
refine_1₁ :
  Eq (α :=
    obj.{0, v, 0, u} (pair (initial.{v, u} C) Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c.pt) { as := WalkingPair.right : Discrete WalkingPair })
    (NatTrans.app (mapPair (initial.to X) (𝟙 Y) ≫ c.ι) { as := WalkingPair.right })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))))
        (Cocone.ι (BinaryCofan.mk (initial.to Y) (𝟙 Y))) (map (const (Discrete WalkingPair)) c.inr))
      { as := WalkingPair.right })
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair (initial.{v, u} C) Y)
      (obj (const (Discrete WalkingPair)) c.pt))
    (mapPair (initial.to X) (𝟙 Y) ≫ c.ι)
    (CategoryStruct.comp (Y :=
      obj (const (Discrete WalkingPair))
        (Cocone.pt.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))))
      (Cocone.ι (BinaryCofan.mk (initial.to Y) (𝟙 Y))) (map (const (Discrete WalkingPair)) c.inr))

Tactic:
ext ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasInitial.{v, u} C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair (initial.{v, u} C) Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c.pt) { as := WalkingPair.left : Discrete WalkingPair })
    (NatTrans.app (mapPair (initial.to X) (𝟙 Y) ≫ c.ι) { as := WalkingPair.left })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))))
        (Cocone.ι (BinaryCofan.mk (initial.to Y) (𝟙 Y))) (map (const (Discrete WalkingPair)) c.inr))
      { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasInitial.{v, u} C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair (initial.{v, u} C) Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) c.pt) { as := WalkingPair.right : Discrete WalkingPair })
    (NatTrans.app (mapPair (initial.to X) (𝟙 Y) ≫ c.ι) { as := WalkingPair.right })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))))
        (Cocone.ι (BinaryCofan.mk (initial.to Y) (𝟙 Y))) (map (const (Discrete WalkingPair)) c.inr))
      { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasInitial.{v, u} C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
dsimp : IsIso.{v, u} (𝟙 Y)
⊢ IsIso.{v, u} (X := obj.{0, v, 0, u} (pair (initial.{v, u} C) Y) { as := WalkingPair.right : Discrete WalkingPair })
    (Y :=
    obj.{0, v, 0, u}
      (obj (const (Discrete WalkingPair))
        (Cocone.pt.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))))
      { as := WalkingPair.right : Discrete WalkingPair })
    (BinaryCofan.inr (BinaryCofan.mk (initial.to Y) (𝟙 Y)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasInitial.{v, u} C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
⊢ IsIso.{v, u} (𝟙 Y)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
inst_1 : HasInitial.{v, u} C
c : BinaryCofan.{v, u} X Y
h : IsVanKampenColimit c
⊢ IsColimit.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))

Tactic:
exact ((BinaryCofan.isColimit_iff_isIso_inr initialIsInitial _).mpr (by
      dsimp
      infer_instance)).some

Premises used: Iff.mpr, CategoryTheory.Limits.initialIsInitial, Nonempty.some, CategoryTheory.Limits.BinaryCofan.isColimit_iff_isIso_inr
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
h_obj : ∀ (X : Discrete (Fin (n + 1))), F.obj X = obj.{0, v, 0, u} (Discrete.functor F') X
h_map :
  ∀ (X Y : Discrete (Fin (n + 1))) (f : X ⟶ Y),
    HEq (F.map f) (β := obj.{0, v, 0, u} (Discrete.functor F') X ⟶ obj.{0, v, 0, u} (Discrete.functor F') Y)
      (map (Discrete.functor F') f)
⊢ F = Discrete.functor F'

Tactic:
apply Functor.hext

Premises used: CategoryTheory.Functor.hext
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
⊢ ∀ (X : Discrete (Fin (n + 1))), F.obj X = obj.{0, v, 0, u} (Discrete.functor F') X

Tactic:
fun i ↦ rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan.{0, v, u} (C := C) fun (i : Fin n) ↦ f i.succ
c₂ : BinaryCofan.{v, u} (f 0) c₁.pt
t₁ : IsUniversalColimit c₁
t₂ : IsUniversalColimit c₂
inst_1 : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i
F : Functor.{0, v, 0, u} (Discrete (Fin (n + 1))) C
c : Cocone F
α : F ⟶ Discrete.functor f
i : c.pt ⟶ (extendCofan c₁ c₂).pt
e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ map (const (Discrete (Fin (n + 1)))) i
hα : NatTrans.Equifibered α
H : ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
F' : Fin (n + 1) → C := F.obj ∘ Discrete.mk
⊢ ∀ (X : Discrete (Fin (n + 1))), F.obj X = obj.{0, v, 0, u} (Discrete.functor F') X

Tactic:
exact fun i ↦ rfl

Premises used: rfl