mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
ψ : LeftHomologyMapData φ h₁ h₂
⊢ (ψ.φH.unop ≫ h₁.unop.ι).op = (h₂.unop.ι ≫ ψ.φK.unop).op

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (ψ.φQ.op ≫ h₁.op.i).unop = (h₂.op.i ≫ (opMap φ).τ₂).unop

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (h₂.op.f' ≫ ψ.φQ.op).unop = ((opMap φ).τ₁ ≫ h₁.op.f').unop

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (h₂.op.π ≫ ψ.φH.op).unop = (ψ.φQ.op ≫ h₁.op.π).unop

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (ψ.φQ.unop ≫ h₁.unop.i).op = (h₂.unop.i ≫ (unopMap φ).τ₂).op

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (h₂.unop.f' ≫ ψ.φQ.unop).op = ((unopMap φ).τ₁ ≫ h₁.unop.f').op

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁✝ S₂✝ S₃ : ShortComplex C
S₁ S₂ : ShortComplex Cᵒᵖ
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
⊢ (h₂.unop.π ≫ ψ.φH.unop).op = (ψ.φQ.unop ≫ h₁.unop.π).op

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝¹ : S.HasLeftHomology
inst✝ : HasKernel S.g
⊢ S.iCycles ≫ S.g = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝¹ : S.HasLeftHomology
inst✝ : HasKernel S.g
⊢ kernel.ι S.g ≫ S.g = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A : C
k : A ⟶ S.X₂
hk : k ≫ S.g = 0
inst✝¹ : S.HasLeftHomology
φ : S ⟶ S₁
inst✝ : S₁.HasLeftHomology
⊢ (k ≫ φ.τ₂) ≫ S₁.g = 0

Tactic:
by rw [assoc, φ.comm₂₃, reassoc_of% hk, zero_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S S₁ S₂ : ShortComplex C
h : S.LeftHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesLimit (parallelPair S.g 0) F
this : PreservesColimit (parallelPair h.f' 0) F
wi : F.map h.i ≫ F.map S.g = 0
hi : IsLimit ((KernelFork.ofι h.i ⋯).map F)
f' : F.obj S.X₁ ⟶ F.obj h.K := hi.lift (KernelFork.ofι (S.map F).f ⋯)
hf' : f' = F.map h.f'
wπ : f' ≫ F.map h.π = 0
⊢ (parallelPair f' 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair f' 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair f' 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (F.map h.f') 0).map WalkingParallelPairHom.right

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.LeftHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasLeftHomology
inst✝ : HasKernel S.g
h : S.LeftHomologyData := S.leftHomologyData
this : HasColimit (parallelPair h.f' 0)
⊢ (parallelPair (kernel.lift S.g S.f ⋯) 0).map WalkingParallelPairHom.right ≫
      ((kernelIsKernel S.g).conePointUniqueUpToIso h.hi).hom =
    (Iso.refl ((parallelPair (kernel.lift S.g S.f ⋯) 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair h.f' 0).map WalkingParallelPairHom.right

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst✝ : S.HasHomology
⊢ S.iCycles ≫ S.g = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst✝ : S.HasHomology
⊢ S.f ≫ S.pOpcycles = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
⊢ S.f ≫ cokernel.π S.f = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.RightHomologyData
A : C
k : S.X₂ ⟶ A
hk : S.f ≫ k = 0
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
⊢ S.f ≫ S.pOpcycles = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
S S₁ S₂ : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : 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 ((CokernelCofork.ofπ h.p ⋯).map F)
g' : F.obj h.Q ⟶ F.obj S.X₃ := hp.desc (CokernelCofork.ofπ (S.map F).g ⋯)
hg' : g' = F.map h.g'
wι : F.map h.ι ≫ g' = 0
⊢ (parallelPair g' 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.one)).hom =
    (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair (F.map h.g') 0).map WalkingParallelPairHom.right

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
this : HasLimit (parallelPair h.g' 0)
⊢ coequalizer.π S.f 0 ≫
      (parallelPair (cokernel.desc S.f S.g ⋯) 0).map WalkingParallelPairHom.left ≫
        (Iso.refl ((parallelPair (cokernel.desc S.f S.g ⋯) 0).obj WalkingParallelPair.one)).hom =
    coequalizer.π S.f 0 ≫
      ((colimit.isColimit (parallelPair S.f 0)).coconePointUniqueUpToIso h.hp).hom ≫
        (parallelPair h.g' 0).map WalkingParallelPairHom.left

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasRightHomology
inst✝ : HasCokernel S.f
h : S.RightHomologyData := S.rightHomologyData
this : HasLimit (parallelPair h.g' 0)
⊢ (parallelPair (cokernel.desc S.f S.g ⋯) 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair (cokernel.desc S.f S.g ⋯) 0).obj WalkingParallelPair.one)).hom =
    ((colimit.isColimit (parallelPair S.f 0)).coconePointUniqueUpToIso h.hp).hom ≫
      (parallelPair h.g' 0).map WalkingParallelPairHom.right

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
j : J
⊢ limit.π (F ⋙ π₁) j ≫ (F.obj j).f =
    (((const J).obj
              { X₁ := limit (F ⋙ π₁), X₂ := limit (F ⋙ π₂), X₃ := limit (F ⋙ π₃), f := limMap (F.whiskerLeft π₁Toπ₂),
                g := limMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).obj
          j).f ≫
      limit.π (F ⋙ π₂) j

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasLimit (F ⋙ π₁)
inst✝¹ : HasLimit (F ⋙ π₂)
inst✝ : HasLimit (F ⋙ π₃)
j : J
⊢ limit.π (F ⋙ π₂) j ≫ (F.obj j).g =
    (((const J).obj
              { X₁ := limit (F ⋙ π₁), X₂ := limit (F ⋙ π₂), X₃ := limit (F ⋙ π₃), f := limMap (F.whiskerLeft π₁Toπ₂),
                g := limMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).obj
          j).g ≫
      limit.π (F ⋙ π₃) j

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
⊢ S.abelianImageToKernel ≫ kernel.ι S.g ≫ cokernel.π S.f = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ F.map (hₗ.i ≫ hᵣ.p) = (hₗ.map F).i ≫ (hᵣ.map F).p

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ (hₗ.map F).π ≫ leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F) ≫ (hᵣ.map F).ι =
    (Cofork.π (CokernelCofork.ofπ (hₗ.map F).π ⋯) ≫ leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)) ≫
      Fork.ι (KernelFork.ofι (hᵣ.map F).ι ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : h.IsPreservedBy F
h' : S.LeftHomologyData
this : PreservesColimit (parallelPair h.f' 0) F
⊢ (parallelPair h.f' 0).map WalkingParallelPairHom.left ≫ (ShortComplex.cyclesMapIso' (Iso.refl S) h h').hom =
    (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair h'.f' 0).map WalkingParallelPairHom.left

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
h : S.LeftHomologyData
inst✝ : h.IsPreservedBy F
h' : S.LeftHomologyData
this : PreservesColimit (parallelPair h.f' 0) F
⊢ (parallelPair h.f' 0).map WalkingParallelPairHom.right ≫ (ShortComplex.cyclesMapIso' (Iso.refl S) h h').hom =
    (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair h'.f' 0).map WalkingParallelPairHom.right

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
h : S.RightHomologyData
inst✝ : h.IsPreservedBy F
h' : S.RightHomologyData
this : PreservesLimit (parallelPair h.g' 0) F
⊢ (parallelPair h.g' 0).map WalkingParallelPairHom.left ≫
      (Iso.refl ((parallelPair h.g' 0).obj WalkingParallelPair.one)).hom =
    (ShortComplex.opcyclesMapIso' (Iso.refl S) h h').hom ≫ (parallelPair h'.g' 0).map WalkingParallelPairHom.left

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
h : S.RightHomologyData
inst✝ : h.IsPreservedBy F
h' : S.RightHomologyData
this : PreservesLimit (parallelPair h.g' 0) F
⊢ (parallelPair h.g' 0).map WalkingParallelPairHom.right ≫
      (Iso.refl ((parallelPair h.g' 0).obj WalkingParallelPair.one)).hom =
    (ShortComplex.opcyclesMapIso' (Iso.refl S) h h').hom ≫ (parallelPair h'.g' 0).map WalkingParallelPairHom.right

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' (φ - φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ - leftHomologyMap' φ' h₁ h₂

Tactic:
by
  simp only [sub_eq_add_neg, leftHomologyMap'_add, leftHomologyMap'_neg]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (kernel.ι S.g ≫ cokernel.π S.f) ≫ S.cokernelToAbelianCoimage = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
⊢ F.map (leftHomologyMap' φ hl₁ hl₂) = leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)

Tactic:
γ.leftHomologyMap'_eq,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : hl₁.IsPreservedBy F
inst✝ : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
⊢ F.map γ.φH = leftHomologyMap' (F.mapShortComplex.map φ) (hl₁.map F) (hl₂.map F)
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Category.{v_2, u_2} D
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ (S.map F).pOpcycles ≫ opcyclesMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (S.rightHomologyData.map F) =
    (S.map F).pOpcycles ≫
      opcyclesMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (hr.map F) ≫
        F.map (opcyclesMap' (𝟙 S) hr S.rightHomologyData)

Tactic:
simp only [map_opcyclesMap', ← opcyclesMap'_comp, Functor.map_id, comp_id,
    Functor.mapShortComplex_obj]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
j : J
⊢ colimit.ι (F ⋙ π₁) j ≫
      (((const J).obj
              { X₁ := colimit (F ⋙ π₁), X₂ := colimit (F ⋙ π₂), X₃ := colimit (F ⋙ π₃),
                f := colimMap (F.whiskerLeft π₁Toπ₂), g := colimMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).obj
          j).f =
    (F.obj j).f ≫ colimit.ι (F ⋙ π₂) j

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
inst✝² : HasColimit (F ⋙ π₁)
inst✝¹ : HasColimit (F ⋙ π₂)
inst✝ : HasColimit (F ⋙ π₃)
j : J
⊢ colimit.ι (F ⋙ π₂) j ≫
      (((const J).obj
              { X₁ := colimit (F ⋙ π₁), X₂ := colimit (F ⋙ π₂), X₃ := colimit (F ⋙ π₃),
                f := colimMap (F.whiskerLeft π₁Toπ₂), g := colimMap (F.whiskerLeft π₂Toπ₃), zero := ⋯ }).obj
          j).g =
    (F.obj j).g ≫ colimit.ι (F ⋙ π₃) j

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
S : ShortComplex C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ (Iso.refl kf.pt).hom ≫ Fork.ι (KernelFork.ofι (Fork.ι kf) ⋯) = Fork.ι kf

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
S : ShortComplex C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ Cofork.π cc ≫ (Iso.refl cc.pt).hom = Cofork.π (CokernelCofork.ofπ (Cofork.π cc) ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.ι f.op ≫ f.op).unop = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (f.op ≫ cokernel.π f.op).unop = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.ι g.unop).op = eqToHom ⋯ ≫ cokernel.π g ≫ (kernelUnopOp g).inv

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π g.unop).op = (cokernelUnopOp g).hom ≫ kernel.ι g ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ F.map (adj.unit.app P ≫ G.map f) ≫ adj.counit.app X✝ = f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝¹ : HasProduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ∏ᶜ c
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ Pi.lift fun b ↦ factorThru (g ≫ Pi.π c b) f) = g

Tactic:
ext b

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
β : Type v
c : β → C
inst✝¹ : HasProduct c
inst✝ : ∀ (b : β), Injective (c b)
X✝ Y✝ : C
g : X✝ ⟶ ∏ᶜ c
f : X✝ ⟶ Y✝
mono : Mono f
b : β
⊢ (f ≫ Pi.lift fun b ↦ factorThru (g ≫ Pi.π c b) f) ≫ Pi.π c b = g ≫ Pi.π c b
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : Cᵒᵖ
inst✝ : Projective P
X✝ Y✝ : C
g : X✝ ⟶ unop P
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ (Projective.factorThru g.op f.op).unop).op = g.op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Cᵒᵖ
inst✝ : Injective J
E✝ X✝ : C
f : unop J ⟶ X✝
e : E✝ ⟶ X✝
he : Epi e
⊢ ((factorThru f.op e.op).unop ≫ e).op = f.op

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : C
inst✝ : Injective J
E✝ X✝ : Cᵒᵖ
f : op J ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ ((factorThru f.unop e.unop).op ≫ e).unop = f.unop

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.LeftHomologyData
⊢ S.f = 0

Tactic:
hf

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hf : S.f = 0
inst✝ : PreservesLimit (parallelPair S.g 0) F
h : S.LeftHomologyData
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : C
inst✝ : Projective P
X✝ Y✝ : Cᵒᵖ
g : X✝ ⟶ op P
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ (Projective.factorThru g.unop f.unop).op).unop = g.unop

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
this : IsIso h.i
⊢ (parallelPair h.f' 0).map WalkingParallelPairHom.left ≫ (asIso h.i).hom =
    (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)).hom ≫
      (parallelPair S.f 0).map WalkingParallelPairHom.left

Tactic:
simp

Goal state after: