Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: case refine_1
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 := 0 } =
    (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 := 0 }

pp: case refine_2
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)
⊢ ∀ (i : Fin n),
    (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 := i.castSucc } =
        (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 := i.castSucc } →
      (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 := i.succ } =
        (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 := i.succ }

Tactic:
· apply (Category.id_comp _).symm

Goal state after:
case refine_2
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)
⊢ ∀ (i : Fin n),
    (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 := i.castSucc } =
        (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 := i.castSucc } →
      (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 := i.succ } =
        (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 := i.succ }