awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
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')
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
this : IsIso.{v, u} (𝟙 X')
⊢ IsPullback c'.inl (𝟙 X' ≫ αX) (e.hom ≫ e.inv ≫ f) c.inl
have this₁ : c'.inl ≫ e.hom = 𝟙 X' ≫ (cofans X' Y').inl
Tactic: have : c'.inl ≫ e.hom = 𝟙 X' ≫ (cofans X' Y').inl := by
        dsimp [e]
        simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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')
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
⊢ IsPullback c'.inr αY f c.inr
have mp : IsPullback c'.inr (𝟙 Y' ≫ αY) (e.hom ≫ e.inv ≫ f) c.inr
Tactic: rw [← Category.id_comp αY, ← Iso.hom_inv_id_assoc e f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
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')
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
⊢ IsPullback c'.inr (𝟙 Y' ≫ αY) (e.hom ≫ e.inv ≫ f) c.inr
have this : IsIso.{v, u} (𝟙 Y')
Tactic: haveI : IsIso (𝟙 Y') := inferInstance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
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')
hl : IsPullback (cofans X' Y').inl αX (e.inv ≫ f) c.inl
hr : IsPullback (cofans X' Y').inr αY (e.inv ≫ f) c.inr
this : IsIso.{v, u} (𝟙 Y')
⊢ IsPullback c'.inr (𝟙 Y' ≫ αY) (e.hom ≫ e.inv ≫ f) c.inr
have this₁ : c'.inr ≫ e.hom = 𝟙 Y' ≫ (cofans X' Y').inr
Tactic: have : c'.inr ≫ e.hom = 𝟙 Y' ≫ (cofans X' Y').inr := by
        dsimp [e]
        simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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
⊢ Nonempty (IsColimit c')
have mpr : IsColimit (BinaryCofan.mk c'.inl c'.inr)
Tactic: refine ⟨IsColimit.ofIsoColimit ?_ <| (isoBinaryCofanMk _).symm⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
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)
⊢ IsColimit (BinaryCofan.mk c'.inl c'.inr)
have he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst
Tactic: have he₁ : c'.inl = e₁.hom ≫ (cones f c.inl).fst := by simp [e₁]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
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
⊢ IsColimit (BinaryCofan.mk c'.inl c'.inr)
have he₂ : c'.inr = e₂.hom ≫ (cones f c.inr).fst
Tactic: have he₂ : c'.inr = e₂.hom ≫ (cones f c.inr).fst := by simp [e₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 c'.inl c'.inr)
have mpr : IsColimit (BinaryCofan.mk (e₁.hom ≫ (cones f c.inl).fst) (e₂.hom ≫ (cones f c.inr).fst))
Tactic: rw [he₁, he₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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
have 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
Tactic: refine PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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
have 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))
Tactic: refine (h (BinaryCofan.mk (initial.to Y) (𝟙 Y)) (mapPair (initial.to X) (𝟙 Y)) c.inr ?_
      (.of_discrete _)).mp ⟨?_⟩ ⟨WalkingPair.right⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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))
⊢ 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
have refine_2 : IsColimit.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))
Tactic: refine (h (BinaryCofan.mk (initial.to Y) (𝟙 Y)) (mapPair (initial.to X) (𝟙 Y)) c.inr ?_
      (.of_discrete _)).mp ⟨?_⟩ ⟨WalkingPair.right⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 (α :=
    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))
have 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 })
Tactic: ext ⟨⟨⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 })
⊢ 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))
have 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 })
Tactic: ext ⟨⟨⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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} (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)))
have dsimp : IsIso.{v, u} (𝟙 Y)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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
have 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))
Tactic: refine ((h (BinaryCofan.mk (initial.to Y) (𝟙 Y)) (mapPair (initial.to X) (𝟙 Y)) c.inr ?_
      (.of_discrete _)).mp ⟨?_⟩ ⟨WalkingPair.left⟩).flip
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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))
⊢ 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
have refine_2 : IsColimit.{0, v, 0, u} (F := pair (initial.{v, u} C) Y) (BinaryCofan.mk (initial.to Y) (𝟙 Y))
Tactic: refine ((h (BinaryCofan.mk (initial.to Y) (𝟙 Y)) (mapPair (initial.to X) (𝟙 Y)) c.inr ?_
      (.of_discrete _)).mp ⟨?_⟩ ⟨WalkingPair.left⟩).flip
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 (α :=
    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))
have 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 })
Tactic: ext ⟨⟨⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 })
⊢ 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))
have 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 })
Tactic: ext ⟨⟨⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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} (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)))
have dsimp : IsIso.{v, u} (𝟙 Y)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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
⊢ F = Discrete.functor F'
have h_obj : ∀ (X : Discrete (Fin (n + 1))), F.obj X = obj.{0, v, 0, u} (Discrete.functor F') X
Tactic: apply Functor.hext