-- Mathlib/CategoryTheory/Sites/LeftExact.lean
theorem liftToPlusObjLimitObj_fac {K : Type max v u} [SmallCategory K] [FinCategory K]
    [HasLimitsOfShape K D] [PreservesLimitsOfShape K (forget D)]
    [ReflectsLimitsOfShape K (forget D)] (F : K ⥤ Cᵒᵖ ⥤ D) (X : C)
    (S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))) (k) :
    liftToPlusObjLimitObj.{w, v, u} F X S ≫ (J.plusMap (limit.π F k)).app (op X) = S.π.app k

Proof state:
C : Type u
inst✝¹⁰ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁹ : Category.{max v u, w} D
inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁶ : HasForget D
inst✝⁵ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
K : Type (max v u)
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
k : K
⊢ (limit.lift (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) S ≫
        (HasLimit.isoOfNatIso
              (NatIso.ofComponents (fun k => colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k)
                  ⋯).symm).hom ≫
          (colimitLimitIso (F ⋙ J.diagramFunctor D X)).inv ≫
            (HasColimit.isoOfNatIso
                ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso
                  (limit.isLimit (F ⋙ J.diagramFunctor D X)))).inv) ≫
      (J.plusMap (limit.π F k)).app (op X) =
    S.π.app k

Tactic:
rw [← (limit.isLimit (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))).fac S k,
  Category.assoc]

Result:
C : Type u
inst✝¹⁰ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁹ : Category.{max v u, w} D
inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁶ : HasForget D
inst✝⁵ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
K : Type (max v u)
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
k : K
⊢ limit.lift (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) S ≫
      ((HasLimit.isoOfNatIso
              (NatIso.ofComponents (fun k => colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k)
                  ⋯).symm).hom ≫
          (colimitLimitIso (F ⋙ J.diagramFunctor D X)).inv ≫
            (HasColimit.isoOfNatIso
                ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso
                  (limit.isLimit (F ⋙ J.diagramFunctor D X)))).inv) ≫
        (J.plusMap (limit.π F k)).app (op X) =
    (limit.isLimit (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))).lift S ≫
      (limit.cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))).π.app k

Proof state:
case e_a
C : Type u
inst✝¹⁰ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁹ : Category.{max v u, w} D
inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁶ : HasForget D
inst✝⁵ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
K : Type (max v u)
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
⊢ Multiequalizer.lift ((unop j).index (F.obj k)) (multiequalizer ((unop j).index (limit F)))
        (fun x => Multiequalizer.ι ((unop j).index (limit F)) x ≫ (limit.π F k).app (op x.Y)) ⋯ ≫
      colimit.ι (J.diagram (F.obj k) X) j =
    (((J.diagramFunctor D X).mapCone (limit.cone F)).π.app k).app j ≫
      (colimit.ι (F ⋙ J.diagramFunctor D X).flip j).app k ≫
        (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k).hom

Tactic:
congr 1

Result:
case e_a.e_a
C : Type u
inst✝¹⁰ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁹ : Category.{max v u, w} D
inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁶ : HasForget D
inst✝⁵ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
K : Type (max v u)
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
k : K
j : (J.Cover (unop (op X)))ᵒᵖ
⊢ colimit.ι (J.diagram (F.obj k) X) j =
    (colimit.ι (F ⋙ J.diagramFunctor D X).flip j).app k ≫
      (colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k).hom

Proof state:
C : Type u
inst✝¹⁰ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁹ : Category.{max v u, w} D
inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁶ : HasForget D
inst✝⁵ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
K : Type (max v u)
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
k : K
⊢ limit.lift (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) S ≫
      ((HasLimit.isoOfNatIso
              (NatIso.ofComponents (fun k => colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k)
                  ⋯).symm).hom ≫
          (colimitLimitIso (F ⋙ J.diagramFunctor D X)).inv ≫
            (HasColimit.isoOfNatIso
                ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso
                  (limit.isLimit (F ⋙ J.diagramFunctor D X)))).inv) ≫
        (J.plusMap (limit.π F k)).app (op X) =
    (limit.isLimit (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))).lift S ≫
      (limit.cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))).π.app k

Tactic:
congr 1

Result:
case e_a
C : Type u
inst✝¹⁰ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝⁹ : Category.{max v u, w} D
inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝⁶ : HasForget D
inst✝⁵ : ∀ (X : C), PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)
K : Type (max v u)
inst✝⁴ : SmallCategory K
inst✝³ : FinCategory K
inst✝² : HasLimitsOfShape K D
inst✝¹ : PreservesLimitsOfShape K (forget D)
inst✝ : ReflectsLimitsOfShape K (forget D)
F : K ⥤ Cᵒᵖ ⥤ D
X : C
S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))
k : K
⊢ ((HasLimit.isoOfNatIso
            (NatIso.ofComponents (fun k => colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k)
                ⋯).symm).hom ≫
        (colimitLimitIso (F ⋙ J.diagramFunctor D X)).inv ≫
          (HasColimit.isoOfNatIso
              ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso
                (limit.isLimit (F ⋙ J.diagramFunctor D X)))).inv) ≫
      (J.plusMap (limit.π F k)).app (op X) =
    (limit.cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))).π.app k