awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
⊢ S.Exact ↔ Mono S.g
have mp : S.Exact → Mono S.g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
mp : S.Exact → Mono S.g
⊢ S.Exact ↔ Mono S.g
have mpr : Mono S.g → S.Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
h : S.Exact
⊢ Mono S.g
have this : S.HasHomology
Tactic: have := h.hasHomology
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
h : S.Exact
this : S.HasHomology
⊢ Mono S.g
have h₁ : IsZero.{v_1, u_1} S.homology
Tactic: simp only [exact_iff_isZero_homology] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
this : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
⊢ Mono S.g
have this₁ : IsIso (Y := S.opcycles) S.pOpcycles
Tactic: have := S.isIso_pOpcycles hf
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
this_1 : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
this : IsIso (Y := S.opcycles) S.pOpcycles
⊢ Mono S.g
have this₁ : Mono (X := S.opcycles) S.fromOpcycles
Tactic: have := mono_of_isZero_kernel' _ S.homologyIsKernel h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
this_1 : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
this_2 : IsIso (Y := S.opcycles) S.pOpcycles
this : Mono (X := S.opcycles) S.fromOpcycles
⊢ Mono S.g
have mp : Mono (CategoryStruct.comp (Y := S.opcycles) S.pOpcycles S.fromOpcycles)
Tactic: rw [← S.p_fromOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hf : S.f = 0
h : Mono S.g
⊢ S.Exact
have mpr : IsZero.{v_1, u_1}
  (HomologyData.ofIsLimitKernelFork S hf (KernelFork.ofι (Z := 0) 0 sorry)
        (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι (Z := 0) 0 sorry) sorry sorry)).left.H
Tactic: rw [(HomologyData.ofIsLimitKernelFork S hf _
      (KernelFork.IsLimit.ofMonoOfIsZero (KernelFork.ofι (0 : 0 ⟶ S.X₂) zero_comp)
        inferInstance (isZero_zero C))).exact_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
⊢ S.Exact ↔ Epi S.f
have mp : S.Exact → Epi S.f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
mp : S.Exact → Epi S.f
⊢ S.Exact ↔ Epi S.f
have mpr : Epi S.f → S.Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
h : S.Exact
⊢ Epi S.f
have this : S.HasHomology
Tactic: have := h.hasHomology
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
h : S.Exact
this : S.HasHomology
⊢ Epi S.f
have h₁ : IsZero.{v_1, u_1} S.homology
Tactic: simp only [exact_iff_isZero_homology] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
this : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
⊢ Epi S.f
have this₁ : IsIso (X := S.cycles) S.iCycles
Tactic: haveI := S.isIso_iCycles hg
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
this_1 : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
this : IsIso (X := S.cycles) S.iCycles
⊢ Epi S.f
have this₁ : Epi (Y := S.cycles) S.toCycles
Tactic: haveI : Epi S.toCycles := epi_of_isZero_cokernel' _ S.homologyIsCokernel h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
this_1 : S.HasHomology
h : IsZero.{v_1, u_1} S.homology
this_2 : IsIso (X := S.cycles) S.iCycles
this : Epi (Y := S.cycles) S.toCycles
⊢ Epi S.f
have mp : Epi (CategoryStruct.comp (Y := S.cycles) S.toCycles S.iCycles)
Tactic: rw [← S.toCycles_i]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
hg : S.g = 0
h : Epi S.f
⊢ S.Exact
have mpr : IsZero.{v_1, u_1}
  (HomologyData.ofIsColimitCokernelCofork S hg (CokernelCofork.ofπ (Z := 0) 0 sorry)
        (CokernelCofork.IsColimit.ofEpiOfIsZero (CokernelCofork.ofπ (Z := 0) 0 sorry) sorry sorry)).left.H
Tactic: rw [(HomologyData.ofIsColimitCokernelCofork S hg _
      (CokernelCofork.IsColimit.ofEpiOfIsZero (CokernelCofork.ofπ (0 : S.X₂ ⟶ 0) comp_zero)
        inferInstance (isZero_zero C))).exact_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
h : S.LeftHomologyData
⊢ IsZero.{v_1, u_1} (CokernelCofork.ofπ h.π ⋯).pt
have this : S.HasHomology
Tactic: haveI := hS.hasHomology
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
h : S.LeftHomologyData
this : S.HasHomology
⊢ IsZero.{v_1, u_1} (CokernelCofork.ofπ h.π ⋯).pt
have dsimp : IsZero.{v_1, u_1} h.H
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
h : S.RightHomologyData
⊢ IsZero.{v_1, u_1} (KernelFork.ofι h.ι ⋯).pt
have this : S.HasHomology
Tactic: haveI := hS.hasHomology
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
h : S.RightHomologyData
this : S.HasHomology
⊢ IsZero.{v_1, u_1} (KernelFork.ofι h.ι ⋯).pt
have dsimp : IsZero.{v_1, u_1} h.H
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.LeftHomologyData
⊢ S.Exact ↔ Epi h.f'
have mp : S.Exact → Epi h.f'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.LeftHomologyData
mp : S.Exact → Epi h.f'
⊢ S.Exact ↔ Epi h.f'
have mpr : Epi h.f' → S.Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.RightHomologyData
⊢ S.Exact ↔ Mono h.g'
have mp : S.Exact → Mono h.g'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
h : S.RightHomologyData
mp : S.Exact → Mono h.g'
⊢ S.Exact ↔ Mono h.g'
have mpr : Mono h.g' → S.Exact
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (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 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
kf : KernelFork S.g
hkf : IsLimit kf
⊢ Epi (X := (KernelFork.ofι S.f ⋯).pt) ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))
have this : S.HasHomology
Tactic: have := hS.hasHomology
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (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 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
kf : KernelFork S.g
hkf : IsLimit kf
this : S.HasHomology
⊢ Epi (X := (KernelFork.ofι S.f ⋯).pt) ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))
have refine : Arrow.mk (Y := S.cycles) S.toCycles ≅
  Arrow.mk (X := (KernelFork.ofι S.f sorry).pt) ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) sorry)).lift (KernelFork.ofι S.f sorry))
Tactic: refine ((MorphismProperty.epimorphisms C).arrow_mk_iso_iff ?_).1
      hS.epi_toCycles
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (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 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
kf : KernelFork S.g
hkf : IsLimit kf
this : S.HasHomology
⊢ Arrow.mk (Y := S.cycles) S.toCycles ≅
    Arrow.mk (X := (KernelFork.ofι S.f ⋯).pt)
      ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))
have refine : Iso.hom (Iso.refl (Arrow.mk (Y := S.cycles) S.toCycles).left) ≫
    (Arrow.mk (X := (KernelFork.ofι S.f sorry).pt)
        ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) sorry)).lift (KernelFork.ofι S.f sorry))).hom =
  (Arrow.mk (Y := S.cycles) S.toCycles).hom ≫ Iso.hom (IsLimit.conePointUniqueUpToIso S.cyclesIsKernel hkf)
Tactic: refine Arrow.isoMk (Iso.refl _)
      (IsLimit.conePointUniqueUpToIso S.cyclesIsKernel hkf) ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (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 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
kf : KernelFork S.g
hkf : IsLimit kf
this : S.HasHomology
⊢ Iso.hom (Iso.refl (Arrow.mk (Y := S.cycles) S.toCycles).left) ≫
      (Arrow.mk (X := (KernelFork.ofι S.f ⋯).pt)
          ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))).hom =
    (Arrow.mk (Y := S.cycles) S.toCycles).hom ≫ Iso.hom (IsLimit.conePointUniqueUpToIso S.cyclesIsKernel hkf)
have apply : (Iso.hom (Iso.refl (Arrow.mk (Y := S.cycles) S.toCycles).left) ≫
      (Arrow.mk (X := (KernelFork.ofι S.f sorry).pt)
          ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) sorry)).lift (KernelFork.ofι S.f sorry))).hom) ≫
    Fork.ι kf =
  ((Arrow.mk (Y := S.cycles) S.toCycles).hom ≫ Iso.hom (IsLimit.conePointUniqueUpToIso S.cyclesIsKernel hkf)) ≫
    Fork.ι kf
Tactic: apply Fork.IsLimit.hom_ext hkf
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (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 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
cc : CokernelCofork S.f
hcc : IsColimit cc
⊢ Mono (Y := (CokernelCofork.ofπ S.g ⋯).pt)
    ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))
have this : S.HasHomology
Tactic: have := hS.hasHomology
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (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 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
cc : CokernelCofork S.f
hcc : IsColimit cc
this : S.HasHomology
⊢ Mono (Y := (CokernelCofork.ofπ S.g ⋯).pt)
    ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))
have refine : Arrow.mk (Y := (CokernelCofork.ofπ S.g sorry).pt)
    ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) sorry)).desc (CokernelCofork.ofπ S.g sorry)) ≅
  Arrow.mk (X := S.opcycles) S.fromOpcycles
Tactic: refine ((MorphismProperty.monomorphisms C).arrow_mk_iso_iff ?_).2
      hS.mono_fromOpcycles
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (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 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
cc : CokernelCofork S.f
hcc : IsColimit cc
this : S.HasHomology
⊢ Arrow.mk (Y := (CokernelCofork.ofπ S.g ⋯).pt)
      ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯)) ≅
    Arrow.mk (X := S.opcycles) S.fromOpcycles
have refine : Iso.hom (hcc.coconePointUniqueUpToIso S.opcyclesIsCokernel) ≫ (Arrow.mk (X := S.opcycles) S.fromOpcycles).hom =
  (Arrow.mk (Y := (CokernelCofork.ofπ S.g sorry).pt)
        ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) sorry)).desc (CokernelCofork.ofπ S.g sorry))).hom ≫
    Iso.hom
      (Iso.refl
        (Arrow.mk (Y := (CokernelCofork.ofπ S.g sorry).pt)
            ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) sorry)).desc (CokernelCofork.ofπ S.g sorry))).right)
Tactic: refine Arrow.isoMk (IsColimit.coconePointUniqueUpToIso hcc S.opcyclesIsCokernel)
      (Iso.refl _) ?_
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (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 : Preadditive.{v_1, u_1} C
inst_3 : Preadditive.{v_2, u_2} D
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
inst_4 : HasZeroObject.{v_1, u_1} C
cc : CokernelCofork S.f
hcc : IsColimit cc
this : S.HasHomology
⊢ Iso.hom (hcc.coconePointUniqueUpToIso S.opcyclesIsCokernel) ≫ (Arrow.mk (X := S.opcycles) S.fromOpcycles).hom =
    (Arrow.mk (Y := (CokernelCofork.ofπ S.g ⋯).pt)
          ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).hom ≫
      Iso.hom
        (Iso.refl
          (Arrow.mk (Y := (CokernelCofork.ofπ S.g ⋯).pt)
              ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) ⋯)).desc (CokernelCofork.ofπ S.g ⋯))).right)
have apply : Cofork.π cc ≫
    Iso.hom (hcc.coconePointUniqueUpToIso S.opcyclesIsCokernel) ≫ (Arrow.mk (X := S.opcycles) S.fromOpcycles).hom =
  Cofork.π cc ≫
    (Arrow.mk (Y := (CokernelCofork.ofπ S.g sorry).pt)
          ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) sorry)).desc (CokernelCofork.ofπ S.g sorry))).hom ≫
      Iso.hom
        (Iso.refl
          (Arrow.mk (Y := (CokernelCofork.ofπ S.g sorry).pt)
              ((hcc.ofIsoColimit (Cofork.ext (Iso.refl cc.pt) sorry)).desc (CokernelCofork.ofπ S.g sorry))).right)
Tactic: apply Cofork.IsColimit.hom_ext hcc
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasKernel S.g
⊢ S.Exact ↔ Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯)
have rw : Epi (Y := S.cycles) S.toCycles ↔ Epi (Y := kernel S.g) (kernel.lift S.g S.f sorry)
Tactic: rw [exact_iff_epi_toCycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasKernel S.g
⊢ Epi (Y := S.cycles) S.toCycles ↔ Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯)
have apply : Arrow.mk (Y := S.cycles) S.toCycles ≅ Arrow.mk (Y := kernel S.g) (kernel.lift S.g S.f sorry)
Tactic: apply (MorphismProperty.epimorphisms C).arrow_mk_iso_iff
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasCokernel S.f
⊢ S.Exact ↔ Mono (X := cokernel S.f) (cokernel.desc S.f S.g ⋯)
have rw : Mono (X := S.opcycles) S.fromOpcycles ↔ Mono (X := cokernel S.f) (cokernel.desc S.f S.g sorry)
Tactic: rw [exact_iff_mono_fromOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
inst_2 : S.HasHomology
inst_3 : HasCokernel S.f
⊢ Mono (X := S.opcycles) S.fromOpcycles ↔ Mono (X := cokernel S.f) (cokernel.desc S.f S.g ⋯)
have refine : Arrow.mk (X := cokernel S.f) (cokernel.desc S.f S.g sorry) ≅ Arrow.mk (X := S.opcycles) S.fromOpcycles
Tactic: refine (MorphismProperty.monomorphisms C).arrow_mk_iso_iff (Iso.symm ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S₁ S₂ : ShortComplex.{v_1, u_1} C
φ : S₁ ⟶ S₂
inst_2 : S₁.HasHomology
inst_3 : S₂.HasHomology
inst_4 : QuasiIso φ
⊢ S₁.Exact ↔ S₂.Exact
have simp : IsZero.{v_1, u_1} S₁.homology ↔ IsZero.{v_1, u_1} S₂.homology
Tactic: simp only [exact_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst_2 : S.HasHomology
⊢ S.Exact
have rw : Epi (Y := S.cycles) S.toCycles
Tactic: rw [exact_iff_epi_toCycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst_2 : S.HasHomology
⊢ Eq (α := S.cycles ⟶ S.cycles)
    (hS.lift (KernelFork.ofι (Z := S.cycles) S.iCycles ⋯) ≫ S.toCycles : S.cycles ⟶ S.cycles)
    (𝟙 S.cycles : S.cycles ⟶ S.cycles)
have rw : Eq (α := S.cycles ⟶ S.X₂) (hS.lift (KernelFork.ofι (Z := S.cycles) S.iCycles sorry) ≫ S.f : S.cycles ⟶ S.X₂)
  (S.iCycles : S.cycles ⟶ S.X₂)
Tactic: rw [← cancel_mono S.iCycles, assoc, toCycles_i, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst_2 : S.HasHomology
⊢ Epi (Y := S.cycles) S.toCycles
have this : IsSplitEpi (Y := S.cycles) S.toCycles
Tactic: have : IsSplitEpi S.toCycles :=
    ⟨⟨{ section_ := hS.lift (KernelFork.ofι S.iCycles S.iCycles_g)
        id := by
          rw [← cancel_mono S.iCycles, assoc, toCycles_i, id_comp]
          exact Fork.IsLimit.lift_ι hS }⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst_2 : S.HasHomology
⊢ S.Exact
have rw : Mono (X := S.opcycles) S.fromOpcycles
Tactic: rw [exact_iff_mono_fromOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst_2 : S.HasHomology
⊢ Eq (α := S.opcycles ⟶ S.opcycles)
    (S.fromOpcycles ≫ hS.desc (CokernelCofork.ofπ (Z := S.opcycles) S.pOpcycles ⋯) : S.opcycles ⟶ S.opcycles)
    (𝟙 S.opcycles : S.opcycles ⟶ S.opcycles)
have rw : Eq (α := S.X₂ ⟶ S.opcycles) (S.g ≫ hS.desc (CokernelCofork.ofπ (Z := S.opcycles) S.pOpcycles sorry) : S.X₂ ⟶ S.opcycles)
  (S.pOpcycles : S.X₂ ⟶ S.opcycles)
Tactic: rw [← cancel_epi S.pOpcycles, p_fromOpcycles_assoc, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst_2 : S.HasHomology
⊢ Mono (X := S.opcycles) S.fromOpcycles
have this : IsSplitMono (X := S.opcycles) S.fromOpcycles
Tactic: have : IsSplitMono S.fromOpcycles :=
    ⟨⟨{ retraction := hS.desc (CokernelCofork.ofπ S.pOpcycles S.f_pOpcycles)
        id := by
          rw [← cancel_epi S.pOpcycles, p_fromOpcycles_assoc, comp_id]
          exact Cofork.IsColimit.π_desc hS }⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : S.f = 0
⊢ Mono S.g
have this : S.HasHomology
Tactic: have := hS.hasHomology
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : S.f = 0
this : S.HasHomology
⊢ Mono S.g
have this₁ : Epi (Y := S.cycles) S.toCycles
Tactic: have := hS.epi_toCycles
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : S.f = 0
this_1 : S.HasHomology
this : Epi (Y := S.cycles) S.toCycles
⊢ Eq (α := S.cycles ⟶ S.X₂) S.iCycles 0
have rw : CategoryStruct.comp (Y := S.cycles) S.toCycles S.iCycles = CategoryStruct.comp (Y := S.cycles) S.toCycles 0
Tactic: rw [← cancel_epi S.toCycles, comp_zero, toCycles_i, hf]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.Exact (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C
hS : S.Exact
hf : S.f = 0
this_1 : S.HasHomology
this : Epi (Y := S.cycles) S.toCycles
rw : CategoryStruct.comp (Y := S.cycles) S.toCycles S.iCycles = CategoryStruct.comp (Y := S.cycles) S.toCycles 0
⊢ Eq (α := S.cycles ⟶ S.X₂) S.iCycles 0
have rw₁ : CategoryStruct.comp (Y := S.cycles) S.toCycles S.iCycles = 0
Tactic: rw [← cancel_epi S.toCycles, comp_zero, toCycles_i, hf]