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

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive 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
⊢ IsVanKampenColimit c

Tactic:
clear_value f

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

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsVanKampenColimit 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 mk.mk.up.up
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive 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:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsVanKampenColimit 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:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsVanKampenColimit 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✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit
    (extendCofan (Cofan.mk (∐ fun i => f i.succ) (Sigma.ι fun i => f i.succ)) (BinaryCofan.mk coprod.inl coprod.inr))

Tactic:
apply @isVanKampenColimit_extendCofan _ _ _ _ _ _ _ _ ?_

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit (Cofan.mk (∐ fun i => f i.succ) (Sigma.ι fun i => f i.succ))

C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit (BinaryCofan.mk coprod.inl coprod.inr)

C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsVanKampenColimit 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✝ : FinitaryExtensive 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✝ : FinitaryExtensive 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:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit (Cofan.mk (∐ fun i => f i.succ) (Sigma.ι fun i => f i.succ))

Tactic:
apply IH

Result:
case hc
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsColimit (Cofan.mk (∐ fun i => f i.succ) (Sigma.ι fun i => f i.succ))

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

Tactic:
subst this

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

Proof state:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsColimit (BinaryCofan.mk coprod.inl coprod.inr)

Tactic:
exact coprodIsCoprod _ _

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit (BinaryCofan.mk coprod.inl coprod.inr)

Tactic:
apply FinitaryExtensive.van_kampen'

Result:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsColimit (BinaryCofan.mk coprod.inl coprod.inr)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
f : Fin n → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit c

Tactic:
induction' n with n IH

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

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

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

Tactic:
exact isVanKampenColimit_of_isEmpty _ hc

Result:
no goals

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

Tactic:
apply IsVanKampenColimit.of_iso _
  ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : FinitaryExtensive C
n : ℕ
IH : ∀ (f : Fin n → C) {c : Cocone (Discrete.functor f)}, IsColimit c → IsVanKampenColimit c
f : Fin (n + 1) → C
c : Cocone (Discrete.functor f)
hc : IsColimit c
⊢ IsVanKampenColimit
    (extendCofan (Cofan.mk (∐ fun i => f i.succ) (Sigma.ι fun i => f i.succ)) (BinaryCofan.mk coprod.inl coprod.inr))