-- Mathlib/CategoryTheory/Limits/VanKampen.lean
theorem BinaryCofan.isVanKampen_iff (c : BinaryCofan X Y) :
    IsVanKampenColimit c ↔
      ∀ {X' Y' : C} (c' : BinaryCofan 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

Proof state:
case mp.mpr.mk.left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H✝ : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan 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 (c'.ι.app { as := WalkingPair.left }) ((mapPair αX αY).app { as := WalkingPair.left }) f
    (c.ι.app { as := WalkingPair.left })

case mp.mpr.mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H✝ : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan 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 (c'.ι.app { as := WalkingPair.right }) ((mapPair αX αY).app { as := WalkingPair.right }) f
    (c.ι.app { as := WalkingPair.right })

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

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan 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' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
X' : C := F'.obj { as := WalkingPair.left }
Y' : C := F'.obj { as := WalkingPair.right }
this : F' = pair X' Y'
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

Tactic:
clear_value X' Y'

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan 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' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
Y' X' : C
this : F' = pair X' Y'
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

Proof state:
case mpr.mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H✝ :
  ∀ {X' Y' : C} (c' : BinaryCofan 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)
Y' X' : C
α : pair X' Y' ⟶ pair X Y
h : NatTrans.Equifibered α
c' : BinaryCofan X' Y'
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
H : ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)
⊢ IsPullback c'.inl (α.app { as := WalkingPair.left })
      (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inl ∧
    IsPullback c'.inr (α.app { as := WalkingPair.right })
      (((Functor.const (Discrete WalkingPair)).map f).app { as := WalkingPair.left }) c.inr

Tactic:
exact ⟨H _, H _⟩

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
⊢ (∀ {X' Y' : C} (c' : BinaryCofan 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:
introv H F' hα h

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H :
  ∀ {X' Y' : C} (c' : BinaryCofan 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' : Discrete WalkingPair ⥤ C
c' : Cocone F'
α : F' ⟶ pair X Y
f : c'.pt ⟶ c.pt
hα : α ≫ c.ι = c'.ι ≫ (Functor.const (Discrete WalkingPair)).map f
h : NatTrans.Equifibered α
⊢ Nonempty (IsColimit c') ↔ ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) (α.app j) f (c.ι.app j)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
⊢ IsVanKampenColimit c ↔
    ∀ {X' Y' : C} (c' : BinaryCofan 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

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
⊢ IsVanKampenColimit c →
    ∀ {X' Y' : C} (c' : BinaryCofan 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)

case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
⊢ (∀ {X' Y' : C} (c' : BinaryCofan 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

Proof state:
case mp.mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan 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
⊢ IsPullback c'.inl αX f c.inl ∧ IsPullback c'.inr αY f c.inr →
    ∀ (j : Discrete WalkingPair), IsPullback (c'.ι.app j) ((mapPair αX αY).app j) f (c.ι.app j)

Tactic:
rintro H ⟨⟨⟩⟩

Result:
case mp.mpr.mk.left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H✝ : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan 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 (c'.ι.app { as := WalkingPair.left }) ((mapPair αX αY).app { as := WalkingPair.left }) f
    (c.ι.app { as := WalkingPair.left })

case mp.mpr.mk.right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
c : BinaryCofan X Y
H✝ : IsVanKampenColimit c
X' Y' : C
c' : BinaryCofan 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 (c'.ι.app { as := WalkingPair.right }) ((mapPair αX αY).app { as := WalkingPair.right }) f
    (c.ι.app { as := WalkingPair.right })