-- Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean
/-- If `F` preserves the initial object and binary coproducts, then it preserves products indexed by
`Fin n` for any `n`.
-/
lemma preserves_fin_of_preserves_binary_and_initial :
    ∀ (n : ℕ) (f : Fin n → C), PreservesColimit (Discrete.functor f) F
  | 0 => fun f => by
    letI : PreservesColimitsOfShape (Discrete (Fin 0)) F :=
      preservesColimitsOfShape_of_equiv.{0, 0} (Discrete.equivalence finZeroEquiv'.symm) _
    infer_instance
  | n + 1 => by
    haveI := preserves_fin_of_preserves_binary_and_initial n
    intro f
    apply
      preservesColimit_of_preserves_colimit_cocone
        (extendCofanIsColimit f (colimit.isColimit _) (colimit.isColimit _)) _
    apply (isColimitMapCoconeCofanMkEquiv _ _ _).symm _
    let this :=
      extendCofanIsColimit (fun i => F.obj (f i))
        (isColimitOfHasCoproductOfPreservesColimit F _)
        (isColimitOfHasBinaryCoproductOfPreservesColimit F _ _)
    refine IsColimit.ofIsoColimit this ?_
    apply Cocones.ext _ _
    · apply Iso.refl _
    rintro ⟨j⟩
    refine Fin.inductionOn j ?_ ?_
    · apply Category.comp_id
    · rintro i _
      dsimp [extendCofan_ι_app, Iso.refl_hom, Cofan.mk_ι_app]
      rw [comp_id, ← F.map_comp]

Proof state:
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))
⊢ 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)) ≅
    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)

Tactic:
apply Cocones.ext _ _

Result:
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))
⊢ (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 ≅
    (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)).pt

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 : Discrete (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
          j ≫
        Iso.hom ?m.42766 =
      (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
        j

Proof state:
case mk.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
a✝ :
  (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 }
⊢ (F.map (Sigma.ι (fun i => f i.succ) i) ≫ F.map coprod.inr) ≫ 𝟙 (F.obj (f 0 ⨿ ∐ fun i => f i.succ)) =
    F.map
      (colimit.ι (Discrete.functor fun i => f i.succ) { as := i } ≫
        colimit.ι (pair (f 0) (colimit (Discrete.functor fun i => f i.succ))) { as := WalkingPair.right })

Tactic:
rw [comp_id, ← F.map_comp]

Result:
no goals