awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ 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'
have apply : Cofork.π ((CokernelCofork.ofπ h.p sorry).map F) ≫ g' = Cofork.π ((CokernelCofork.ofπ h.p sorry).map F) ≫ F.map h.g'
Tactic: apply Cofork.IsColimit.hom_ext hp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ 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)) ⋯)
⊢ Cofork.π ((CokernelCofork.ofπ h.p ⋯).map F) ≫ g' = Cofork.π ((CokernelCofork.ofπ h.p ⋯).map F) ≫ F.map h.g'
have rw : Eq (α := F.obj S.X₂ ⟶ F.obj S.X₃)
  (Cofork.π (CokernelCofork.ofπ (Z := X₃ (S.map F)) (g (S.map F)) sorry) :
    F.obj S.X₂ ⟶
      Cocone.pt (F := parallelPair (F.map S.f) 0)
        (CokernelCofork.ofπ (Z := X₃ (S.map F)) (g (S.map F)) sorry : CokernelCofork (F.map S.f)))
  (Cofork.π ((CokernelCofork.ofπ h.p sorry).map F) ≫ F.map h.g' : F.obj S.X₂ ⟶ F.obj S.X₃)
Tactic: rw [Cofork.IsColimit.π_desc hp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (hypothesis)
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)) ⋯)
⊢ RightHomologyData (S.map F)
have hg' : 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']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ 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
have rw : F.map h.ι ≫ F.map h.g' = 0
Tactic: rw [hg', ← F.map_comp, ι_g', F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ 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
⊢ F.map h.ι ≫ g' = 0
have rw₁ : F.map (h.ι ≫ h.g') = 0
Tactic: rw [hg', ← F.map_comp, ι_g', F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ 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
⊢ F.map h.ι ≫ g' = 0
have rw₂ : Eq (α := F.obj h.H ⟶ F.obj S.X₃) (F.map 0) 0
Tactic: rw [hg', ← F.map_comp, ι_g', F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ 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
⊢ F.map h.ι ≫ g' = 0
have rw₃ : Eq.{v_2 + 1} (α := F.obj h.H ⟶ F.obj S.X₃) 0 0
Tactic: rw [hg', ← F.map_comp, ι_g', F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (hypothesis)
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'
⊢ RightHomologyData (S.map F)
have wι : F.map h.ι ≫ g' = 0
Tactic: have wι : F.map h.ι ≫ g' = 0 := by rw [hg', ← F.map_comp, ι_g', F.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ 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)) ⋯ ⋯
⊢ IsLimit (KernelFork.ofι (F.map h.ι) wι)
have refine : (KernelFork.ofι h.ι sorry).map F ≅ (Cone.postcompose e.hom).obj (KernelFork.ofι (F.map h.ι) wι)
Tactic: refine IsLimit.postcomposeHomEquiv e _
      (IsLimit.ofIsoLimit (KernelFork.mapIsLimit _ h.hι' F) ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S S₁ 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
⊢ RightHomologyData (S.map F)
have have : (hι : IsLimit (KernelFork.ofι (F.map h.ι) wι)) → 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])
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
h : S.RightHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : h.IsPreservedBy F
⊢ g' (h.map F) = F.map h.g'
have 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')
Tactic: rw [← cancel_epi (h.map F).p, p_g', map_g, map_p, ← F.map_comp, p_g']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
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')
⊢ g' (h.map F) = F.map h.g'
have rw₁ : Eq (α := X₂ (S.map F) ⟶ X₃ (S.map F)) (g (S.map F)) (p (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']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
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')
⊢ g' (h.map F) = F.map h.g'
have rw₂ : F.map S.g = p (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']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
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'
⊢ g' (h.map F) = F.map h.g'
have rw₃ : F.map S.g = F.map h.p ≫ F.map h.g'
Tactic: rw [← cancel_epi (h.map F).p, p_g', map_g, map_p, ← F.map_comp, p_g']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
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'
⊢ g' (h.map F) = F.map h.g'
have rw₄ : F.map S.g = F.map (h.p ≫ h.g')
Tactic: rw [← cancel_epi (h.map F).p, p_g', map_g, map_p, ← F.map_comp, p_g']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
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')
⊢ g' (h.map F) = F.map h.g'
have rw₅ : F.map S.g = F.map S.g
Tactic: rw [← cancel_epi (h.map F).p, p_g', map_g, map_p, ← F.map_comp, p_g']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
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 (leftRightHomologyComparison' hₗ hᵣ) = leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)
have apply : Eq (α := LeftHomologyData.K (S := S.map F) (hₗ.map F) ⟶ F.obj hᵣ.H)
  (Cofork.π (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) sorry) ≫ 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)) sorry)) (Y :=
        LeftHomologyData.K (S := S.map F) (hₗ.map F))
        (IsLimit.lift (LeftHomologyData.hi (hₗ.map F)) (KernelFork.ofι (f (S.map F)) sorry) :
          Cone.pt (F := parallelPair (X := X₂ (S.map F)) (g (S.map F)) 0) (KernelFork.ofι (f (S.map F)) sorry) ⟶
            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)) sorry))
        0)
      (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) sorry))
    (Cofork.π (CokernelCofork.ofπ (LeftHomologyData.π (hₗ.map F)) sorry))
    (leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)))
Tactic: apply Cofork.IsColimit.hom_ext (hₗ.map F).hπ
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
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) =
    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)) ⋯))
have trans : 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: trans (hₗ.map F).π ≫ ShortComplex.leftRightHomologyComparison'
    (hₗ.map F) (hᵣ.map F) ≫ (hᵣ.map F).ι
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
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) =
    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)))
have rw : F.map (hₗ.i ≫ hᵣ.p) = LeftHomologyData.i (hₗ.map F) ≫ RightHomologyData.p (hᵣ.map F)
Tactic: rw [ShortComplex.π_leftRightHomologyComparison'_ι]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (hypothesis)
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
have this : PreservesColimit (parallelPair h.f' 0) F
Tactic: have := ShortComplex.LeftHomologyData.IsPreservedBy.hf' h F
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (hypothesis)
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
have this : PreservesLimit (parallelPair h.g' 0) F
Tactic: have := ShortComplex.RightHomologyData.IsPreservedBy.hg' h F
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hl₁.IsPreservedBy F
inst_6 : hl₂.IsPreservedBy F
⊢ F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
have have : ∀ (γ : LeftHomologyMapData φ hl₁ hl₂),
  F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
Tactic: have γ : ShortComplex.LeftHomologyMapData φ hl₁ hl₂ := default
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hl₁.IsPreservedBy F
inst_6 : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
⊢ F.map (cyclesMap' φ hl₁ hl₂) = cyclesMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
have rw : F.map γ.φK = cyclesMap' (Functor.map F.mapShortComplex φ) (hl₁.map F) (hl₂.map F)
Tactic: rw [γ.cyclesMap'_eq, (γ.map F).cyclesMap'_eq, ShortComplex.LeftHomologyMapData.map_φK]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.PreservesHomology (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroMorphisms.{v_2, u_2} D
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
hl₁ : S₁.LeftHomologyData
hl₂ : S₂.LeftHomologyData
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : hl₁.IsPreservedBy F
inst_6 : hl₂.IsPreservedBy F
γ : LeftHomologyMapData φ hl₁ hl₂
rw : F.map γ.φK = 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)
have rw₁ : F.map γ.φK = LeftHomologyMapData.φK (γ.map F)
Tactic: rw [γ.cyclesMap'_eq, (γ.map F).cyclesMap'_eq, ShortComplex.LeftHomologyMapData.map_φK]