Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: case h₁
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((const J).obj
              { X₁ := limit (F ⋙ π₁), X₂ := limit (F ⋙ π₂), X₃ := limit (F ⋙ π₃), f := limMap (F.whiskerLeft π₁Toπ₂),
                g := limMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).map
          f ≫
        { τ₁ := limit.π (F ⋙ π₁) x✝, τ₂ := limit.π (F ⋙ π₂) x✝, τ₃ := limit.π (F ⋙ π₃) x✝, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₁ =
    ({ τ₁ := limit.π (F ⋙ π₁) x✝¹, τ₂ := limit.π (F ⋙ π₂) x✝¹, τ₃ := limit.π (F ⋙ π₃) x✝¹, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
        F.map f).τ₁

pp: case h₂
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((const J).obj
              { X₁ := limit (F ⋙ π₁), X₂ := limit (F ⋙ π₂), X₃ := limit (F ⋙ π₃), f := limMap (F.whiskerLeft π₁Toπ₂),
                g := limMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).map
          f ≫
        { τ₁ := limit.π (F ⋙ π₁) x✝, τ₂ := limit.π (F ⋙ π₂) x✝, τ₃ := limit.π (F ⋙ π₃) x✝, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₂ =
    ({ τ₁ := limit.π (F ⋙ π₁) x✝¹, τ₂ := limit.π (F ⋙ π₂) x✝¹, τ₃ := limit.π (F ⋙ π₃) x✝¹, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
        F.map f).τ₂

pp: case h₃
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((const J).obj
              { X₁ := limit (F ⋙ π₁), X₂ := limit (F ⋙ π₂), X₃ := limit (F ⋙ π₃), f := limMap (F.whiskerLeft π₁Toπ₂),
                g := limMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).map
          f ≫
        { τ₁ := limit.π (F ⋙ π₁) x✝, τ₂ := limit.π (F ⋙ π₂) x✝, τ₃ := limit.π (F ⋙ π₃) x✝, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₃ =
    ({ τ₁ := limit.π (F ⋙ π₁) x✝¹, τ₂ := limit.π (F ⋙ π₂) x✝¹, τ₃ := limit.π (F ⋙ π₃) x✝¹, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
        F.map f).τ₃

Tactic:
<;>

Goal state after:
case h₁
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((const J).obj
              { X₁ := limit (F ⋙ π₁), X₂ := limit (F ⋙ π₂), X₃ := limit (F ⋙ π₃), f := limMap (F.whiskerLeft π₁Toπ₂),
                g := limMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).map
          f ≫
        { τ₁ := limit.π (F ⋙ π₁) x✝, τ₂ := limit.π (F ⋙ π₂) x✝, τ₃ := limit.π (F ⋙ π₃) x✝, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₁ =
    ({ τ₁ := limit.π (F ⋙ π₁) x✝¹, τ₂ := limit.π (F ⋙ π₂) x✝¹, τ₃ := limit.π (F ⋙ π₃) x✝¹, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
        F.map f).τ₁

case h₂
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((const J).obj
              { X₁ := limit (F ⋙ π₁), X₂ := limit (F ⋙ π₂), X₃ := limit (F ⋙ π₃), f := limMap (F.whiskerLeft π₁Toπ₂),
                g := limMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).map
          f ≫
        { τ₁ := limit.π (F ⋙ π₁) x✝, τ₂ := limit.π (F ⋙ π₂) x✝, τ₃ := limit.π (F ⋙ π₃) x✝, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₂ =
    ({ τ₁ := limit.π (F ⋙ π₁) x✝¹, τ₂ := limit.π (F ⋙ π₂) x✝¹, τ₃ := limit.π (F ⋙ π₃) x✝¹, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
        F.map f).τ₂

case h₃
J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ (((const J).obj
              { X₁ := limit (F ⋙ π₁), X₂ := limit (F ⋙ π₂), X₃ := limit (F ⋙ π₃), f := limMap (F.whiskerLeft π₁Toπ₂),
                g := limMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).map
          f ≫
        { τ₁ := limit.π (F ⋙ π₁) x✝, τ₂ := limit.π (F ⋙ π₂) x✝, τ₃ := limit.π (F ⋙ π₃) x✝, comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₃ =
    ({ τ₁ := limit.π (F ⋙ π₁) x✝¹, τ₂ := limit.π (F ⋙ π₂) x✝¹, τ₃ := limit.π (F ⋙ π₃) x✝¹, comm₁₂ := ⋯, comm₂₃ := ⋯ } ≫
        F.map f).τ₃