awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
⊢ ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
    PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl
have this₁ : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
Tactic: have : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y) := by
      apply Functor.hext
      · rintro ⟨⟨⟩⟩ <;> rfl
      · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
this : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
⊢ ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
    PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl
have rw : ∀ (Z : C) (i : Discrete WalkingPair)
  (f : Z ⟶ Cocone.pt.{0, v, 0, u} (F := pair (Gr.obj X) (Gr.obj Y)) (colimit.cocone (pair (Gr.obj X) (Gr.obj Y)))),
  PreservesLimit (cospan f (NatTrans.app (Cocone.ι (colimit.cocone (pair (Gr.obj X) (Gr.obj Y)))) i)) Gl
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
this : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
Z : C
f : Z ⟶ Cocone.pt.{0, v, 0, u} (F := pair (Gr.obj X) (Gr.obj Y)) (colimit.cocone (pair (Gr.obj X) (Gr.obj Y)))
⊢ PreservesLimit
    (cospan (Y :=
      Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.left : Discrete WalkingPair }) f
      (NatTrans.app (Cocone.ι (colimit.cocone (pair (Gr.obj X) (Gr.obj Y))))
        { as := WalkingPair.left : Discrete WalkingPair }))
    Gl
have left : PreservesLimit
  (cospan (Y := Gr.obj X) f
    (colimit.ι (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.left : Discrete WalkingPair } :
      Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.left : Discrete WalkingPair } ⟶
        colimit.{0, 0, v, u} (pair (Gr.obj X) (Gr.obj Y))))
  Gl
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
this : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
Z : C
f : Z ⟶ Cocone.pt.{0, v, 0, u} (F := pair (Gr.obj X) (Gr.obj Y)) (colimit.cocone (pair (Gr.obj X) (Gr.obj Y)))
⊢ PreservesLimit
    (cospan (Y :=
      Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.right : Discrete WalkingPair }) f
      (NatTrans.app (Cocone.ι (colimit.cocone (pair (Gr.obj X) (Gr.obj Y))))
        { as := WalkingPair.right : Discrete WalkingPair }))
    Gl
have right : PreservesLimit
  (cospan (Y := Gr.obj Y) f
    (colimit.ι (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.right : Discrete WalkingPair } :
      Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) { as := WalkingPair.right : Discrete WalkingPair } ⟶
        colimit.{0, 0, v, u} (pair (Gr.obj X) (Gr.obj Y))))
  Gl
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
⊢ IsVanKampenColimit
    (Functor.obj
      (Cocone.precompose
        (Iso.hom (Functor.isoWhiskerLeft (pair X Y) (asIso adj.counit) ≪≫ Functor.rightUnitor (pair X Y))))
      c)
have this₁ : ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
  PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl
Tactic: have : ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
        PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl := by
    have : pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y) := by
      apply Functor.hext
      · rintro ⟨⟨⟩⟩ <;> rfl
      · rintro ⟨⟨⟩⟩ ⟨j⟩ ⟨⟨rfl : _ = j⟩⟩ <;> simp
    rw [this]
    rintro Z ⟨_ | _⟩ f <;> dsimp <;> infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
this :
  ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
    PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl
⊢ IsVanKampenColimit
    (Functor.obj
      (Cocone.precompose
        (Iso.hom (Functor.isoWhiskerLeft (pair X Y) (asIso adj.counit) ≪≫ Functor.rightUnitor (pair X Y))))
      c)
have van_kampen' : IsColimit (Gl.mapCocone (colimit.cocone (pair X Y ⋙ Gr)))
Tactic: refine ((FinitaryExtensive.vanKampen _ (colimit.isColimit <| pair X Y ⋙ _)).map_reflective
    adj).of_iso (IsColimit.uniqueUpToIso ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this_1 : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
this :
  ∀ (Z : C) (i : Discrete WalkingPair) (f : Z ⟶ (colimit.cocone (pair X Y ⋙ Gr)).pt),
    PreservesLimit (cospan f ((colimit.cocone (pair X Y ⋙ Gr)).ι.app i)) Gl
van_kampen' : IsColimit (Gl.mapCocone (colimit.cocone (pair X Y ⋙ Gr)))
⊢ IsVanKampenColimit
    (Functor.obj
      (Cocone.precompose
        (Iso.hom (Functor.isoWhiskerLeft (pair X Y) (asIso adj.counit) ≪≫ Functor.rightUnitor (pair X Y))))
      c)
have van_kampen'₁ : IsColimit
  (Functor.obj
    (Cocone.precompose
      (Iso.hom (Functor.isoWhiskerLeft (pair X Y) (asIso adj.counit) ≪≫ Functor.rightUnitor (pair X Y))))
    c)
Tactic: refine ((FinitaryExtensive.vanKampen _ (colimit.isColimit <| pair X Y ⋙ _)).map_reflective
    adj).of_iso (IsColimit.uniqueUpToIso ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : FinitaryExtensive.{v'', u''} D
inst_3 : HasFiniteCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
inst_5 : PreservesPullbacksOfInclusions F
inst_6 : ReflectsLimitsOfShape WalkingCospan F
inst_7 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_8 : ReflectsColimitsOfShape (Discrete WalkingPair) F
⊢ FinitaryExtensive.{v, u} C
have van_kampen' : ∀ {X Y : C} (c : BinaryCofan.{v, u} X Y) (a : IsColimit c), IsVanKampenColimit c
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : FinitaryExtensive.{v'', u''} D
inst_3 : HasFiniteCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
inst_5 : PreservesPullbacksOfInclusions F
inst_6 : ReflectsLimitsOfShape WalkingCospan F
inst_7 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_8 : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
⊢ IsVanKampenColimit c
have van_kampen' : IsVanKampenColimit.{0, 0, v, u} (C := C) (F := pair X Y) (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)
Tactic: refine IsVanKampenColimit.of_iso ?_ (hc.uniqueUpToIso (coprodIsCoprod X Y)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : FinitaryExtensive.{v'', u''} D
inst_3 : HasFiniteCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
inst_5 : PreservesPullbacksOfInclusions F
inst_6 : ReflectsLimitsOfShape WalkingCospan F
inst_7 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_8 : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
i : Discrete WalkingPair
Z : C
f : Z ⟶ coprod.{v, u} X Y
⊢ PreservesLimit (cospan f (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)) i))
    F
have left : PreservesLimit
  (cospan (Y := Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) f
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
      { as := WalkingPair.left : Discrete WalkingPair }))
  F
Tactic: rcases i with ⟨_ | _⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : FinitaryExtensive.{v'', u''} D
inst_3 : HasFiniteCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
inst_5 : PreservesPullbacksOfInclusions F
inst_6 : ReflectsLimitsOfShape WalkingCospan F
inst_7 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_8 : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
i : Discrete WalkingPair
Z : C
f : Z ⟶ coprod.{v, u} X Y
left :
  PreservesLimit
    (cospan (Y := Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) f
      (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
        { as := WalkingPair.left : Discrete WalkingPair }))
    F
⊢ PreservesLimit (cospan f (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)) i))
    F
have right : PreservesLimit
  (cospan (Y := Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) f
    (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
      { as := WalkingPair.right : Discrete WalkingPair }))
  F
Tactic: rcases i with ⟨_ | _⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : FinitaryExtensive.{v'', u''} D
inst_3 : HasFiniteCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
inst_5 : PreservesPullbacksOfInclusions F
inst_6 : ReflectsLimitsOfShape WalkingCospan F
inst_7 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_8 : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
Z : C
f : Z ⟶ coprod.{v, u} X Y
⊢ PreservesLimit
    (cospan (Y := Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) f
      (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
        { as := WalkingPair.left : Discrete WalkingPair }))
    F
have left : PreservesLimit (cospan f coprod.inl) F
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : FinitaryExtensive.{v'', u''} D
inst_3 : HasFiniteCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
inst_5 : PreservesPullbacksOfInclusions F
inst_6 : ReflectsLimitsOfShape WalkingCospan F
inst_7 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_8 : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
Z : C
f : Z ⟶ coprod.{v, u} X Y
⊢ PreservesLimit
    (cospan (Y := Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) f
      (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr))
        { as := WalkingPair.right : Discrete WalkingPair }))
    F
have right : PreservesLimit (cospan f coprod.inr) F
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : FinitaryExtensive.{v'', u''} D
inst_3 : HasFiniteCoproducts.{v, u} C
inst_4 : HasPullbacksOfInclusions.{v, u} C
inst_5 : PreservesPullbacksOfInclusions F
inst_6 : ReflectsLimitsOfShape WalkingCospan F
inst_7 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_8 : ReflectsColimitsOfShape (Discrete WalkingPair) F
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
⊢ IsVanKampenColimit.{0, 0, v, u} (C := C) (F := pair X Y)
    (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)
have this : ∀ (i : Discrete WalkingPair) (Z : C) (f : Z ⟶ coprod.{v, u} X Y),
  PreservesLimit (cospan f (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)) i))
    F
Tactic: have (i : Discrete WalkingPair) (Z : C) (f : Z ⟶ X ⨿ Y) :
    PreservesLimit (cospan f ((BinaryCofan.mk coprod.inl coprod.inr).ι.app i)) F := by
    rcases i with ⟨_ | _⟩ <;> dsimp <;> infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : FinitaryExtensive.{v'', u''} D
inst_3 : HasFiniteCoproducts.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : PreservesLimitsOfShape WalkingCospan F
inst_6 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_7 : F.ReflectsIsomorphisms
⊢ FinitaryExtensive.{v, u} C
have this : ReflectsLimitsOfShape WalkingCospan F
Tactic: haveI : ReflectsLimitsOfShape WalkingCospan F := reflectsLimitsOfShape_of_reflectsIsomorphisms
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
F : Functor.{v, v'', u, u''} C D
inst_2 : FinitaryExtensive.{v'', u''} D
inst_3 : HasFiniteCoproducts.{v, u} C
inst_4 : HasPullbacks.{v, u} C
inst_5 : PreservesLimitsOfShape WalkingCospan F
inst_6 : PreservesColimitsOfShape (Discrete WalkingPair) F
inst_7 : F.ReflectsIsomorphisms
this : ReflectsLimitsOfShape WalkingCospan F
⊢ FinitaryExtensive.{v, u} C
have this₁ : ReflectsColimitsOfShape (Discrete WalkingPair) F
Tactic: haveI : ReflectsColimitsOfShape (Discrete WalkingPair) F :=
    reflectsColimitsOfShape_of_reflectsIsomorphisms
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
n : ℕ
F : Functor.{0, v, 0, u} (Discrete (Fin n)) C
c : Cocone F
hc : IsColimit c
f : Fin n → C := F.obj ∘ Discrete.mk
⊢ IsUniversalColimit c
have this : F = Discrete.functor f
Tactic: have : F = Discrete.functor f :=
    Functor.hext (fun _ ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
n : ℕ
F : Functor.{0, v, 0, u} (Discrete (Fin n)) C
c : Cocone F
hc : IsColimit c
f : Fin n → C := F.obj ∘ Discrete.mk
this : F = Discrete.functor f
⊢ IsUniversalColimit c
have clear_value : ∀ (f : Fin n → C) (this : F = Discrete.functor f), IsUniversalColimit c
Tactic: clear_value f
Cleared hypotheses: f, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
n : ℕ
F : Functor.{0, v, 0, u} (Discrete (Fin n)) C
c : Cocone F
hc : IsColimit c
f : Fin n → C
this : F = Discrete.functor f
⊢ IsUniversalColimit c
have subst : ∀ {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsUniversalColimit c
Tactic: subst this
Cleared hypotheses: F, c, hc, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsUniversalColimit c
f : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
⊢ IsUniversalColimit c
have succ : ∀ {Z : C}
  (i :
    Z ⟶
      Cocone.pt.{0, v, 0, u} (F :=
        pair (f 0)
          (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
            (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
        (BinaryCofan.mk (P :=
          coprod.{v, u} (f 0)
            (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
          coprod.inl coprod.inr)),
  HasPullback
    (BinaryCofan.inr
      (BinaryCofan.mk (P :=
        coprod.{v, u} (f 0)
          (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
            (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
        coprod.inl coprod.inr))
    i
Tactic: refine IsUniversalColimit.of_iso (@isUniversalColimit_extendCofan _ _ _ _ _ _
      (IH _ (coproductIsCoproduct _)) (FinitaryPreExtensive.universal' _ (coprodIsCoprod _ _)) ?_)
      ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsUniversalColimit c
f : Fin (n + 1) → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
⊢ ∀ {Z : C}
    (i :
      Z ⟶
        Cocone.pt.{0, v, 0, u} (F :=
          pair (f 0)
            (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
          (BinaryCofan.mk (P :=
            coprod.{v, u} (f 0)
              (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
                (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
            coprod.inl coprod.inr)),
    HasPullback
      (BinaryCofan.inr
        (BinaryCofan.mk (P :=
          coprod.{v, u} (f 0)
            (Cocone.pt.{0, v, 0, u} (J := Discrete (Fin n)) (F := Discrete.functor fun (i : Fin n) ↦ f i.succ)
              (Cofan.mk (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ) (Sigma.ι fun (i : Fin n) ↦ f i.succ))))
          coprod.inl coprod.inr))
      i
have succ : ∀ {Z : C} (i : Z ⟶ coprod.{v, u} (f 0) (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)), HasPullback coprod.inr i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
n : ℕ
f : Fin n → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
⊢ IsUniversalColimit c
have zero : ∀ (f : Fin 0 → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsUniversalColimit c
Tactic: induction n with
  | zero => exact (isVanKampenColimit_of_isEmpty _ hc).isUniversal
  | succ n IH =>
    refine IsUniversalColimit.of_iso (@isUniversalColimit_extendCofan _ _ _ _ _ _
      (IH _ (coproductIsCoproduct _)) (FinitaryPreExtensive.universal' _ (coprodIsCoprod _ _)) ?_)
      ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)
    · dsimp
      infer_instance
Cleared hypotheses: n, f, c, hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
n : ℕ
f : Fin n → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
zero : ∀ (f : Fin 0 → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsUniversalColimit c
⊢ IsUniversalColimit c
have succ : ∀ (n : ℕ)
  (IH : ∀ (f : Fin n → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsUniversalColimit c)
  (f : Fin (n + 1) → C) {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsUniversalColimit c
Tactic: induction n with
  | zero => exact (isVanKampenColimit_of_isEmpty _ hc).isUniversal
  | succ n IH =>
    refine IsUniversalColimit.of_iso (@isUniversalColimit_extendCofan _ _ _ _ _ _
      (IH _ (coproductIsCoproduct _)) (FinitaryPreExtensive.universal' _ (coprodIsCoprod _ _)) ?_)
      ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)
    · dsimp
      infer_instance
Cleared hypotheses: n, f, c, hc