awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
hj : ∀ (i : ι), ¬c.Rel i j
this_1 : Mono S.f
this : Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
neg :
  Eq (α := S.X₁.homology j ⟶ S.X₃.homology j)
    (CategoryStruct.comp (Y := S.X₂.homology j) (𝟙 (S.X₁.homology j) ≫ HomologicalComplex.homologyMap S.f j)
      (HomologicalComplex.homologyMap S.g j))
    (CategoryStruct.comp (Y := S.X₂.homology j)
      (CategoryStruct.comp (Y := S.X₁.homology j) 0 (HomologicalComplex.homologyMap S.f j))
      (HomologicalComplex.homologyMap S.g j))
⊢ IsZero.{v_1, u_1} (S.X₁.homology j)

Tactic:
rw [IsZero.iff_id_eq_zero,
      ← cancel_mono (HomologicalComplex.homologyMap S.f j),
      ← cancel_mono (HomologicalComplex.homologyMap S.g j)]

Premises used: CategoryTheory.cancel_mono, HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.IsZero.iff_id_eq_zero, CategoryTheory.ShortComplex.g
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
j : ι
h₁ : Mono (X := S.X₂.homology j) (Y := S.X₃.homology j) (HomologicalComplex.homologyMap S.g j)
h₂ : ∀ (i : ι), c.Rel i j → Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
hj : ∀ (i : ι), ¬c.Rel i j
this_1 : Mono S.f
this : Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
⊢ Eq (α := S.X₁.homology j ⟶ S.X₃.homology j)
    (CategoryStruct.comp (Y := S.X₂.homology j) (𝟙 (S.X₁.homology j) ≫ HomologicalComplex.homologyMap S.f j)
      (HomologicalComplex.homologyMap S.g j))
    (CategoryStruct.comp (Y := S.X₂.homology j)
      (CategoryStruct.comp (Y := S.X₁.homology j) 0 (HomologicalComplex.homologyMap S.f j))
      (HomologicalComplex.homologyMap S.g j))

Tactic:
simp [← HomologicalComplex.homologyMap_comp]

Premises used: HomologicalComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
i : ι
h₁ : S.X₁.ExactAt i
h₃ : S.X₃.ExactAt i
rw :
  ∀ (h₁ : IsZero.{v_1, u_1} (S.X₁.homology i)) (h₃ : IsZero.{v_1, u_1} (S.X₃.homology i)),
    IsZero.{v_1, u_1} (S.X₂.homology i)
⊢ S.X₂.ExactAt i

Tactic:
rw [exactAt_iff_isZero_homology] at h₁ h₃ ⊢

Premises used: HomologicalComplex.exactAt_iff_isZero_homology
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
i : ι
h₁ : IsZero.{v_1, u_1} (S.X₁.homology i)
h₃ : IsZero.{v_1, u_1} (S.X₃.homology i)
⊢ IsZero.{v_1, u_1} (S.X₂.homology i)

Tactic:
(hS.homology_exact₂ i).isZero_X₂ (h₁.eq_of_src _ _) (h₃.eq_of_tgt _ _)

Premises used: CategoryTheory.ShortComplex.homology, CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.Limits.IsZero.eq_of_tgt, CategoryTheory.ShortComplex.Exact.isZero_X₂, HomologicalComplex.homology, CategoryTheory.ShortComplex.ShortExact.homology_exact₂
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
i : ι
h₁ : IsZero.{v_1, u_1} (S.X₁.homology i)
h₃ : IsZero.{v_1, u_1} (S.X₃.homology i)
⊢ IsZero.{v_1, u_1} (S.X₂.homology i)

Tactic:
exact (hS.homology_exact₂ i).isZero_X₂ (h₁.eq_of_src _ _) (h₃.eq_of_tgt _ _)

Premises used: CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.Limits.IsZero.eq_of_tgt, CategoryTheory.ShortComplex.Exact.isZero_X₂, CategoryTheory.ShortComplex.ShortExact.homology_exact₂
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
rw : IsZero.{v_1, u_1} (S.X₃.homology i)
⊢ S.X₃.ExactAt i

Tactic:
rw [exactAt_iff_isZero_homology]

Premises used: HomologicalComplex.exactAt_iff_isZero_homology
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
pos : ∀ (hi : ∃ (j : ι), c.Rel i j), IsZero.{v_1, u_1} (S.X₃.homology i)
neg : ∀ (hi : ∀ (j : ι), ¬c.Rel i j), IsZero.{v_1, u_1} (S.X₃.homology i)
⊢ IsZero.{v_1, u_1} (S.X₃.homology i)

Tactic:
by_cases! hi : ∃ j, c.Rel i j
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
hi : ∃ (j : ι), c.Rel i j
pos : ∀ (j : ι) (hij : c.Rel i j), IsZero.{v_1, u_1} (S.X₃.homology i)
⊢ IsZero.{v_1, u_1} (S.X₃.homology i)

Tactic:
obtain ⟨j, hij⟩ := hi
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
⊢ Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)

Tactic:
have := h₂ j hij
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
pos :
  { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ : ShortComplex.{v_1, u_1} C }.f =
    0
pos₁ :
  { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g =
    0
⊢ IsZero.{v_1, u_1} (S.X₃.homology i)

Tactic:
apply (hS.homology_exact₃ i j hij).isZero_X₂

Premises used: CategoryTheory.ShortComplex.ShortExact.homology_exact₃, CategoryTheory.ShortComplex.Exact.isZero_X₂
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ : ShortComplex.{v_1, u_1} C }.f =
    0

Tactic:
simp [← cancel_epi (HomologicalComplex.homologyMap S.f i),
        ← HomologicalComplex.homologyMap_comp]

Premises used: HomologicalComplex.homologyMap_comp, HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.f, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ : ShortComplex.{v_1, u_1} C }.g =
    0

Tactic:
simp [← cancel_mono (HomologicalComplex.homologyMap S.f j)]

Premises used: CategoryTheory.cancel_mono, HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.f
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
⊢ Epi S.g

Tactic:
have := hS.epi_g
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
this : Epi S.g
⊢ Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)

Tactic:
have := HomologicalComplex.epi_homologyMap_of_epi_of_not_rel S.g i hi
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
this_1 : Epi S.g
this : Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
neg :
  Eq (α := S.X₁.homology i ⟶ S.X₃.homology i)
    (CategoryStruct.comp (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
      (HomologicalComplex.homologyMap S.g i ≫ 𝟙 (S.X₃.homology i)))
    (CategoryStruct.comp (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
      (CategoryStruct.comp (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i) 0))
⊢ IsZero.{v_1, u_1} (S.X₃.homology i)

Tactic:
rw [IsZero.iff_id_eq_zero,
      ← cancel_epi (HomologicalComplex.homologyMap S.g i),
      ← cancel_epi (HomologicalComplex.homologyMap S.f i)]

Premises used: HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.f, CategoryTheory.Limits.IsZero.iff_id_eq_zero, CategoryTheory.cancel_epi, CategoryTheory.ShortComplex.g
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
i : ι
h₁ : Epi (X := S.X₁.homology i) (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (X := S.X₁.homology j) (Y := S.X₂.homology j) (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
this_1 : Epi S.g
this : Epi (X := S.X₂.homology i) (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i)
⊢ Eq (α := S.X₁.homology i ⟶ S.X₃.homology i)
    (CategoryStruct.comp (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
      (HomologicalComplex.homologyMap S.g i ≫ 𝟙 (S.X₃.homology i)))
    (CategoryStruct.comp (Y := S.X₂.homology i) (HomologicalComplex.homologyMap S.f i)
      (CategoryStruct.comp (Y := S.X₃.homology i) (HomologicalComplex.homologyMap S.g i) 0))

Tactic:
simp [← HomologicalComplex.homologyMap_comp]

Premises used: HomologicalComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
hg : _root_.QuasiIso S.g
⊢ S.X₁.Acyclic

Tactic:
fun j ↦ hS.exactAt_X₁ j

Premises used: CategoryTheory.ShortComplex.ShortExact.exactAt_X₁, HomologicalComplex.Acyclic
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
h₁ : S.X₁.Acyclic
h₃ : S.X₃.Acyclic
⊢ S.X₂.Acyclic

Tactic:
fun i ↦ hS.exactAt_X₂ i (h₁ _) (h₃ _)

Premises used: CategoryTheory.ShortComplex.ShortExact.exactAt_X₂, HomologicalComplex.Acyclic
-- Module: Mathlib.Algebra.Homology.HomologySequenceLemmas
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.ShortExact
h : _root_.QuasiIso S.f
⊢ S.X₃.Acyclic

Tactic:
fun i ↦ hS.exactAt_X₃ i

Premises used: CategoryTheory.ShortComplex.ShortExact.exactAt_X₃, HomologicalComplex.Acyclic
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
⊢ Eq.{v + 1} (α := C.X i ⟶ D.X i) ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f : C.X i ⟶ D.X i)
    (C.dFrom i ≫ (fromNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.xNext i ⟶ D.X i) f : C.X i ⟶ D.X i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
i i' : ι
w : c.Rel i i'
obtain :
  ∀ (w : c.Rel i (c.next i)),
    (dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f =
      CategoryStruct.comp (Y := C.X (c.next i)) (C.d i (c.next i)) (f (c.next i) i)
⊢ (dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f = C.d i i' ≫ f i' i

Tactic:
obtain rfl := c.next_eq' w

Premises used: rfl, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
w : c.Rel i (c.next i)
⊢ (dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f =
    CategoryStruct.comp (Y := C.X (c.next i)) (C.d i (c.next i)) (f (c.next i) i)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel i (c.next i)
dsimp : CategoryStruct.comp (Y := C.X (c.next i)) (C.d i (c.next i)) (f (c.next i) i) = 0
⊢ Eq.{v + 1} (α := C.X i ⟶ D.X i) ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f : C.X i ⟶ D.X i)
    (0 : C.X i ⟶ D.X i)

Tactic:
dsimp [dNext]

Premises used: dNext
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel i (c.next i)
rw : Eq.{v + 1} (α := C.X i ⟶ D.X i) (CategoryStruct.comp (Y := C.X (c.next i)) 0 (f (c.next i) i)) 0
rw₁ rw₂ : Eq.{v + 1} (α := C.X i ⟶ D.X i) 0 0
⊢ CategoryStruct.comp (Y := C.X (c.next i)) (C.d i (c.next i)) (f (c.next i) i) = 0

Tactic:
rw [shape _ _ _ hi, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
g : (i j : ι) → D.X i ⟶ E.X j
i : ι
⊢ Eq (α := C.X i ⟶ E.X i) ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ f.f i ≫ g i j)
    (f.f i ≫ (dNext i : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X i ⟶ E.X i) g)

Tactic:
(f.comm_assoc _ _ _).symm

Premises used: HomologicalComplex.Hom.comm_assoc, Eq.symm
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
i : ι
⊢ Eq.{v + 1} (α := C.X i ⟶ E.X i)
    ((dNext i : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X i ⟶ E.X i) fun (i j : ι) ↦ f i j ≫ g.f j : C.X i ⟶ E.X i)
    ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f ≫ g.f i : C.X i ⟶ E.X i)

Tactic:
(assoc _ _ _).symm

Premises used: CategoryTheory.Category.assoc, Eq.symm
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel (c.prev i) i
dsimp : CategoryStruct.comp (Y := D.X (c.prev i)) (f i (c.prev i)) (D.d (c.prev i) i) = 0
⊢ Eq.{v + 1} (α := C.X i ⟶ D.X i) ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f : C.X i ⟶ D.X i)
    (0 : C.X i ⟶ D.X i)

Tactic:
dsimp [prevD]

Premises used: prevD
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
i : ι
hi : ¬c.Rel (c.prev i) i
rw : Eq.{v + 1} (α := C.X i ⟶ D.X i) (CategoryStruct.comp (Y := D.X (c.prev i)) (f i (c.prev i)) 0) 0
rw₁ rw₂ : Eq.{v + 1} (α := C.X i ⟶ D.X i) 0 0
⊢ CategoryStruct.comp (Y := D.X (c.prev i)) (f i (c.prev i)) (D.d (c.prev i) i) = 0

Tactic:
rw [shape _ _ _ hi, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
j : ι
⊢ Eq.{v + 1} (α := C.X j ⟶ D.X j) ((prevD j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) f : C.X j ⟶ D.X j)
    ((toPrev j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.xPrev j) f ≫ D.dTo j : C.X j ⟶ D.X j)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
j j' : ι
w : c.Rel j' j
obtain :
  ∀ (w : c.Rel (c.prev j) j),
    (prevD j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) f =
      CategoryStruct.comp (Y := D.X (c.prev j)) (f j (c.prev j)) (D.d (c.prev j) j)
⊢ (prevD j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) f = f j j' ≫ D.d j' j

Tactic:
obtain rfl := c.prev_eq' w

Premises used: ComplexShape.prev_eq', rfl
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
j : ι
w : c.Rel (c.prev j) j
⊢ (prevD j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) f =
    CategoryStruct.comp (Y := D.X (c.prev j)) (f j (c.prev j)) (D.d (c.prev j) j)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
g : (i j : ι) → D.X i ⟶ E.X j
j : ι
⊢ Eq (α := C.X j ⟶ E.X j) ((prevD j : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X j ⟶ E.X j) fun (i j : ι) ↦ f.f i ≫ g i j)
    (f.f j ≫ (prevD j : (a : (i j : ι) → D.X i ⟶ E.X j) → D.X j ⟶ E.X j) g)

Tactic:
assoc _ _ _

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
j : ι
dsimp :
  CategoryStruct.comp (Y := E.X (c.prev j)) (f j (c.prev j) ≫ g.f (c.prev j)) (E.d (c.prev j) j) =
    CategoryStruct.comp (Y := D.X (c.prev j)) (f j (c.prev j)) (D.d (c.prev j) j) ≫ g.f j
⊢ Eq.{v + 1} (α := C.X j ⟶ E.X j)
    ((prevD j : (a : (i j : ι) → C.X i ⟶ E.X j) → C.X j ⟶ E.X j) fun (i j : ι) ↦ f i j ≫ g.f j : C.X j ⟶ E.X j)
    ((prevD j : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X j ⟶ D.X j) f ≫ g.f j : C.X j ⟶ E.X j)

Tactic:
dsimp [prevD]

Premises used: prevD
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
j : ι
⊢ CategoryStruct.comp (Y := E.X (c.prev j)) (f j (c.prev j) ≫ g.f (c.prev j)) (E.d (c.prev j) j) =
    CategoryStruct.comp (Y := D.X (c.prev j)) (f j (c.prev j)) (D.d (c.prev j) j) ≫ g.f j

Tactic:
simp only [assoc, g.comm]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.Hom.comm
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
C D : ChainComplex.{v, u, 0} V ℕ
i : ℕ
f : (i j : ℕ) → C.X i ⟶ D.X j
dsimp :
  CategoryStruct.comp (Y := C.X ((ComplexShape.down ℕ).next i)) (C.d i ((ComplexShape.down ℕ).next i))
      (f ((ComplexShape.down ℕ).next i) i) =
    CategoryStruct.comp (Y := C.X (i - 1)) (C.d i (i - 1)) (f (i - 1) i)
⊢ (dNext i : (a : (i j : ℕ) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) f =
    CategoryStruct.comp (Y := C.X (i - 1)) (C.d i (i - 1)) (f (i - 1) i)

Tactic:
dsimp [dNext]

Premises used: dNext