-- Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean
/-- If `F` preserves the terminal object and binary products, then it preserves products indexed by
`Fin n` for any `n`.
-/
lemma preservesFinOfPreservesBinaryAndTerminal :
    ∀ (n : ℕ) (f : Fin n → C), PreservesLimit (Discrete.functor f) F
  | 0 => fun f => by
    letI : PreservesLimitsOfShape (Discrete (Fin 0)) F :=
      preservesLimitsOfShape_of_equiv.{0, 0} (Discrete.equivalence finZeroEquiv'.symm) _
    infer_instance
  | n + 1 => by
    haveI := preservesFinOfPreservesBinaryAndTerminal n
    intro f
    apply
      preservesLimit_of_preserves_limit_cone
        (extendFanIsLimit f (limit.isLimit _) (limit.isLimit _)) _
    apply (isLimitMapConeFanMkEquiv _ _ _).symm _
    let this :=
      extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F _)
        (isLimitOfHasBinaryProductOfPreservesLimit F _ _)
    refine IsLimit.ofIsoLimit this ?_
    apply Cones.ext _ _
    · apply Iso.refl _
    rintro ⟨j⟩
    refine Fin.inductionOn j ?_ ?_
    · apply (Category.id_comp _).symm
    · rintro i _
      dsimp [extendFan_π_app, Iso.refl_hom, Fan.mk_π_app]
      change F.map _ ≫ _ = 𝟙 _ ≫ _
      simp only [id_comp, ← F.map_comp]
      rfl

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ᶜ fun i => f i.succ)) fun j => F.map (Pi.π (fun i => f i.succ) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f i.succ)
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ᶜ fun i => f i.succ))
⊢ IsLimit
    (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f i.succ)).pt)).pt) fun j =>
      F.map
        (Fin.cases (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f i.succ)).pt)))
          (fun i =>
            BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f i.succ)).pt)) ≫
              (limit.cone (Discrete.functor fun i => f i.succ)).π.app { as := i })
          j))

Tactic:
refine IsLimit.ofIsoLimit this ?_

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ᶜ fun i => f i.succ)) fun j => F.map (Pi.π (fun i => f i.succ) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f i.succ)
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ᶜ fun i => f i.succ))
⊢ extendFan (Fan.mk (F.obj (∏ᶜ fun i => f i.succ)) fun j => F.map (Pi.π (fun i => f i.succ) j))
      (BinaryFan.mk (F.map prod.fst) (F.map prod.snd)) ≅
    Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f i.succ)).pt)).pt) fun j =>
      F.map
        (Fin.cases (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f i.succ)).pt)))
          (fun i =>
            BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f i.succ)).pt)) ≫
              (limit.cone (Discrete.functor fun i => f i.succ)).π.app { as := i })
          j)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
f : Fin 0 → C
this : PreservesLimitsOfShape (Discrete (Fin 0)) F :=
  preservesLimitsOfShape_of_equiv (Discrete.equivalence finZeroEquiv'.symm) F
⊢ PreservesLimit (Discrete.functor f) F

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ᶜ fun i => f i.succ)) fun j => F.map (Pi.π (fun i => f i.succ) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f i.succ)
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ᶜ fun i => f i.succ))
⊢ ∀ (j : Discrete (Fin (n + 1))),
    (extendFan (Fan.mk (F.obj (∏ᶜ fun i => f i.succ)) fun j => F.map (Pi.π (fun i => f i.succ) j))
              (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π.app
        j =
      (Iso.refl
            (extendFan (Fan.mk (F.obj (∏ᶜ fun i => f i.succ)) fun j => F.map (Pi.π (fun i => f i.succ) j))
                (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
        (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f i.succ)).pt)).pt) fun j =>
                F.map
                  (Fin.cases
                    (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f i.succ)).pt)))
                    (fun i =>
                      BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f i.succ)).pt)) ≫
                        (limit.cone (Discrete.functor fun i => f i.succ)).π.app { as := i })
                    j)).π.app
          j

Tactic:
rintro ⟨j⟩

Result:
case mk
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
this✝ : ∀ (f : Fin n → C), PreservesLimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsLimit
  (extendFan (Fan.mk (F.obj (∏ᶜ fun i => f i.succ)) fun j => F.map (Pi.π (fun i => f i.succ) j))
    (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))) :=
  extendFanIsLimit (fun i => F.obj (f i)) (isLimitOfHasProductOfPreservesLimit F fun i => f i.succ)
    (isLimitOfHasBinaryProductOfPreservesLimit F (f 0) (∏ᶜ fun i => f i.succ))
j : Fin (n + 1)
⊢ (extendFan (Fan.mk (F.obj (∏ᶜ fun i => f i.succ)) fun j => F.map (Pi.π (fun i => f i.succ) j))
            (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).π.app
      { as := j } =
    (Iso.refl
          (extendFan (Fan.mk (F.obj (∏ᶜ fun i => f i.succ)) fun j => F.map (Pi.π (fun i => f i.succ) j))
              (BinaryFan.mk (F.map prod.fst) (F.map prod.snd))).pt).hom ≫
      (Fan.mk (F.obj (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f i.succ)).pt)).pt) fun j =>
              F.map
                (Fin.cases
                  (BinaryFan.fst (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f i.succ)).pt)))
                  (fun i =>
                    BinaryFan.snd (limit.cone (pair (f 0) (limit.cone (Discrete.functor fun i => f i.succ)).pt)) ≫
                      (limit.cone (Discrete.functor fun i => f i.succ)).π.app { as := i })
                  j)).π.app
        { as := j }