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
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.right : Discrete WalkingPair })
    (c'.ι.app { as := WalkingPair.right }) (NatTrans.app (mapPair αX αY) { as := WalkingPair.right }) f
    (c.ι.app { as := WalkingPair.right })

Tactic:
H.2

Premises used: And.right
-- 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:
exacts [H.1, H.2]

Premises used: And.right, And.left
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {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)
F' : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
h_obj : ∀ (X : Discrete WalkingPair), F'.obj X = obj.{0, v, 0, u} (pair X' Y') X
h_map :
  ∀ (X Y : Discrete WalkingPair) (f : X ⟶ Y),
    HEq (F'.map f) (β := obj.{0, v, 0, u} (pair X' Y') X ⟶ obj.{0, v, 0, u} (pair X' Y') Y) (map (pair X' Y') f)
⊢ F' = pair X' Y'

Tactic:
apply Functor.hext

Premises used: CategoryTheory.Functor.hext
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {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)
F' : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ F'.obj { as := WalkingPair.left : Discrete WalkingPair } =
    obj.{0, v, 0, u} (pair X' Y') { as := WalkingPair.left : Discrete WalkingPair }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {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)
F' : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ F'.obj { as := WalkingPair.right : Discrete WalkingPair } =
    obj.{0, v, 0, u} (pair X' Y') { as := WalkingPair.right : Discrete WalkingPair }

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {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)
F' : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ HEq
    (F'.map
      {
        down :=
          { down := ⋯ :
            PLift
              ({ as := WalkingPair.left : Discrete WalkingPair }.as =
                { as := { as := WalkingPair.left : Discrete WalkingPair }.as : Discrete WalkingPair }.as) } :
        ULift.{0, 0}
          (PLift
            ({ as := WalkingPair.left : Discrete WalkingPair }.as =
              { as := { as := WalkingPair.left : Discrete WalkingPair }.as : Discrete WalkingPair }.as)) })
    (β :=
    obj.{0, v, 0, u} (pair X' Y') { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (pair X' Y')
        { as := { as := WalkingPair.left : Discrete WalkingPair }.as : Discrete WalkingPair })
    (map (pair X' Y') { down := { down := ⋯ } })

Tactic:
simp [X', Y']
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {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)
F' : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ HEq
    (F'.map
      {
        down :=
          { down := ⋯ :
            PLift
              ({ as := WalkingPair.right : Discrete WalkingPair }.as =
                { as := { as := WalkingPair.right : Discrete WalkingPair }.as : Discrete WalkingPair }.as) } :
        ULift.{0, 0}
          (PLift
            ({ as := WalkingPair.right : Discrete WalkingPair }.as =
              { as := { as := WalkingPair.right : Discrete WalkingPair }.as : Discrete WalkingPair }.as)) })
    (β :=
    obj.{0, v, 0, u} (pair X' Y') { as := WalkingPair.right : Discrete WalkingPair } ⟶
      obj.{0, v, 0, u} (pair X' Y')
        { as := { as := WalkingPair.right : Discrete WalkingPair }.as : Discrete WalkingPair })
    (map (pair X' Y') { down := { down := ⋯ } })

Tactic:
simp [X', Y']
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {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)
F' : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
⊢ F' = pair X' Y'

Tactic:
have : F' = pair X' Y' := by
      apply Functor.hext
      · rintro ⟨⟨⟩⟩ <;> rfl
      · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp [X', Y']
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {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)
F' : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
this : F' = pair X' Y'
mpr :
  ∀ (X' Y' : C) (this : F' = pair X' Y'),
    Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

Tactic:
clear_value X' Y'
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {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)
F' : Functor.{0, v, 0, u} (Discrete WalkingPair) C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
X' Y' : C
this : F' = pair X' Y'
mpr :
  ∀ (c' : Cocone.{0, v, 0, u} (pair X' Y'))
    (α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair X' Y') (pair X Y)) (f : c'.pt ⟶ c.pt)
    (hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f) (h : NatTrans.Equifibered α),
    Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

Tactic:
subst this
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {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)
X' Y' : C
c' : Cocone.{0, v, 0, u} (pair X' Y')
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair X' Y') (pair X Y)
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
h : NatTrans.Equifibered α
mpr :
  ∀ (c' : BinaryCofan.{v, u} X' Y') (f : c'.pt ⟶ c.pt) (hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f),
    Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

Tactic:
change BinaryCofan X' Y' at c'

Premises used: CategoryTheory.Limits.BinaryCofan
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {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)
X' Y' : C
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair X' Y') (pair X Y)
h : NatTrans.Equifibered α
c' : BinaryCofan.{v, u} X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
mpr :
  IsPullback c'.inl (α.app { as := WalkingPair.left })
        (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
      IsPullback c'.inr (α.app { as := WalkingPair.right })
        (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inr ↔
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

Tactic:
rw [H c' _ _ _ (NatTrans.congr_app hα ⟨WalkingPair.left⟩)
        (NatTrans.congr_app hα ⟨WalkingPair.right⟩)]

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk, CategoryTheory.NatTrans.congr_app, CategoryTheory.Limits.WalkingPair.left
-- Module: Mathlib.CategoryTheory.Limits.VanKampen
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
H :
  ∀ {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)
X' Y' : C
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair X' Y') (pair X Y)
h : NatTrans.Equifibered α
c' : BinaryCofan.{v, u} X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
mpr :
  IsPullback c'.inl (α.app { as := WalkingPair.left })
        (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
      IsPullback c'.inr (α.app { as := WalkingPair.right })
        (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inr →
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
mpr₁ :
  (∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)) →
    IsPullback c'.inl (α.app { as := WalkingPair.left })
        (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
      IsPullback c'.inr (α.app { as := WalkingPair.right })
        (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inr
⊢ IsPullback c'.inl (α.app { as := WalkingPair.left })
        (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
      IsPullback c'.inr (α.app { as := WalkingPair.right })
        (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inr ↔
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

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 :
  ∀ {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)
X' Y' : C
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair X' Y') (pair X Y)
h : NatTrans.Equifibered α
c' : BinaryCofan.{v, u} X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
H :
  IsPullback c'.inl (α.app { as := WalkingPair.left })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
    IsPullback c'.inr (α.app { as := WalkingPair.right })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inr
⊢ IsPullback (P := obj.{0, v, 0, u} (pair X' Y') { as := WalkingPair.left : Discrete WalkingPair })
    (c'.ι.app { as := WalkingPair.left }) (α.app { as := WalkingPair.left }) f (c.ι.app { as := WalkingPair.left })

Tactic:
H.1

Premises used: And.left
-- 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 :
  ∀ {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)
X' Y' : C
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair X' Y') (pair X Y)
h : NatTrans.Equifibered α
c' : BinaryCofan.{v, u} X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
H :
  IsPullback c'.inl (α.app { as := WalkingPair.left })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
    IsPullback c'.inr (α.app { as := WalkingPair.right })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inr
⊢ IsPullback (P := obj.{0, v, 0, u} (pair X' Y') { as := WalkingPair.right : Discrete WalkingPair })
    (c'.ι.app { as := WalkingPair.right }) (α.app { as := WalkingPair.right }) f (c.ι.app { as := WalkingPair.right })

Tactic:
H.2

Premises used: And.right
-- 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 :
  ∀ {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)
X' Y' : C
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair X' Y') (pair X Y)
h : NatTrans.Equifibered α
c' : BinaryCofan.{v, u} X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
H :
  IsPullback c'.inl (α.app { as := WalkingPair.left })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
    IsPullback c'.inr (α.app { as := WalkingPair.right })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inr
⊢ IsPullback (P := obj.{0, v, 0, u} (pair X' Y') { as := WalkingPair.left : Discrete WalkingPair })
    (c'.ι.app { as := WalkingPair.left }) (α.app { as := WalkingPair.left }) f (c.ι.app { as := WalkingPair.left })

Tactic:
exacts [H.1, H.2]

Premises used: And.right, And.left
-- 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 :
  ∀ {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)
X' Y' : C
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair X' Y') (pair X Y)
h : NatTrans.Equifibered α
c' : BinaryCofan.{v, u} X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
H : ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
⊢ IsPullback c'.inl (α.app { as := WalkingPair.left })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
    IsPullback c'.inr (α.app { as := WalkingPair.right })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) 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 :
  ∀ {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)
X' Y' : C
α : Quiver.Hom (V := Functor.{0, v, 0, u} (Discrete WalkingPair) C) (pair X' Y') (pair X Y)
h : NatTrans.Equifibered α
c' : BinaryCofan.{v, u} X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ map (const (Discrete WalkingPair)) f
H : ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
⊢ IsPullback c'.inl (α.app { as := WalkingPair.left })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) c.inl ∧
    IsPullback c'.inr (α.app { as := WalkingPair.right })
      (NatTrans.app (map (const (Discrete WalkingPair)) f) { as := WalkingPair.left }) 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
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)
rw :
  ∀ {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

Tactic:
rw [BinaryCofan.isVanKampen_iff]

Premises used: CategoryTheory.BinaryCofan.isVanKampen_iff
-- 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
mp : Nonempty (IsColimit c') → IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr
mpr : IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr → Nonempty (IsColimit c')
⊢ 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
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 : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := h.coconePointUniqueUpToIso (colimits X' Y')
⊢ αX ≫ c.inl = (cofans X' Y').inl ≫ e.inv ≫ f

Tactic:
simp [e, hX]
-- 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 : IsColimit c'
e : c'.pt ≅ (cofans X' Y').pt := h.coconePointUniqueUpToIso (colimits X' Y')
⊢ αY ≫ c.inr = (cofans X' Y').inr ≫ e.inv ≫ f

Tactic:
simp [e, hY]