awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
S : ShortComplex.{v_1, u_1} C
⊢ 𝟙 S ≫ 𝟙 S = 𝟙 S

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
e : S₁.HomotopyEquiv S₂
e' : S₂.HomotopyEquiv S₃
⊢ (e.hom ≫ e'.hom) ≫ e'.inv ≫ e.inv = e.hom ≫ (e'.hom ≫ e'.inv) ≫ e.inv

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
e : S₁.HomotopyEquiv S₂
e' : S₂.HomotopyEquiv S₃
⊢ e.hom ≫ 𝟙 S₂ ≫ e.inv = e.hom ≫ e.inv

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
e : S₁.HomotopyEquiv S₂
e' : S₂.HomotopyEquiv S₃
⊢ (e'.inv ≫ e.inv) ≫ e.hom ≫ e'.hom = e'.inv ≫ (e.inv ≫ e.hom) ≫ e'.hom

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ : ShortComplex.{v_1, u_1} C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
e : S₁.HomotopyEquiv S₂
e' : S₂.HomotopyEquiv S₃
⊢ e'.inv ≫ 𝟙 S₂ ≫ e'.hom = e'.inv ≫ e'.hom

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
rw : k ≫ S.g + k' ≫ S.g = 0
rw₁ : 0 + k' ≫ S.g = 0
rw₂ : HAdd.hAdd (α := A ⟶ S.X₃) 0 0 = 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := A ⟶ S.X₃) 0 0
⊢ (k + k') ≫ S.g = 0

Tactic:
rw [add_comp, hk, hk', add_zero]

Premises used: CategoryTheory.Preadditive.add_comp, add_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
⊢ HAdd.hAdd (α := A ⟶ S.cycles) (S.liftCycles k hk) (S.liftCycles k' hk') = S.liftCycles (k + k') ⋯

Tactic:
simp only [← cancel_mono S.iCycles, liftCycles_i, add_comp]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Preadditive.add_comp, CategoryTheory.ShortComplex.liftCycles_i, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ S₃ S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
rw : k ≫ S.g - k' ≫ S.g = 0
rw₁ : 0 - k' ≫ S.g = 0
rw₂ : HSub.hSub (α := A ⟶ S.X₃) 0 0 = 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := A ⟶ S.X₃) 0 0
⊢ (k - k') ≫ S.g = 0

Tactic:
rw [sub_comp, hk, hk', sub_zero]

Premises used: sub_zero, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
⊢ HSub.hSub (α := A ⟶ S.cycles) (S.liftCycles k hk) (S.liftCycles k' hk') = S.liftCycles (k - k') ⋯

Tactic:
simp only [← cancel_mono S.iCycles, liftCycles_i, sub_comp]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.liftCycles_i, CategoryTheory.ShortComplex.iCycles, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : F.PreservesHomology
X Y : C
f : X ⟶ Y
⊢ PreservesLimit (parallelPair f 0) F

Tactic:
PreservesHomology.preservesKernels _

Premises used: CategoryTheory.Functor.PreservesHomology.preservesKernels
-- 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
inst_5 : F.PreservesHomology
X Y : C
f : X ⟶ Y
⊢ PreservesColimit (parallelPair f 0) F

Tactic:
PreservesHomology.preservesCokernels _

Premises used: CategoryTheory.Functor.PreservesHomology.preservesCokernels
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
⊢ PreservesLimit (parallelPair S.g 0) F

Tactic:
@IsPreservedBy.g _ _ _ _ _ _ _ h F _ _

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.g
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
⊢ PreservesColimit (parallelPair h.f' 0) F

Tactic:
IsPreservedBy.f'

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.IsPreservedBy.f'
-- 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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
rw :
  Eq (α := X₁ (S.map F) ⟶ X₂ (S.map F))
    (CategoryStruct.comp (Y := K (S := S.map F) (h.map F)) (f' (h.map F)) (i (h.map F))) (F.map h.f' ≫ i (h.map F))
rw₁ : Eq (α := X₁ (S.map F) ⟶ X₂ (S.map F)) (f (S.map F)) (F.map h.f' ≫ i (h.map F))
rw₂ : F.map S.f = F.map h.f' ≫ i (h.map F)
rw₃ : F.map S.f = F.map h.f' ≫ F.map h.i
rw₄ : F.map S.f = F.map (h.f' ≫ h.i)
rw₅ rw₆ : F.map S.f = F.map S.f
⊢ f' (h.map F) = F.map h.f'

Tactic:
rw [← cancel_mono (h.map F).i, f'_i, map_f, map_i, ← F.map_comp, f'_i]

Premises used: CategoryTheory.ShortComplex.map_f, CategoryTheory.ShortComplex.LeftHomologyData.map, CategoryTheory.ShortComplex.LeftHomologyData.map_i, CategoryTheory.ShortComplex.LeftHomologyData.f'_i, CategoryTheory.cancel_mono, CategoryTheory.Functor.map_comp, CategoryTheory.ShortComplex.LeftHomologyData.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 S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h₁.IsPreservedBy F
inst_6 : h₂.IsPreservedBy F
⊢ Eq (α :=
    LeftHomologyData.K (S := Functor.obj F.mapShortComplex S₁) (h₁.map F : LeftHomologyData (S₁.map F)) ⟶
      X₂ (Functor.obj F.mapShortComplex S₂))
    (F.map ψ.φK ≫ LeftHomologyData.i (h₂.map F))
    (LeftHomologyData.i (h₁.map F) ≫ Hom.τ₂ (Functor.map F.mapShortComplex φ))

Tactic:
simpa only [F.map_comp] using F.congr_map ψ.commi

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map, CategoryTheory.ShortComplex.LeftHomologyMapData.commi
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h₁.IsPreservedBy F
inst_6 : h₂.IsPreservedBy F
⊢ Eq (α :=
    X₁ (Functor.obj F.mapShortComplex S₁) ⟶
      LeftHomologyData.K (S := Functor.obj F.mapShortComplex S₂) (h₂.map F : LeftHomologyData (S₂.map F)))
    (LeftHomologyData.f' (h₁.map F) ≫ F.map ψ.φK :
      X₁ (Functor.obj F.mapShortComplex S₁) ⟶
        LeftHomologyData.K (S := Functor.obj F.mapShortComplex S₂) (h₂.map F : LeftHomologyData (S₂.map F)))
    (Hom.τ₁ (Functor.map F.mapShortComplex φ) ≫ LeftHomologyData.f' (h₂.map F) :
      X₁ (Functor.obj F.mapShortComplex S₁) ⟶
        LeftHomologyData.K (S := Functor.obj F.mapShortComplex S₂) (h₂.map F : LeftHomologyData (S₂.map F)))

Tactic:
simpa only [LeftHomologyData.map_f', F.map_comp] using F.congr_map ψ.commf'

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.commf', CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map, CategoryTheory.ShortComplex.LeftHomologyData.map_f'
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h₁.IsPreservedBy F
inst_6 : h₂.IsPreservedBy F
⊢ Eq (α :=
    LeftHomologyData.K (S := Functor.obj F.mapShortComplex S₁) (h₁.map F : LeftHomologyData (S₁.map F)) ⟶
      LeftHomologyData.H (S := Functor.obj F.mapShortComplex S₂) (h₂.map F : LeftHomologyData (S₂.map F)))
    (LeftHomologyData.π (h₁.map F) ≫ F.map ψ.φH) (F.map ψ.φK ≫ LeftHomologyData.π (h₂.map F))

Tactic:
simpa only [F.map_comp] using F.congr_map ψ.commπ

Premises used: CategoryTheory.ShortComplex.LeftHomologyMapData.commπ, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_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 : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
⊢ PreservesColimit (parallelPair S.f 0) F

Tactic:
@IsPreservedBy.f _ _ _ _ _ _ _ h F _ _

Premises used: CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.f
-- 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.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
⊢ PreservesLimit (parallelPair h.g' 0) F

Tactic:
@IsPreservedBy.g' _ _ _ _ _ _ _ h F _ _

Premises used: CategoryTheory.ShortComplex.RightHomologyData.IsPreservedBy.g'
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
⊢ PreservesColimit (parallelPair S.f 0) F

Tactic:
have := IsPreservedBy.hf h F
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this : PreservesColimit (parallelPair S.f 0) F
⊢ PreservesLimit (parallelPair h.g' 0) F

Tactic:
have := IsPreservedBy.hg' h F
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
rw : F.map (S.f ≫ h.p) = 0
rw₁ : Eq (α := F.obj S.X₁ ⟶ F.obj h.Q) (F.map 0) 0
rw₂ rw₃ : Eq.{v_2 + 1} (α := F.obj S.X₁ ⟶ F.obj h.Q) 0 0
⊢ F.map S.f ≫ F.map h.p = 0

Tactic:
rw [← F.map_comp, h.wp, F.map_zero]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.wp, CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
⊢ F.map S.f ≫ F.map h.p = 0

Tactic:
have wp : F.map S.f ≫ F.map h.p = 0 := by rw [← F.map_comp, h.wp, F.map_zero]
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
have :
  (hp : IsColimit (F := parallelPair (F.map S.f) 0) ((CokernelCofork.ofπ h.p ⋯).map F)) → RightHomologyData (S.map F)
⊢ RightHomologyData (S.map F)

Tactic:
have hp := CokernelCofork.mapIsColimit _ h.hp F
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit (F := parallelPair (F.map S.f) 0) ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (Z := X₃ (S.map F)) (g (S.map F)) ⋯)
apply : Cofork.π ((CokernelCofork.ofπ h.p ⋯).map F) ≫ g' = Cofork.π ((CokernelCofork.ofπ h.p ⋯).map F) ≫ F.map h.g'
⊢ g' = F.map h.g'

Tactic:
apply Cofork.IsColimit.hom_ext hp

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_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 S₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit (F := parallelPair (F.map S.f) 0) ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (Z := X₃ (S.map F)) (g (S.map F)) ⋯)
rw :
  Eq (α := F.obj S.X₂ ⟶ F.obj S.X₃)
    (Cofork.π (CokernelCofork.ofπ (Z := X₃ (S.map F)) (g (S.map F)) ⋯) :
      F.obj S.X₂ ⟶
        Cocone.pt (F := parallelPair (F.map S.f) 0)
          (CokernelCofork.ofπ (Z := X₃ (S.map F)) (g (S.map F)) ⋯ : CokernelCofork (F.map S.f)))
    (Cofork.π ((CokernelCofork.ofπ h.p ⋯).map F) ≫ F.map h.g' : F.obj S.X₂ ⟶ F.obj S.X₃)
⊢ Cofork.π ((CokernelCofork.ofπ h.p ⋯).map F) ≫ g' = Cofork.π ((CokernelCofork.ofπ h.p ⋯).map F) ≫ F.map h.g'

Tactic:
rw [Cofork.IsColimit.π_desc hp]

Premises used: CategoryTheory.Limits.Cofork.IsColimit.π_desc
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit (F := parallelPair (F.map S.f) 0) ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (Z := X₃ (S.map F)) (g (S.map F)) ⋯)
⊢ Eq (α := F.obj S.X₂ ⟶ F.obj S.X₃)
    (Cofork.π (CokernelCofork.ofπ (Z := X₃ (S.map F)) (g (S.map F)) ⋯) :
      F.obj S.X₂ ⟶
        Cocone.pt (F := parallelPair (F.map S.f) 0)
          (CokernelCofork.ofπ (Z := X₃ (S.map F)) (g (S.map F)) ⋯ : CokernelCofork (F.map S.f)))
    (Cofork.π ((CokernelCofork.ofπ h.p ⋯).map F) ≫ F.map h.g' : F.obj S.X₂ ⟶ F.obj S.X₃)

Tactic:
simp only [Cofork.π_ofπ, CokernelCofork.map_π, map_g, ← F.map_comp, p_g']

Premises used: CategoryTheory.ShortComplex.map_g, CategoryTheory.Limits.CokernelCofork.map_π, CategoryTheory.Functor.map_comp, CategoryTheory.Limits.Cofork.π_ofπ, CategoryTheory.ShortComplex.RightHomologyData.p_g'
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit (F := parallelPair (F.map S.f) 0) ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (Z := X₃ (S.map F)) (g (S.map F)) ⋯)
⊢ g' = F.map h.g'

Tactic:
have hg' : g' = F.map h.g' := by
    apply Cofork.IsColimit.hom_ext hp
    rw [Cofork.IsColimit.π_desc hp]
    simp only [Cofork.π_ofπ, CokernelCofork.map_π, map_g, ← F.map_comp, p_g']
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit (F := parallelPair (F.map S.f) 0) ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (Z := X₃ (S.map F)) (g (S.map F)) ⋯)
hg' : g' = F.map h.g'
rw : F.map h.ι ≫ F.map h.g' = 0
rw₁ : F.map (h.ι ≫ h.g') = 0
rw₂ : Eq (α := F.obj h.H ⟶ F.obj S.X₃) (F.map 0) 0
rw₃ rw₄ : Eq.{v_2 + 1} (α := F.obj h.H ⟶ F.obj S.X₃) 0 0
⊢ F.map h.ι ≫ g' = 0

Tactic:
rw [hg', ← F.map_comp, ι_g', F.map_zero]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.ι_g', CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit (F := parallelPair (F.map S.f) 0) ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (Z := X₃ (S.map F)) (g (S.map F)) ⋯)
hg' : g' = F.map h.g'
⊢ F.map h.ι ≫ g' = 0

Tactic:
have wι : F.map h.ι ≫ g' = 0 := by rw [hg', ← F.map_comp, ι_g', F.map_zero]
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit (F := parallelPair (F.map S.f) 0) ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (Z := X₃ (S.map F)) (g (S.map F)) ⋯)
hg' : g' = F.map h.g'
wι : F.map h.ι ≫ g' = 0
⊢ (parallelPair g' 0).map WalkingParallelPairHom.left ≫
      Iso.hom (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair (F.map h.g') 0).map WalkingParallelPairHom.left

Tactic:
simpa using hg'
-- 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₁ S₂ : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
this_1 : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
wp : F.map S.f ≫ F.map h.p = 0
hp : IsColimit (F := parallelPair (F.map S.f) 0) ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (Z := X₃ (S.map F)) (g (S.map F)) ⋯)
hg' : g' = F.map h.g'
wι : F.map h.ι ≫ g' = 0
⊢ (parallelPair g' 0).map WalkingParallelPairHom.right ≫
      Iso.hom (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair (F.map h.g') 0).map WalkingParallelPairHom.right

Tactic:
simp