awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Extensive
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
⊢ IsColimit
    (Functor.obj
      (Cocone.precompose
        (Iso.hom (Functor.isoWhiskerLeft (pair X Y) (asIso adj.counit) ≪≫ Functor.rightUnitor (pair X Y))))
      c)

Tactic:
exact (IsColimit.precomposeHomEquiv _ _).symm hc

Premises used: Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeHomEquiv
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
inst_3 : HasPullbacks.{v, u} C
inst_4 : FinitaryExtensive.{v, u} C
⊢ FinitaryExtensive (Functor.{v'', v, u'', u} D C)

Tactic:
haveI : HasFiniteCoproducts (D ⥤ C) := ⟨fun _ => Limits.functorCategoryHasColimitsOfShape⟩
  ⟨fun c hc => isVanKampenColimit_of_evaluation _ c fun _ =>
    FinitaryExtensive.vanKampen _ <| isColimitOfPreserves _ hc⟩

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.FinitaryExtensive.mk, CategoryTheory.FinitaryExtensive.vanKampen, CategoryTheory.Limits.pair, CategoryTheory.evaluation, CategoryTheory.isVanKampenColimit_of_evaluation, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C_1 : Type u
inst_1 : Category.{v, u} C_1
D_1 : Type u''
inst_2 : Category.{v'', u''} D_1
X_1 Y_1 : C_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_5 : IsIso f
this : HasPullback f g
⊢ Eq (α := F.obj (pullback f g) ⟶ F.obj Z) (F.map (pullback.fst f g) ≫ F.map f) (F.map (pullback.snd f g) ≫ F.map g)

Tactic:
simp only [← F.map_comp, pullback.condition]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C_1 : Type u
inst_1 : Category.{v, u} C_1
D_1 : Type u''
inst_2 : Category.{v'', u''} D_1
X_1 Y_1 : C_1
C : Type u_1
inst_3 : Category.{v_1, u_1} C
D : Type u_2
inst_4 : Category.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_5 : IsIso g
⊢ PreservesLimit (cospan f g) F

Tactic:
preservesPullback_symmetry _ _ _

Premises used: CategoryTheory.Limits.preservesPullback_symmetry
-- Module: Mathlib.CategoryTheory.Extensive
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
van_kampen' : ∀ {X Y : C} (c : BinaryCofan.{v, u} X Y) (a : IsColimit c), IsVanKampenColimit c
⊢ FinitaryExtensive.{v, u} C

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Extensive
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

Tactic:
IsVanKampenColimit.of_iso ?_ (hc.uniqueUpToIso (coprodIsCoprod X Y)).symm

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.IsVanKampenColimit.of_iso, CategoryTheory.Limits.IsColimit.uniqueUpToIso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Extensive
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
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)
⊢ IsVanKampenColimit c

Tactic:
refine IsVanKampenColimit.of_iso ?_ (hc.uniqueUpToIso (coprodIsCoprod X Y)).symm

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.IsVanKampenColimit.of_iso, CategoryTheory.Limits.IsColimit.uniqueUpToIso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Extensive
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
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
⊢ PreservesLimit (cospan f (NatTrans.app (Cocone.ι (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)) i))
    F

Tactic:
rcases i with ⟨_ | _⟩
-- Module: Mathlib.CategoryTheory.Extensive
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
left : PreservesLimit (cospan f coprod.inl) F
⊢ 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:
dsimp
-- Module: Mathlib.CategoryTheory.Extensive
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
right : PreservesLimit (cospan f coprod.inr) F
⊢ 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:
dsimp
-- Module: Mathlib.CategoryTheory.Extensive
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 f coprod.inl) F

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Extensive
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 f coprod.inr) F

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Extensive
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

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
-- Module: Mathlib.CategoryTheory.Extensive
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
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
⊢ IsVanKampenColimit.{0, 0, v, u} (C := C) (F := pair X Y)
    (BinaryCofan.mk (P := coprod.{v, u} X Y) coprod.inl coprod.inr)

Tactic:
(FinitaryExtensive.vanKampen _
    (isColimitOfPreserves F (coprodIsCoprod X Y))).of_mapCocone F

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.FinitaryExtensive.vanKampen, CategoryTheory.IsVanKampenColimit.of_mapCocone, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Extensive
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
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
⊢ 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 (FinitaryExtensive.vanKampen _
    (isColimitOfPreserves F (coprodIsCoprod X Y))).of_mapCocone F

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.FinitaryExtensive.vanKampen, CategoryTheory.IsVanKampenColimit.of_mapCocone, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Extensive
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
⊢ ReflectsLimitsOfShape WalkingCospan F

Tactic:
haveI : ReflectsLimitsOfShape WalkingCospan F := reflectsLimitsOfShape_of_reflectsIsomorphisms
-- Module: Mathlib.CategoryTheory.Extensive
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
⊢ ReflectsColimitsOfShape (Discrete WalkingPair) F

Tactic:
haveI : ReflectsColimitsOfShape (Discrete WalkingPair) F :=
    reflectsColimitsOfShape_of_reflectsIsomorphisms
-- Module: Mathlib.CategoryTheory.Extensive
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_1 : ReflectsLimitsOfShape WalkingCospan F
this : ReflectsColimitsOfShape (Discrete WalkingPair) F
⊢ FinitaryExtensive.{v, u} C

Tactic:
finitaryExtensive_of_preserves_and_reflects F

Premises used: CategoryTheory.finitaryExtensive_of_preserves_and_reflects
-- Module: Mathlib.CategoryTheory.Extensive
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_1 : ReflectsLimitsOfShape WalkingCospan F
this : ReflectsColimitsOfShape (Discrete WalkingPair) F
⊢ FinitaryExtensive.{v, u} C

Tactic:
exact finitaryExtensive_of_preserves_and_reflects F

Premises used: CategoryTheory.finitaryExtensive_of_preserves_and_reflects
-- Module: Mathlib.CategoryTheory.Extensive
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
i : Fin n
⊢ HEq
    (F.map
      { down := { down := ⋯ : PLift ({ as := i : Discrete (Fin n) }.as = { as := i : Discrete (Fin n) }.as) } :
        ULift.{0, 0} (PLift ({ as := i : Discrete (Fin n) }.as = { as := i : Discrete (Fin n) }.as)) })
    (β :=
    Functor.obj.{0, v, 0, u} (Discrete.functor f) { as := i : Discrete (Fin n) } ⟶
      Functor.obj.{0, v, 0, u} (Discrete.functor f) { as := i : Discrete (Fin n) })
    (Functor.map (Discrete.functor f) { down := { down := ⋯ } })

Tactic:
simp [f]
-- Module: Mathlib.CategoryTheory.Extensive
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
⊢ F = Discrete.functor f

Tactic:
have : F = Discrete.functor f :=
    Functor.hext (fun _ ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])
-- Module: Mathlib.CategoryTheory.Extensive
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
clear_value : ∀ (f : Fin n → C) (this : F = Discrete.functor f), IsUniversalColimit c
⊢ IsUniversalColimit c

Tactic:
clear_value f
-- Module: Mathlib.CategoryTheory.Extensive
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
subst : ∀ {c : Cocone.{0, v, 0, u} (Discrete.functor f)} (hc : IsColimit c), IsUniversalColimit c
⊢ IsUniversalColimit c

Tactic:
subst this
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : FinitaryPreExtensive.{v, u} C
f : Fin 0 → C
c : Cocone.{0, v, 0, u} (Discrete.functor f)
hc : IsColimit c
⊢ IsUniversalColimit c

Tactic:
exact (isVanKampenColimit_of_isEmpty _ hc).isUniversal

Premises used: CategoryTheory.isVanKampenColimit_of_isEmpty, CategoryTheory.IsVanKampenColimit.isUniversal
-- Module: Mathlib.CategoryTheory.Extensive
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

Tactic:
IsUniversalColimit.of_iso (@isUniversalColimit_extendCofan _ _ _ _ _ _
      (IH _ (coproductIsCoproduct _)) (FinitaryPreExtensive.universal' _ (coprodIsCoprod _ _)) ?_)
      ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.extendCofanIsColimit, CategoryTheory.IsUniversalColimit.of_iso, CategoryTheory.Limits.IsColimit.uniqueUpToIso, CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.FinitaryPreExtensive.universal', CategoryTheory.isUniversalColimit_extendCofan
-- Module: Mathlib.CategoryTheory.Extensive
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
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
⊢ IsUniversalColimit c

Tactic:
refine IsUniversalColimit.of_iso (@isUniversalColimit_extendCofan _ _ _ _ _ _
      (IH _ (coproductIsCoproduct _)) (FinitaryPreExtensive.universal' _ (coprodIsCoprod _ _)) ?_)
      ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.extendCofanIsColimit, CategoryTheory.IsUniversalColimit.of_iso, CategoryTheory.Limits.IsColimit.uniqueUpToIso, CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.FinitaryPreExtensive.universal', CategoryTheory.isUniversalColimit_extendCofan
-- Module: Mathlib.CategoryTheory.Extensive
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
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
⊢ ∀ {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:
dsimp
-- Module: Mathlib.CategoryTheory.Extensive
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 ⟶ coprod.{v, u} (f 0) (sigmaObj.{0, v, u} fun (i : Fin n) ↦ f i.succ)), HasPullback coprod.inr i

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Extensive
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
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
⊢ 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