awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
this : IsColimit.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))
h₁ :
  CategoryStruct.comp (Y :=
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl (BinaryCofan.mk (𝟙 A) (𝟙 A))) (𝟙 A) =
    f ≫ initial.to A
h₂ :
  Eq.{v + 1} (α := obj.{0, v, 0, u} (pair A A) { as := WalkingPair.right : Discrete WalkingPair } ⟶ A)
    (CategoryStruct.comp (Y :=
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (BinaryCofan.inr (BinaryCofan.mk (𝟙 A) (𝟙 A))) (𝟙 A))
    (𝟙 A)
⊢ IsIso f

Tactic:
⟨⟨_, ((Category.id_comp _).symm.trans h₁).symm, initialIsInitial.hom_ext _ _⟩⟩

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.initialIsInitial, And.intro, Exists.intro, Eq.symm, CategoryTheory.IsIso.mk, Eq.trans, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
this : IsColimit.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))
h₁ :
  CategoryStruct.comp (Y :=
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))))
        { as := WalkingPair.left : Discrete WalkingPair })
      (BinaryCofan.inl (BinaryCofan.mk (𝟙 A) (𝟙 A))) (𝟙 A) =
    f ≫ initial.to A
h₂ :
  Eq.{v + 1} (α := obj.{0, v, 0, u} (pair A A) { as := WalkingPair.right : Discrete WalkingPair } ⟶ A)
    (CategoryStruct.comp (Y :=
      obj.{0, v, 0, u} (obj (const (Discrete WalkingPair)) (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))))
        { as := WalkingPair.right : Discrete WalkingPair })
      (BinaryCofan.inr (BinaryCofan.mk (𝟙 A) (𝟙 A))) (𝟙 A))
    (𝟙 A)
⊢ IsIso f

Tactic:
exact ⟨⟨_, ((Category.id_comp _).symm.trans h₁).symm, initialIsInitial.hom_ext _ _⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
suffices : IsColimit.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))
⊢ IsIso f

Tactic:
suffices IsColimit (BinaryCofan.mk (𝟙 A) (𝟙 A)) by
        obtain ⟨l, h₁, h₂⟩ := Limits.BinaryCofan.IsColimit.desc' this (f ≫ initial.to A) (𝟙 A)
        rcases (Category.id_comp _).symm.trans h₂ with rfl
        exact ⟨⟨_, ((Category.id_comp _).symm.trans h₁).symm, initialIsInitial.hom_ext _ _⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
w :
  Eq.{v + 1} (α :=
    obj.{0, v, 0, u} (pair A A) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u}
        (obj (const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))))
        { as := WalkingPair.left : Discrete WalkingPair })
    (NatTrans.app (mapPair f f ≫ Cocone.ι (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C))))
      { as := WalkingPair.left })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete WalkingPair)) (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))))
        (Cocone.ι (BinaryCofan.mk (𝟙 A) (𝟙 A))) (map (const (Discrete WalkingPair)) f))
      { as := WalkingPair.left })
w₁ :
  Eq.{v + 1} (α :=
    obj.{0, v, 0, u} (pair A A) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u}
        (obj (const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))))
        { as := WalkingPair.right : Discrete WalkingPair })
    (NatTrans.app (mapPair f f ≫ Cocone.ι (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C))))
      { as := WalkingPair.right })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete WalkingPair)) (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))))
        (Cocone.ι (BinaryCofan.mk (𝟙 A) (𝟙 A))) (map (const (Discrete WalkingPair)) f))
      { as := WalkingPair.right })
⊢ Eq.{v + 1} (α :=
    Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair A A)
      (obj (const (Discrete WalkingPair))
        (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C))))))
    (mapPair f f ≫ Cocone.ι (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C))))
    (CategoryStruct.comp (Y := obj (const (Discrete WalkingPair)) (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))))
      (Cocone.ι (BinaryCofan.mk (𝟙 A) (𝟙 A))) (map (const (Discrete WalkingPair)) f))

Tactic:
ext ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
⊢ Eq.{v + 1} (α :=
    obj.{0, v, 0, u} (pair A A) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u}
        (obj (const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))))
        { as := WalkingPair.left : Discrete WalkingPair })
    (NatTrans.app (mapPair f f ≫ Cocone.ι (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C))))
      { as := WalkingPair.left })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete WalkingPair)) (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))))
        (Cocone.ι (BinaryCofan.mk (𝟙 A) (𝟙 A))) (map (const (Discrete WalkingPair)) f))
      { 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
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
⊢ Eq.{v + 1} (α :=
    obj.{0, v, 0, u} (pair A A) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u}
        (obj (const (Discrete WalkingPair))
          (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))))
        { as := WalkingPair.right : Discrete WalkingPair })
    (NatTrans.app (mapPair f f ≫ Cocone.ι (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C))))
      { as := WalkingPair.right })
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (const (Discrete WalkingPair)) (Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))))
        (Cocone.ι (BinaryCofan.mk (𝟙 A) (𝟙 A))) (map (const (Discrete WalkingPair)) f))
      { 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
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
refine :
  ∀ (j : Discrete WalkingPair),
    IsPullback (P := obj.{0, v, 0, u} (pair A A) j) (Y :=
      obj.{0, v, 0, u} (pair (initial.{v, u} C) (initial.{v, u} C)) j)
      (NatTrans.app (Cocone.ι (BinaryCofan.mk (𝟙 A) (𝟙 A))) j) (NatTrans.app (mapPair f f) j) f
      (NatTrans.app (Cocone.ι (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))) j)
⊢ IsColimit.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))

Tactic:
refine (H (BinaryCofan.mk (𝟙 _) (𝟙 _)) (mapPair f f) f (by ext ⟨⟨⟩⟩ <;> simp)
        (.of_discrete _) ?_).some

Premises used: CategoryTheory.CategoryStruct.id, Nonempty.some, CategoryTheory.NatTrans.Equifibered.of_discrete, CategoryTheory.Limits.BinaryCofan.mk, CategoryTheory.Limits.mapPair
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
left : IsPullback (𝟙 A) f f (𝟙 (initial.{v, u} C))
⊢ IsPullback (P := obj.{0, v, 0, u} (pair A A) { as := WalkingPair.left : Discrete WalkingPair }) (Y :=
    obj.{0, v, 0, u} (pair (initial.{v, u} C) (initial.{v, u} C)) { as := WalkingPair.left : Discrete WalkingPair })
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (𝟙 A) (𝟙 A))) { as := WalkingPair.left })
    (NatTrans.app (mapPair f f) { as := WalkingPair.left }) f
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))) { as := WalkingPair.left })

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
right : IsPullback (𝟙 A) f f (𝟙 (initial.{v, u} C))
⊢ IsPullback (P := obj.{0, v, 0, u} (pair A A) { as := WalkingPair.right : Discrete WalkingPair }) (Y :=
    obj.{0, v, 0, u} (pair (initial.{v, u} C) (initial.{v, u} C)) { as := WalkingPair.right : Discrete WalkingPair })
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (𝟙 A) (𝟙 A))) { as := WalkingPair.right })
    (NatTrans.app (mapPair f f) { as := WalkingPair.right }) f
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))) { as := WalkingPair.right })

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
⊢ IsPullback (𝟙 A) f f (𝟙 (initial.{v, u} C))

Tactic:
IsPullback.of_horiz_isIso ⟨(Category.id_comp _).trans (Category.comp_id _).symm⟩

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.CommSq.mk, Eq.symm, Eq.trans, CategoryTheory.Category.id_comp, CategoryTheory.IsPullback.of_horiz_isIso
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasInitial.{v, u} C
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
⊢ IsPullback (𝟙 A) f f (𝟙 (initial.{v, u} C))

Tactic:
exact IsPullback.of_horiz_isIso ⟨(Category.id_comp _).trans (Category.comp_id _).symm⟩

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.CommSq.mk, Eq.symm, Eq.trans, CategoryTheory.Category.id_comp, CategoryTheory.IsPullback.of_horiz_isIso
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasStrictInitialObjects.{v, u} C
inst_3 : IsEmpty J
F : Functor.{u', v, v', u} J C
c : Cocone F
hc : IsColimit c
have :
  (this :
      IsColimit
        ((Cocone.precompose
              (uniqueFromEmpty (Equivalence.functor (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J) ⋙ F)).inv).obj
          (Cocone.whisker (Equivalence.functor (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J)) c))) →
    IsInitial.{v, u} c.pt
⊢ IsInitial.{v, u} c.pt

Tactic:
have := (IsColimit.precomposeInvEquiv (Functor.uniqueFromEmpty _) _).symm
      (hc.whiskerEquivalence (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J))
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasStrictInitialObjects.{v, u} C
inst_3 : IsEmpty J
F : Functor.{u', v, v', u} J C
c : Cocone F
hc : IsColimit c
this :
  IsColimit
    ((Cocone.precompose
          (uniqueFromEmpty (Equivalence.functor (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J) ⋙ F)).inv).obj
      (Cocone.whisker (Equivalence.functor (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J)) c))
⊢ IsInitial.{v, u} c.pt

Tactic:
exact IsColimit.ofIsoColimit this (Cocone.ext (Iso.refl c.pt) (fun {X} ↦ isEmptyElim X))
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasStrictInitialObjects.{v, u} C
inst_3 : IsEmpty J
F : Functor.{u', v, v', u} J C
c : Cocone F
hc : IsColimit c
have : ∀ (this : IsInitial.{v, u} c.pt), IsVanKampenColimit c
⊢ IsVanKampenColimit c

Tactic:
have : IsInitial c.pt := by
    have := (IsColimit.precomposeInvEquiv (Functor.uniqueFromEmpty _) _).symm
      (hc.whiskerEquivalence (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J))
    exact IsColimit.ofIsoColimit this (Cocone.ext (Iso.refl c.pt) (fun {X} ↦ isEmptyElim X))
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasStrictInitialObjects.{v, u} C
inst_3 : IsEmpty J
F : Functor.{u', v, v', u} J C
c : Cocone F
hc : IsColimit c
this : IsInitial.{v, u} c.pt
⊢ IsVanKampenColimit.{0, 0, v, u} (asEmptyCocone c.pt)

Tactic:
replace this := IsInitial.isVanKampenColimit this
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasStrictInitialObjects.{v, u} C
inst_3 : IsEmpty J
F : Functor.{u', v, v', u} J C
c : Cocone F
hc : IsColimit c
this : IsVanKampenColimit.{0, 0, v, u} (asEmptyCocone c.pt)
apply :
  IsVanKampenColimit (J := Discrete PEmpty.{1}) (F :=
    Equivalence.functor (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J) ⋙ F)
    (Cocone.whisker (Equivalence.functor (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J)) c)
⊢ IsVanKampenColimit c

Tactic:
apply (IsVanKampenColimit.whiskerEquivalence_iff
    (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J)).mp

Premises used: CategoryTheory.equivalenceOfIsEmpty, PEmpty, CategoryTheory.IsVanKampenColimit.whiskerEquivalence_iff, Iff.mp, CategoryTheory.Discrete
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasStrictInitialObjects.{v, u} C
inst_3 : IsEmpty J
F : Functor.{u', v, v', u} J C
c : Cocone F
hc : IsColimit c
this : IsVanKampenColimit.{0, 0, v, u} (asEmptyCocone c.pt)
⊢ ∀ (j : Discrete PEmpty.{1}),
    ((Cocone.precompose
                    (uniqueFromEmpty (Equivalence.functor (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J) ⋙ F)).hom).obj
                (asEmptyCocone c.pt)).ι.app
          j ≫
        Iso.hom
          (Iso.refl
            ((Cocone.precompose
                    (uniqueFromEmpty (Equivalence.functor (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J) ⋙ F)).hom).obj
                (asEmptyCocone c.pt)).pt) =
      NatTrans.app (Cocone.ι (Cocone.whisker (Equivalence.functor (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J)) c)) j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasStrictInitialObjects.{v, u} C
inst_3 : IsEmpty J
F : Functor.{u', v, v', u} J C
c : Cocone F
hc : IsColimit c
this : IsVanKampenColimit.{0, 0, v, u} (asEmptyCocone c.pt)
⊢ IsVanKampenColimit (J := Discrete PEmpty.{1}) (F :=
    Equivalence.functor (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J) ⋙ F)
    (Cocone.whisker (Equivalence.functor (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J)) c)

Tactic:
exact (this.precompose_isIso (Functor.uniqueFromEmpty
    ((equivalenceOfIsEmpty (Discrete PEmpty.{1}) J).functor ⋙ F)).hom).of_iso
    (Cocone.ext (Iso.refl _) (by simp))

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.equivalenceOfIsEmpty, CategoryTheory.Functor.comp, CategoryTheory.IsVanKampenColimit.of_iso, CategoryTheory.Iso.refl, CategoryTheory.Equivalence.functor, CategoryTheory.IsVanKampenColimit.precompose_isIso, PEmpty, CategoryTheory.Functor.uniqueFromEmpty, CategoryTheory.Iso.hom, CategoryTheory.Discrete
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
mp :
  IsVanKampenColimit c →
    ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      αX ≫ c.inl = c'.inl ≫ f →
        αY ≫ c.inr = c'.inr ≫ f →
          (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)
mpr :
  (∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      αX ≫ c.inl = c'.inl ≫ f →
        αY ≫ c.inr = c'.inr ≫ f →
          (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)) →
    IsVanKampenColimit c
⊢ IsVanKampenColimit c ↔
    ∀ {X' Y' : C} (c' : BinaryCofan.{v, u} X' Y') (αX : X' ⟶ X) (αY : Y' ⟶ Y) (f : c'.pt ⟶ c.pt),
      αX ≫ c.inl = c'.inl ≫ f →
        αY ≫ c.inr = c'.inr ≫ f →
          (Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
w :
  Eq (α :=
    obj.{0, v, 0, u} (pair X' 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 αX αY ≫ c.ι) { as := WalkingPair.left })
    ((c'.ι ≫ map (const (Discrete WalkingPair)) f).app { as := WalkingPair.left })
w₁ :
  Eq (α :=
    obj.{0, v, 0, u} (pair X' 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 αX αY ≫ c.ι) { as := WalkingPair.right })
    ((c'.ι ≫ map (const (Discrete WalkingPair)) f).app { as := WalkingPair.right })
⊢ mapPair αX αY ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f

Tactic:
ext ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
w : Eq (α := X' ⟶ c.pt) (αX ≫ c.ι.app { as := WalkingPair.left }) (c'.ι.app { as := WalkingPair.left } ≫ f)
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair X' 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 αX αY ≫ c.ι) { as := WalkingPair.left })
    ((c'.ι ≫ map (const (Discrete WalkingPair)) f).app { as := WalkingPair.left })

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
w : Eq (α := Y' ⟶ c.pt) (αY ≫ c.ι.app { as := WalkingPair.right }) (c'.ι.app { as := WalkingPair.right } ≫ f)
⊢ Eq (α :=
    obj.{0, v, 0, u} (pair X' 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 αX αY ≫ c.ι) { as := WalkingPair.right })
    ((c'.ι ≫ map (const (Discrete WalkingPair)) f).app { as := WalkingPair.right })

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
⊢ Eq (α := X' ⟶ c.pt) (αX ≫ c.ι.app { as := WalkingPair.left }) (c'.ι.app { as := WalkingPair.left } ≫ f)

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
⊢ Eq (α := Y' ⟶ c.pt) (αY ≫ c.ι.app { as := WalkingPair.right }) (c'.ι.app { as := WalkingPair.right } ≫ f)

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
mp :
  (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (NatTrans.app (mapPair αX αY) j) f (c.ι.app j)) ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
⊢ Nonempty (IsColimit c') ↔ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr

Tactic:
rw [H c' (mapPair αX αY) f (by ext ⟨⟨⟩⟩ <;> dsimp <;> assumption) (.of_discrete _)]

Premises used: CategoryTheory.NatTrans.Equifibered.of_discrete, CategoryTheory.Limits.mapPair
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
mp :
  (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (NatTrans.app (mapPair αX αY) j) f (c.ι.app j)) →
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
mp₁ :
  IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr →
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (NatTrans.app (mapPair αX αY) j) f (c.ι.app j)
⊢ (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (NatTrans.app (mapPair αX αY) j) f (c.ι.app j)) ↔
    IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H_1 : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
H : ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (NatTrans.app (mapPair αX αY) j) f (c.ι.app j)
⊢ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr

Tactic:
⟨H _, H _⟩

Premises used: And.intro
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H_1 : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
H : ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (NatTrans.app (mapPair αX αY) j) f (c.ι.app j)
⊢ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr

Tactic:
exact ⟨H _, H _⟩
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H_1 : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan.{v, u} X' Y'
αX : X' ⟶ X
αY : Y' ⟶ Y
f : c'.pt ⟶ c.pt
hαX : αX ≫ c.inl = c'.inl ≫ f
hαY : αY ≫ c.inr = c'.inr ≫ f
H : IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
⊢ IsPullback (P := obj.{0, v, 0, u} (pair X' Y') { as := WalkingPair.left : Discrete WalkingPair })
    (c'.ι.app { as := WalkingPair.left }) (NatTrans.app (mapPair αX αY) { as := WalkingPair.left }) f
    (c.ι.app { as := WalkingPair.left })

Tactic:
H.1

Premises used: And.left