awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') :=
  ((IsColimit.precomposeHomEquiv β c').symm : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this_3 : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
this_4 :
  f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
this :
  IsPullback (Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)) (Gl.map ((whiskerRight α' Gr).app j))
    (Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })) (Gl.map (c.ι.app j))
⊢ IsPullback (c'.ι.app j) (β.inv.app j) (hl.coconePointUniqueUpToIso hr).hom
    (Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j))
have refine_2 : c'.ι.app j ≫ (hl.coconePointUniqueUpToIso hr).hom = β.inv.app j ≫ Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)
Tactic: refine IsPullback.of_vert_isIso ⟨?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') :=
  ((IsColimit.precomposeHomEquiv β c').symm : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this_3 : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
this_4 :
  f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
this :
  IsPullback (Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)) (Gl.map ((whiskerRight α' Gr).app j))
    (Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })) (Gl.map (c.ι.app j))
⊢ c'.ι.app j ≫ (hl.coconePointUniqueUpToIso hr).hom = β.inv.app j ≫ Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)
have refine_2 : (β.hom.app j ≫ c'.ι.app j) ≫ (hl.coconePointUniqueUpToIso hr).hom = Gl.map ((colimit.cocone (F' ⋙ Gr)).ι.app j)
Tactic: rw [← IsIso.inv_comp_eq, ← Category.assoc, NatIso.inv_inv_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ F.whiskerLeft adj.counit ≫ F.rightUnitor.hom
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') :=
  ((IsColimit.precomposeHomEquiv β c').symm : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this_3 : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
this :
  f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
⊢ whiskerRight α' Gr ≫ c.ι =
    (colimit.cocone (F' ⋙ Gr)).ι ≫ map (const J) (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
have refine_1 : ∀ (α' : F' ⟶ F) (hα' : NatTrans.Equifibered α')
  (hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j),
  let β := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor;
  let hl : IsColimit ((Cocone.precompose β.hom).obj c') :=
    ((IsColimit.precomposeHomEquiv β c').symm : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc';
  let hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr));
  ∀ (this : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j)))
    (this :
      f =
        (hl.coconePointUniqueUpToIso hr).hom ≫
          Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })),
    whiskerRight α' Gr ≫ c.ι =
      (colimit.cocone (F' ⋙ Gr)).ι ≫
        map (const J) (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
Tactic: clear_value α'
Cleared hypotheses: α', hα', hα'', β, hl, hr, this_3, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : HasColimitsOfShape.{u', v', v, u} J C
Gl : Functor.{v, v_2, u, u_2} C D
Gr : Functor.{v_2, v, u_2, u} D C
adj : Gl ⊣ Gr
inst_4 : Gr.Full
inst_5 : Gr.Faithful
F : Functor.{u', v_2, v', u_2} J D
c : Cocone (F ⋙ Gr)
H : IsVanKampenColimit c
inst_6 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)
inst_7 : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl
inst_8 : ∀ (X : C) (i : J) (f : X ⟶ c.pt), PreservesLimit (cospan f (c.ι.app i)) Gl
this_1 : PreservesLimitsOfSize.{v, v, v_2, v, u_2, u} Gr
this_2 : PreservesColimitsOfSize.{u', v', v, v_2, u, u_2} Gl
F' : Functor.{u', v_2, v', u_2} J D
c' : Cocone F'
α : F' ⟶ (F ⋙ Gr) ⋙ Gl
f : c'.pt ⟶ (Gl.mapCocone c).pt
h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ map (const J) f
hα : NatTrans.Equifibered α
hc' : IsColimit c'
j : J
α' : F' ⟶ F
hα' : NatTrans.Equifibered α'
hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.1 j) ≫ α.app j
β : F' ⋙ Gr ⋙ Gl ≅ F' := F'.isoWhiskerLeft (asIso adj.counit) ≪≫ F'.rightUnitor
hl : IsColimit ((Cocone.precompose β.hom).obj c') :=
  ((IsColimit.precomposeHomEquiv β c').symm : (a : IsColimit c') → IsColimit ((Cocone.precompose β.hom).obj c')) hc'
hr : IsColimit (Gl.mapCocone (colimit.cocone (F' ⋙ Gr))) := isColimitOfPreserves Gl (colimit.isColimit (F' ⋙ Gr))
this_3 : α.app j = β.inv.app j ≫ Gl.map (Gr.map (α'.app j))
this :
  f =
    (hl.coconePointUniqueUpToIso hr).hom ≫ Gl.map (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
⊢ whiskerRight α' Gr ≫ c.ι =
    (colimit.cocone (F' ⋙ Gr)).ι ≫ map (const J) (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι })
have refine_1 : ∀ (j : J),
  (whiskerRight α' Gr ≫ c.ι).app j =
    NatTrans.app
      ((colimit.cocone (F' ⋙ Gr)).ι ≫
        map (const J) (colimit.desc (F' ⋙ Gr) { pt := c.pt, ι := whiskerRight α' Gr ≫ c.ι }))
      j
Tactic: ext j
-- 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
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))
⊢ IsIso f
have obtain : ∀ (l : Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A)) ⟶ A)
  (h₁ : BinaryCofan.inl (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l = f ≫ initial.to A)
  (h₂ :
    Eq.{v + 1} (α := obj.{0, v, 0, u} (pair A A) { as := WalkingPair.right : Discrete WalkingPair } ⟶ A)
      (BinaryCofan.inr (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l) (𝟙 A)),
  IsIso f
Tactic: obtain ⟨l, h₁, h₂⟩ := Limits.BinaryCofan.IsColimit.desc' this (f ≫ initial.to A) (𝟙 A)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
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))
l : Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A)) ⟶ A
h₁ : BinaryCofan.inl (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l = f ≫ initial.to A
h₂ :
  Eq.{v + 1} (α := obj.{0, v, 0, u} (pair A A) { as := WalkingPair.right : Discrete WalkingPair } ⟶ A)
    (BinaryCofan.inr (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l) (𝟙 A)
⊢ IsIso f
have 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
Tactic: rcases (Category.id_comp _).symm.trans h₂ with rfl
Cleared hypotheses: l, h₁, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
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))
l : Cocone.pt.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A)) ⟶ A
h₁ : BinaryCofan.inl (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l = f ≫ initial.to A
h₂ :
  Eq.{v + 1} (α := obj.{0, v, 0, u} (pair A A) { as := WalkingPair.right : Discrete WalkingPair } ⟶ A)
    (BinaryCofan.inr (BinaryCofan.mk (𝟙 A) (𝟙 A)) ≫ l) (𝟙 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
⊢ IsIso f
have 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)
Tactic: rcases (Category.id_comp _).symm.trans h₂ with rfl
Cleared hypotheses: l, h₁, h₂
-- 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
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
⊢ IsIso f
have suffices : IsColimit.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))
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 _ _⟩⟩
-- 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
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} (α :=
    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))
have 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 })
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
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 })
⊢ 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))
have 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 })
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
H : IsUniversalColimit.{0, 0, v, u} (BinaryCofan.mk (𝟙 (initial.{v, u} C)) (𝟙 (initial.{v, u} C)))
A : C
f : A ⟶ initial.{v, u} C
⊢ IsColimit.{0, v, 0, u} (BinaryCofan.mk (𝟙 A) (𝟙 A))
have 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)
Tactic: refine (H (BinaryCofan.mk (𝟙 _) (𝟙 _)) (mapPair f f) f (by ext ⟨⟨⟩⟩ <;> simp)
        (.of_discrete _) ?_).some
-- 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
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 (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 })
have left : IsPullback (𝟙 A) f f (𝟙 (initial.{v, u} C))
Tactic: dsimp
-- 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
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 (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 })
have right : IsPullback (𝟙 A) f f (𝟙 (initial.{v, u} C))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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
⊢ IsInitial.{v, u} c.pt
have 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
Tactic: have := (IsColimit.precomposeInvEquiv (Functor.uniqueFromEmpty _) _).symm
      (hc.whiskerEquivalence (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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
⊢ IsVanKampenColimit c
have have : ∀ (this : IsInitial.{v, u} c.pt), 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))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (hypothesis)
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 c
have this₁ : IsVanKampenColimit.{0, 0, v, u} (asEmptyCocone c.pt)
Tactic: replace this := IsInitial.isVanKampenColimit this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.VanKampen (goal)
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 c
have 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)
Tactic: apply (IsVanKampenColimit.whiskerEquivalence_iff
    (equivalenceOfIsEmpty (Discrete PEmpty.{1}) J)).mp
-- 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
⊢ 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)
have 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)
Tactic: constructor
-- 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
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)
⊢ 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)
have 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
Tactic: constructor