Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: case mpr.refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X.obj
h : Triangle.mk f.hom a b ∈ Pretriangulated.distinguishedTriangles
hZ : (A ⊓ B) Z
⊢ (A.ι.mapTriangle.obj (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).mor₁ ≫
      (Iso.refl
          (A.ι.mapTriangle.obj
              (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₂).hom =
    (Iso.refl
          (A.ι.mapTriangle.obj
              (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₁).hom ≫
      (Triangle.mk f.hom a b).mor₁

pp: case mpr.refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X.obj
h : Triangle.mk f.hom a b ∈ Pretriangulated.distinguishedTriangles
hZ : (A ⊓ B) Z
⊢ (A.ι.mapTriangle.obj (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).mor₂ ≫
      (Iso.refl
          (A.ι.mapTriangle.obj
              (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₃).hom =
    (Iso.refl
          (A.ι.mapTriangle.obj
              (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₂).hom ≫
      (Triangle.mk f.hom a b).mor₂

pp: case mpr.refine_3
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X.obj
h : Triangle.mk f.hom a b ∈ Pretriangulated.distinguishedTriangles
hZ : (A ⊓ B) Z
⊢ (A.ι.mapTriangle.obj (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).mor₃ ≫
      (shiftFunctor C 1).map
        (Iso.refl
            (A.ι.mapTriangle.obj
                (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₁).hom =
    (Iso.refl
          (A.ι.mapTriangle.obj
              (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₃).hom ≫
      (Triangle.mk f.hom a b).mor₃

Tactic:
· cat_disch

Goal state after:
case mpr.refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X.obj
h : Triangle.mk f.hom a b ∈ Pretriangulated.distinguishedTriangles
hZ : (A ⊓ B) Z
⊢ (A.ι.mapTriangle.obj (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).mor₂ ≫
      (Iso.refl
          (A.ι.mapTriangle.obj
              (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₃).hom =
    (Iso.refl
          (A.ι.mapTriangle.obj
              (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₂).hom ≫
      (Triangle.mk f.hom a b).mor₂

case mpr.refine_3
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X.obj
h : Triangle.mk f.hom a b ∈ Pretriangulated.distinguishedTriangles
hZ : (A ⊓ B) Z
⊢ (A.ι.mapTriangle.obj (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).mor₃ ≫
      (shiftFunctor C 1).map
        (Iso.refl
            (A.ι.mapTriangle.obj
                (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₁).hom =
    (Iso.refl
          (A.ι.mapTriangle.obj
              (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₃).hom ≫
      (Triangle.mk f.hom a b).mor₃