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
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
e : parallelPair g' 0 ≅ parallelPair (F.map h.g') 0 :=
  parallelPair.ext (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.zero))
    (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.one)) ⋯ ⋯
refine : (KernelFork.ofι h.ι ⋯).map F ≅ (Cone.postcompose e.hom).obj (KernelFork.ofι (F.map h.ι) wι)
⊢ IsLimit (KernelFork.ofι (F.map h.ι) wι)

Tactic:
refine IsLimit.postcomposeHomEquiv e _
      (IsLimit.ofIsoLimit (KernelFork.mapIsLimit _ h.hι' F) ?_)

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, CategoryTheory.Limits.KernelFork.mapIsLimit, CategoryTheory.ShortComplex.RightHomologyData.hι', CategoryTheory.Limits.IsLimit.ofIsoLimit, DFunLike.coe
-- 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
e : parallelPair g' 0 ≅ parallelPair (F.map h.g') 0 :=
  parallelPair.ext (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.zero))
    (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ Iso.hom (Iso.refl (Cone.pt (F := parallelPair (F.map h.g') 0) ((KernelFork.ofι h.ι ⋯).map F))) ≫
      Fork.ι ((Cone.postcompose e.hom).obj (KernelFork.ofι (F.map h.ι) wι)) =
    Fork.ι ((KernelFork.ofι h.ι ⋯).map F)

Tactic:
simp [e]
-- 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
e : parallelPair g' 0 ≅ parallelPair (F.map h.g') 0 :=
  parallelPair.ext (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.zero))
    (Iso.refl ((parallelPair g' 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ (KernelFork.ofι h.ι ⋯).map F ≅ (Cone.postcompose e.hom).obj (KernelFork.ofι (F.map h.ι) wι)

Tactic:
exact Fork.ext (Iso.refl _) (by simp [e])

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Fork.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)) ⋯)
hg' : g' = F.map h.g'
wι : F.map h.ι ≫ g' = 0
have : (hι : IsLimit (KernelFork.ofι (F.map h.ι) wι)) → RightHomologyData (S.map F)
⊢ RightHomologyData (S.map F)

Tactic:
have hι : IsLimit (KernelFork.ofι (F.map h.ι) wι) := by
    let e : parallelPair g' 0 ≅ parallelPair (F.map h.g') 0 :=
      parallelPair.ext (Iso.refl _) (Iso.refl _) (by simpa using hg') (by simp)
    refine IsLimit.postcomposeHomEquiv e _
      (IsLimit.ofIsoLimit (KernelFork.mapIsLimit _ h.hι' F) ?_)
    exact Fork.ext (Iso.refl _) (by simp [e])
-- 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
hι : IsLimit (KernelFork.ofι (F.map h.ι) wι)
⊢ RightHomologyData (S.map F)

Tactic:
exact
    { Q := F.obj h.Q
      H := F.obj h.H
      p := F.map h.p
      ι := F.map h.ι
      wp := wp
      hp := hp
      wι := wι
      hι := 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 : 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
rw :
  Eq (α := X₂ (S.map F) ⟶ X₃ (S.map F))
    (CategoryStruct.comp (Y := Q (S := S.map F) (h.map F)) (p (h.map F)) (g' (h.map F))) (p (h.map F) ≫ F.map h.g')
rw₁ : Eq (α := X₂ (S.map F) ⟶ X₃ (S.map F)) (g (S.map F)) (p (h.map F) ≫ F.map h.g')
rw₂ : F.map S.g = p (h.map F) ≫ F.map h.g'
rw₃ : F.map S.g = F.map h.p ≫ F.map h.g'
rw₄ : F.map S.g = F.map (h.p ≫ h.g')
rw₅ rw₆ : F.map S.g = F.map S.g
⊢ g' (h.map F) = F.map h.g'

Tactic:
rw [← cancel_epi (h.map F).p, p_g', map_g, map_p, ← F.map_comp, p_g']

Premises used: CategoryTheory.ShortComplex.RightHomologyData.map, CategoryTheory.ShortComplex.map_g, CategoryTheory.ShortComplex.RightHomologyData.map_p, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.RightHomologyData.p, 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
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ 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₁) ⟶
      RightHomologyData.Q (S := Functor.obj F.mapShortComplex S₂) (h₂.map F : RightHomologyData (S₂.map F)))
    (RightHomologyData.p (h₁.map F) ≫ F.map ψ.φQ :
      X₂ (Functor.obj F.mapShortComplex S₁) ⟶
        RightHomologyData.Q (S := Functor.obj F.mapShortComplex S₂) (h₂.map F : RightHomologyData (S₂.map F)))
    (Hom.τ₂ (Functor.map F.mapShortComplex φ) ≫ RightHomologyData.p (h₂.map F) :
      X₂ (Functor.obj F.mapShortComplex S₁) ⟶
        RightHomologyData.Q (S := Functor.obj F.mapShortComplex S₂) (h₂.map F : RightHomologyData (S₂.map F)))

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

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map, CategoryTheory.ShortComplex.RightHomologyMapData.commp
-- 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₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ 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 (α :=
    RightHomologyData.Q (S := Functor.obj F.mapShortComplex S₁) (h₁.map F : RightHomologyData (S₁.map F)) ⟶
      X₃ (Functor.obj F.mapShortComplex S₂))
    (F.map ψ.φQ ≫ RightHomologyData.g' (h₂.map F))
    (RightHomologyData.g' (h₁.map F) ≫ Hom.τ₃ (Functor.map F.mapShortComplex φ))

Tactic:
simpa only [RightHomologyData.map_g', F.map_comp] using F.congr_map ψ.commg'

Premises used: CategoryTheory.ShortComplex.RightHomologyData.map_g', CategoryTheory.ShortComplex.RightHomologyMapData.commg', 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 S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ 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 (α :=
    RightHomologyData.H (S := Functor.obj F.mapShortComplex S₁) (h₁.map F : RightHomologyData (S₁.map F)) ⟶
      RightHomologyData.Q (S := Functor.obj F.mapShortComplex S₂) (h₂.map F : RightHomologyData (S₂.map F)))
    (F.map ψ.φH ≫ RightHomologyData.ι (h₂.map F)) (RightHomologyData.ι (h₁.map F) ≫ F.map ψ.φQ)

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

Premises used: CategoryTheory.ShortComplex.RightHomologyMapData.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 S₁ S₂ : ShortComplex.{v_1, u_1} C
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
⊢ Eq (α := LeftHomologyData.K (S := S.map F) (h.left.map F) ⟶ RightHomologyData.Q (S := S.map F) (h.right.map F))
    (LeftHomologyData.π (h.left.map F) ≫ (F.mapIso h.iso).hom ≫ RightHomologyData.ι (h.right.map F))
    (LeftHomologyData.i (h.left.map F) ≫ RightHomologyData.p (h.right.map F))

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

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map, CategoryTheory.ShortComplex.HomologyData.comm
-- 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
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst_5 : hₗ.IsPreservedBy F
inst_6 : hᵣ.IsPreservedBy F
apply :
  Eq (α := LeftHomologyData.K (S := S.map F) (hₗ.map F) ⟶ F.obj hᵣ.H)
    (Cofork.π (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) ⋯) ≫ F.map (leftRightHomologyComparison' hₗ hᵣ))
    (CategoryStruct.comp (Y :=
      Cocone.pt (F :=
        parallelPair (X :=
          Cone.pt (F := parallelPair (X := X₂ (S.map F)) (g (S.map F)) 0) (KernelFork.ofι (f (S.map F)) ⋯)) (Y :=
          LeftHomologyData.K (S := S.map F) (hₗ.map F))
          (IsLimit.lift (LeftHomologyData.hi (hₗ.map F)) (KernelFork.ofι (f (S.map F)) ⋯) :
            Cone.pt (F := parallelPair (X := X₂ (S.map F)) (g (S.map F)) 0) (KernelFork.ofι (f (S.map F)) ⋯) ⟶
              Cone.pt (F := parallelPair (X := X₂ (S.map F)) (g (S.map F)) 0)
                (KernelFork.ofι (Z := LeftHomologyData.K (S := S.map F) (hₗ.map F)) (LeftHomologyData.i (hₗ.map F)) ⋯))
          0)
        (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) ⋯))
      (Cofork.π (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) ⋯))
      (leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)))
⊢ F.map (leftRightHomologyComparison' hₗ hᵣ) = leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)

Tactic:
apply Cofork.IsColimit.hom_ext (hₗ.map F).hπ

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext, CategoryTheory.ShortComplex.LeftHomologyData.hπ, CategoryTheory.ShortComplex.LeftHomologyData.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
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst_5 : hₗ.IsPreservedBy F
inst_6 : hᵣ.IsPreservedBy F
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F :=
        parallelPair (X := RightHomologyData.Q (S := S.map F) (hᵣ.map F)) (Y :=
          Cocone.pt (F := parallelPair (X := X₁ (S.map F)) (f (S.map F)) 0) (CokernelCofork.ofπ (g (S.map F)) ⋯))
          (IsColimit.desc (RightHomologyData.hp (hᵣ.map F)) (CokernelCofork.ofπ (g (S.map F)) ⋯) :
            Cocone.pt (F := parallelPair (X := X₁ (S.map F)) (f (S.map F)) 0)
                (CokernelCofork.ofπ (Z := RightHomologyData.Q (S := S.map F) (hᵣ.map F))
                  (RightHomologyData.p (hᵣ.map F)) ⋯) ⟶
              Cocone.pt (F := parallelPair (X := X₁ (S.map F)) (f (S.map F)) 0) (CokernelCofork.ofπ (g (S.map F)) ⋯))
          0)
        (KernelFork.ofι (RightHomologyData.ι (hᵣ.map F)) ⋯))
      (Cofork.π (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) ⋯) ≫ F.map (leftRightHomologyComparison' hₗ hᵣ))
      (Fork.ι (KernelFork.ofι (RightHomologyData.ι (hᵣ.map F)) ⋯)) =
    F.map (hₗ.i ≫ hᵣ.p)

Tactic:
simp [← Functor.map_comp]

Premises used: 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 : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst_5 : hₗ.IsPreservedBy F
inst_6 : hᵣ.IsPreservedBy F
rw : F.map (hₗ.i ≫ hᵣ.p) = LeftHomologyData.i (hₗ.map F) ≫ RightHomologyData.p (hᵣ.map F)
⊢ F.map (hₗ.i ≫ hᵣ.p) =
    CategoryStruct.comp (Y := LeftHomologyData.H (S := S.map F) (hₗ.map F)) (LeftHomologyData.π (hₗ.map F))
      (CategoryStruct.comp (Y := RightHomologyData.H (S := S.map F) (hᵣ.map F))
        (leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)) (RightHomologyData.ι (hᵣ.map F)))

Tactic:
rw [ShortComplex.π_leftRightHomologyComparison'_ι]

Premises used: CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι
-- 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
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst_5 : hₗ.IsPreservedBy F
inst_6 : hᵣ.IsPreservedBy F
⊢ F.map (hₗ.i ≫ hᵣ.p) = LeftHomologyData.i (hₗ.map F) ≫ RightHomologyData.p (hᵣ.map F)

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
S : ShortComplex.{v_1, u_1} C
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst_5 : hₗ.IsPreservedBy F
inst_6 : hᵣ.IsPreservedBy F
⊢ Eq (α := F.obj hₗ.K ⟶ F.obj hᵣ.Q)
    (CategoryStruct.comp (Y := LeftHomologyData.H (S := S.map F) (hₗ.map F)) (LeftHomologyData.π (hₗ.map F))
        (CategoryStruct.comp (Y := RightHomologyData.H (S := S.map F) (hᵣ.map F))
          (leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)) (RightHomologyData.ι (hᵣ.map F))) :
      F.obj hₗ.K ⟶ F.obj hᵣ.Q)
    (CategoryStruct.comp (Y :=
        Cone.pt (F :=
          parallelPair (X := RightHomologyData.Q (S := S.map F) (hᵣ.map F)) (Y :=
            Cocone.pt (F := parallelPair (X := X₁ (S.map F)) (f (S.map F)) 0) (CokernelCofork.ofπ (g (S.map F)) ⋯))
            (IsColimit.desc (RightHomologyData.hp (hᵣ.map F)) (CokernelCofork.ofπ (g (S.map F)) ⋯) :
              Cocone.pt (F := parallelPair (X := X₁ (S.map F)) (f (S.map F)) 0)
                  (CokernelCofork.ofπ (Z := RightHomologyData.Q (S := S.map F) (hᵣ.map F))
                    (RightHomologyData.p (hᵣ.map F)) ⋯) ⟶
                Cocone.pt (F := parallelPair (X := X₁ (S.map F)) (f (S.map F)) 0) (CokernelCofork.ofπ (g (S.map F)) ⋯))
            0)
          (KernelFork.ofι (RightHomologyData.ι (hᵣ.map F)) ⋯))
        (CategoryStruct.comp (Y :=
          Cocone.pt (F :=
            parallelPair (X :=
              Cone.pt (F := parallelPair (X := X₂ (S.map F)) (g (S.map F)) 0) (KernelFork.ofι (f (S.map F)) ⋯)) (Y :=
              LeftHomologyData.K (S := S.map F) (hₗ.map F))
              (IsLimit.lift (LeftHomologyData.hi (hₗ.map F)) (KernelFork.ofι (f (S.map F)) ⋯) :
                Cone.pt (F := parallelPair (X := X₂ (S.map F)) (g (S.map F)) 0) (KernelFork.ofι (f (S.map F)) ⋯) ⟶
                  Cone.pt (F := parallelPair (X := X₂ (S.map F)) (g (S.map F)) 0)
                    (KernelFork.ofι (Z := LeftHomologyData.K (S := S.map F) (hₗ.map F)) (LeftHomologyData.i (hₗ.map F))
                      ⋯))
              0)
            (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) ⋯))
          (Cofork.π (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) ⋯))
          (leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)))
        (Fork.ι (KernelFork.ofι (RightHomologyData.ι (hᵣ.map F)) ⋯)) :
      LeftHomologyData.K (S := S.map F) (hₗ.map F) ⟶ RightHomologyData.Q (S := S.map F) (hᵣ.map F))

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 S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_5 : F.PreservesHomology
⊢ F.PreservesLeftHomologyOf S

Tactic:
⟨inferInstance⟩

Premises used: CategoryTheory.Functor.PreservesLeftHomologyOf.mk, inferInstance
-- 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 S₁ S₂ : ShortComplex.{v_1, u_1} C
inst_5 : F.PreservesHomology
⊢ F.PreservesRightHomologyOf S

Tactic:
⟨inferInstance⟩

Premises used: CategoryTheory.Functor.PreservesRightHomologyOf.mk, inferInstance
-- 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.LeftHomologyData
inst_5 : h.IsPreservedBy F
h' : S.LeftHomologyData
⊢ PreservesColimit (parallelPair h.f' 0) F

Tactic:
have := ShortComplex.LeftHomologyData.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
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.LeftHomologyData
inst_5 : 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.hom (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair h'.f' 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.LeftHomologyData
inst_5 : 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.hom (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair h'.f' 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.LeftHomologyData
inst_5 : h.IsPreservedBy F
h' : S.LeftHomologyData
this : PreservesColimit (parallelPair h.f' 0) F
e : parallelPair h.f' 0 ≅ parallelPair h'.f' 0 :=
  parallelPair.ext (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero))
    (ShortComplex.cyclesMapIso' (Iso.refl S) h h') ⋯ ⋯
⊢ PreservesColimit (parallelPair h'.f' 0) F

Tactic:
preservesColimit_of_iso_diagram F e

Premises used: CategoryTheory.Limits.preservesColimit_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.LeftHomologyData
inst_5 : h.IsPreservedBy F
h' : S.LeftHomologyData
this : PreservesColimit (parallelPair h.f' 0) F
e : parallelPair h.f' 0 ≅ parallelPair h'.f' 0 :=
  parallelPair.ext (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero))
    (ShortComplex.cyclesMapIso' (Iso.refl S) h h') ⋯ ⋯
⊢ PreservesColimit (parallelPair h'.f' 0) F

Tactic:
exact preservesColimit_of_iso_diagram F e

Premises used: CategoryTheory.Limits.preservesColimit_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
⊢ PreservesLimit (parallelPair h.g' 0) F

Tactic:
have := ShortComplex.RightHomologyData.IsPreservedBy.hg' h F