awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
hj :
  IsColimit (F := parallelPair (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i))) 0)
    (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : Eq (α := S.X₁.opcycles i ⟶ A) (opcyclesMap S.f i ≫ k) 0
H : { l : S.X₃.X i ⟶ A // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
refine_1 : Eq (α := S.X₃.X (c.prev i) ⟶ A) (S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0
refine_2 :
  CategoryStruct.comp (Y := S.X₃.opcycles i) (opcyclesMap S.g i)
      (S.X₃.descOpcycles (↑H : S.X₃.X i ⟶ A) (c.prev i) ⋯ ⋯) =
    k
⊢ { l : S.X₃.opcycles i ⟶ A // opcyclesMap S.g i ≫ l = k }

Tactic:
refine ⟨S.X₃.descOpcycles H.1 _ rfl ?_, ?_⟩
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
hj :
  IsColimit (F := parallelPair (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i))) 0)
    (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : Eq (α := S.X₁.opcycles i ⟶ A) (opcyclesMap S.f i ≫ k) 0
H : { l : S.X₃.X i ⟶ A // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
refine_1 :
  Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.g.f (c.prev i) ≫ S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) (S.g.f (c.prev i) ≫ 0)
refine_1₁ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.g.f (c.prev i) ≫ S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0
refine_1₂ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.X₂.d (c.prev i) i ≫ S.g.f i ≫ (↑H : S.X₃.X i ⟶ A)) 0
refine_1₃ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (S.X₂.d (c.prev i) i ≫ S.X₂.pOpcycles i ≫ k) 0
refine_1₄ : Eq (α := S.X₂.X (c.prev i) ⟶ A) (0 ≫ k) 0
refine_1₅ refine_1₆ : Eq.{v_1 + 1} (α := S.X₂.X (c.prev i) ⟶ A) 0 0
⊢ Eq (α := S.X₃.X (c.prev i) ⟶ A) (S.X₃.d (c.prev i) i ≫ (↑H : S.X₃.X i ⟶ A)) 0

Tactic:
rw [← cancel_epi (S.g.f (c.prev i)), comp_zero, Hom.comm_assoc, H.2,
        d_pOpcycles_assoc, zero_comp]

Premises used: HomologicalComplex.Hom.f, CategoryTheory.Limits.comp_zero, HomologicalComplex.d_pOpcycles_assoc, ComplexShape.prev, HomologicalComplex.Hom.comm_assoc, CategoryTheory.Limits.zero_comp, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.g, Subtype.property
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
hj :
  IsColimit (F := parallelPair (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i))) 0)
    (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : Eq (α := S.X₁.opcycles i ⟶ A) (opcyclesMap S.f i ≫ k) 0
H : { l : S.X₃.X i ⟶ A // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
refine_2 :
  CategoryStruct.comp (Y := S.X₂.opcycles i) (S.X₂.pOpcycles i)
      (CategoryStruct.comp (Y := S.X₃.opcycles i) (opcyclesMap S.g i)
        (S.X₃.descOpcycles (↑H : S.X₃.X i ⟶ A) (c.prev i) ⋯ ⋯)) =
    S.X₂.pOpcycles i ≫ k
refine_2₁ :
  CategoryStruct.comp (Y := S.X₂.opcycles i) (S.X₂.pOpcycles i)
      (S.X₂.descOpcycles (S.g.f i ≫ (↑H : S.X₃.X i ⟶ A)) (c.prev i) ⋯ ⋯) =
    S.X₂.pOpcycles i ≫ k
refine_2₂ : S.g.f i ≫ (↑H : S.X₃.X i ⟶ A) = S.X₂.pOpcycles i ≫ k
refine_2₃ refine_2₄ : S.X₂.pOpcycles i ≫ k = S.X₂.pOpcycles i ≫ k
⊢ CategoryStruct.comp (Y := S.X₃.opcycles i) (opcyclesMap S.g i)
      (S.X₃.descOpcycles (↑H : S.X₃.X i ⟶ A) (c.prev i) ⋯ ⋯) =
    k

Tactic:
rw [← cancel_epi (S.X₂.pOpcycles i), opcyclesMap_comp_descOpcycles, p_descOpcycles, H.2]

Premises used: HomologicalComplex.opcyclesMap_comp_descOpcycles, HomologicalComplex.pOpcycles, CategoryTheory.cancel_epi, Subtype.property, HomologicalComplex.p_descOpcycles, CategoryTheory.ShortComplex.X₂
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))
hj :
  IsColimit (F := parallelPair (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i))) 0)
    (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) ⋯)
⊢ IsColimit
    (CokernelCofork.ofπ
      (ShortComplex.mk (X₁ := S.X₁.opcycles i) (X₂ := S.X₂.opcycles i) (X₃ := S.X₃.opcycles i) (opcyclesMap S.f i)
          (opcyclesMap S.g i) ⋯).g
      ⋯)

Tactic:
refine CokernelCofork.IsColimit.ofπ' _ _ (fun {A} k hk => by
    dsimp at k hk ⊢
    have H := CokernelCofork.IsColimit.desc' hj (S.X₂.pOpcycles i ≫ k) (by
      dsimp
      rw [← p_opcyclesMap_assoc, hk, comp_zero])
    dsimp at H
    refine ⟨S.X₃.descOpcycles H.1 _ rfl ?_, ?_⟩
    · rw [← cancel_epi (S.g.f (c.prev i)), comp_zero, Hom.comm_assoc, H.2,
        d_pOpcycles_assoc, zero_comp]
    · rw [← cancel_epi (S.X₂.pOpcycles i), opcyclesMap_comp_descOpcycles, p_descOpcycles, H.2])

Premises used: CategoryTheory.Limits.CokernelCofork.IsColimit.ofπ'
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
rw : Eq (α := S.X₁.cycles i ⟶ S.X₃.cycles i) (cyclesMap (S.f ≫ S.g) i) 0
rw₁ : Eq.{v_1 + 1} (α := S.X₁.cycles i ⟶ S.X₃.cycles i) (cyclesMap 0 i) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S.X₁.cycles i ⟶ S.X₃.cycles i) 0 0
⊢ Eq (α := S.X₁.cycles i ⟶ S.X₃.cycles i) (CategoryStruct.comp (Y := S.X₂.cycles i) (cyclesMap S.f i) (cyclesMap S.g i))
    0

Tactic:
rw [← cyclesMap_comp, S.zero, cyclesMap_zero]

Premises used: HomologicalComplex.cyclesMap_comp, HomologicalComplex.cyclesMap_zero, CategoryTheory.ShortComplex.zero
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
dsimp : Mono (S.f.f i)
⊢ Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
⊢ Mono (S.f.f i)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
⊢ Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))

Tactic:
have : Mono (ShortComplex.map S (eval C c i)).f := by dsimp; infer_instance
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
have :
  ∀
    (hi :
      IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
        (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)),
    (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i)
        (cyclesMap S.g i) ⋯).Exact
⊢ (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i) (cyclesMap S.g i)
      ⋯).Exact

Tactic:
have hi := (hS.map (HomologicalComplex.eval C c i)).fIsKernel
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
hS₁ :
  IsLimit
    (KernelFork.ofι
      (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i)
          (cyclesMap S.g i) ⋯).f
      ⋯)
⊢ (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i) (cyclesMap S.g i)
      ⋯).Exact

Tactic:
apply ShortComplex.exact_of_f_is_kernel

Premises used: CategoryTheory.ShortComplex.exact_of_f_is_kernel
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k :
  A ⟶
    (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i)
        (cyclesMap S.g i) ⋯).X₂
hk :
  k ≫
      (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i)
          (cyclesMap S.g i) ⋯).g =
    0
dsimp : { l : A ⟶ S.X₁.cycles i // l ≫ cyclesMap S.f i = k }
⊢ { l :
    A ⟶
      (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i)
          (cyclesMap S.g i) ⋯).X₁ //
    l ≫
        (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i)
            (cyclesMap S.g i) ⋯).f =
      k }

Tactic:
dsimp at k hk ⊢
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
dsimp : (k ≫ S.X₂.iCycles i) ≫ S.g.f i = 0
⊢ Eq (α := A ⟶ ShortComplex.X₃ (S.map (eval C c i))) ((k ≫ S.X₂.iCycles i) ≫ ShortComplex.g (S.map (eval C c i))) 0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
rw : k ≫ S.X₂.iCycles i ≫ S.g.f i = 0
rw₁ : k ≫ CategoryStruct.comp (Y := S.X₃.cycles i) (cyclesMap S.g i) (S.X₃.iCycles i) = 0
rw₂ : Eq (α := A ⟶ S.X₃.X i) (CategoryStruct.comp (Y := S.X₃.cycles i) 0 (S.X₃.iCycles i)) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := A ⟶ S.X₃.X i) 0 0
⊢ (k ≫ S.X₂.iCycles i) ≫ S.g.f i = 0

Tactic:
rw [assoc, ← cyclesMap_i, reassoc_of% hk, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.zero_comp, HomologicalComplex.cyclesMap_i
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
have :
  (H :
      { l :
        A ⟶
          Cone.pt (F :=
            parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
            (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯) //
        l ≫ Fork.ι (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯) = k ≫ S.X₂.iCycles i }) →
    { l : A ⟶ S.X₁.cycles i // l ≫ cyclesMap S.f i = k }
⊢ { l : A ⟶ S.X₁.cycles i // l ≫ cyclesMap S.f i = k }

Tactic:
have H := KernelFork.IsLimit.lift' hi (k ≫ S.X₂.iCycles i) (by
      dsimp
      rw [assoc, ← cyclesMap_i, reassoc_of% hk, zero_comp])
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
refine_1 : Eq (α := A ⟶ S.X₁.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) 0
refine_2 :
  CategoryStruct.comp (Y := S.X₁.cycles i) (S.X₁.liftCycles (↑H : A ⟶ S.X₁.X i) (c.next i) ⋯ ⋯) (cyclesMap S.f i) = k
⊢ { l : A ⟶ S.X₁.cycles i // l ≫ cyclesMap S.f i = k }

Tactic:
refine ⟨S.X₁.liftCycles H.1 _ rfl ?_, ?_⟩
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
refine_1 :
  Eq (α := A ⟶ S.X₂.X (c.next i)) (((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) ≫ S.f.f (c.next i))
    (0 ≫ S.f.f (c.next i))
refine_1₁ :
  Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i) ≫ S.f.f (c.next i)) (0 ≫ S.f.f (c.next i))
refine_1₂ : Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i) ≫ S.f.f (c.next i)) 0
refine_1₃ : Eq (α := A ⟶ S.X₂.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.f.f i ≫ S.X₂.d i (c.next i)) 0
refine_1₄ : Eq (α := A ⟶ S.X₂.X (c.next i)) (k ≫ S.X₂.iCycles i ≫ S.X₂.d i (c.next i)) 0
refine_1₅ : Eq (α := A ⟶ S.X₂.X (c.next i)) (k ≫ 0) 0
refine_1₆ refine_1₇ : Eq.{v_1 + 1} (α := A ⟶ S.X₂.X (c.next i)) 0 0
⊢ Eq (α := A ⟶ S.X₁.X (c.next i)) ((↑H : A ⟶ S.X₁.X i) ≫ S.X₁.d i (c.next i)) 0

Tactic:
rw [← cancel_mono (S.f.f _), assoc, zero_comp, ← Hom.comm, reassoc_of% H.2,
        iCycles_d, comp_zero]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.Hom.f, CategoryTheory.Limits.comp_zero, HomologicalComplex.iCycles_d, CategoryTheory.cancel_mono, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.zero_comp, HomologicalComplex.Hom.comm, Subtype.property
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
A : C
k : A ⟶ S.X₂.cycles i
hk : Eq (α := A ⟶ S.X₃.cycles i) (k ≫ cyclesMap S.g i) 0
H : { l : A ⟶ S.X₁.X i // l ≫ S.f.f i = k ≫ S.X₂.iCycles i }
refine_2 :
  CategoryStruct.comp (Y := S.X₂.cycles i)
      (CategoryStruct.comp (Y := S.X₁.cycles i) (S.X₁.liftCycles (↑H : A ⟶ S.X₁.X i) (c.next i) ⋯ ⋯) (cyclesMap S.f i))
      (S.X₂.iCycles i) =
    k ≫ S.X₂.iCycles i
refine_2₁ :
  CategoryStruct.comp (Y := S.X₂.cycles i) (S.X₂.liftCycles ((↑H : A ⟶ S.X₁.X i) ≫ S.f.f i) (c.next i) ⋯ ⋯)
      (S.X₂.iCycles i) =
    k ≫ S.X₂.iCycles i
refine_2₂ : (↑H : A ⟶ S.X₁.X i) ≫ S.f.f i = k ≫ S.X₂.iCycles i
refine_2₃ refine_2₄ : k ≫ S.X₂.iCycles i = k ≫ S.X₂.iCycles i
⊢ CategoryStruct.comp (Y := S.X₁.cycles i) (S.X₁.liftCycles (↑H : A ⟶ S.X₁.X i) (c.next i) ⋯ ⋯) (cyclesMap S.f i) = k

Tactic:
rw [← cancel_mono (S.X₂.iCycles i), liftCycles_comp_cyclesMap, liftCycles_i, H.2]

Premises used: HomologicalComplex.liftCycles_comp_cyclesMap, HomologicalComplex.iCycles, CategoryTheory.cancel_mono, HomologicalComplex.liftCycles_i, Subtype.property, CategoryTheory.ShortComplex.X₂
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS : S.Exact
inst_2 : Mono S.f
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
this : Mono (X := ShortComplex.X₁ (S.map (eval C c i))) (ShortComplex.f (S.map (eval C c i)))
hi :
  IsLimit (F := parallelPair (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i))) 0)
    (KernelFork.ofι (ShortComplex.f (S.map (eval C c i))) ⋯)
⊢ IsLimit
    (KernelFork.ofι
      (ShortComplex.mk (X₁ := S.X₁.cycles i) (X₂ := S.X₂.cycles i) (X₃ := S.X₃.cycles i) (cyclesMap S.f i)
          (cyclesMap S.g i) ⋯).f
      ⋯)

Tactic:
exact KernelFork.IsLimit.ofι' _ _ (fun {A} k hk => by
    dsimp at k hk ⊢
    have H := KernelFork.IsLimit.lift' hi (k ≫ S.X₂.iCycles i) (by
      dsimp
      rw [assoc, ← cyclesMap_i, reassoc_of% hk, zero_comp])
    dsimp at H
    refine ⟨S.X₁.liftCycles H.1 _ rfl ?_, ?_⟩
    · rw [← cancel_mono (S.f.f _), assoc, zero_comp, ← Hom.comm, reassoc_of% H.2,
        iCycles_d, comp_zero]
    · rw [← cancel_mono (S.X₂.iCycles i), liftCycles_comp_cyclesMap, liftCycles_i, H.2])

Premises used: CategoryTheory.Limits.KernelFork.IsLimit.ofι'
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
h₁ :
  IsLimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₁)
    (Functor.mapCone ShortComplex.π₁ (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))
h₂ :
  IsLimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₂)
    (Functor.mapCone ShortComplex.π₂ (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))
h₃ :
  IsLimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₃)
    (Functor.mapCone ShortComplex.π₃ (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))
⊢ IsLimit (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯)

Tactic:
apply ShortComplex.isLimitOfIsLimitπ

Premises used: CategoryTheory.ShortComplex.isLimitOfIsLimitπ
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex.{v_1, u_1, u_2} C c)
hS_1 : S.ShortExact
i_1 j_1 : ι
hij_1 : c.Rel i_1 j_1
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsLimit (F :=
    Functor.comp (D := ShortComplex.{v_1, u_1} C)
      (parallelPair (X := Functor.obj (Functor.mapShortComplex (opcyclesFunctor C c i)) S) (Y :=
        Functor.obj (Functor.mapShortComplex (cyclesFunctor C c j)) S)
        (S.mapNatTrans (natTransOpCyclesToCycles C c i j) :
          Quiver.Hom (V := ShortComplex.{v_1, u_1} C) (S.map (opcyclesFunctor C c i)) (S.map (cyclesFunctor C c j)))
        0)
      ShortComplex.π₁)
    (Functor.mapCone ShortComplex.π₁ (KernelFork.ofι (S.mapNatTrans (natTransHomologyι C c i)) ⋯))

Tactic:
exact (KernelFork.isLimitMapConeEquiv _ _).symm
        ((composableArrows₃_exact _ i j hij).exact 0).fIsKernel