awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.opcycles i) (X₂ := K.cycles j) (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₂ := K.cycles j) (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ T'.Exact

Tactic:
T'.exact_of_g_is_cokernel (K.homologyIsCokernel i j (c.prev_eq' hij))

Premises used: CategoryTheory.ShortComplex.exact_of_g_is_cokernel, ComplexShape.prev_eq', HomologicalComplex.homologyIsCokernel
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.opcycles i) (X₂ := K.cycles j) (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₂ := K.cycles j) (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ T'.Exact

Tactic:
exact T'.exact_of_g_is_cokernel (K.homologyIsCokernel i j (c.prev_eq' hij))

Premises used: CategoryTheory.ShortComplex.exact_of_g_is_cokernel, ComplexShape.prev_eq', HomologicalComplex.homologyIsCokernel
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.opcycles i) (X₂ := K.cycles j) (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₂ := K.cycles j) (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ T.Exact

Tactic:
have hT : T.Exact := by
    rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono π]
    exact T'.exact_of_g_is_cokernel (K.homologyIsCokernel i j (c.prev_eq' hij))
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.opcycles i) (X₂ := K.cycles j) (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₂ := K.cycles j) (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hT : T.Exact
h :
  (ComposableArrows.mk₂ (X₀ := (composableArrows₃ K i j).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1))) (X₁ :=
      (composableArrows₃ K i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1))) (X₂ :=
      (composableArrows₃ K i j).obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
      ((composableArrows₃ K i j).map' 0 1 ComposableArrows.isComplex₂_iff._proof_2 ⋯ :
        (composableArrows₃ K i j).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
          (composableArrows₃ K i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
      ((composableArrows₃ K i j).map' 1 2 ComposableArrows.isComplex₂_iff._proof_4 ⋯ :
        (composableArrows₃ K i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
          (composableArrows₃ K i j).obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))).Exact
h₀ : (composableArrows₃ K i j).δ₀.Exact
⊢ (composableArrows₃ K i j).Exact

Tactic:
apply ComposableArrows.exact_of_δ₀

Premises used: CategoryTheory.ComposableArrows.exact_of_δ₀
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.opcycles i) (X₂ := K.cycles j) (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₂ := K.cycles j) (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hT : T.Exact
⊢ (ComposableArrows.mk₂ (X₀ := (composableArrows₃ K i j).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1))) (X₁ :=
      (composableArrows₃ K i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1))) (X₂ :=
      (composableArrows₃ K i j).obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
      ((composableArrows₃ K i j).map' 0 1 ComposableArrows.isComplex₂_iff._proof_2 ⋯ :
        (composableArrows₃ K i j).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
          (composableArrows₃ K i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
      ((composableArrows₃ K i j).map' 1 2 ComposableArrows.isComplex₂_iff._proof_4 ⋯ :
        (composableArrows₃ K i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
          (composableArrows₃ K i j).obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))).Exact

Tactic:
hS.exact_toComposableArrows

Premises used: CategoryTheory.ShortComplex.opcycles, CategoryTheory.ShortComplex.LeftHomologyData.liftK, CategoryTheory.ComposableArrows.Mk₁.obj, HomologicalComplex.opcycles, CategoryTheory.ComposableArrows.Precomp.obj, HomologicalComplex.homologyι, CategoryTheory.ShortComplex.toComposableArrows, CategoryTheory.ComposableArrows.precomp, HomologicalComplex.opcyclesToCycles, CategoryTheory.ShortComplex.Exact.exact_toComposableArrows, CategoryTheory.ShortComplex.liftCycles, HomologicalComplex.liftCycles, CategoryTheory.ShortComplex.homologyι, CategoryTheory.ShortComplex.cycles, HomologicalComplex.homology, CategoryTheory.ComposableArrows.Precomp.map, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.opcycles i) (X₂ := K.cycles j) (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₂ := K.cycles j) (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hT : T.Exact
⊢ (ComposableArrows.mk₂ (X₀ := (composableArrows₃ K i j).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1))) (X₁ :=
      (composableArrows₃ K i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1))) (X₂ :=
      (composableArrows₃ K i j).obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
      ((composableArrows₃ K i j).map' 0 1 ComposableArrows.isComplex₂_iff._proof_2 ⋯ :
        (composableArrows₃ K i j).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
          (composableArrows₃ K i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))
      ((composableArrows₃ K i j).map' 1 2 ComposableArrows.isComplex₂_iff._proof_4 ⋯ :
        (composableArrows₃ K i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)) ⟶
          (composableArrows₃ K i j).obj (⟨2, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 1 2 + 1)))).Exact

Tactic:
exact hS.exact_toComposableArrows

Premises used: CategoryTheory.ShortComplex.Exact.exact_toComposableArrows
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.opcycles i) (X₂ := K.cycles j) (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₂ := K.cycles j) (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hT : T.Exact
⊢ (composableArrows₃ K i j).δ₀.Exact

Tactic:
hT.exact_toComposableArrows

Premises used: CategoryTheory.ShortComplex.opcycles, HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.LeftHomologyData.liftK, CategoryTheory.ShortComplex.homologyπ, CategoryTheory.Functor.comp, HomologicalComplex.opcycles, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ShortComplex.toComposableArrows, CategoryTheory.ComposableArrows.whiskerLeft, CategoryTheory.ShortComplex.homology, CategoryTheory.ComposableArrows.precomp, HomologicalComplex.opcyclesToCycles, CategoryTheory.ShortComplex.Exact.exact_toComposableArrows, CategoryTheory.ShortComplex.liftCycles, HomologicalComplex.liftCycles, CategoryTheory.ShortComplex.cycles, HomologicalComplex.homology, CategoryTheory.ComposableArrows.Precomp.map, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.opcycles i) (X₂ := K.cycles j) (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₂ := K.cycles j) (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hT : T.Exact
⊢ (composableArrows₃ K i j).δ₀.Exact

Tactic:
exact hT.exact_toComposableArrows

Premises used: CategoryTheory.ShortComplex.Exact.exact_toComposableArrows
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K_1 : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
⊢ Eq (α :=
    (composableArrows₃ K i j).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶
      (composableArrows₃ L i j).obj' 1 _proof_298✝)
    ((composableArrows₃ K i j).map' 0 1 ComposableArrows.homMk₁._proof_4 _proof_298✝ ≫ opcyclesMap φ i :
      (composableArrows₃ K i j).obj (⟨0, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶
        (composableArrows₃ L i j).obj' 1 _proof_298✝)
    (homologyMap φ i ≫ (composableArrows₃ L i j).map' 0 1 ComposableArrows.homMk₁._proof_4 _proof_298✝ :
      (composableArrows₃ K i j).obj' 0 _proof_297✝ ⟶
        (composableArrows₃ L i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K_1 : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
⊢ Eq (α :=
    (composableArrows₃ K i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶
      (composableArrows₃ L i j).obj' 2 _proof_299✝)
    ((composableArrows₃ K i j).map' 1 2 _proof_246✝ _proof_299✝ ≫ cyclesMap φ j :
      (composableArrows₃ K i j).obj (⟨1, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 3 1)) ⟶
        (composableArrows₃ L i j).obj' 2 _proof_299✝)
    (opcyclesMap φ i ≫ (composableArrows₃ L i j).map' 1 2 _proof_246✝ _proof_299✝ :
      (composableArrows₃ K i j).obj' 1 _proof_298✝ ⟶ (composableArrows₃ L i j).obj ⟨2, ⋯⟩)

Tactic:
simp [-Fin.reduceFinMk]

Premises used: Fin.reduceFinMk
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K_1 : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
⊢ (composableArrows₃ K i j).map' 2 3 _proof_299✝ _proof_300✝ ≫ homologyMap φ j =
    cyclesMap φ j ≫ (composableArrows₃ L i j).map' 2 3 _proof_299✝ _proof_300✝

Tactic:
simp [-Fin.reduceFinMk]

Premises used: Fin.reduceFinMk
-- 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
rw : Eq (α := S.X₁.opcycles i ⟶ S.X₃.opcycles i) (opcyclesMap (S.f ≫ S.g) i) 0
rw₁ : Eq.{v_1 + 1} (α := S.X₁.opcycles i ⟶ S.X₃.opcycles i) (opcyclesMap 0 i) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S.X₁.opcycles i ⟶ S.X₃.opcycles i) 0 0
⊢ Eq (α := S.X₁.opcycles i ⟶ S.X₃.opcycles i)
    (CategoryStruct.comp (Y := S.X₂.opcycles i) (opcyclesMap S.f i) (opcyclesMap S.g i)) 0

Tactic:
rw [← opcyclesMap_comp, S.zero, opcyclesMap_zero]

Premises used: HomologicalComplex.opcyclesMap_comp, CategoryTheory.ShortComplex.zero, HomologicalComplex.opcyclesMap_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 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
dsimp : Epi (S.g.f i)
⊢ Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (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 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
⊢ Epi (S.g.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 : Epi S.g
i : ι
inst_3 : S.X₁.HasHomology i
inst_4 : S.X₂.HasHomology i
inst_5 : S.X₃.HasHomology i
⊢ Epi (X := ShortComplex.X₂ (S.map (eval C c i))) (ShortComplex.g (S.map (eval C c i)))

Tactic:
have : Epi (ShortComplex.map S (eval C c i)).g := 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 : 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)))
have :
  ∀
    (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))) ⋯)),
    (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) ⋯).Exact
⊢ (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) ⋯).Exact

Tactic:
have hj := (hS.map (HomologicalComplex.eval C c i)).gIsCokernel
-- 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))) ⋯)
hS₁ :
  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
      ⋯)
⊢ (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) ⋯).Exact

Tactic:
apply ShortComplex.exact_of_g_is_cokernel

Premises used: CategoryTheory.ShortComplex.exact_of_g_is_cokernel
-- 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 :
  (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) ⋯).X₂ ⟶
    A
hk :
  (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) ⋯).f ≫
      k =
    0
dsimp : { l : S.X₃.opcycles i ⟶ A // opcyclesMap S.g i ≫ l = k }
⊢ { l :
    (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) ⋯).X₃ ⟶
      A //
    (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 ≫
        l =
      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 : 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
dsimp : S.f.f i ≫ S.X₂.pOpcycles i ≫ k = 0
⊢ ShortComplex.f (S.map (eval C c i)) ≫ S.X₂.pOpcycles i ≫ k = 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 : 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
rw : CategoryStruct.comp (Y := S.X₁.opcycles i) (S.X₁.pOpcycles i) (opcyclesMap S.f i ≫ k) = 0
rw₁ : Eq (α := S.X₁.X i ⟶ A) (CategoryStruct.comp (Y := S.X₁.opcycles i) (S.X₁.pOpcycles i) 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := S.X₁.X i ⟶ A) 0 0
⊢ S.f.f i ≫ S.X₂.pOpcycles i ≫ k = 0

Tactic:
rw [← p_opcyclesMap_assoc, hk, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.p_opcyclesMap_assoc
-- 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
have :
  (H :
      { l :
        Cocone.pt (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 //
        Cofork.π (CokernelCofork.ofπ (ShortComplex.g (S.map (eval C c i))) ⋯) ≫ l = S.X₂.pOpcycles i ≫ k }) →
    { l : S.X₃.opcycles i ⟶ A // opcyclesMap S.g i ≫ l = k }
⊢ { l : S.X₃.opcycles i ⟶ A // opcyclesMap S.g i ≫ l = k }

Tactic:
have H := CokernelCofork.IsColimit.desc' hj (S.X₂.pOpcycles i ≫ k) (by
      dsimp
      rw [← p_opcyclesMap_assoc, hk, comp_zero])