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 : ShortComplex.{v_1, u_1} C
hl : S.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasLeftHomology
inst_6 : F.PreservesLeftHomologyOf S
⊢ Eq (α := cycles (S.map F) ⟶ F.obj S.leftHomology)
    (leftHomologyπ (S.map F) ≫ leftHomologyMap' (𝟙 (S.map F)) (leftHomologyData (S.map F)) (S.leftHomologyData.map F) :
      cycles (S.map F) ⟶ F.obj S.leftHomology)
    (leftHomologyπ (S.map F) ≫
        CategoryStruct.comp (Y := F.obj hl.H)
          (leftHomologyMap' (𝟙 (S.map F)) (leftHomologyData (S.map F)) (hl.map F) :
            H (S := S.map F) (leftHomologyData (S.map F)) ⟶ H (S := S.map F) (hl.map F))
          (F.map (leftHomologyMap' (𝟙 S) hl S.leftHomologyData)) :
      cycles (S.map F) ⟶ F.obj S.leftHomology)

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

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_comp, CategoryTheory.ShortComplex.LeftHomologyData.map_leftHomologyMap', CategoryTheory.Category.comp_id, CategoryTheory.Functor.mapShortComplex_obj, CategoryTheory.Functor.map_id
-- 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
hr : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasRightHomology
inst_6 : F.PreservesRightHomologyOf S
w :
  Eq (α := X₂ (S.map F) ⟶ F.obj S.opcycles)
    (CategoryStruct.comp (Y := opcycles (S.map F)) (pOpcycles (S.map F) : X₂ (S.map F) ⟶ opcycles (S.map F))
      (Iso.hom (S.mapOpcyclesIso F) : opcycles (S.map F) ⟶ F.obj S.opcycles))
    (CategoryStruct.comp (Y := opcycles (S.map F)) (pOpcycles (S.map F))
      (Iso.hom
        (Iso.trans (Y := Q (S := S.map F) (hr.map F)) (opcyclesIso (hr.map F)) (F.mapIso (Iso.symm hr.opcyclesIso)))))
⊢ Eq (α := opcycles (S.map F) ≅ F.obj S.opcycles) (S.mapOpcyclesIso F : opcycles (S.map F) ≅ F.obj S.opcycles)
    (Iso.trans (Y := Q (S := S.map F) (hr.map F)) (opcyclesIso (hr.map F)) (F.mapIso (Iso.symm hr.opcyclesIso)) :
      opcycles (S.map F) ≅ F.obj S.opcycles)

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
hr : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasRightHomology
inst_6 : F.PreservesRightHomologyOf S
w :
  Eq (α := F.obj S.X₂ ⟶ F.obj S.opcycles)
    (CategoryStruct.comp (Y := opcycles (S.map F)) (pOpcycles (S.map F))
        (opcyclesMap' (𝟙 (S.map F)) (rightHomologyData (S.map F)) (S.rightHomologyData.map F)) :
      F.obj S.X₂ ⟶ F.obj S.opcycles)
    (CategoryStruct.comp (Y := opcycles (S.map F)) (pOpcycles (S.map F))
        (CategoryStruct.comp (Y := F.obj hr.Q)
          (opcyclesMap' (𝟙 (S.map F)) (rightHomologyData (S.map F)) (hr.map F) :
            Q (S := S.map F) (rightHomologyData (S.map F)) ⟶ Q (S := S.map F) (hr.map F))
          (F.map (opcyclesMap' (𝟙 S) hr S.rightHomologyData))) :
      F.obj S.X₂ ⟶ F.obj S.opcycles)
⊢ Eq (α := X₂ (S.map F) ⟶ F.obj S.opcycles)
    (CategoryStruct.comp (Y := opcycles (S.map F)) (pOpcycles (S.map F) : X₂ (S.map F) ⟶ opcycles (S.map F))
      (Iso.hom (S.mapOpcyclesIso F) : opcycles (S.map F) ⟶ F.obj S.opcycles))
    (CategoryStruct.comp (Y := opcycles (S.map F)) (pOpcycles (S.map F))
      (Iso.hom
        (Iso.trans (Y := Q (S := S.map F) (hr.map F)) (opcyclesIso (hr.map F)) (F.mapIso (Iso.symm hr.opcyclesIso)))))

Tactic:
dsimp [mapOpcyclesIso, opcyclesIso]

Premises used: CategoryTheory.ShortComplex.mapOpcyclesIso, CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso
-- 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
hr : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasRightHomology
inst_6 : F.PreservesRightHomologyOf S
⊢ Eq (α := F.obj S.X₂ ⟶ F.obj S.opcycles)
    (CategoryStruct.comp (Y := opcycles (S.map F)) (pOpcycles (S.map F))
        (opcyclesMap' (𝟙 (S.map F)) (rightHomologyData (S.map F)) (S.rightHomologyData.map F)) :
      F.obj S.X₂ ⟶ F.obj S.opcycles)
    (CategoryStruct.comp (Y := opcycles (S.map F)) (pOpcycles (S.map F))
        (CategoryStruct.comp (Y := F.obj hr.Q)
          (opcyclesMap' (𝟙 (S.map F)) (rightHomologyData (S.map F)) (hr.map F) :
            Q (S := S.map F) (rightHomologyData (S.map F)) ⟶ Q (S := S.map F) (hr.map F))
          (F.map (opcyclesMap' (𝟙 S) hr S.rightHomologyData))) :
      F.obj S.X₂ ⟶ F.obj S.opcycles)

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

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.mapShortComplex_obj, CategoryTheory.Functor.map_id, CategoryTheory.ShortComplex.RightHomologyData.map_opcyclesMap', CategoryTheory.ShortComplex.opcyclesMap'_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 : ShortComplex.{v_1, u_1} C
hr : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasRightHomology
inst_6 : F.PreservesRightHomologyOf S
w :
  Eq (α := rightHomology (S.map F) ⟶ F.obj S.rightHomology)
    (Iso.hom (S.mapRightHomologyIso F) : rightHomology (S.map F) ⟶ F.obj S.rightHomology)
    (Iso.hom
        (Iso.trans (Y := H (S := S.map F) (hr.map F)) (rightHomologyIso (hr.map F))
          (F.mapIso (Iso.symm hr.rightHomologyIso))) :
      rightHomology (S.map F) ⟶ F.obj S.rightHomology)
⊢ Eq (α := rightHomology (S.map F) ≅ F.obj S.rightHomology)
    (S.mapRightHomologyIso F : rightHomology (S.map F) ≅ F.obj S.rightHomology)
    (Iso.trans (Y := H (S := S.map F) (hr.map F)) (rightHomologyIso (hr.map F))
        (F.mapIso (Iso.symm hr.rightHomologyIso)) :
      rightHomology (S.map F) ≅ F.obj S.rightHomology)

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
hr : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasRightHomology
inst_6 : F.PreservesRightHomologyOf S
w :
  Eq (α := rightHomology (S.map F) ⟶ F.obj S.rightHomology)
    (rightHomologyMap' (𝟙 (S.map F)) (rightHomologyData (S.map F)) (S.rightHomologyData.map F) :
      H (S := S.map F) (rightHomologyData (S.map F)) ⟶ H (S := S.map F) (S.rightHomologyData.map F))
    (CategoryStruct.comp (Y := F.obj hr.H)
      (rightHomologyMap' (𝟙 (S.map F)) (rightHomologyData (S.map F)) (hr.map F) :
        H (S := S.map F) (rightHomologyData (S.map F)) ⟶ H (S := S.map F) (hr.map F))
      (F.map (rightHomologyMap' (𝟙 S) hr S.rightHomologyData)))
⊢ Eq (α := rightHomology (S.map F) ⟶ F.obj S.rightHomology)
    (Iso.hom (S.mapRightHomologyIso F) : rightHomology (S.map F) ⟶ F.obj S.rightHomology)
    (Iso.hom
        (Iso.trans (Y := H (S := S.map F) (hr.map F)) (rightHomologyIso (hr.map F))
          (F.mapIso (Iso.symm hr.rightHomologyIso))) :
      rightHomology (S.map F) ⟶ F.obj S.rightHomology)

Tactic:
dsimp [mapRightHomologyIso, rightHomologyIso]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso, 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 : ShortComplex.{v_1, u_1} C
hr : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasRightHomology
inst_6 : F.PreservesRightHomologyOf S
⊢ Eq (α := rightHomology (S.map F) ⟶ F.obj S.rightHomology)
    (rightHomologyMap' (𝟙 (S.map F)) (rightHomologyData (S.map F)) (S.rightHomologyData.map F) :
      H (S := S.map F) (rightHomologyData (S.map F)) ⟶ H (S := S.map F) (S.rightHomologyData.map F))
    (CategoryStruct.comp (Y := F.obj hr.H)
      (rightHomologyMap' (𝟙 (S.map F)) (rightHomologyData (S.map F)) (hr.map F) :
        H (S := S.map F) (rightHomologyData (S.map F)) ⟶ H (S := S.map F) (hr.map F))
      (F.map (rightHomologyMap' (𝟙 S) hr S.rightHomologyData)))

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

Premises used: CategoryTheory.ShortComplex.RightHomologyData.map_rightHomologyMap', CategoryTheory.Category.comp_id, CategoryTheory.Functor.mapShortComplex_obj, CategoryTheory.ShortComplex.rightHomologyMap'_comp, CategoryTheory.Functor.map_id
-- 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
hl : S.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasHomology
inst_6 : HasHomology (S.map F)
inst_7 : F.PreservesLeftHomologyOf S
w :
  Eq (α := homology (S.map F) ⟶ F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
    (Iso.hom
      (Iso.trans (Y := H (S := S.map F) (hl.map F)) (homologyIso (hl.map F)) (F.mapIso (Iso.symm hl.homologyIso))))
⊢ Eq (α := homology (S.map F) ≅ F.obj S.homology) (S.mapHomologyIso F)
    (Iso.trans (Y := H (S := S.map F) (hl.map F)) (homologyIso (hl.map F)) (F.mapIso (Iso.symm hl.homologyIso)))

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
hl : S.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasHomology
inst_6 : HasHomology (S.map F)
inst_7 : F.PreservesLeftHomologyOf S
w :
  Eq (α := homology (S.map F) ⟶ 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) ⟶ H (S := S.map F) (S.homologyData.left.map F))
    (CategoryStruct.comp (Y := H (S := S.map F) (hl.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)) (hl.map F)))
      (F.map
        (CategoryStruct.comp (Y := S.leftHomology) (leftHomologyMap' (𝟙 S) hl S.leftHomologyData)
          (leftHomologyMap' (𝟙 S) S.leftHomologyData S.homologyData.left))))
⊢ Eq (α := homology (S.map F) ⟶ F.obj S.homology) (Iso.hom (S.mapHomologyIso F))
    (Iso.hom
      (Iso.trans (Y := H (S := S.map F) (hl.map F)) (homologyIso (hl.map F)) (F.mapIso (Iso.symm hl.homologyIso))))

Tactic:
dsimp only [mapHomologyIso, homologyIso, ShortComplex.leftHomologyIso,
    leftHomologyMapIso', leftHomologyIso, Functor.mapIso,
    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.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.ShortComplex.leftHomologyIso, 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 : ShortComplex.{v_1, u_1} C
hl : S.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasHomology
inst_6 : HasHomology (S.map F)
inst_7 : F.PreservesLeftHomologyOf S
⊢ Eq (α := homology (S.map F) ⟶ 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) ⟶ H (S := S.map F) (S.homologyData.left.map F))
    (CategoryStruct.comp (Y := H (S := S.map F) (hl.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)) (hl.map F)))
      (F.map
        (CategoryStruct.comp (Y := S.leftHomology) (leftHomologyMap' (𝟙 S) hl S.leftHomologyData)
          (leftHomologyMap' (𝟙 S) S.leftHomologyData S.homologyData.left))))

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

Premises used: CategoryTheory.ShortComplex.leftHomologyMap'_comp, CategoryTheory.ShortComplex.LeftHomologyData.map_leftHomologyMap', CategoryTheory.Category.comp_id, CategoryTheory.Functor.mapShortComplex_obj, CategoryTheory.Functor.map_id
-- 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
hr : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasHomology
inst_6 : HasHomology (S.map F)
inst_7 : F.PreservesRightHomologyOf S
w :
  Eq (α := homology (S.map F) ⟶ F.obj S.homology) (Iso.hom (S.mapHomologyIso' F))
    (Iso.hom
      (Iso.trans (Y := H (S := S.map F) (hr.map F)) (homologyIso (hr.map F)) (F.mapIso (Iso.symm hr.homologyIso))))
⊢ Eq (α := homology (S.map F) ≅ F.obj S.homology) (S.mapHomologyIso' F)
    (Iso.trans (Y := H (S := S.map F) (hr.map F)) (homologyIso (hr.map F)) (F.mapIso (Iso.symm hr.homologyIso)))

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
hr : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasHomology
inst_6 : HasHomology (S.map F)
inst_7 : F.PreservesRightHomologyOf S
w :
  Eq (α := homology (S.map F) ⟶ F.obj S.homology)
    (CategoryStruct.comp (Y := H (S := S.map F) (S.homologyData.right.map F))
      (CategoryStruct.comp (Y := rightHomology (S.map F))
        (Iso.hom (HomologyData.iso (homologyData (S.map F))) ≫
          rightHomologyMap' (𝟙 (S.map F)) (HomologyData.right (homologyData (S.map F))) (rightHomologyData (S.map F)))
        (rightHomologyMap' (𝟙 (S.map F)) (rightHomologyData (S.map F)) (S.homologyData.right.map F)))
      (F.map
        (CategoryStruct.comp (Y := S.rightHomology) (rightHomologyMap' (𝟙 S) S.homologyData.right S.rightHomologyData)
          (rightHomologyMap' (𝟙 S) S.rightHomologyData S.homologyData.right ≫ S.homologyData.iso.inv))))
    (CategoryStruct.comp (Y := rightHomology (S.map F))
        (Iso.hom (HomologyData.iso (homologyData (S.map F))) ≫
          rightHomologyMap' (𝟙 (S.map F)) (HomologyData.right (homologyData (S.map F))) (rightHomologyData (S.map F)))
        (rightHomologyMap' (𝟙 (S.map F)) (rightHomologyData (S.map F)) (hr.map F)) ≫
      F.map
        (CategoryStruct.comp (Y := S.rightHomology) (rightHomologyMap' (𝟙 S) hr S.rightHomologyData)
          (rightHomologyMap' (𝟙 S) S.rightHomologyData S.homologyData.right ≫ S.homologyData.iso.inv)))
⊢ Eq (α := homology (S.map F) ⟶ F.obj S.homology) (Iso.hom (S.mapHomologyIso' F))
    (Iso.hom
      (Iso.trans (Y := H (S := S.map F) (hr.map F)) (homologyIso (hr.map F)) (F.mapIso (Iso.symm hr.homologyIso))))

Tactic:
dsimp only [Iso.trans, Iso.symm, Iso.refl, Functor.mapIso, mapHomologyIso', homologyIso,
    rightHomologyIso, rightHomologyMapIso', ShortComplex.rightHomologyIso]

Premises used: CategoryTheory.ShortComplex.rightHomologyMapIso', CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso, CategoryTheory.ShortComplex.rightHomologyIso, CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.RightHomologyData.homologyIso, 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 : ShortComplex.{v_1, u_1} C
hr : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasHomology
inst_6 : HasHomology (S.map F)
inst_7 : F.PreservesRightHomologyOf S
⊢ Eq (α := homology (S.map F) ⟶ F.obj S.homology)
    (CategoryStruct.comp (Y := H (S := S.map F) (S.homologyData.right.map F))
      (CategoryStruct.comp (Y := rightHomology (S.map F))
        (Iso.hom (HomologyData.iso (homologyData (S.map F))) ≫
          rightHomologyMap' (𝟙 (S.map F)) (HomologyData.right (homologyData (S.map F))) (rightHomologyData (S.map F)))
        (rightHomologyMap' (𝟙 (S.map F)) (rightHomologyData (S.map F)) (S.homologyData.right.map F)))
      (F.map
        (CategoryStruct.comp (Y := S.rightHomology) (rightHomologyMap' (𝟙 S) S.homologyData.right S.rightHomologyData)
          (rightHomologyMap' (𝟙 S) S.rightHomologyData S.homologyData.right ≫ S.homologyData.iso.inv))))
    (CategoryStruct.comp (Y := rightHomology (S.map F))
        (Iso.hom (HomologyData.iso (homologyData (S.map F))) ≫
          rightHomologyMap' (𝟙 (S.map F)) (HomologyData.right (homologyData (S.map F))) (rightHomologyData (S.map F)))
        (rightHomologyMap' (𝟙 (S.map F)) (rightHomologyData (S.map F)) (hr.map F)) ≫
      F.map
        (CategoryStruct.comp (Y := S.rightHomology) (rightHomologyMap' (𝟙 S) hr S.rightHomologyData)
          (rightHomologyMap' (𝟙 S) S.rightHomologyData S.homologyData.right ≫ S.homologyData.iso.inv)))

Tactic:
simp only [assoc, F.map_comp, map_rightHomologyMap', ← rightHomologyMap'_comp_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.RightHomologyData.map_rightHomologyMap', CategoryTheory.ShortComplex.rightHomologyMap'_comp_assoc, CategoryTheory.Functor.map_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₁.HasLeftHomology
inst_6 : S₂.HasLeftHomology
inst_7 : F.PreservesLeftHomologyOf S₁
inst_8 : F.PreservesLeftHomologyOf S₂
dsimp :
  Eq (α := cycles (Functor.obj F.mapShortComplex S₁) ⟶ F.obj S₂.cycles)
    (CategoryStruct.comp (Y := cycles (Functor.obj F.mapShortComplex S₂))
      (cyclesMap' (Functor.map F.mapShortComplex φ) (leftHomologyData (Functor.obj F.mapShortComplex S₁))
        (leftHomologyData (Functor.obj F.mapShortComplex S₂)))
      (cyclesMap' (𝟙 (S₂.map F)) (leftHomologyData (S₂.map F)) (S₂.leftHomologyData.map F)))
    (CategoryStruct.comp (Y := F.obj S₁.cycles)
      (cyclesMap' (𝟙 (S₁.map F)) (leftHomologyData (S₁.map F)) (S₁.leftHomologyData.map F) :
        LeftHomologyData.K (S := S₁.map F) (leftHomologyData (S₁.map F)) ⟶
          LeftHomologyData.K (S := S₁.map F) (S₁.leftHomologyData.map F))
      (F.map (cyclesMap' φ S₁.leftHomologyData S₂.leftHomologyData)))
⊢ Eq (α := cycles (Functor.obj F.mapShortComplex S₁) ⟶ F.obj S₂.cycles)
    (CategoryStruct.comp (Y := cycles (Functor.obj F.mapShortComplex S₂))
      (cyclesMap (Functor.map F.mapShortComplex φ) :
        cycles (Functor.obj F.mapShortComplex S₁) ⟶ cycles (Functor.obj F.mapShortComplex S₂))
      (Iso.hom (S₂.mapCyclesIso F) : cycles (S₂.map F) ⟶ F.obj S₂.cycles))
    (CategoryStruct.comp (Y := F.obj S₁.cycles) (Iso.hom (S₁.mapCyclesIso F)) (F.map (cyclesMap φ)))

Tactic:
dsimp only [cyclesMap, mapCyclesIso, LeftHomologyData.cyclesIso, cyclesMapIso', Iso.refl]

Premises used: CategoryTheory.Iso.refl, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso, CategoryTheory.ShortComplex.cyclesMapIso', CategoryTheory.ShortComplex.cyclesMap, CategoryTheory.ShortComplex.mapCyclesIso
-- 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 (α := cycles (Functor.obj F.mapShortComplex S₁) ⟶ F.obj S₂.cycles)
    (CategoryStruct.comp (Y := cycles (Functor.obj F.mapShortComplex S₂))
      (cyclesMap' (Functor.map F.mapShortComplex φ) (leftHomologyData (Functor.obj F.mapShortComplex S₁))
        (leftHomologyData (Functor.obj F.mapShortComplex S₂)))
      (cyclesMap' (𝟙 (S₂.map F)) (leftHomologyData (S₂.map F)) (S₂.leftHomologyData.map F)))
    (CategoryStruct.comp (Y := F.obj S₁.cycles)
      (cyclesMap' (𝟙 (S₁.map F)) (leftHomologyData (S₁.map F)) (S₁.leftHomologyData.map F) :
        LeftHomologyData.K (S := S₁.map F) (leftHomologyData (S₁.map F)) ⟶
          LeftHomologyData.K (S := S₁.map F) (S₁.leftHomologyData.map F))
      (F.map (cyclesMap' φ S₁.leftHomologyData S₂.leftHomologyData)))

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

Premises used: CategoryTheory.ShortComplex.cyclesMap'_comp, CategoryTheory.ShortComplex.LeftHomologyData.map_cyclesMap', CategoryTheory.Category.comp_id, CategoryTheory.Functor.mapShortComplex_obj, CategoryTheory.Category.id_comp