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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
inst_5 : h.IsPreservedBy F
h' : S.RightHomologyData
this : PreservesLimit (parallelPair h.g' 0) F
⊢ (parallelPair h.g' 0).map WalkingParallelPairHom.left ≫
      Iso.hom (Iso.refl ((parallelPair h.g' 0).obj WalkingParallelPair.one)) =
    (ShortComplex.opcyclesMapIso' (Iso.refl S) h h').hom ≫ (parallelPair h'.g' 0).map WalkingParallelPairHom.left

Tactic:
simp
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
inst_5 : h.IsPreservedBy F
h' : S.RightHomologyData
this : PreservesLimit (parallelPair h.g' 0) F
⊢ (parallelPair h.g' 0).map WalkingParallelPairHom.right ≫
      Iso.hom (Iso.refl ((parallelPair h.g' 0).obj WalkingParallelPair.one)) =
    (ShortComplex.opcyclesMapIso' (Iso.refl S) h h').hom ≫ (parallelPair h'.g' 0).map WalkingParallelPairHom.right

Tactic:
simp
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
inst_5 : h.IsPreservedBy F
h' : S.RightHomologyData
this : PreservesLimit (parallelPair h.g' 0) F
e : parallelPair h.g' 0 ≅ parallelPair h'.g' 0 :=
  parallelPair.ext (ShortComplex.opcyclesMapIso' (Iso.refl S) h h')
    (Iso.refl ((parallelPair h.g' 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ PreservesLimit (parallelPair h'.g' 0) F

Tactic:
preservesLimit_of_iso_diagram F e

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
inst_5 : h.IsPreservedBy F
h' : S.RightHomologyData
this : PreservesLimit (parallelPair h.g' 0) F
e : parallelPair h.g' 0 ≅ parallelPair h'.g' 0 :=
  parallelPair.ext (ShortComplex.opcyclesMapIso' (Iso.refl S) h h')
    (Iso.refl ((parallelPair h.g' 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ PreservesLimit (parallelPair h'.g' 0) F

Tactic:
exact preservesLimit_of_iso_diagram F e

Premises used: CategoryTheory.Limits.preservesLimit_of_iso_diagram
-- 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
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesLeftHomologyOf S
⊢ h₁.IsPreservedBy F

Tactic:
Functor.PreservesLeftHomologyOf.isPreservedBy _

Premises used: CategoryTheory.Functor.PreservesLeftHomologyOf.isPreservedBy
-- 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
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesRightHomologyOf S
⊢ h₂.IsPreservedBy F

Tactic:
Functor.PreservesRightHomologyOf.isPreservedBy _

Premises used: CategoryTheory.Functor.PreservesRightHomologyOf.isPreservedBy
-- 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
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
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
⊢ HasLeftHomology (S.map F)

Tactic:
HasLeftHomology.mk' (S.leftHomologyData.map F)

Premises used: CategoryTheory.ShortComplex.leftHomologyData, CategoryTheory.ShortComplex.LeftHomologyData.map, CategoryTheory.ShortComplex.HasLeftHomology.mk'
-- 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
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
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
⊢ HasLeftHomology (S.map F)

Tactic:
infer_instance
-- 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
h₁ : S.LeftHomologyData
h₂ : 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
⊢ HasRightHomology (S.map F)

Tactic:
HasRightHomology.mk' (S.rightHomologyData.map F)

Premises used: CategoryTheory.ShortComplex.RightHomologyData.map, CategoryTheory.ShortComplex.rightHomologyData, CategoryTheory.ShortComplex.HasRightHomology.mk'
-- 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
h₁ : S.LeftHomologyData
h₂ : 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
⊢ HasRightHomology (S.map F)

Tactic:
infer_instance
-- 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
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasHomology
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
⊢ HasHomology (S.map F)

Tactic:
HasHomology.mk' (S.homologyData.map F)

Premises used: CategoryTheory.ShortComplex.HasHomology.mk', CategoryTheory.ShortComplex.HomologyData.map, CategoryTheory.ShortComplex.homologyData
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasHomology
inst_6 : F.PreservesLeftHomologyOf S
inst_7 : F.PreservesRightHomologyOf S
⊢ HasHomology (S.map F)

Tactic:
infer_instance
-- 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₂
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
have :
  ∀ (γ : LeftHomologyMapData φ hl₁ hl₂),
    F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
⊢ F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)

Tactic:
have γ : ShortComplex.LeftHomologyMapData φ hl₁ hl₂ := default
-- 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₂
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)
rw₂ rw₃ : F.map γ.φK = F.map γ.φK
⊢ F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)

Tactic:
rw [γ.cyclesMap'_eq, (γ.map F).cyclesMap'_eq, ShortComplex.LeftHomologyMapData.map_φK]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.map, CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap'_eq, CategoryTheory.ShortComplex.LeftHomologyMapData.map_φK
-- 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₂
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
have :
  ∀ (γ : LeftHomologyMapData φ hl₁ hl₂),
    F.map (leftHomologyMap' φ hl₁ hl₂) = 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)

Tactic:
have γ : ShortComplex.LeftHomologyMapData φ hl₁ hl₂ := default
-- 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₂
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)
rw₂ rw₃ : F.map γ.φH = F.map γ.φH
⊢ F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)

Tactic:
rw [γ.leftHomologyMap'_eq, (γ.map F).leftHomologyMap'_eq,
    ShortComplex.LeftHomologyMapData.map_φH]

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.map_φH, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq, CategoryTheory.ShortComplex.LeftHomologyMapData.map
-- 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₂
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
have :
  ∀ (γ : RightHomologyMapData φ hr₁ hr₂),
    F.map (opcyclesMap' φ hr₁ hr₂) = 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)

Tactic:
have γ : ShortComplex.RightHomologyMapData φ hr₁ hr₂ := default
-- 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₂
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)
rw₂ rw₃ : F.map γ.φQ = F.map γ.φQ
⊢ F.map (opcyclesMap' φ hr₁ hr₂) = opcyclesMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)

Tactic:
rw [γ.opcyclesMap'_eq, (γ.map F).opcyclesMap'_eq, ShortComplex.RightHomologyMapData.map_φQ]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.map, CategoryTheory.ShortComplex.RightHomologyMapData.map_φQ
-- 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₂
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
have :
  ∀ (γ : RightHomologyMapData φ hr₁ hr₂),
    F.map (rightHomologyMap' φ hr₁ hr₂) = 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)

Tactic:
have γ : ShortComplex.RightHomologyMapData φ hr₁ hr₂ := default
-- 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₂
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)
rw₂ rw₃ : F.map γ.φH = F.map γ.φH
⊢ F.map (rightHomologyMap' φ hr₁ hr₂) = rightHomologyMap' (Functor.map F.mapShortComplex φ) (hr₁.map F) (hr₂.map F)

Tactic:
rw [γ.rightHomologyMap'_eq, (γ.map F).rightHomologyMap'_eq,
    ShortComplex.RightHomologyMapData.map_φH]

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.map, CategoryTheory.ShortComplex.RightHomologyMapData.map_φH
-- 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₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h₁.left.IsPreservedBy F
inst_6 : h₁.right.IsPreservedBy F
inst_7 : h₂.left.IsPreservedBy F
inst_8 : h₂.right.IsPreservedBy F
⊢ F.map (homologyMap' φ h₁ h₂) = homologyMap' (Functor.map F.mapShortComplex φ) (h₁.map F) (h₂.map F)

Tactic:
LeftHomologyData.map_leftHomologyMap' _ _ _ _

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.map_leftHomologyMap', CategoryTheory.ShortComplex.LeftHomologyData.map, CategoryTheory.ShortComplex.homologyMap'
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : S.HasLeftHomology
inst_6 : F.PreservesLeftHomologyOf S
⊢ Eq (α := cycles (S.map F) ⟶ F.obj S.X₂)
    (CategoryStruct.comp (Y := F.obj S.cycles) (Iso.hom (S.mapCyclesIso F)) (F.map S.iCycles) :
      cycles (S.map F) ⟶ F.obj S.X₂)
    (iCycles (S.map F) : cycles (S.map F) ⟶ X₂ (S.map F))

Tactic:
apply LeftHomologyData.cyclesIso_hom_comp_i

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i
-- 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
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)
⊢ 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)

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.HasLeftHomology
inst_6 : F.PreservesLeftHomologyOf S
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)))
⊢ 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:
dsimp [mapCyclesIso, cyclesIso]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso, 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 : 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)
    (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:
simp only [map_cyclesMap', ← cyclesMap'_comp, Functor.map_id, comp_id,
    Functor.mapShortComplex_obj]

Premises used: CategoryTheory.ShortComplex.cyclesMap'_comp, CategoryTheory.ShortComplex.LeftHomologyData.map_cyclesMap', 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
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
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)
⊢ 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)

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.HasLeftHomology
inst_6 : F.PreservesLeftHomologyOf S
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)
⊢ 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:
dsimp [mapLeftHomologyIso, leftHomologyIso]

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso, CategoryTheory.ShortComplex.mapLeftHomologyIso