-- Mathlib/CategoryTheory/Extensive.lean
theorem FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin [FinitaryPreExtensive C] {n : ℕ}
    {F : Discrete (Fin n) ⥤ C} {c : Cocone F} (hc : IsColimit c) : IsUniversalColimit c

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
F : Discrete (Fin n) ⥤ C
c : Cocone F
hc : IsColimit c
f : Fin n → C
this : F = Discrete.functor f
⊢ IsUniversalColimit c

Tactic:
subst this

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
f : Fin n → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsUniversalColimit c

Proof state:
case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsUniversalColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ ∀ {Z : C} (i : Z ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt),
    HasPullback (BinaryCofan.mk coprod.inl coprod.inr).inr i

Tactic:
dsimp

Result:
case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsUniversalColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ ∀ {Z : C} (i : Z ⟶ f 0 ⨿ ∐ fun i => f i.succ), HasPullback coprod.inr i

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
F : 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

Tactic:
clear_value f

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
F : Discrete (Fin n) ⥤ C
c : Cocone F
hc : IsColimit c
f : Fin n → C
this : F = Discrete.functor f
⊢ IsUniversalColimit c

Proof state:
case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsUniversalColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ ∀ {Z : C} (i : Z ⟶ f 0 ⨿ ∐ fun i => f i.succ), HasPullback coprod.inr i

Tactic:
infer_instance

Result:
no goals

Proof state:
case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsUniversalColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsUniversalColimit c

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

Result:
case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsUniversalColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ ∀ {Z : C} (i : Z ⟶ (BinaryCofan.mk coprod.inl coprod.inr).pt),
    HasPullback (BinaryCofan.mk coprod.inl coprod.inr).inr i

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
F : Discrete (Fin n) ⥤ C
c : Cocone F
hc : IsColimit c
f : Fin n → C := F.obj ∘ Discrete.mk
⊢ IsUniversalColimit c

Tactic:
have : F = Discrete.functor f :=
  Functor.hext (fun _ ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp [f])

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
F : 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

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
F : Discrete (Fin n) ⥤ C
c : Cocone F
hc : IsColimit c
f : Fin n → C := F.obj ∘ Discrete.mk
⊢ ∀ (X Y : Discrete (Fin n)) (f_1 : X ⟶ Y), HEq (F.map f_1) ((Discrete.functor f).map f_1)

Tactic:
rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩

Result:
case mk.mk.up.up
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
F : 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 := ⋯ } }) ((Discrete.functor f).map { down := { down := ⋯ } })

Proof state:
case mk.mk.up.up
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
F : 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 := ⋯ } }) ((Discrete.functor f).map { down := { down := ⋯ } })

Tactic:
simp [f]

Result:
no goals

Proof state:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
f : Fin 0 → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsUniversalColimit c

Tactic:
exact (isVanKampenColimit_of_isEmpty _ hc).isUniversal

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
F : Discrete (Fin n) ⥤ C
c : Cocone F
hc : IsColimit c
⊢ IsUniversalColimit c

Tactic:
let f : Fin n → C := F.obj ∘ Discrete.mk

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryPreExtensive C
n : ℕ
F : Discrete (Fin n) ⥤ C
c : Cocone F
hc : IsColimit c
f : Fin n → C := F.obj ∘ Discrete.mk
⊢ IsUniversalColimit c