awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S₁.HasLeftHomology
inst_6 : S₂.HasLeftHomology
inst_7 : F.PreservesLeftHomologyOf S₁
inst_8 : F.PreservesLeftHomologyOf S₂
dsimp :
  Eq (α := leftHomology (Functor.obj F.mapShortComplex S₁) ⟶ F.obj S₂.leftHomology)
    (CategoryStruct.comp (Y := leftHomology (Functor.obj F.mapShortComplex S₂))
      (leftHomologyMap' (Functor.map F.mapShortComplex φ) (leftHomologyData (Functor.obj F.mapShortComplex S₁))
        (leftHomologyData (Functor.obj F.mapShortComplex S₂)))
      (leftHomologyMap' (𝟙 (S₂.map F)) (leftHomologyData (S₂.map F)) (S₂.leftHomologyData.map F)))
    (CategoryStruct.comp (Y := F.obj S₁.leftHomology)
      (leftHomologyMap' (𝟙 (S₁.map F)) (leftHomologyData (S₁.map F)) (S₁.leftHomologyData.map F) :
        LeftHomologyData.H (S := S₁.map F) (leftHomologyData (S₁.map F)) ⟶
          LeftHomologyData.H (S := S₁.map F) (S₁.leftHomologyData.map F))
      (F.map (leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData)))
⊢ Eq (α := leftHomology (Functor.obj F.mapShortComplex S₁) ⟶ F.obj S₂.leftHomology)
    (CategoryStruct.comp (Y := leftHomology (Functor.obj F.mapShortComplex S₂))
      (leftHomologyMap (Functor.map F.mapShortComplex φ) :
        leftHomology (Functor.obj F.mapShortComplex S₁) ⟶ leftHomology (Functor.obj F.mapShortComplex S₂))
      (Iso.hom (S₂.mapLeftHomologyIso F) : leftHomology (S₂.map F) ⟶ F.obj S₂.leftHomology))
    (CategoryStruct.comp (Y := F.obj S₁.leftHomology) (Iso.hom (S₁.mapLeftHomologyIso F)) (F.map (leftHomologyMap φ)))

Tactic:
dsimp only [leftHomologyMap, mapLeftHomologyIso, LeftHomologyData.leftHomologyIso,
    leftHomologyMapIso', Iso.refl]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap, CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso, CategoryTheory.ShortComplex.leftHomologyMapIso', CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.mapLeftHomologyIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S₁.HasLeftHomology
inst_6 : S₂.HasLeftHomology
inst_7 : F.PreservesLeftHomologyOf S₁
inst_8 : F.PreservesLeftHomologyOf S₂
⊢ Eq (α := leftHomology (Functor.obj F.mapShortComplex S₁) ⟶ F.obj S₂.leftHomology)
    (CategoryStruct.comp (Y := leftHomology (Functor.obj F.mapShortComplex S₂))
      (leftHomologyMap' (Functor.map F.mapShortComplex φ) (leftHomologyData (Functor.obj F.mapShortComplex S₁))
        (leftHomologyData (Functor.obj F.mapShortComplex S₂)))
      (leftHomologyMap' (𝟙 (S₂.map F)) (leftHomologyData (S₂.map F)) (S₂.leftHomologyData.map F)))
    (CategoryStruct.comp (Y := F.obj S₁.leftHomology)
      (leftHomologyMap' (𝟙 (S₁.map F)) (leftHomologyData (S₁.map F)) (S₁.leftHomologyData.map F) :
        LeftHomologyData.H (S := S₁.map F) (leftHomologyData (S₁.map F)) ⟶
          LeftHomologyData.H (S := S₁.map F) (S₁.leftHomologyData.map F))
      (F.map (leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData)))

Tactic:
simp only [LeftHomologyData.map_leftHomologyMap', Functor.mapShortComplex_obj,
    ← leftHomologyMap'_comp, comp_id, id_comp]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_comp, CategoryTheory.ShortComplex.LeftHomologyData.map_leftHomologyMap', CategoryTheory.Category.comp_id, CategoryTheory.Functor.mapShortComplex_obj, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S₁.HasRightHomology
inst_6 : S₂.HasRightHomology
inst_7 : F.PreservesRightHomologyOf S₁
inst_8 : F.PreservesRightHomologyOf S₂
dsimp :
  Eq (α := opcycles (Functor.obj F.mapShortComplex S₁) ⟶ F.obj S₂.opcycles)
    (CategoryStruct.comp (Y := opcycles (Functor.obj F.mapShortComplex S₂))
      (opcyclesMap' (Functor.map F.mapShortComplex φ) (rightHomologyData (Functor.obj F.mapShortComplex S₁))
        (rightHomologyData (Functor.obj F.mapShortComplex S₂)))
      (opcyclesMap' (𝟙 (S₂.map F)) (rightHomologyData (S₂.map F)) (S₂.rightHomologyData.map F)))
    (CategoryStruct.comp (Y := F.obj S₁.opcycles)
      (opcyclesMap' (𝟙 (S₁.map F)) (rightHomologyData (S₁.map F)) (S₁.rightHomologyData.map F) :
        RightHomologyData.Q (S := S₁.map F) (rightHomologyData (S₁.map F)) ⟶
          RightHomologyData.Q (S := S₁.map F) (S₁.rightHomologyData.map F))
      (F.map (opcyclesMap' φ S₁.rightHomologyData S₂.rightHomologyData)))
⊢ Eq (α := opcycles (Functor.obj F.mapShortComplex S₁) ⟶ F.obj S₂.opcycles)
    (CategoryStruct.comp (Y := opcycles (Functor.obj F.mapShortComplex S₂))
      (opcyclesMap (Functor.map F.mapShortComplex φ) :
        opcycles (Functor.obj F.mapShortComplex S₁) ⟶ opcycles (Functor.obj F.mapShortComplex S₂))
      (Iso.hom (S₂.mapOpcyclesIso F) : opcycles (S₂.map F) ⟶ F.obj S₂.opcycles))
    (CategoryStruct.comp (Y := F.obj S₁.opcycles) (Iso.hom (S₁.mapOpcyclesIso F)) (F.map (opcyclesMap φ)))

Tactic:
dsimp only [opcyclesMap, mapOpcyclesIso, RightHomologyData.opcyclesIso,
    opcyclesMapIso', Iso.refl]

Premises used: CategoryTheory.ShortComplex.mapOpcyclesIso, CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso, CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.opcyclesMapIso', CategoryTheory.ShortComplex.opcyclesMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S₁.HasRightHomology
inst_6 : S₂.HasRightHomology
inst_7 : F.PreservesRightHomologyOf S₁
inst_8 : F.PreservesRightHomologyOf S₂
⊢ Eq (α := opcycles (Functor.obj F.mapShortComplex S₁) ⟶ F.obj S₂.opcycles)
    (CategoryStruct.comp (Y := opcycles (Functor.obj F.mapShortComplex S₂))
      (opcyclesMap' (Functor.map F.mapShortComplex φ) (rightHomologyData (Functor.obj F.mapShortComplex S₁))
        (rightHomologyData (Functor.obj F.mapShortComplex S₂)))
      (opcyclesMap' (𝟙 (S₂.map F)) (rightHomologyData (S₂.map F)) (S₂.rightHomologyData.map F)))
    (CategoryStruct.comp (Y := F.obj S₁.opcycles)
      (opcyclesMap' (𝟙 (S₁.map F)) (rightHomologyData (S₁.map F)) (S₁.rightHomologyData.map F) :
        RightHomologyData.Q (S := S₁.map F) (rightHomologyData (S₁.map F)) ⟶
          RightHomologyData.Q (S := S₁.map F) (S₁.rightHomologyData.map F))
      (F.map (opcyclesMap' φ S₁.rightHomologyData S₂.rightHomologyData)))

Tactic:
simp only [RightHomologyData.map_opcyclesMap', Functor.mapShortComplex_obj, ← opcyclesMap'_comp,
    comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.mapShortComplex_obj, CategoryTheory.ShortComplex.RightHomologyData.map_opcyclesMap', CategoryTheory.ShortComplex.opcyclesMap'_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S₁.HasRightHomology
inst_6 : S₂.HasRightHomology
inst_7 : F.PreservesRightHomologyOf S₁
inst_8 : F.PreservesRightHomologyOf S₂
dsimp :
  Eq (α := rightHomology (Functor.obj F.mapShortComplex S₁) ⟶ F.obj S₂.rightHomology)
    (CategoryStruct.comp (Y := rightHomology (Functor.obj F.mapShortComplex S₂))
      (rightHomologyMap' (Functor.map F.mapShortComplex φ) (rightHomologyData (Functor.obj F.mapShortComplex S₁))
        (rightHomologyData (Functor.obj F.mapShortComplex S₂)))
      (rightHomologyMap' (𝟙 (S₂.map F)) (rightHomologyData (S₂.map F)) (S₂.rightHomologyData.map F)))
    (CategoryStruct.comp (Y := F.obj S₁.rightHomology)
      (rightHomologyMap' (𝟙 (S₁.map F)) (rightHomologyData (S₁.map F)) (S₁.rightHomologyData.map F) :
        RightHomologyData.H (S := S₁.map F) (rightHomologyData (S₁.map F)) ⟶
          RightHomologyData.H (S := S₁.map F) (S₁.rightHomologyData.map F))
      (F.map (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData)))
⊢ Eq (α := rightHomology (Functor.obj F.mapShortComplex S₁) ⟶ F.obj S₂.rightHomology)
    (CategoryStruct.comp (Y := rightHomology (Functor.obj F.mapShortComplex S₂))
      (rightHomologyMap (Functor.map F.mapShortComplex φ) :
        rightHomology (Functor.obj F.mapShortComplex S₁) ⟶ rightHomology (Functor.obj F.mapShortComplex S₂))
      (Iso.hom (S₂.mapRightHomologyIso F) : rightHomology (S₂.map F) ⟶ F.obj S₂.rightHomology))
    (CategoryStruct.comp (Y := F.obj S₁.rightHomology) (Iso.hom (S₁.mapRightHomologyIso F))
      (F.map (rightHomologyMap φ)))

Tactic:
dsimp only [rightHomologyMap, mapRightHomologyIso, RightHomologyData.rightHomologyIso,
    rightHomologyMapIso', Iso.refl]

Premises used: CategoryTheory.ShortComplex.rightHomologyMapIso', CategoryTheory.ShortComplex.rightHomologyMap, CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso, CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.mapRightHomologyIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S₁.HasRightHomology
inst_6 : S₂.HasRightHomology
inst_7 : F.PreservesRightHomologyOf S₁
inst_8 : F.PreservesRightHomologyOf S₂
⊢ Eq (α := rightHomology (Functor.obj F.mapShortComplex S₁) ⟶ F.obj S₂.rightHomology)
    (CategoryStruct.comp (Y := rightHomology (Functor.obj F.mapShortComplex S₂))
      (rightHomologyMap' (Functor.map F.mapShortComplex φ) (rightHomologyData (Functor.obj F.mapShortComplex S₁))
        (rightHomologyData (Functor.obj F.mapShortComplex S₂)))
      (rightHomologyMap' (𝟙 (S₂.map F)) (rightHomologyData (S₂.map F)) (S₂.rightHomologyData.map F)))
    (CategoryStruct.comp (Y := F.obj S₁.rightHomology)
      (rightHomologyMap' (𝟙 (S₁.map F)) (rightHomologyData (S₁.map F)) (S₁.rightHomologyData.map F) :
        RightHomologyData.H (S := S₁.map F) (rightHomologyData (S₁.map F)) ⟶
          RightHomologyData.H (S := S₁.map F) (S₁.rightHomologyData.map F))
      (F.map (rightHomologyMap' φ S₁.rightHomologyData S₂.rightHomologyData)))

Tactic:
simp only [RightHomologyData.map_rightHomologyMap', Functor.mapShortComplex_obj,
    ← rightHomologyMap'_comp, comp_id, id_comp]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.map_rightHomologyMap', CategoryTheory.Category.comp_id, CategoryTheory.Functor.mapShortComplex_obj, CategoryTheory.ShortComplex.rightHomologyMap'_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S₁.HasHomology
inst_6 : S₂.HasHomology
inst_7 : HasHomology (S₁.map F)
inst_8 : HasHomology (S₂.map F)
inst_9 : F.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
dsimp :
  Eq (α := homology (S₁.map F) ⟶ F.obj S₂.homology)
    (CategoryStruct.comp (Y := homology (S₂.map F))
        (leftHomologyMap' (Functor.map F.mapShortComplex φ) (HomologyData.left (homologyData (S₁.map F)))
          (HomologyData.left (homologyData (S₂.map F))))
        (CategoryStruct.comp (Y := leftHomology (S₂.map F))
          (leftHomologyMap' (𝟙 (S₂.map F)) (HomologyData.left (homologyData (S₂.map F))) (leftHomologyData (S₂.map F)))
          (leftHomologyMap' (𝟙 (S₂.map F)) (leftHomologyData (S₂.map F)) (S₂.homologyData.left.map F))) :
      homology (S₁.map F) ⟶ F.obj S₂.homology)
    (CategoryStruct.comp (Y := F.obj S₁.homology)
        (CategoryStruct.comp (Y := leftHomology (S₁.map F))
            (leftHomologyMap' (𝟙 (S₁.map F)) (HomologyData.left (homologyData (S₁.map F)))
              (leftHomologyData (S₁.map F)))
            (leftHomologyMap' (𝟙 (S₁.map F)) (leftHomologyData (S₁.map F)) (S₁.homologyData.left.map F)) :
          homology (S₁.map F) ⟶ LeftHomologyData.H (S := S₁.map F) (S₁.homologyData.left.map F))
        (F.map (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left)) :
      homology (S₁.map F) ⟶ F.obj S₂.homology)
⊢ Eq (α := homology (S₁.map F) ⟶ F.obj S₂.homology)
    (CategoryStruct.comp (Y := homology (S₂.map F)) (homologyMap (Functor.map F.mapShortComplex φ))
        (Iso.hom (S₂.mapHomologyIso F)) :
      homology (S₁.map F) ⟶ F.obj S₂.homology)
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F)) (F.map (homologyMap φ)) :
      homology (S₁.map F) ⟶ F.obj S₂.homology)

Tactic:
dsimp only [homologyMap, homologyMap', mapHomologyIso, LeftHomologyData.homologyIso,
    LeftHomologyData.leftHomologyIso, leftHomologyMapIso', leftHomologyIso,
    Iso.symm, Iso.trans, Iso.refl]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso, CategoryTheory.ShortComplex.leftHomologyMapIso', CategoryTheory.ShortComplex.mapHomologyIso, CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.LeftHomologyData.homologyIso, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.ShortComplex.leftHomologyIso, CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S₁.HasHomology
inst_6 : S₂.HasHomology
inst_7 : HasHomology (S₁.map F)
inst_8 : HasHomology (S₂.map F)
inst_9 : F.PreservesLeftHomologyOf S₁
inst_10 : F.PreservesLeftHomologyOf S₂
⊢ Eq (α := homology (S₁.map F) ⟶ F.obj S₂.homology)
    (CategoryStruct.comp (Y := homology (S₂.map F))
        (leftHomologyMap' (Functor.map F.mapShortComplex φ) (HomologyData.left (homologyData (S₁.map F)))
          (HomologyData.left (homologyData (S₂.map F))))
        (CategoryStruct.comp (Y := leftHomology (S₂.map F))
          (leftHomologyMap' (𝟙 (S₂.map F)) (HomologyData.left (homologyData (S₂.map F))) (leftHomologyData (S₂.map F)))
          (leftHomologyMap' (𝟙 (S₂.map F)) (leftHomologyData (S₂.map F)) (S₂.homologyData.left.map F))) :
      homology (S₁.map F) ⟶ F.obj S₂.homology)
    (CategoryStruct.comp (Y := F.obj S₁.homology)
        (CategoryStruct.comp (Y := leftHomology (S₁.map F))
            (leftHomologyMap' (𝟙 (S₁.map F)) (HomologyData.left (homologyData (S₁.map F)))
              (leftHomologyData (S₁.map F)))
            (leftHomologyMap' (𝟙 (S₁.map F)) (leftHomologyData (S₁.map F)) (S₁.homologyData.left.map F)) :
          homology (S₁.map F) ⟶ LeftHomologyData.H (S := S₁.map F) (S₁.homologyData.left.map F))
        (F.map (leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left)) :
      homology (S₁.map F) ⟶ F.obj S₂.homology)

Tactic:
simp only [LeftHomologyData.map_leftHomologyMap', ← leftHomologyMap'_comp, comp_id, id_comp]

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_comp, CategoryTheory.ShortComplex.LeftHomologyData.map_leftHomologyMap', CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S₁.HasHomology
inst_6 : S₂.HasHomology
inst_7 : HasHomology (S₁.map F)
inst_8 : HasHomology (S₂.map F)
inst_9 : F.PreservesRightHomologyOf S₁
inst_10 : F.PreservesRightHomologyOf S₂
dsimp :
  Eq (α := homology (S₁.map F) ⟶ F.obj S₂.homology)
    (CategoryStruct.comp (Y := homology (S₂.map F)) (homologyMap (Functor.map F.mapShortComplex φ))
        (CategoryStruct.comp (Y := RightHomologyData.H (S := S₂.map F) (S₂.homologyData.right.map F))
          (Iso.hom (RightHomologyData.homologyIso (S₂.homologyData.right.map F)))
          (F.map (Iso.inv S₂.homologyData.right.homologyIso))) :
      homology (S₁.map F) ⟶ F.obj S₂.homology)
    (CategoryStruct.comp (Y := F.obj S₁.homology)
        (CategoryStruct.comp (Y := RightHomologyData.H (S := S₁.map F) (S₁.homologyData.right.map F))
          (Iso.hom (RightHomologyData.homologyIso (S₁.homologyData.right.map F)))
          (F.map (Iso.inv S₁.homologyData.right.homologyIso)))
        (F.map (homologyMap φ)) :
      homology (S₁.map F) ⟶ F.obj S₂.homology)
⊢ Eq (α := homology (S₁.map F) ⟶ F.obj S₂.homology)
    (CategoryStruct.comp (Y := homology (S₂.map F)) (homologyMap (Functor.map F.mapShortComplex φ))
        (Iso.hom (S₂.mapHomologyIso' F)) :
      homology (S₁.map F) ⟶ F.obj S₂.homology)
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F)) (F.map (homologyMap φ)) :
      homology (S₁.map F) ⟶ F.obj S₂.homology)

Tactic:
dsimp only [Iso.trans, Iso.symm, Functor.mapIso, mapHomologyIso']

Premises used: CategoryTheory.Iso.trans, CategoryTheory.ShortComplex.mapHomologyIso', CategoryTheory.Iso.symm, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S₁.HasHomology
inst_6 : S₂.HasHomology
inst_7 : HasHomology (S₁.map F)
inst_8 : HasHomology (S₂.map F)
inst_9 : F.PreservesRightHomologyOf S₁
inst_10 : F.PreservesRightHomologyOf S₂
⊢ Eq (α := homology (S₁.map F) ⟶ F.obj S₂.homology)
    (CategoryStruct.comp (Y := homology (S₂.map F)) (homologyMap (Functor.map F.mapShortComplex φ))
        (CategoryStruct.comp (Y := RightHomologyData.H (S := S₂.map F) (S₂.homologyData.right.map F))
          (Iso.hom (RightHomologyData.homologyIso (S₂.homologyData.right.map F)))
          (F.map (Iso.inv S₂.homologyData.right.homologyIso))) :
      homology (S₁.map F) ⟶ F.obj S₂.homology)
    (CategoryStruct.comp (Y := F.obj S₁.homology)
        (CategoryStruct.comp (Y := RightHomologyData.H (S := S₁.map F) (S₁.homologyData.right.map F))
          (Iso.hom (RightHomologyData.homologyIso (S₁.homologyData.right.map F)))
          (F.map (Iso.inv S₁.homologyData.right.homologyIso)))
        (F.map (homologyMap φ)) :
      homology (S₁.map F) ⟶ F.obj S₂.homology)

Tactic:
simp only [← RightHomologyData.rightHomologyIso_hom_naturality_assoc _
    ((homologyData S₁).right.map F) ((homologyData S₂).right.map F), assoc,
    ← RightHomologyData.map_rightHomologyMap', ← F.map_comp,
    RightHomologyData.rightHomologyIso_inv_naturality _
      (homologyData S₁).right (homologyData S₂).right]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyData.map, CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_inv_naturality, CategoryTheory.ShortComplex.RightHomologyData.map_rightHomologyMap', CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_hom_naturality_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.ShortComplex.HomologyData.right, CategoryTheory.ShortComplex.homologyData
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasHomology
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
w : Eq (α := homology (S.map F) ⟶ F.obj S.homology) (Iso.hom (S.mapHomologyIso' F)) (Iso.hom (S.mapHomologyIso F))
⊢ Eq (α := homology (S.map F) ≅ F.obj S.homology) (S.mapHomologyIso' F) (S.mapHomologyIso F)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasHomology
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
w :
  Eq (α := homology (S.map F) ⟶ F.obj S.homology)
    (Iso.hom
      (Iso.trans (Y := RightHomologyData.H (S := S.map F) (S.homologyData.right.map F))
        (RightHomologyData.homologyIso (S.homologyData.right.map F))
        (F.mapIso (Iso.symm S.homologyData.right.homologyIso))))
    (Iso.hom
      (Iso.trans (Y := LeftHomologyData.H (S := S.map F) (S.homologyData.left.map F))
        (LeftHomologyData.homologyIso (S.homologyData.left.map F))
        (F.mapIso (Iso.symm S.homologyData.left.homologyIso))))
⊢ Eq (α := homology (S.map F) ⟶ F.obj S.homology) (Iso.hom (S.mapHomologyIso' F)) (Iso.hom (S.mapHomologyIso F))

Tactic:
rw [S.homologyData.left.mapHomologyIso_eq F, S.homologyData.right.mapHomologyIso'_eq F]

Premises used: CategoryTheory.ShortComplex.HomologyData.left, CategoryTheory.ShortComplex.LeftHomologyData.mapHomologyIso_eq, CategoryTheory.ShortComplex.HomologyData.right, CategoryTheory.ShortComplex.RightHomologyData.mapHomologyIso'_eq, CategoryTheory.ShortComplex.homologyData