Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i ↦ F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i ↦ f i.succ)
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i ↦ f i.succ))
j : Fin (n + 1)
⊢ (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι.app
        { as := j } ≫
      (Iso.refl
          (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt).hom =
    (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)).pt) fun j ↦
            F.map
              (Fin.cases
                (BinaryCofan.inl (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
                (fun i ↦
                  (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).ι.app { as := i } ≫
                    BinaryCofan.inr
                      (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
                j)).ι.app
      { as := j }

Tactic:
refine Fin.inductionOn j ?_ ?_

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i ↦ F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i ↦ f i.succ)
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i ↦ f i.succ))
j : Fin (n + 1)
⊢ (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι.app
        { as := 0 } ≫
      (Iso.refl
          (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
              (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt).hom =
    (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)).pt) fun j ↦
            F.map
              (Fin.cases
                (BinaryCofan.inl (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
                (fun i ↦
                  (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).ι.app { as := i } ≫
                    BinaryCofan.inr
                      (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
                j)).ι.app
      { as := 0 }

case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
n : ℕ
this✝ : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i ↦ F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i ↦ f i.succ)
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i ↦ f i.succ))
j : Fin (n + 1)
⊢ ∀ (i : Fin n),
    (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
                  (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι.app
            { as := i.castSucc } ≫
          (Iso.refl
              (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
                  (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt).hom =
        (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)).pt)
                fun j ↦
                F.map
                  (Fin.cases
                    (BinaryCofan.inl
                      (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
                    (fun i ↦
                      (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).ι.app { as := i } ≫
                        BinaryCofan.inr
                          (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
                    j)).ι.app
          { as := i.castSucc } →
      (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
                  (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).ι.app
            { as := i.succ } ≫
          (Iso.refl
              (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
                  (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))).pt).hom =
        (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)).pt)
                fun j ↦
                F.map
                  (Fin.cases
                    (BinaryCofan.inl
                      (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
                    (fun i ↦
                      (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).ι.app { as := i } ≫
                        BinaryCofan.inr
                          (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
                    j)).ι.app
          { as := i.succ }