awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
wπ : Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso
    (limit.isLimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
⊢ f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ
have rw : CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' sorry) (kernel.ι γ) =
  Abelian.factorThruImage S.f ≫ S.abelianImageToKernel
Tactic: rw [hf', he]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
wπ : Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso
    (limit.isLimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
⊢ S.LeftHomologyData
have fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ
Tactic: have fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ := by
    rw [hf', he]
    simp only [γ, f', kernel.lift_ι, abelianImageToKernel, ← cancel_mono (kernel.ι S.g),
      assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
f' : S.X₁ ⟶ kernel S.g := kernel.lift S.g S.f ⋯
hf' : f' = CategoryStruct.comp (Y := kernel γ) (kernel.lift γ f' ⋯) (kernel.ι γ)
wπ : Eq (α := S.X₁ ⟶ cokernel (X := kernel γ) (kernel.ι γ)) (f' ≫ cokernel.π (kernel.ι γ)) 0
e : Abelian.image S.f ≅ kernel γ :=
  S.abelianImageToKernelIsKernel.conePointUniqueUpToIso
    (limit.isLimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
he : e.hom ≫ kernel.ι γ = S.abelianImageToKernel
fac : f' = Abelian.factorThruImage S.f ≫ e.hom ≫ kernel.ι γ
⊢ S.LeftHomologyData
have have : (hπ : IsColimit (CokernelCofork.ofπ (cokernel.π (kernel.ι γ)) wπ)) → S.LeftHomologyData
Tactic: have hπ : IsColimit (CokernelCofork.ofπ _ wπ) :=
    CokernelCofork.IsColimit.ofπ _ _
    (fun x hx => cokernel.desc _ x (by
      simpa only [← cancel_epi e.hom, ← cancel_epi (Abelian.factorThruImage S.f),
        comp_zero, fac, assoc] using hx))
    (fun x hx => cokernel.π_desc _ _ _)
    (fun x hx b hb => coequalizer.hom_ext (by simp only [hb, cokernel.π_desc]))
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
⊢ g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
have rw : g' = g'
Tactic: rw [cokernel.π_desc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
⊢ S.RightHomologyData
have hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' sorry)
Tactic: have hg' : g' = cokernel.π γ ≫ cokernel.desc γ g' (by simp [γ, g']) := by rw [cokernel.π_desc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
⊢ Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) (kernel.ι (cokernel.π γ) ≫ g') 0
have rw : Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃)
  (kernel.ι (cokernel.π γ) ≫ CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' sorry)) 0
Tactic: rw [hg', kernel.condition_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
rw :
  Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃)
    (kernel.ι (cokernel.π γ) ≫ CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)) 0
⊢ Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) (kernel.ι (cokernel.π γ) ≫ g') 0
have rw₁ : Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃)
  (CategoryStruct.comp (Y := cokernel γ) 0 (cokernel.desc γ g' sorry)) 0
Tactic: rw [hg', kernel.condition_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
rw :
  Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃)
    (kernel.ι (cokernel.π γ) ≫ CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)) 0
rw₁ :
  Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃)
    (CategoryStruct.comp (Y := cokernel γ) 0 (cokernel.desc γ g' ⋯)) 0
⊢ Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) (kernel.ι (cokernel.π γ) ≫ g') 0
have rw₂ : Eq.{v + 1} (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) 0 0
Tactic: rw [hg', kernel.condition_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
⊢ S.RightHomologyData
have wι : Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) (kernel.ι (cokernel.π γ) ≫ g') 0
Tactic: have wι : kernel.ι (cokernel.π γ) ≫ g' = 0 := by rw [hg', kernel.condition_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
wι : Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) (kernel.ι (cokernel.π γ) ≫ g') 0
e : cokernel γ ≅ Abelian.coimage S.g :=
  IsColimit.coconePointUniqueUpToIso
    (colimit.isColimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
    S.cokernelToAbelianCoimageIsCokernel
⊢ S.RightHomologyData
have he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage
Tactic: have he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage :=
    IsColimit.comp_coconePointUniqueUpToIso_hom _ _ WalkingParallelPair.one
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
wι : Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) (kernel.ι (cokernel.π γ) ≫ g') 0
e : cokernel γ ≅ Abelian.coimage S.g :=
  IsColimit.coconePointUniqueUpToIso
    (colimit.isColimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
    S.cokernelToAbelianCoimageIsCokernel
he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage
⊢ g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g
have rw : CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' sorry) =
  S.cokernelToAbelianCoimage ≫ Abelian.factorThruCoimage S.g
Tactic: rw [hg', reassoc_of% he]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
wι : Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) (kernel.ι (cokernel.π γ) ≫ g') 0
e : cokernel γ ≅ Abelian.coimage S.g :=
  IsColimit.coconePointUniqueUpToIso
    (colimit.isColimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
    S.cokernelToAbelianCoimageIsCokernel
he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage
⊢ S.RightHomologyData
have fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g
Tactic: have fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g := by
    rw [hg', reassoc_of% he]
    simp only [γ, g', cokernel.π_desc, ← cancel_epi (cokernel.π S.f),
      cokernel_π_comp_cokernelToAbelianCoimage_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
γ : kernel S.g ⟶ cokernel S.f := kernel.ι S.g ≫ cokernel.π S.f
g' : cokernel S.f ⟶ S.X₃ := cokernel.desc S.f S.g ⋯
hg' : g' = CategoryStruct.comp (Y := cokernel γ) (cokernel.π γ) (cokernel.desc γ g' ⋯)
wι : Eq (α := kernel (Y := cokernel γ) (cokernel.π γ) ⟶ S.X₃) (kernel.ι (cokernel.π γ) ≫ g') 0
e : cokernel γ ≅ Abelian.coimage S.g :=
  IsColimit.coconePointUniqueUpToIso
    (colimit.isColimit (parallelPair (X := kernel S.g) (Y := cokernel S.f) (kernel.ι S.g ≫ cokernel.π S.f) 0))
    S.cokernelToAbelianCoimageIsCokernel
he : cokernel.π γ ≫ e.hom = S.cokernelToAbelianCoimage
fac : g' = cokernel.π γ ≫ e.hom ≫ Abelian.factorThruCoimage S.g
⊢ S.RightHomologyData
have have : (hι : IsLimit (KernelFork.ofι (kernel.ι (cokernel.π γ)) wι)) → S.RightHomologyData
Tactic: have hι : IsLimit (KernelFork.ofι _ wι) :=
    KernelFork.IsLimit.ofι _ _
      (fun x hx => kernel.lift _ x (by
        simpa only [← cancel_mono e.hom, ← cancel_mono (Abelian.factorThruCoimage S.g), assoc,
          zero_comp, fac] using hx))
      (fun x hx => kernel.lift_ι _ _ _)
      (fun x hx b hb => equalizer.hom_ext (by simp only [hb, kernel.lift_ι]))
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
X Y : ShortComplex.{v, u} C
i : X ⟶ Y
h : Mono i
⊢ NormalMono i
have refine_1 : IsLimit (F := parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ π₁) (Functor.mapCone π₁ (KernelFork.ofι i sorry))
Tactic: refine NormalMono.mk _ (cokernel.π i) (cokernel.condition _)
    (isLimitOfIsLimitπ _ ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
X Y : ShortComplex.{v, u} C
i : X ⟶ Y
h : Mono i
refine_1 : IsLimit (F := parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ π₁) (Functor.mapCone π₁ (KernelFork.ofι i ⋯))
⊢ NormalMono i
have refine_2 : IsLimit (F := parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ π₂) (Functor.mapCone π₂ (KernelFork.ofι i sorry))
Tactic: refine NormalMono.mk _ (cokernel.π i) (cokernel.condition _)
    (isLimitOfIsLimitπ _ ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
X Y : ShortComplex.{v, u} C
i : X ⟶ Y
h : Mono i
refine_1 : IsLimit (F := parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ π₁) (Functor.mapCone π₁ (KernelFork.ofι i ⋯))
refine_2 : IsLimit (F := parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ π₂) (Functor.mapCone π₂ (KernelFork.ofι i ⋯))
⊢ NormalMono i
have refine_3 : IsLimit (F := parallelPair (Y := cokernel i) (cokernel.π i) 0 ⋙ π₃) (Functor.mapCone π₃ (KernelFork.ofι i sorry))
Tactic: refine NormalMono.mk _ (cokernel.π i) (cokernel.condition _)
    (isLimitOfIsLimitπ _ ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
X Y : ShortComplex.{v, u} C
p : X ⟶ Y
h : Epi p
⊢ NormalEpi p
have refine_1 : IsColimit (F := parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ π₁) (Functor.mapCocone π₁ (CokernelCofork.ofπ p sorry))
Tactic: refine NormalEpi.mk _ (kernel.ι p) (kernel.condition _)
    (isColimitOfIsColimitπ _ ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
X Y : ShortComplex.{v, u} C
p : X ⟶ Y
h : Epi p
refine_1 :
  IsColimit (F := parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ π₁) (Functor.mapCocone π₁ (CokernelCofork.ofπ p ⋯))
⊢ NormalEpi p
have refine_2 : IsColimit (F := parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ π₂) (Functor.mapCocone π₂ (CokernelCofork.ofπ p sorry))
Tactic: refine NormalEpi.mk _ (kernel.ι p) (kernel.condition _)
    (isColimitOfIsColimitπ _ ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} D
X Y : ShortComplex.{v, u} C
p : X ⟶ Y
h : Epi p
refine_1 :
  IsColimit (F := parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ π₁) (Functor.mapCocone π₁ (CokernelCofork.ofπ p ⋯))
refine_2 :
  IsColimit (F := parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ π₂) (Functor.mapCocone π₂ (CokernelCofork.ofπ p ⋯))
⊢ NormalEpi p
have refine_3 : IsColimit (F := parallelPair (X := kernel p) (kernel.ι p) 0 ⋙ π₃) (Functor.mapCocone π₃ (CokernelCofork.ofπ p sorry))
Tactic: refine NormalEpi.mk _ (kernel.ι p) (kernel.condition _)
    (isColimitOfIsColimitπ _ ?_ ?_ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : HasZeroMorphisms.{v', u'} 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_4 : Epi π
inst_5 : Mono ι
⊢ H ≅ image (X := S.cycles) (Y := S.opcycles) (S.iCycles ≫ S.pOpcycles)
have this : Eq (α := S.cycles ⟶ S.opcycles) ((Iso.inv (S.isoCyclesOfIsLimit hkf) ≫ π) ≫ ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc))
  (S.iCycles ≫ S.pOpcycles)
Tactic: have : ((S.isoCyclesOfIsLimit hkf).inv ≫ π) ≫ ι ≫
    (S.isoOpcyclesOfIsColimit hcc).hom = S.iCycles ≫ S.pOpcycles := by
    simp [← reassoc_of% fac]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
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_2 : Epi π
inst_3 : Mono ι
⊢ (isoImage S hkf hcc fac).hom ≫ image.ι (S.iCycles ≫ S.pOpcycles) = ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)
have comm : Eq (α := S.cycles ⟶ S.opcycles) ((Iso.inv (S.isoCyclesOfIsLimit hkf) ≫ π) ≫ ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc))
  (S.iCycles ≫ S.pOpcycles)
Tactic: apply image.isoStrongEpiMono_hom_comp_ι
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
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_2 : Epi π
inst_3 : Mono ι
⊢ π ≫ (isoHomology S hkf hcc fac).hom = Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ
have dsimp : π ≫ (isoImage S hkf hcc fac).hom ≫ S.homologyIsoImageICyclesCompPOpcycles.inv =
  Iso.hom (S.isoCyclesOfIsLimit hkf) ≫ S.homologyπ
Tactic: dsimp [isoHomology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
kf : KernelFork S.g
hkf : IsLimit kf
⊢ hkf.lift (KernelFork.ofι S.f ⋯) = CategoryStruct.comp (Y := S.cycles) S.toCycles (Iso.inv (S.isoCyclesOfIsLimit hkf))
have this : Mono (Fork.ι kf)
Tactic: have := Fork.IsLimit.mono hkf
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
cc : CokernelCofork S.f
hcc : IsColimit cc
⊢ hcc.desc (CokernelCofork.ofπ S.g ⋯) =
    CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc)) S.fromOpcycles
have this : Epi (Cofork.π cc)
Tactic: have := Cofork.IsColimit.epi hcc
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
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_2 : Epi π
inst_3 : Mono ι
⊢ (isoHomology S hkf hcc fac).hom ≫ S.homologyι = ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)
have rw : ((isoHomology S hkf hcc fac).hom ≫ S.homologyι) ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) =
  CategoryStruct.comp (Y := S.opcycles) (ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc))
    (Iso.inv (S.isoOpcyclesOfIsColimit hcc))
Tactic: rw [← cancel_mono (S.isoOpcyclesOfIsColimit hcc).inv, assoc, assoc, Iso.hom_inv_id,
    comp_id, ← isoHomology_hom_comp_ι S hkf hcc fac, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
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_2 : Epi π
inst_3 : Mono ι
rw :
  ((isoHomology S hkf hcc fac).hom ≫ S.homologyι) ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) =
    CategoryStruct.comp (Y := S.opcycles) (ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc))
      (Iso.inv (S.isoOpcyclesOfIsColimit hcc))
⊢ (isoHomology S hkf hcc fac).hom ≫ S.homologyι = ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)
have rw₁ : (isoHomology S hkf hcc fac).hom ≫ S.homologyι ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) =
  CategoryStruct.comp (Y := S.opcycles) (ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc))
    (Iso.inv (S.isoOpcyclesOfIsColimit hcc))
Tactic: rw [← cancel_mono (S.isoOpcyclesOfIsColimit hcc).inv, assoc, assoc, Iso.hom_inv_id,
    comp_id, ← isoHomology_hom_comp_ι S hkf hcc fac, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
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_2 : Epi π
inst_3 : Mono ι
rw :
  ((isoHomology S hkf hcc fac).hom ≫ S.homologyι) ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) =
    CategoryStruct.comp (Y := S.opcycles) (ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc))
      (Iso.inv (S.isoOpcyclesOfIsColimit hcc))
rw₁ :
  (isoHomology S hkf hcc fac).hom ≫ S.homologyι ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) =
    CategoryStruct.comp (Y := S.opcycles) (ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc))
      (Iso.inv (S.isoOpcyclesOfIsColimit hcc))
⊢ (isoHomology S hkf hcc fac).hom ≫ S.homologyι = ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)
have rw₂ : (isoHomology S hkf hcc fac).hom ≫ S.homologyι ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) =
  ι ≫
    CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc))
      (Iso.inv (S.isoOpcyclesOfIsColimit hcc))
Tactic: rw [← cancel_mono (S.isoOpcyclesOfIsColimit hcc).inv, assoc, assoc, Iso.hom_inv_id,
    comp_id, ← isoHomology_hom_comp_ι S hkf hcc fac, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
S : ShortComplex.{v, u} C
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_2 : Epi π
inst_3 : Mono ι
rw :
  ((isoHomology S hkf hcc fac).hom ≫ S.homologyι) ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) =
    CategoryStruct.comp (Y := S.opcycles) (ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc))
      (Iso.inv (S.isoOpcyclesOfIsColimit hcc))
rw₁ :
  (isoHomology S hkf hcc fac).hom ≫ S.homologyι ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) =
    CategoryStruct.comp (Y := S.opcycles) (ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc))
      (Iso.inv (S.isoOpcyclesOfIsColimit hcc))
rw₂ :
  (isoHomology S hkf hcc fac).hom ≫ S.homologyι ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) =
    ι ≫
      CategoryStruct.comp (Y := S.opcycles) (Iso.hom (S.isoOpcyclesOfIsColimit hcc))
        (Iso.inv (S.isoOpcyclesOfIsColimit hcc))
⊢ (isoHomology S hkf hcc fac).hom ≫ S.homologyι = ι ≫ Iso.hom (S.isoOpcyclesOfIsColimit hcc)
have rw₃ : (isoHomology S hkf hcc fac).hom ≫ S.homologyι ≫ Iso.inv (S.isoOpcyclesOfIsColimit hcc) = ι ≫ 𝟙 cc.pt
Tactic: rw [← cancel_mono (S.isoOpcyclesOfIsColimit hcc).inv, assoc, assoc, Iso.hom_inv_id,
    comp_id, ← isoHomology_hom_comp_ι S hkf hcc fac, Iso.hom_inv_id_assoc]