awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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
⊢ 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) ψ)))
have 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) ψ)))
Tactic: rw [Functor.map_comp, ShortComplex.cyclesMap_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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) ψ)))
⊢ 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) ψ)))
have 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) ψ)))
Tactic: rw [Functor.map_comp, ShortComplex.cyclesMap_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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
⊢ Eq (α := K.opcycles i ⟶ M.opcycles i) (opcyclesMap (φ ≫ ψ) i)
    (CategoryStruct.comp (Y := L.opcycles i) (opcyclesMap φ i) (opcyclesMap ψ i))
have 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) ψ)))
Tactic: dsimp [opcyclesMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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
⊢ 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) ψ)))
have 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) ψ)))
Tactic: rw [Functor.map_comp, ShortComplex.opcyclesMap_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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) ψ)))
⊢ 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) ψ)))
have 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) ψ)))
Tactic: rw [Functor.map_comp, ShortComplex.opcyclesMap_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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
φ_1 : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
A : C
k : L.X i ⟶ A
j : ι
hj : c.prev i = j
hk : L.d j i ≫ k = 0
φ : K ⟶ L
⊢ K.d j i ≫ φ.f i ≫ k = 0
have rw : φ.f j ≫ L.d j i ≫ k = 0
Tactic: rw [← φ.comm_assoc, hk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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
φ_1 : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
A : C
k : L.X i ⟶ A
j : ι
hj : c.prev i = j
hk : L.d j i ≫ k = 0
φ : K ⟶ L
rw : φ.f j ≫ L.d j i ≫ k = 0
⊢ K.d j i ≫ φ.f i ≫ k = 0
have rw₁ : Eq (α := K.X j ⟶ A) (φ.f j ≫ 0) 0
Tactic: rw [← φ.comm_assoc, hk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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
φ_1 : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
A : C
k : L.X i ⟶ A
j : ι
hj : c.prev i = j
hk : L.d j i ≫ k = 0
φ : K ⟶ L
rw : φ.f j ≫ L.d j i ≫ k = 0
rw₁ : Eq (α := K.X j ⟶ A) (φ.f j ≫ 0) 0
⊢ K.d j i ≫ φ.f i ≫ k = 0
have rw₂ : Eq.{v_1 + 1} (α := K.X j ⟶ A) 0 0
Tactic: rw [← φ.comm_assoc, hk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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
φ_1 : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
φ : K ⟶ L
⊢ (k ≫ φ.f i) ≫ L.d i j = 0
have rw : k ≫ φ.f i ≫ L.d i j = 0
Tactic: rw [assoc, φ.comm, reassoc_of% hk, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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
φ_1 : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
φ : K ⟶ L
rw : k ≫ φ.f i ≫ L.d i j = 0
⊢ (k ≫ φ.f i) ≫ L.d i j = 0
have rw₁ : k ≫ K.d i j ≫ φ.f j = 0
Tactic: rw [assoc, φ.comm, reassoc_of% hk, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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
φ_1 : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
φ : K ⟶ L
rw : k ≫ φ.f i ≫ L.d i j = 0
rw₁ : k ≫ K.d i j ≫ φ.f j = 0
⊢ (k ≫ φ.f i) ≫ L.d i j = 0
have rw₂ : Eq (α := A ⟶ L.X j) (0 ≫ φ.f j) 0
Tactic: rw [assoc, φ.comm, reassoc_of% hk, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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
φ_1 : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
φ : K ⟶ L
rw : k ≫ φ.f i ≫ L.d i j = 0
rw₁ : k ≫ K.d i j ≫ φ.f j = 0
rw₂ : Eq (α := A ⟶ L.X j) (0 ≫ φ.f j) 0
⊢ (k ≫ φ.f i) ≫ L.d i j = 0
have rw₃ : Eq.{v_1 + 1} (α := A ⟶ L.X j) 0 0
Tactic: rw [assoc, φ.comm, reassoc_of% hk, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (hypothesis)
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 : ι
hj : c.next i = j
h : K.d i j = 0
inst_2 : K.HasHomology i
⊢ IsIso (X := K.cycles i) (K.iCycles i)
have h₁ : Eq (α := K.X i ⟶ K.X (c.next i)) (K.d i (c.next i)) 0
Tactic: subst hj
Cleared hypotheses: j, hj, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (hypothesis)
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 : ι
hi : c.prev j = i
h : K.d i j = 0
inst_2 : K.HasHomology j
⊢ IsIso (Y := K.opcycles j) (K.pOpcycles j)
have h₁ : Eq (α := K.X (c.prev j) ⟶ K.X j) (K.d (c.prev j) j) 0
Tactic: obtain rfl := hi
Cleared hypotheses: i, hi, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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 : ι
hK : K.ExactAt i
L : HomologicalComplex.{v_1, u_1, u_2} C c
e : K ≅ L
⊢ L.ExactAt i
have rw : ∀ (hK : (K.sc i).Exact) {L : HomologicalComplex.{v_1, u_1, u_2} C c} (e : K ≅ L), (L.sc i).Exact
Tactic: rw [exactAt_iff] at hK ⊢
Cleared hypotheses: hK, L, e
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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
⊢ K.ExactAt i ↔ IsZero.{v_1, u_1} (K.sc i).homology
have rw : (K.sc i).Exact ↔ IsZero.{v_1, u_1} (K.sc i).homology
Tactic: rw [exactAt_iff, ShortComplex.exact_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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
rw : (K.sc i).Exact ↔ IsZero.{v_1, u_1} (K.sc i).homology
⊢ K.ExactAt i ↔ IsZero.{v_1, u_1} (K.sc i).homology
have rw₁ : IsZero.{v_1, u_1} (K.sc i).homology ↔ IsZero.{v_1, u_1} (K.sc i).homology
Tactic: rw [exactAt_iff, ShortComplex.exact_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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
hK : IsZero K
i : ι
⊢ K.ExactAt i
have h : IsZero.{v_1, u_1} (K.sc i).X₂
Tactic: apply ShortComplex.exact_of_isZero_X₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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 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.homology i ⟶ L.homology i) (homologyMap (-φ) i) (-homologyMap φ i)
have dsimp : Eq (α := K.homology i ⟶ L.homology i)
  (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (-φ)))
  (-ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
Tactic: dsimp [homologyMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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 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.homology i ⟶ L.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (-φ)))
    (-ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
have rw : Eq (α := K.homology i ⟶ L.homology i)
  (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (-φ)))
  (ShortComplex.homologyMap (-CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
Tactic: rw [← ShortComplex.homologyMap_neg]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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 L : HomologicalComplex.{v_1, u_1, u_2} C c
φ ψ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ homologyMap (φ + ψ) i = HAdd.hAdd (α := K.homology i ⟶ L.homology i) (homologyMap φ i) (homologyMap ψ i)
have dsimp : ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ + ψ)) =
  HAdd.hAdd (α := K.homology i ⟶ L.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ))
Tactic: dsimp [homologyMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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 L : HomologicalComplex.{v_1, u_1, u_2} C c
φ ψ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ + ψ)) =
    HAdd.hAdd (α := K.homology i ⟶ L.homology i)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ))
have rw : Eq (α := K.homology i ⟶ L.homology i)
  (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ + ψ)))
  (ShortComplex.homologyMap
    (HAdd.hAdd (α := Functor.obj (shortComplexFunctor C c i) K ⟶ Functor.obj (shortComplexFunctor C c i) L)
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ)
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
Tactic: rw [← ShortComplex.homologyMap_add]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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 L : HomologicalComplex.{v_1, u_1, u_2} C c
φ ψ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ homologyMap (φ - ψ) i = HSub.hSub (α := K.homology i ⟶ L.homology i) (homologyMap φ i) (homologyMap ψ i)
have dsimp : ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ - ψ)) =
  HSub.hSub (α := K.homology i ⟶ L.homology i)
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
    (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ))
Tactic: dsimp [homologyMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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 L : HomologicalComplex.{v_1, u_1, u_2} C c
φ ψ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ - ψ)) =
    HSub.hSub (α := K.homology i ⟶ L.homology i)
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ))
      (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ))
have rw : Eq (α := K.homology i ⟶ L.homology i)
  (ShortComplex.homologyMap (CategoryTheory.Functor.map (shortComplexFunctor C c i) (φ - ψ)))
  (ShortComplex.homologyMap
    (HSub.hSub (α := Functor.obj (shortComplexFunctor C c i) K ⟶ Functor.obj (shortComplexFunctor C c i) L)
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) φ)
      (CategoryTheory.Functor.map (shortComplexFunctor C c i) ψ)))
Tactic: rw [← ShortComplex.homologyMap_sub]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : CochainComplex.{v_1, u_1, 0} C ℕ
X : C
φ : X ⟶ K.X 0
inst_2 : HomologicalComplex.HasHomology K 0
hφ : Eq (α := X ⟶ K.X 1) (φ ≫ K.d 0 1) 0
⊢ IsIso (Y := HomologicalComplex.cycles K 0) (HomologicalComplex.liftCycles K φ 1 isIso_liftCycles_iff._proof_1 hφ) ↔
    { X₁ := X, X₂ := K.X 0, X₃ := K.X 1, f := φ, g := K.d 0 1, zero := hφ : ShortComplex.{v_1, u_1} C }.Exact ∧ Mono φ
have suffices : ∀ (i : ℕ) (hx : (ComplexShape.up ℕ).next 0 = i) (hφ : φ ≫ K.d 0 i = 0),
  IsIso (Y := HomologicalComplex.cycles K 0) (HomologicalComplex.liftCycles K φ i hx hφ) ↔
    { X₁ := X, X₂ := K.X 0, X₃ := K.X i, f := φ, g := K.d 0 i, zero := hφ : ShortComplex.{v_1, u_1} C }.Exact ∧ Mono φ
Tactic: suffices ∀ (i : ℕ) (hx : (ComplexShape.up ℕ).next 0 = i)
    (hφ : φ ≫ K.d 0 i = 0), IsIso (K.liftCycles φ i hx hφ) ↔
      (ShortComplex.mk _ _ hφ).Exact ∧ Mono φ from this 1 (by simp) hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
X : C
φ : K.X 0 ⟶ X
inst_2 : HomologicalComplex.HasHomology K 0
hφ : Eq (α := K.X 1 ⟶ X) (K.d 1 0 ≫ φ) 0
⊢ IsIso (X := HomologicalComplex.opcycles K 0)
      (HomologicalComplex.descOpcycles K φ 1 isIso_descOpcycles_iff._proof_1 hφ) ↔
    { X₁ := K.X 1, X₂ := K.X 0, X₃ := X, f := K.d 1 0, g := φ, zero := hφ : ShortComplex.{v_1, u_1} C }.Exact ∧ Epi φ
have suffices : ∀ (i : ℕ) (hx : (ComplexShape.down ℕ).prev 0 = i) (hφ : K.d i 0 ≫ φ = 0),
  IsIso (X := HomologicalComplex.opcycles K 0) (HomologicalComplex.descOpcycles K φ i hx hφ) ↔
    { X₁ := K.X i, X₂ := K.X 0, X₃ := X, f := K.d i 0, g := φ, zero := hφ : ShortComplex.{v_1, u_1} C }.Exact ∧ Epi φ
Tactic: suffices ∀ (i : ℕ) (hx : (ComplexShape.down ℕ).prev 0 = i)
    (hφ : K.d i 0 ≫ φ = 0), IsIso (K.descOpcycles φ i hx hφ) ↔
      (ShortComplex.mk _ _ hφ).Exact ∧ Epi φ from this 1 (by simp) hφ
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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 k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
⊢ Eq (α := K.cycles j ⟶ (K.sc' i j k).X₂)
    (CategoryStruct.comp (Y := (K.sc' i j k).cycles)
      (Iso.hom (K.cyclesIsoSc' i j k hi hk) : K.cycles j ⟶ (K.sc' i j k).cycles)
      ((K.sc' i j k).iCycles : (K.sc' i j k).cycles ⟶ (K.sc' i j k).X₂))
    (K.iCycles j)
have dsimp : Eq (α := K.cycles j ⟶ K.X j)
  (CategoryStruct.comp (Y := (K.sc' i j k).cycles)
      (ShortComplex.cyclesMap (NatTrans.app (Iso.hom (natIsoSc' C c i j k hi hk)) K)) (K.sc' i j k).iCycles :
    K.cycles j ⟶ K.X j)
  (K.iCycles j : K.cycles j ⟶ K.X j)
Tactic: dsimp [cyclesIsoSc']
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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 k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
⊢ Eq (α := K.cycles j ⟶ K.X j)
    (CategoryStruct.comp (Y := (K.sc' i j k).cycles)
        (ShortComplex.cyclesMap (NatTrans.app (Iso.hom (natIsoSc' C c i j k hi hk)) K)) (K.sc' i j k).iCycles :
      K.cycles j ⟶ K.X j)
    (K.iCycles j : K.cycles j ⟶ K.X j)
have simp : Eq (α := K.cycles j ⟶ K.X j) ((K.sc j).iCycles : (K.sc j).cycles ⟶ (K.sc j).X₂) (K.iCycles j : K.cycles j ⟶ K.X j)
Tactic: simp only [ShortComplex.cyclesMap_i, shortComplexFunctor_obj_X₂, shortComplexFunctor'_obj_X₂,
    natIsoSc'_hom_app_τ₂, comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex (goal)
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 k : ι
hi : c.prev j = i
hk : c.next j = k
inst_2 : K.HasHomology j
inst_3 : (K.sc' i j k).HasHomology
⊢ Eq (α := (K.sc' i j k).X₂ ⟶ K.opcycles j)
    (CategoryStruct.comp (Y := (K.sc' i j k).opcycles)
      ((K.sc' i j k).pOpcycles : (K.sc' i j k).X₂ ⟶ (K.sc' i j k).opcycles)
      (Iso.inv (K.opcyclesIsoSc' i j k hi hk) : (K.sc' i j k).opcycles ⟶ K.opcycles j))
    (K.pOpcycles j)
have dsimp : Eq (α := K.X j ⟶ K.opcycles j)
  (CategoryStruct.comp (Y := (K.sc' i j k).opcycles) (K.sc' i j k).pOpcycles
      (ShortComplex.opcyclesMap (NatTrans.app (Iso.inv (natIsoSc' C c i j k hi hk)) K)) :
    K.X j ⟶ K.opcycles j)
  (K.pOpcycles j : K.X j ⟶ K.opcycles j)
Tactic: dsimp [opcyclesIsoSc']