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₁ 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 φ) :
        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 φ)))
have 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)))
Tactic: dsimp only [rightHomologyMap, mapRightHomologyIso, RightHomologyData.rightHomologyIso,
    rightHomologyMapIso', 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₁.rightHomology ⟶ rightHomology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.rightHomology) (F.map (rightHomologyMap φ))
        (Iso.inv (S₂.mapRightHomologyIso F)) :
      F.obj S₁.rightHomology ⟶ rightHomology (S₂.map F))
    (CategoryStruct.comp (Y := rightHomology (S₁.map F))
        (Iso.inv (S₁.mapRightHomologyIso F) : F.obj S₁.rightHomology ⟶ rightHomology (S₁.map F))
        (rightHomologyMap (Functor.map F.mapShortComplex φ) :
          rightHomology (S₁.map F) ⟶ rightHomology (Functor.obj F.mapShortComplex S₂)) :
      F.obj S₁.rightHomology ⟶ rightHomology (Functor.obj F.mapShortComplex S₂))
have rw : Eq (α := rightHomology (S₁.map F) ⟶ rightHomology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.rightHomology) (Iso.hom (S₁.mapRightHomologyIso F))
      (CategoryStruct.comp (Y := F.obj S₂.rightHomology) (F.map (rightHomologyMap φ))
        (Iso.inv (S₂.mapRightHomologyIso F))) :
    rightHomology (S₁.map F) ⟶ rightHomology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.rightHomology) (Iso.hom (S₁.mapRightHomologyIso F))
      (CategoryStruct.comp (Y := rightHomology (S₁.map F))
        (Iso.inv (S₁.mapRightHomologyIso F) : F.obj S₁.rightHomology ⟶ rightHomology (S₁.map F))
        (rightHomologyMap (Functor.map F.mapShortComplex φ) :
          rightHomology (S₁.map F) ⟶ rightHomology (Functor.obj F.mapShortComplex S₂))) :
    rightHomology (S₁.map F) ⟶ rightHomology (S₂.map F))
Tactic: rw [← cancel_epi (S₁.mapRightHomologyIso F).hom, ← mapRightHomologyIso_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 (α := rightHomology (S₁.map F) ⟶ rightHomology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.rightHomology) (Iso.hom (S₁.mapRightHomologyIso F))
        (CategoryStruct.comp (Y := F.obj S₂.rightHomology) (F.map (rightHomologyMap φ))
          (Iso.inv (S₂.mapRightHomologyIso F))) :
      rightHomology (S₁.map F) ⟶ rightHomology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.rightHomology) (Iso.hom (S₁.mapRightHomologyIso F))
        (CategoryStruct.comp (Y := rightHomology (S₁.map F))
          (Iso.inv (S₁.mapRightHomologyIso F) : F.obj S₁.rightHomology ⟶ rightHomology (S₁.map F))
          (rightHomologyMap (Functor.map F.mapShortComplex φ) :
            rightHomology (S₁.map F) ⟶ rightHomology (Functor.obj F.mapShortComplex S₂))) :
      rightHomology (S₁.map F) ⟶ rightHomology (S₂.map F))
⊢ Eq (α := F.obj S₁.rightHomology ⟶ rightHomology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.rightHomology) (F.map (rightHomologyMap φ))
        (Iso.inv (S₂.mapRightHomologyIso F)) :
      F.obj S₁.rightHomology ⟶ rightHomology (S₂.map F))
    (CategoryStruct.comp (Y := rightHomology (S₁.map F))
        (Iso.inv (S₁.mapRightHomologyIso F) : F.obj S₁.rightHomology ⟶ rightHomology (S₁.map F))
        (rightHomologyMap (Functor.map F.mapShortComplex φ) :
          rightHomology (S₁.map F) ⟶ rightHomology (Functor.obj F.mapShortComplex S₂)) :
      F.obj S₁.rightHomology ⟶ rightHomology (Functor.obj F.mapShortComplex S₂))
have rw₁ : Eq (α := rightHomology (S₁.map F) ⟶ rightHomology (S₂.map F))
  (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₂))
      (CategoryStruct.comp (Y := F.obj S₂.rightHomology) (Iso.hom (S₂.mapRightHomologyIso F))
          (Iso.inv (S₂.mapRightHomologyIso F)) :
        rightHomology (Functor.obj F.mapShortComplex S₂) ⟶ rightHomology (S₂.map F)) :
    rightHomology (Functor.obj F.mapShortComplex S₁) ⟶ rightHomology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.rightHomology) (Iso.hom (S₁.mapRightHomologyIso F))
    (CategoryStruct.comp (Y := rightHomology (S₁.map F))
      (Iso.inv (S₁.mapRightHomologyIso F) : F.obj S₁.rightHomology ⟶ rightHomology (S₁.map F))
      (rightHomologyMap (Functor.map F.mapShortComplex φ) :
        rightHomology (S₁.map F) ⟶ rightHomology (Functor.obj F.mapShortComplex S₂))))
Tactic: rw [← cancel_epi (S₁.mapRightHomologyIso F).hom, ← mapRightHomologyIso_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₁.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)) (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)
have 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)
Tactic: dsimp only [homologyMap, homologyMap', mapHomologyIso, LeftHomologyData.homologyIso,
    LeftHomologyData.leftHomologyIso, leftHomologyMapIso', leftHomologyIso,
    Iso.symm, Iso.trans, 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₁.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 (α := F.obj S₁.homology ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso F)))
    (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
      (homologyMap (Functor.map F.mapShortComplex φ)))
have rw : Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
    (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso F))))
  (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
    (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
      (homologyMap (Functor.map F.mapShortComplex φ))))
Tactic: rw [← cancel_epi (S₁.mapHomologyIso F).hom, ← mapHomologyIso_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₁.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₂
rw :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
      (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso F))))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
      (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
        (homologyMap (Functor.map F.mapShortComplex φ))))
⊢ Eq (α := F.obj S₁.homology ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso F)))
    (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
      (homologyMap (Functor.map F.mapShortComplex φ)))
have rw₁ : Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
  (CategoryStruct.comp (Y := homology (S₂.map F)) (homologyMap (Functor.map F.mapShortComplex φ))
      (CategoryStruct.comp (Y := F.obj S₂.homology) (Iso.hom (S₂.mapHomologyIso F)) (Iso.inv (S₂.mapHomologyIso F))) :
    homology (S₁.map F) ⟶ homology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
      (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
        (homologyMap (Functor.map F.mapShortComplex φ))) :
    homology (S₁.map F) ⟶ homology (S₂.map F))
Tactic: rw [← cancel_epi (S₁.mapHomologyIso F).hom, ← mapHomologyIso_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₁.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₂
rw :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
      (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso F))))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
      (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
        (homologyMap (Functor.map F.mapShortComplex φ))))
rw₁ :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := homology (S₂.map F)) (homologyMap (Functor.map F.mapShortComplex φ))
        (CategoryStruct.comp (Y := F.obj S₂.homology) (Iso.hom (S₂.mapHomologyIso F)) (Iso.inv (S₂.mapHomologyIso F))) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
        (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
          (homologyMap (Functor.map F.mapShortComplex φ))) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
⊢ Eq (α := F.obj S₁.homology ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso F)))
    (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
      (homologyMap (Functor.map F.mapShortComplex φ)))
have rw₂ : Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
  (homologyMap (Functor.map F.mapShortComplex φ) ≫ 𝟙 (homology (S₂.map F)) : homology (S₁.map F) ⟶ homology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
      (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
        (homologyMap (Functor.map F.mapShortComplex φ))) :
    homology (S₁.map F) ⟶ homology (S₂.map F))
Tactic: rw [← cancel_epi (S₁.mapHomologyIso F).hom, ← mapHomologyIso_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₁.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₂
rw :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
      (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso F))))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
      (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
        (homologyMap (Functor.map F.mapShortComplex φ))))
rw₁ :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := homology (S₂.map F)) (homologyMap (Functor.map F.mapShortComplex φ))
        (CategoryStruct.comp (Y := F.obj S₂.homology) (Iso.hom (S₂.mapHomologyIso F)) (Iso.inv (S₂.mapHomologyIso F))) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
        (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
          (homologyMap (Functor.map F.mapShortComplex φ))) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
rw₂ :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (homologyMap (Functor.map F.mapShortComplex φ) ≫ 𝟙 (homology (S₂.map F)) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
        (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
          (homologyMap (Functor.map F.mapShortComplex φ))) :
      homology (S₁.map F) ⟶ homology (S₂.map F))
⊢ Eq (α := F.obj S₁.homology ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso F)))
    (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
      (homologyMap (Functor.map F.mapShortComplex φ)))
have rw₃ : Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
  (homologyMap (Functor.map F.mapShortComplex φ) : homology (S₁.map F) ⟶ homology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso F))
      (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso F))
        (homologyMap (Functor.map F.mapShortComplex φ))) :
    homology (S₁.map F) ⟶ homology (S₂.map F))
Tactic: rw [← cancel_epi (S₁.mapHomologyIso F).hom, ← mapHomologyIso_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₁.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 φ))
        (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)
have 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)
Tactic: dsimp only [Iso.trans, Iso.symm, Functor.mapIso, mapHomologyIso']
-- 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₁.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 (α := F.obj S₁.homology ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso' F)))
    (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso' F))
      (homologyMap (Functor.map F.mapShortComplex φ)))
have rw : Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F))
    (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso' F))))
  (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F))
    (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso' F))
      (homologyMap (Functor.map F.mapShortComplex φ))))
Tactic: rw [← cancel_epi (S₁.mapHomologyIso' F).hom, ← mapHomologyIso'_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₁.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₂
rw :
  Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F))
      (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso' F))))
    (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F))
      (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso' F))
        (homologyMap (Functor.map F.mapShortComplex φ))))
⊢ Eq (α := F.obj S₁.homology ⟶ homology (S₂.map F))
    (CategoryStruct.comp (Y := F.obj S₂.homology) (F.map (homologyMap φ)) (Iso.inv (S₂.mapHomologyIso' F)))
    (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso' F))
      (homologyMap (Functor.map F.mapShortComplex φ)))
have rw₁ : Eq (α := homology (S₁.map F) ⟶ homology (S₂.map F))
  (CategoryStruct.comp (Y := homology (S₂.map F)) (homologyMap (Functor.map F.mapShortComplex φ))
      (CategoryStruct.comp (Y := F.obj S₂.homology) (Iso.hom (S₂.mapHomologyIso' F)) (Iso.inv (S₂.mapHomologyIso' F))) :
    homology (S₁.map F) ⟶ homology (S₂.map F))
  (CategoryStruct.comp (Y := F.obj S₁.homology) (Iso.hom (S₁.mapHomologyIso' F))
      (CategoryStruct.comp (Y := homology (S₁.map F)) (Iso.inv (S₁.mapHomologyIso' F))
        (homologyMap (Functor.map F.mapShortComplex φ))) :
    homology (S₁.map F) ⟶ homology (S₂.map F))
Tactic: rw [← cancel_epi (S₁.mapHomologyIso' F).hom, ← mapHomologyIso'_hom_naturality_assoc,
    Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]