awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
A A' : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
hk : K.d j i ≫ k = 0
α : A ⟶ A'
rw : Eq (α := K.X j ⟶ A') (0 ≫ α) 0
rw₁ rw₂ : Eq.{v_1 + 1} (α := K.X j ⟶ A') 0 0
⊢ K.d j i ≫ k ≫ α = 0

Tactic:
rw [reassoc_of% hk, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A A' : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
hk : K.d j i ≫ k = 0
α : A ⟶ A'
⊢ Eq (α := K.opcycles i ⟶ A') (K.descOpcycles k j hj hk ≫ α) (K.descOpcycles (k ≫ α) j hj ⋯)

Tactic:
simp only [← cancel_epi (K.pOpcycles i), p_descOpcycles_assoc, p_descOpcycles]

Premises used: HomologicalComplex.p_descOpcycles_assoc, HomologicalComplex.pOpcycles, CategoryTheory.cancel_epi, HomologicalComplex.p_descOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
rw : K.d j i ≫ K.d i i' ≫ x = 0
rw₁ : Eq (α := K.X j ⟶ A) (0 ≫ x) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := K.X j ⟶ A) 0 0
⊢ K.d j i ≫ k = 0

Tactic:
rw [hx, K.d_comp_d_assoc, zero_comp]

Premises used: HomologicalComplex.d_comp_d_assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
pos : ∀ (h : c.Rel i i'), Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0
neg : ∀ (h : ¬c.Rel i i'), Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0
⊢ Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0

Tactic:
by_cases h : c.Rel i i'

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : c.Rel i i'
pos :
  ∀ (x : K.X (c.next i) ⟶ A) (hx : k = K.d i (c.next i) ≫ x) (h : c.Rel i (c.next i)),
    Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0
⊢ Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0

Tactic:
obtain rfl := c.next_eq' h

Premises used: rfl, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
x : K.X (c.next i) ⟶ A
hx : k = K.d i (c.next i) ≫ x
h : c.Rel i (c.next i)
⊢ Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0

Tactic:
(K.sc i).homologyι_descOpcycles_eq_zero_of_boundary _ x hx

Premises used: HomologicalComplex.opcycles, CategoryTheory.ShortComplex.homologyι_descOpcycles_eq_zero_of_boundary, HomologicalComplex.homologyι, HomologicalComplex.sc, HomologicalComplex.descOpcycles, HomologicalComplex.homology
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
x : K.X (c.next i) ⟶ A
hx : k = K.d i (c.next i) ≫ x
h : c.Rel i (c.next i)
⊢ Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0

Tactic:
exact (K.sc i).homologyι_descOpcycles_eq_zero_of_boundary _ x hx

Premises used: CategoryTheory.ShortComplex.homologyι_descOpcycles_eq_zero_of_boundary, HomologicalComplex.sc
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
rw : K.d j i ≫ K.d i i' ≫ x = 0
rw₁ : Eq (α := K.X j ⟶ A) (0 ≫ x) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := K.X j ⟶ A) 0 0
⊢ K.d j i ≫ k = 0

Tactic:
rw [hx, K.d_comp_d_assoc, zero_comp]

Premises used: HomologicalComplex.d_comp_d_assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ k = 0

Tactic:
rw [K.shape _ _ h, zero_comp] at hx

Premises used: CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
hx₁ : k = 0
⊢ ¬c.Rel i i'

Tactic:
rw [K.shape _ _ h, zero_comp] at hx

Premises used: CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx_1 : k = K.d i i' ≫ x
hx : k = 0
h : ¬c.Rel i i'
rw :
  CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) (K.descOpcycles k j hj ⋯) =
    CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) 0
rw₁ : CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) (K.descOpcycles k j hj ⋯) = 0
rw₂ : k = 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := K.X i ⟶ A) 0 0
⊢ Eq (α := K.opcycles i ⟶ A) (K.descOpcycles k j hj ⋯) 0

Tactic:
rw [← cancel_epi (K.pOpcycles i), comp_zero, p_descOpcycles, hx]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.pOpcycles, CategoryTheory.cancel_epi, HomologicalComplex.p_descOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
⊢ Eq (α := K.opcycles i ⟶ A) (K.descOpcycles k j hj ⋯) 0

Tactic:
have : K.descOpcycles k j hj (by rw [hx, K.d_comp_d_assoc, zero_comp]) = 0 := by
      rw [K.shape _ _ h, zero_comp] at hx
      rw [← cancel_epi (K.pOpcycles i), comp_zero, p_descOpcycles, hx]
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
A : C
k : K.X i ⟶ A
j : ι
hj : c.prev i = j
i' : ι
x : K.X i' ⟶ A
hx : k = K.d i i' ≫ x
h : ¬c.Rel i i'
this : Eq (α := K.opcycles i ⟶ A) (K.descOpcycles k j hj ⋯) 0
neg : Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ 0) 0
neg₁ neg₂ : Eq.{v_1 + 1} (α := K.homology i ⟶ A) 0 0
⊢ Eq (α := K.homology i ⟶ A) (K.homologyι i ≫ K.descOpcycles k j hj ⋯) 0

Tactic:
rw [this, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
inst_2 : K.HasHomology i
⊢ K.d i j = K.d i j ≫ 𝟙 (K.X j)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
hi : c.next i = j
subst :
  IsLimit (F := parallelPair (X := K.opcycles i) (Y := K.X (c.next i)) (K.fromOpcycles i (c.next i)) 0)
    (KernelFork.ofι (K.homologyι i) ⋯)
⊢ IsLimit (F := parallelPair (X := K.opcycles i) (K.fromOpcycles i j) 0) (KernelFork.ofι (K.homologyι i) ⋯)

Tactic:
subst hi
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i k : ι
inst_2 : K.HasHomology i
⊢ IsLimit (F := parallelPair (X := K.opcycles i) (Y := K.X (c.next i)) (K.fromOpcycles i (c.next i)) 0)
    (KernelFork.ofι (K.homologyι i) ⋯)

Tactic:
exact (K.sc i).homologyIsKernel

Premises used: CategoryTheory.ShortComplex.homologyIsKernel, HomologicalComplex.sc
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq (α := K.cycles i ⟶ L.X i) (CategoryStruct.comp (Y := L.cycles i) (cyclesMap φ i) (L.iCycles i))
    (K.iCycles i ≫ φ.f i)

Tactic:
ShortComplex.cyclesMap_i _

Premises used: HomologicalComplex.iCycles, HomologicalComplex.cyclesMap, CategoryTheory.ShortComplex.cyclesMap_i, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq (α := K.X i ⟶ L.opcycles i) (CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) (opcyclesMap φ i))
    (φ.f i ≫ L.pOpcycles i)

Tactic:
ShortComplex.p_opcyclesMap _

Premises used: HomologicalComplex.opcycles, HomologicalComplex.opcyclesMap, HomologicalComplex.pOpcycles, CategoryTheory.ShortComplex.p_opcyclesMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
inst_5 : Mono (φ.f i)
⊢ Mono (X := K.cycles i) (Y := L.cycles i) (cyclesMap φ i)

Tactic:
mono_of_mono_fac (cyclesMap_i φ i)

Premises used: HomologicalComplex.cyclesMap_i, CategoryTheory.mono_of_mono_fac
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
inst_5 : Epi (φ.f i)
⊢ Epi (X := K.opcycles i) (Y := L.opcycles i) (opcyclesMap φ i)

Tactic:
epi_of_epi_fac (p_opcyclesMap φ i)

Premises used: HomologicalComplex.p_opcyclesMap, CategoryTheory.epi_of_epi_fac
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
⊢ homologyMap (𝟙 K) i = 𝟙 (K.homology i)

Tactic:
ShortComplex.homologyMap_id _

Premises used: CategoryTheory.ShortComplex.Hom.id, HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.homologyMap_id, HomologicalComplex.homology
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
⊢ cyclesMap (𝟙 K) i = 𝟙 (K.cycles i)

Tactic:
ShortComplex.cyclesMap_id _

Premises used: CategoryTheory.ShortComplex.Hom.id, HomologicalComplex.cyclesMap, CategoryTheory.ShortComplex.cyclesMap_id, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
⊢ opcyclesMap (𝟙 K) i = 𝟙 (K.opcycles i)

Tactic:
ShortComplex.opcyclesMap_id _

Premises used: HomologicalComplex.opcycles, HomologicalComplex.opcyclesMap, CategoryTheory.ShortComplex.Hom.id, CategoryTheory.ShortComplex.opcyclesMap_id
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
dsimp :
  Eq (α := K.homology i ⟶ M.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ ≫ ψ)))
    (CategoryStruct.comp (Y := L.homology i)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
⊢ Eq (α := K.homology i ⟶ M.homology i) (homologyMap (φ ≫ ψ) i)
    (CategoryStruct.comp (Y := L.homology i) (homologyMap φ i) (homologyMap ψ i))

Tactic:
dsimp [homologyMap]

Premises used: HomologicalComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
rw :
  Eq (α := K.homology i ⟶ M.homology i)
    (ShortComplex.homologyMap
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ ≫
        CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ))
    (CategoryStruct.comp (Y := L.homology i)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
rw₁ rw₂ :
  Eq (α := K.homology i ⟶ M.homology i)
    (CategoryStruct.comp (Y := (Functor.obj (shortComplexFunctor C c i) L).homology)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
    (CategoryStruct.comp (Y := L.homology i)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
⊢ Eq (α := K.homology i ⟶ M.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ ≫ ψ)))
    (CategoryStruct.comp (Y := L.homology i)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))

Tactic:
rw [Functor.map_comp, ShortComplex.homologyMap_comp]

Premises used: CategoryTheory.ShortComplex.homologyMap_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
dsimp :
  Eq (α := K.cycles i ⟶ M.cycles i)
    (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ ≫ ψ)))
    (CategoryStruct.comp (Y := L.cycles i)
      (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
⊢ Eq (α := K.cycles i ⟶ M.cycles i) (cyclesMap (φ ≫ ψ) i)
    (CategoryStruct.comp (Y := L.cycles i) (cyclesMap φ i) (cyclesMap ψ i))

Tactic:
dsimp [cyclesMap]

Premises used: HomologicalComplex.cyclesMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
rw :
  Eq (α := K.cycles i ⟶ M.cycles i)
    (ShortComplex.cyclesMap
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ ≫
        CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ))
    (CategoryStruct.comp (Y := L.cycles i)
      (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
rw₁ rw₂ :
  Eq (α := K.cycles i ⟶ M.cycles i)
    (CategoryStruct.comp (Y := (Functor.obj (shortComplexFunctor C c i) L).cycles)
      (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
    (CategoryStruct.comp (Y := L.cycles i)
      (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
⊢ Eq (α := K.cycles i ⟶ M.cycles i)
    (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ ≫ ψ)))
    (CategoryStruct.comp (Y := L.cycles i)
      (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.cyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))

Tactic:
rw [Functor.map_comp, ShortComplex.cyclesMap_comp]

Premises used: CategoryTheory.ShortComplex.cyclesMap_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
dsimp :
  Eq (α := K.opcycles i ⟶ M.opcycles i)
    (ShortComplex.opcyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ ≫ ψ)))
    (CategoryStruct.comp (Y := L.opcycles i)
      (ShortComplex.opcyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.opcyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
⊢ Eq (α := K.opcycles i ⟶ M.opcycles i) (opcyclesMap (φ ≫ ψ) i)
    (CategoryStruct.comp (Y := L.opcycles i) (opcyclesMap φ i) (opcyclesMap ψ i))

Tactic:
dsimp [opcyclesMap]

Premises used: HomologicalComplex.opcyclesMap
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
ψ : L ⟶ M
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
rw :
  Eq (α := K.opcycles i ⟶ M.opcycles i)
    (ShortComplex.opcyclesMap
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ ≫
        CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ))
    (CategoryStruct.comp (Y := L.opcycles i)
      (ShortComplex.opcyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.opcyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
rw₁ rw₂ :
  Eq (α := K.opcycles i ⟶ M.opcycles i)
    (CategoryStruct.comp (Y := (Functor.obj (shortComplexFunctor C c i) L).opcycles)
      (ShortComplex.opcyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.opcyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
    (CategoryStruct.comp (Y := L.opcycles i)
      (ShortComplex.opcyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.opcyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
⊢ Eq (α := K.opcycles i ⟶ M.opcycles i)
    (ShortComplex.opcyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ ≫ ψ)))
    (CategoryStruct.comp (Y := L.opcycles i)
      (ShortComplex.opcyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.opcyclesMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))

Tactic:
rw [Functor.map_comp, ShortComplex.opcyclesMap_comp]

Premises used: CategoryTheory.ShortComplex.opcyclesMap_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq.{v_1 + 1} (α := K.homology i ⟶ L.homology i) (homologyMap 0 i) 0

Tactic:
ShortComplex.homologyMap_zero _ _

Premises used: CategoryTheory.ShortComplex.homologyMap_zero, HomologicalComplex.homologyMap, HomologicalComplex.homology
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq.{v_1 + 1} (α := K.cycles i ⟶ L.cycles i) (cyclesMap 0 i) 0

Tactic:
ShortComplex.cyclesMap_zero _ _

Premises used: CategoryTheory.ShortComplex.cyclesMap_zero, HomologicalComplex.cyclesMap, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq.{v_1 + 1} (α := K.opcycles i ⟶ L.opcycles i) (opcyclesMap 0 i) 0

Tactic:
ShortComplex.opcyclesMap_zero _ _

Premises used: HomologicalComplex.opcycles, HomologicalComplex.opcyclesMap, CategoryTheory.ShortComplex.opcyclesMap_zero
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq (α := K.cycles i ⟶ L.homology i) (K.homologyπ i ≫ homologyMap φ i) (cyclesMap φ i ≫ L.homologyπ i)

Tactic:
ShortComplex.homologyπ_naturality _

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.homologyπ_naturality, HomologicalComplex.cyclesMap, HomologicalComplex.homologyMap, HomologicalComplex.homology, HomologicalComplex.cycles