awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
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) (S.mapHomologyIso' F)
    (Iso.trans (Y := H (S := S.map F) (hr.map F)) (homologyIso (hr.map F)) (F.mapIso (Iso.symm hr.homologyIso)))
have 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))))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
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) (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))))
have 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)))
Tactic: dsimp only [Iso.trans, Iso.symm, Iso.refl, Functor.mapIso, mapHomologyIso', homologyIso,
    rightHomologyIso, rightHomologyMapIso', ShortComplex.rightHomologyIso]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
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 φ) :
        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 φ)))
have 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)))
Tactic: dsimp only [cyclesMap, mapCyclesIso, LeftHomologyData.cyclesIso, cyclesMapIso', Iso.refl]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
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 (α := F.obj S₁.cycles ⟶ cycles (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.cycles) (F.map (cyclesMap φ)) (Iso.inv (S₂.mapCyclesIso F)) :
      F.obj S₁.cycles ⟶ cycles (S₂.map F))
    (CategoryStruct.comp (Y := cycles (S₁.map F)) (Iso.inv (S₁.mapCyclesIso F) : F.obj S₁.cycles ⟶ cycles (S₁.map F))
        (cyclesMap (Functor.map F.mapShortComplex φ) : cycles (S₁.map F) ⟶ cycles (Functor.obj F.mapShortComplex S₂)) :
      F.obj S₁.cycles ⟶ cycles (Functor.obj F.mapShortComplex S₂))
have rw : Eq (α := cycles (S₁.map F) ⟶ cycles (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.cycles) (Iso.hom (S₁.mapCyclesIso F))
      (CategoryStruct.comp (Y := F.obj S₂.cycles) (F.map (cyclesMap φ)) (Iso.inv (S₂.mapCyclesIso F))) :
    cycles (S₁.map F) ⟶ cycles (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.cycles) (Iso.hom (S₁.mapCyclesIso F))
      (CategoryStruct.comp (Y := cycles (S₁.map F)) (Iso.inv (S₁.mapCyclesIso F) : F.obj S₁.cycles ⟶ cycles (S₁.map F))
        (cyclesMap (Functor.map F.mapShortComplex φ) : cycles (S₁.map F) ⟶ cycles (Functor.obj F.mapShortComplex S₂))) :
    cycles (S₁.map F) ⟶ cycles (S₂.map F))
Tactic: rw [← cancel_epi (S₁.mapCyclesIso F).hom, ← mapCyclesIso_hom_naturality_assoc,
    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
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₂
rw :
  Eq (α := cycles (S₁.map F) ⟶ cycles (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.cycles) (Iso.hom (S₁.mapCyclesIso F))
        (CategoryStruct.comp (Y := F.obj S₂.cycles) (F.map (cyclesMap φ)) (Iso.inv (S₂.mapCyclesIso F))) :
      cycles (S₁.map F) ⟶ cycles (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.cycles) (Iso.hom (S₁.mapCyclesIso F))
        (CategoryStruct.comp (Y := cycles (S₁.map F))
          (Iso.inv (S₁.mapCyclesIso F) : F.obj S₁.cycles ⟶ cycles (S₁.map F))
          (cyclesMap (Functor.map F.mapShortComplex φ) :
            cycles (S₁.map F) ⟶ cycles (Functor.obj F.mapShortComplex S₂))) :
      cycles (S₁.map F) ⟶ cycles (S₂.map F))
⊢ Eq (α := F.obj S₁.cycles ⟶ cycles (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.cycles) (F.map (cyclesMap φ)) (Iso.inv (S₂.mapCyclesIso F)) :
      F.obj S₁.cycles ⟶ cycles (S₂.map F))
    (CategoryStruct.comp (Y := cycles (S₁.map F)) (Iso.inv (S₁.mapCyclesIso F) : F.obj S₁.cycles ⟶ cycles (S₁.map F))
        (cyclesMap (Functor.map F.mapShortComplex φ) : cycles (S₁.map F) ⟶ cycles (Functor.obj F.mapShortComplex S₂)) :
      F.obj S₁.cycles ⟶ cycles (Functor.obj F.mapShortComplex S₂))
have rw₁ : Eq (α := cycles (S₁.map F) ⟶ cycles (S₂.map F))
  (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₂))
      (CategoryStruct.comp (Y := F.obj S₂.cycles) (Iso.hom (S₂.mapCyclesIso F)) (Iso.inv (S₂.mapCyclesIso F)) :
        cycles (Functor.obj F.mapShortComplex S₂) ⟶ cycles (S₂.map F)) :
    cycles (Functor.obj F.mapShortComplex S₁) ⟶ cycles (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.cycles) (Iso.hom (S₁.mapCyclesIso F))
    (CategoryStruct.comp (Y := cycles (S₁.map F)) (Iso.inv (S₁.mapCyclesIso F) : F.obj S₁.cycles ⟶ cycles (S₁.map F))
      (cyclesMap (Functor.map F.mapShortComplex φ) : cycles (S₁.map F) ⟶ cycles (Functor.obj F.mapShortComplex S₂))))
Tactic: rw [← cancel_epi (S₁.mapCyclesIso F).hom, ← mapCyclesIso_hom_naturality_assoc,
    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
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 φ) :
        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 φ)))
have 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)))
Tactic: dsimp only [leftHomologyMap, mapLeftHomologyIso, LeftHomologyData.leftHomologyIso,
    leftHomologyMapIso', Iso.refl]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
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 (α := F.obj S₁.leftHomology ⟶ leftHomology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.leftHomology) (F.map (leftHomologyMap φ)) (Iso.inv (S₂.mapLeftHomologyIso F)) :
      F.obj S₁.leftHomology ⟶ leftHomology (S₂.map F))
    (CategoryStruct.comp (Y := leftHomology (S₁.map F))
        (Iso.inv (S₁.mapLeftHomologyIso F) : F.obj S₁.leftHomology ⟶ leftHomology (S₁.map F))
        (leftHomologyMap (Functor.map F.mapShortComplex φ) :
          leftHomology (S₁.map F) ⟶ leftHomology (Functor.obj F.mapShortComplex S₂)) :
      F.obj S₁.leftHomology ⟶ leftHomology (Functor.obj F.mapShortComplex S₂))
have rw : Eq (α := leftHomology (S₁.map F) ⟶ leftHomology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.leftHomology) (Iso.hom (S₁.mapLeftHomologyIso F))
      (CategoryStruct.comp (Y := F.obj S₂.leftHomology) (F.map (leftHomologyMap φ))
        (Iso.inv (S₂.mapLeftHomologyIso F))) :
    leftHomology (S₁.map F) ⟶ leftHomology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.leftHomology) (Iso.hom (S₁.mapLeftHomologyIso F))
      (CategoryStruct.comp (Y := leftHomology (S₁.map F))
        (Iso.inv (S₁.mapLeftHomologyIso F) : F.obj S₁.leftHomology ⟶ leftHomology (S₁.map F))
        (leftHomologyMap (Functor.map F.mapShortComplex φ) :
          leftHomology (S₁.map F) ⟶ leftHomology (Functor.obj F.mapShortComplex S₂))) :
    leftHomology (S₁.map F) ⟶ leftHomology (S₂.map F))
Tactic: rw [← cancel_epi (S₁.mapLeftHomologyIso F).hom, ← mapLeftHomologyIso_hom_naturality_assoc,
    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
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₂
rw :
  Eq (α := leftHomology (S₁.map F) ⟶ leftHomology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.leftHomology) (Iso.hom (S₁.mapLeftHomologyIso F))
        (CategoryStruct.comp (Y := F.obj S₂.leftHomology) (F.map (leftHomologyMap φ))
          (Iso.inv (S₂.mapLeftHomologyIso F))) :
      leftHomology (S₁.map F) ⟶ leftHomology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.leftHomology) (Iso.hom (S₁.mapLeftHomologyIso F))
        (CategoryStruct.comp (Y := leftHomology (S₁.map F))
          (Iso.inv (S₁.mapLeftHomologyIso F) : F.obj S₁.leftHomology ⟶ leftHomology (S₁.map F))
          (leftHomologyMap (Functor.map F.mapShortComplex φ) :
            leftHomology (S₁.map F) ⟶ leftHomology (Functor.obj F.mapShortComplex S₂))) :
      leftHomology (S₁.map F) ⟶ leftHomology (S₂.map F))
⊢ Eq (α := F.obj S₁.leftHomology ⟶ leftHomology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.leftHomology) (F.map (leftHomologyMap φ)) (Iso.inv (S₂.mapLeftHomologyIso F)) :
      F.obj S₁.leftHomology ⟶ leftHomology (S₂.map F))
    (CategoryStruct.comp (Y := leftHomology (S₁.map F))
        (Iso.inv (S₁.mapLeftHomologyIso F) : F.obj S₁.leftHomology ⟶ leftHomology (S₁.map F))
        (leftHomologyMap (Functor.map F.mapShortComplex φ) :
          leftHomology (S₁.map F) ⟶ leftHomology (Functor.obj F.mapShortComplex S₂)) :
      F.obj S₁.leftHomology ⟶ leftHomology (Functor.obj F.mapShortComplex S₂))
have rw₁ : Eq (α := leftHomology (S₁.map F) ⟶ leftHomology (S₂.map F))
  (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₂))
      (CategoryStruct.comp (Y := F.obj S₂.leftHomology) (Iso.hom (S₂.mapLeftHomologyIso F))
          (Iso.inv (S₂.mapLeftHomologyIso F)) :
        leftHomology (Functor.obj F.mapShortComplex S₂) ⟶ leftHomology (S₂.map F)) :
    leftHomology (Functor.obj F.mapShortComplex S₁) ⟶ leftHomology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.leftHomology) (Iso.hom (S₁.mapLeftHomologyIso F))
    (CategoryStruct.comp (Y := leftHomology (S₁.map F))
      (Iso.inv (S₁.mapLeftHomologyIso F) : F.obj S₁.leftHomology ⟶ leftHomology (S₁.map F))
      (leftHomologyMap (Functor.map F.mapShortComplex φ) :
        leftHomology (S₁.map F) ⟶ leftHomology (Functor.obj F.mapShortComplex S₂))))
Tactic: rw [← cancel_epi (S₁.mapLeftHomologyIso F).hom, ← mapLeftHomologyIso_hom_naturality_assoc,
    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
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 φ) :
        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 φ)))
have 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)))
Tactic: dsimp only [opcyclesMap, mapOpcyclesIso, RightHomologyData.opcyclesIso,
    opcyclesMapIso', Iso.refl]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
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 (α := F.obj S₁.opcycles ⟶ opcycles (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.opcycles) (F.map (opcyclesMap φ)) (Iso.inv (S₂.mapOpcyclesIso F)) :
      F.obj S₁.opcycles ⟶ opcycles (S₂.map F))
    (CategoryStruct.comp (Y := opcycles (S₁.map F))
        (Iso.inv (S₁.mapOpcyclesIso F) : F.obj S₁.opcycles ⟶ opcycles (S₁.map F))
        (opcyclesMap (Functor.map F.mapShortComplex φ) :
          opcycles (S₁.map F) ⟶ opcycles (Functor.obj F.mapShortComplex S₂)) :
      F.obj S₁.opcycles ⟶ opcycles (Functor.obj F.mapShortComplex S₂))
have rw : Eq (α := opcycles (S₁.map F) ⟶ opcycles (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.opcycles) (Iso.hom (S₁.mapOpcyclesIso F))
      (CategoryStruct.comp (Y := F.obj S₂.opcycles) (F.map (opcyclesMap φ)) (Iso.inv (S₂.mapOpcyclesIso F))) :
    opcycles (S₁.map F) ⟶ opcycles (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.opcycles) (Iso.hom (S₁.mapOpcyclesIso F))
      (CategoryStruct.comp (Y := opcycles (S₁.map F))
        (Iso.inv (S₁.mapOpcyclesIso F) : F.obj S₁.opcycles ⟶ opcycles (S₁.map F))
        (opcyclesMap (Functor.map F.mapShortComplex φ) :
          opcycles (S₁.map F) ⟶ opcycles (Functor.obj F.mapShortComplex S₂))) :
    opcycles (S₁.map F) ⟶ opcycles (S₂.map F))
Tactic: rw [← cancel_epi (S₁.mapOpcyclesIso F).hom, ← mapOpcyclesIso_hom_naturality_assoc,
    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
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₂
rw :
  Eq (α := opcycles (S₁.map F) ⟶ opcycles (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.opcycles) (Iso.hom (S₁.mapOpcyclesIso F))
        (CategoryStruct.comp (Y := F.obj S₂.opcycles) (F.map (opcyclesMap φ)) (Iso.inv (S₂.mapOpcyclesIso F))) :
      opcycles (S₁.map F) ⟶ opcycles (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.opcycles) (Iso.hom (S₁.mapOpcyclesIso F))
        (CategoryStruct.comp (Y := opcycles (S₁.map F))
          (Iso.inv (S₁.mapOpcyclesIso F) : F.obj S₁.opcycles ⟶ opcycles (S₁.map F))
          (opcyclesMap (Functor.map F.mapShortComplex φ) :
            opcycles (S₁.map F) ⟶ opcycles (Functor.obj F.mapShortComplex S₂))) :
      opcycles (S₁.map F) ⟶ opcycles (S₂.map F))
⊢ Eq (α := F.obj S₁.opcycles ⟶ opcycles (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.opcycles) (F.map (opcyclesMap φ)) (Iso.inv (S₂.mapOpcyclesIso F)) :
      F.obj S₁.opcycles ⟶ opcycles (S₂.map F))
    (CategoryStruct.comp (Y := opcycles (S₁.map F))
        (Iso.inv (S₁.mapOpcyclesIso F) : F.obj S₁.opcycles ⟶ opcycles (S₁.map F))
        (opcyclesMap (Functor.map F.mapShortComplex φ) :
          opcycles (S₁.map F) ⟶ opcycles (Functor.obj F.mapShortComplex S₂)) :
      F.obj S₁.opcycles ⟶ opcycles (Functor.obj F.mapShortComplex S₂))
have rw₁ : Eq (α := opcycles (S₁.map F) ⟶ opcycles (S₂.map F))
  (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₂))
      (CategoryStruct.comp (Y := F.obj S₂.opcycles) (Iso.hom (S₂.mapOpcyclesIso F)) (Iso.inv (S₂.mapOpcyclesIso F)) :
        opcycles (Functor.obj F.mapShortComplex S₂) ⟶ opcycles (S₂.map F)) :
    opcycles (Functor.obj F.mapShortComplex S₁) ⟶ opcycles (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.opcycles) (Iso.hom (S₁.mapOpcyclesIso F))
    (CategoryStruct.comp (Y := opcycles (S₁.map F))
      (Iso.inv (S₁.mapOpcyclesIso F) : F.obj S₁.opcycles ⟶ opcycles (S₁.map F))
      (opcyclesMap (Functor.map F.mapShortComplex φ) :
        opcycles (S₁.map F) ⟶ opcycles (Functor.obj F.mapShortComplex S₂))))
Tactic: rw [← cancel_epi (S₁.mapOpcyclesIso F).hom, ← mapOpcyclesIso_hom_naturality_assoc,
    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]