-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
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
refine_1 :
  ∀
    (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))
        (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))),
    x ∈ coboundaries K L n
refine_2 :
  ∀ (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))
⊢ 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)) ↔
    x ∈ coboundaries K L n

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩