awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x : Cocycle K L n
h : x ∈ coboundaries K L n
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk x) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    (0 :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
have h₁ : mk x = 0
Tactic: rw [← mk_eq_zero_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x : Cocycle K L n
h : mk x = 0
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk x) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    (0 :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
have refine_2 : Eq.{v + 1} (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
  ((toHom :
      (a : CohomologyClass K L n) →
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
          (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
            ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
    0)
  0
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x : Cocycle K L n
h : mk x = 0
refine_2 :
  Eq.{v + 1} (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
        (a : CohomologyClass K L n) →
          (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
              ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
      0)
    0
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk x) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    (0 :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
have refine_2₁ : Eq.{v + 1} (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
  0 0
Tactic: rw [h, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ Function.Bijective.{v + 1, v + 1} (α := CohomologyClass K L n) (β :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    (⇑toHom :
      (a : CohomologyClass K L n) →
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
          (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
            ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
have refine_1 : ∀ (x y : CohomologyClass K L n)
  (h :
    Eq (α :=
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
      ((toHom :
            (a : CohomologyClass K L n) →
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
                (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                  ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
          x :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
      ((toHom :
            (a : CohomologyClass K L n) →
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
                (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                  ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
          y :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))),
  x = y
Tactic: refine ⟨fun x y h ↦ ?_, fun f ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
refine_1 :
  ∀ (x y : CohomologyClass K L n)
    (h :
      Eq (α :=
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
        ((toHom :
              (a : CohomologyClass K L n) →
                (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
                  (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                    ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
            x :
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
            Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
        ((toHom :
              (a : CohomologyClass K L n) →
                (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
                  (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                    ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
            y :
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
            Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
              (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))),
    x = y
⊢ Function.Bijective.{v + 1, v + 1} (α := CohomologyClass K L n) (β :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    (⇑toHom :
      (a : CohomologyClass K L n) →
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
          (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
            ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
have refine_2 : ∀
  (f :
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L)),
  ∃ (a : CohomologyClass K L n),
    (toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        a =
      f
Tactic: refine ⟨fun x y h ↦ ?_, fun f ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x y : CohomologyClass K L n
h :
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        x :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        y :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
⊢ x = y
have refine_1 : ∀ (x : Cocycle K L n)
  (h :
    Eq (α :=
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
      ((toHom :
            (a : CohomologyClass K L n) →
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
                (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                  ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
          (mk x) :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
      ((toHom :
            (a : CohomologyClass K L n) →
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
                (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                  ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
          y :
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
          Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
            (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))),
  mk x = y
Tactic: obtain ⟨x, rfl⟩ := x.mk_surjective
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x y : Cocycle K L n
h :
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk x) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk y) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
⊢ mk x = mk y
have refine_1 : mk x - mk y = 0
Tactic: rw [← sub_eq_zero, ← mk_sub, mk_eq_zero_iff, ← toHom_mk_eq_zero_iff,
      mk_sub, map_sub, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x y : Cocycle K L n
h :
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk x) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk y) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
refine_1 : mk x - mk y = 0
⊢ mk x = mk y
have refine_1₁ : mk (x - y) = 0
Tactic: rw [← sub_eq_zero, ← mk_sub, mk_eq_zero_iff, ← toHom_mk_eq_zero_iff,
      mk_sub, map_sub, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x y : Cocycle K L n
h :
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk x) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk y) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
refine_1 : mk x - mk y = 0
refine_1₁ : mk (x - y) = 0
⊢ mk x = mk y
have refine_1₂ : x - y ∈ coboundaries K L n
Tactic: rw [← sub_eq_zero, ← mk_sub, mk_eq_zero_iff, ← toHom_mk_eq_zero_iff,
      mk_sub, map_sub, h, sub_self]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
x y : Cocycle K L n
h :
  Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk x) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
    ((toHom :
          (a : CohomologyClass K L n) →
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
              (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
        (mk y) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
refine_1 : mk x - mk y = 0
refine_1₁ : mk (x - y) = 0
refine_1₂ : x - y ∈ coboundaries K L n
⊢ mk x = mk y
have refine_1₃ : Eq (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
      (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
  ((toHom :
        (a : CohomologyClass K L n) →
          (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶
            (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
              ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L))
      (mk (x - y)) :
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
  (0 :
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))
Tactic: rw [← sub_eq_zero, ← mk_sub, mk_eq_zero_iff, ← toHom_mk_eq_zero_iff,
      mk_sub, map_sub, h, sub_self]