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₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hl₁.IsPreservedBy F
inst_6 : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
rw : F.map γ.φK = cyclesMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
rw₁ : F.map γ.φK = LeftHomologyMapData.φK (γ.map F)
⊢ F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
have rw₂ : F.map γ.φK = F.map γ.φK
Tactic: rw [γ.cyclesMap'_eq, (γ.map F).cyclesMap'_eq, ShortComplex.LeftHomologyMapData.map_φK]
-- 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₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hl₁.IsPreservedBy F
inst_6 : hl₂.IsPreservedBy F
⊢ F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
have have : ∀ (γ : LeftHomologyMapData φ hl₁ hl₂),
  F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
Tactic: have γ : ShortComplex.LeftHomologyMapData φ hl₁ hl₂ := default
-- 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₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hl₁.IsPreservedBy F
inst_6 : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
⊢ F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
have rw : F.map γ.φH = leftHomologyMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
Tactic: rw [γ.leftHomologyMap'_eq, (γ.map F).leftHomologyMap'_eq,
    ShortComplex.LeftHomologyMapData.map_φH]
-- 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₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hl₁.IsPreservedBy F
inst_6 : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
rw : F.map γ.φH = leftHomologyMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
⊢ F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
have rw₁ : F.map γ.φH = LeftHomologyMapData.φH (γ.map F)
Tactic: rw [γ.leftHomologyMap'_eq, (γ.map F).leftHomologyMap'_eq,
    ShortComplex.LeftHomologyMapData.map_φH]
-- 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₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hl₁.IsPreservedBy F
inst_6 : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
rw : F.map γ.φH = leftHomologyMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
rw₁ : F.map γ.φH = LeftHomologyMapData.φH (γ.map F)
⊢ F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
have rw₂ : F.map γ.φH = F.map γ.φH
Tactic: rw [γ.leftHomologyMap'_eq, (γ.map F).leftHomologyMap'_eq,
    ShortComplex.LeftHomologyMapData.map_φH]
-- 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₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hr₁.IsPreservedBy F
inst_6 : hr₂.IsPreservedBy F
⊢ F.map (opcyclesMap' φ hr₁ hr₂) = opcyclesMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
have have : ∀ (γ : RightHomologyMapData φ hr₁ hr₂),
  F.map (opcyclesMap' φ hr₁ hr₂) = opcyclesMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
Tactic: have γ : ShortComplex.RightHomologyMapData φ hr₁ hr₂ := default
-- 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₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hr₁.IsPreservedBy F
inst_6 : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
⊢ F.map (opcyclesMap' φ hr₁ hr₂) = opcyclesMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
have rw : F.map γ.φQ = opcyclesMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
Tactic: rw [γ.opcyclesMap'_eq, (γ.map F).opcyclesMap'_eq, ShortComplex.RightHomologyMapData.map_φQ]
-- 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₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hr₁.IsPreservedBy F
inst_6 : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
rw : F.map γ.φQ = opcyclesMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
⊢ F.map (opcyclesMap' φ hr₁ hr₂) = opcyclesMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
have rw₁ : F.map γ.φQ = RightHomologyMapData.φQ (γ.map F)
Tactic: rw [γ.opcyclesMap'_eq, (γ.map F).opcyclesMap'_eq, ShortComplex.RightHomologyMapData.map_φQ]
-- 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₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hr₁.IsPreservedBy F
inst_6 : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
rw : F.map γ.φQ = opcyclesMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
rw₁ : F.map γ.φQ = RightHomologyMapData.φQ (γ.map F)
⊢ F.map (opcyclesMap' φ hr₁ hr₂) = opcyclesMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
have rw₂ : F.map γ.φQ = F.map γ.φQ
Tactic: rw [γ.opcyclesMap'_eq, (γ.map F).opcyclesMap'_eq, ShortComplex.RightHomologyMapData.map_φQ]
-- 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₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hr₁.IsPreservedBy F
inst_6 : hr₂.IsPreservedBy F
⊢ F.map (rightHomologyMap' φ hr₁ hr₂) = rightHomologyMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
have have : ∀ (γ : RightHomologyMapData φ hr₁ hr₂),
  F.map (rightHomologyMap' φ hr₁ hr₂) = rightHomologyMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
Tactic: have γ : ShortComplex.RightHomologyMapData φ hr₁ hr₂ := default
-- 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₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hr₁.IsPreservedBy F
inst_6 : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
⊢ F.map (rightHomologyMap' φ hr₁ hr₂) = rightHomologyMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
have rw : F.map γ.φH = rightHomologyMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
Tactic: rw [γ.rightHomologyMap'_eq, (γ.map F).rightHomologyMap'_eq,
    ShortComplex.RightHomologyMapData.map_φH]
-- 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₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hr₁.IsPreservedBy F
inst_6 : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
rw : F.map γ.φH = rightHomologyMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
⊢ F.map (rightHomologyMap' φ hr₁ hr₂) = rightHomologyMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
have rw₁ : F.map γ.φH = RightHomologyMapData.φH (γ.map F)
Tactic: rw [γ.rightHomologyMap'_eq, (γ.map F).rightHomologyMap'_eq,
    ShortComplex.RightHomologyMapData.map_φH]
-- 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₂
hr₁ : S₁.RightHomologyData
hr₂ : S₂.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hr₁.IsPreservedBy F
inst_6 : hr₂.IsPreservedBy F
γ : RightHomologyMapData φ hr₁ hr₂
rw : F.map γ.φH = rightHomologyMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
rw₁ : F.map γ.φH = RightHomologyMapData.φH (γ.map F)
⊢ F.map (rightHomologyMap' φ hr₁ hr₂) = rightHomologyMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)
have rw₂ : F.map γ.φH = F.map γ.φH
Tactic: rw [γ.rightHomologyMap'_eq, (γ.map F).rightHomologyMap'_eq,
    ShortComplex.RightHomologyMapData.map_φH]
-- 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
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.cycles) (S.mapCyclesIso F : cycles (S.map F) ≅ F.obj S.cycles)
    (Iso.trans (Y := K (S := S.map F) (hl.map F)) (cyclesIso (hl.map F)) (F.mapIso (Iso.symm hl.cyclesIso)) :
      cycles (S.map F) ≅ F.obj S.cycles)
have w : Eq (α := cycles (S.map F) ⟶ F.obj S.cycles) (Iso.hom (S.mapCyclesIso F) : cycles (S.map F) ⟶ F.obj S.cycles)
  (Iso.hom (Iso.trans (Y := K (S := S.map F) (hl.map F)) (cyclesIso (hl.map F)) (F.mapIso (Iso.symm hl.cyclesIso))) :
    cycles (S.map F) ⟶ F.obj S.cycles)
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
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.cycles) (Iso.hom (S.mapCyclesIso F) : cycles (S.map F) ⟶ F.obj S.cycles)
    (Iso.hom (Iso.trans (Y := K (S := S.map F) (hl.map F)) (cyclesIso (hl.map F)) (F.mapIso (Iso.symm hl.cyclesIso))) :
      cycles (S.map F) ⟶ F.obj S.cycles)
have w : Eq (α := cycles (S.map F) ⟶ F.obj S.cycles)
  (cyclesMap' (𝟙 (S.map F)) (leftHomologyData (S.map F)) (S.leftHomologyData.map F) :
    K (S := S.map F) (leftHomologyData (S.map F)) ⟶ K (S := S.map F) (S.leftHomologyData.map F))
  (CategoryStruct.comp (Y := F.obj hl.K)
    (cyclesMap' (𝟙 (S.map F)) (leftHomologyData (S.map F)) (hl.map F) :
      K (S := S.map F) (leftHomologyData (S.map F)) ⟶ K (S := S.map F) (hl.map F))
    (F.map (cyclesMap' (𝟙 S) hl S.leftHomologyData)))
Tactic: dsimp [mapCyclesIso, cyclesIso]
-- 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
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 (α := leftHomology (S.map F) ≅ F.obj S.leftHomology)
    (S.mapLeftHomologyIso F : leftHomology (S.map F) ≅ F.obj S.leftHomology)
    (Iso.trans (Y := H (S := S.map F) (hl.map F)) (leftHomologyIso (hl.map F))
        (F.mapIso (Iso.symm hl.leftHomologyIso)) :
      leftHomology (S.map F) ≅ F.obj S.leftHomology)
have w : Eq (α := cycles (S.map F) ⟶ F.obj S.leftHomology)
  (leftHomologyπ (S.map F) ≫ Iso.hom (S.mapLeftHomologyIso F) : cycles (S.map F) ⟶ F.obj S.leftHomology)
  (leftHomologyπ (S.map F) ≫
      Iso.hom
        (Iso.trans (Y := H (S := S.map F) (hl.map F)) (leftHomologyIso (hl.map F))
          (F.mapIso (Iso.symm hl.leftHomologyIso))) :
    cycles (S.map F) ⟶ F.obj S.leftHomology)
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
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) ≫ Iso.hom (S.mapLeftHomologyIso F) : cycles (S.map F) ⟶ F.obj S.leftHomology)
    (leftHomologyπ (S.map F) ≫
        Iso.hom
          (Iso.trans (Y := H (S := S.map F) (hl.map F)) (leftHomologyIso (hl.map F))
            (F.mapIso (Iso.symm hl.leftHomologyIso))) :
      cycles (S.map F) ⟶ F.obj S.leftHomology)
have w : 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: dsimp [mapLeftHomologyIso, leftHomologyIso]
-- 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.HasRightHomology
inst_6 : F.PreservesRightHomologyOf S
⊢ 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)
have 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)))))
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.HasRightHomology
inst_6 : F.PreservesRightHomologyOf S
⊢ 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)))))
have 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)
Tactic: dsimp [mapOpcyclesIso, opcyclesIso]
-- 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.HasRightHomology
inst_6 : F.PreservesRightHomologyOf S
⊢ 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)
have 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)
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.HasRightHomology
inst_6 : F.PreservesRightHomologyOf S
⊢ 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)
have 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)))
Tactic: dsimp [mapRightHomologyIso, 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 : 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) (S.mapHomologyIso F)
    (Iso.trans (Y := H (S := S.map F) (hl.map F)) (homologyIso (hl.map F)) (F.mapIso (Iso.symm hl.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) (hl.map F)) (homologyIso (hl.map F)) (F.mapIso (Iso.symm hl.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
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) (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))))
have 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))))
Tactic: dsimp only [mapHomologyIso, homologyIso, ShortComplex.leftHomologyIso,
    leftHomologyMapIso', leftHomologyIso, Functor.mapIso,
    Iso.symm, Iso.trans, Iso.refl]