Module: Mathlib.Algebra.Homology.ShortComplex.Retract

Goal state before:
pp: case h₁
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
⊢ Arrow.Hom.left
      (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.i;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.i;
            this))
          ⋯ ≫
        Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.r;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.r;
            this))
          ⋯) =
    Arrow.Hom.left (𝟙 (Arrow.mk (homologyMap f₁)))

pp: case h₂
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
⊢ Arrow.Hom.right
      (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.i;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.i;
            this))
          ⋯ ≫
        Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.r;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.r;
            this))
          ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk (homologyMap f₁)))

Tactic:
<;>

Goal state after:
case h₁
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
⊢ Arrow.Hom.left
      (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.i;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.i;
            this))
          ⋯ ≫
        Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.r;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.r;
            this))
          ⋯) =
    Arrow.Hom.left (𝟙 (Arrow.mk (homologyMap f₁)))

case h₂
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
⊢ Arrow.Hom.right
      (Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.i;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.i;
            this))
          ⋯ ≫
        Arrow.homMk
          (homologyMap
            (have this := Arrow.Hom.left h.r;
            this))
          (homologyMap
            (have this := Arrow.Hom.right h.r;
            this))
          ⋯) =
    Arrow.Hom.right (𝟙 (Arrow.mk (homologyMap f₁)))