awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n m_1 p m : ℤ
hm : m + 1 = n
β : Cochain K L m
property : δ m n β ∈ cocycle K L n
simp :
  Nonempty.{max 1 (v + 1)}
    (Homotopy
      (Cocycle.rightShift (Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n) (δ m n β) property) n 0
          ⋯).homOf
      0)
⊢ Membership.mem (γ := AddSubgroup (Cocycle K L n))
    (AddMonoidHom.ker (M :=
      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))
      (AddMonoidHom.comp (Functor.mapAddHom (HomotopyCategory.quotient C (ComplexShape.up ℤ)))
        (AddEquiv.toAddMonoidHom (AddEquiv.symm Cocycle.equivHomShift))))
    (Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n) (δ m n β) property)

Tactic:
simp only [AddMonoidHom.mem_ker, AddMonoidHom.coe_comp, AddMonoidHom.coe_coe,
      AddEquiv.toAddMonoidHom_eq_coe, Function.comp_apply, Cocycle.equivHomShift_symm_apply,
      Functor.mapAddHom_apply, HomotopyCategory.quotient_map_eq_zero_iff]

Premises used: AddEquiv.toAddMonoidHom_eq_coe, HomotopyCategory.quotient_map_eq_zero_iff, AddMonoidHom.coe_coe, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_apply, CategoryTheory.Functor.mapAddHom_apply, AddMonoidHom.coe_comp, Function.comp_apply, AddMonoidHom.mem_ker
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n m_1 p m : ℤ
hm : m + 1 = n
β : Cochain K L m
property : δ m n β ∈ cocycle K L n
⊢ -1 + n = m

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n m_1 p m : ℤ
hm : m + 1 = n
β : Cochain K L m
property : δ m n β ∈ cocycle K L n
⊢ Cochain.ofHom
      (Cocycle.rightShift (Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n) (δ m n β) property) n 0
          ⋯).homOf =
    δ (-1) 0 (n.negOnePow • β.rightShift n (-1) ⋯) + Cochain.ofHom 0

Tactic:
simp [Cochain.δ_rightShift _ _ _ _ _ _ (zero_add n), smul_smul]

Premises used: smul_smul, zero_add, CochainComplex.HomComplex.Cochain.δ_rightShift
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type u_1
inst_2 : Ring R
inst_3 : Linear.{u_1, v, u} R C
K L : CochainComplex.{v, u, 0} C ℤ
n m_1 p m : ℤ
hm : m + 1 = n
β : Cochain K L m
property : δ m n β ∈ cocycle K L n
⊢ Nonempty.{max 1 (v + 1)}
    (Homotopy
      (Cocycle.rightShift (Subtype.mk (p := fun (x : Cochain K L n) ↦ x ∈ cocycle K L n) (δ m n β) property) n 0
          ⋯).homOf
      0)

Tactic:
exact ⟨(Cochain.equivHomotopy _ _).symm ⟨n.negOnePow • β.rightShift _ _ (by lia),
      by simp [Cochain.δ_rightShift _ _ _ _ _ _ (zero_add n), smul_smul]⟩⟩
-- 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
⊢ 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))
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ))
        ((AddEquiv.symm Cocycle.equivHomShift :
            (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
          x) :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- 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
⊢ 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:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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
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))
refine_1 : ∃ (m : ℤ), m + 1 = n ∧ ∃ (β : Cochain K L m), δ m n β = (↑x : Cochain K L n)
⊢ x ∈ coboundaries K L n

Tactic:
simp only [coboundaries, exists_prop, AddSubgroup.mem_mk, AddSubmonoid.mem_mk,
      AddSubsemigroup.mem_mk, Set.mem_setOf_eq]

Premises used: CochainComplex.HomComplex.coboundaries, AddSubsemigroup.mem_mk, Set.mem_setOf_eq, exists_prop, AddSubgroup.mem_mk, AddSubmonoid.mem_mk
-- 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
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))
⊢ Nonempty.{max 1 (v + 1)}
    (Homotopy.{v, u, 0} (ι := ℤ) (V := C) (c := ComplexShape.up ℤ) (C := K) (D :=
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
        x)
      0)

Tactic:
rw [toHom_mk, HomotopyCategory.quotient_map_eq_zero_iff] at h

Premises used: HomotopyCategory.quotient_map_eq_zero_iff, CochainComplex.HomComplex.CohomologyClass.toHom_mk
-- 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
h :
  Nonempty.{max 1 (v + 1)}
    (Homotopy.{v, u, 0} (ι := ℤ) (V := C) (c := ComplexShape.up ℤ) (C := K) (D :=
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
        x)
      0)
refine_1 :
  ∀ (γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L) (-1))
    (h :
      Cochain.ofHom
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
            x) =
        δ (-1) 0 γ + Cochain.ofHom 0),
    ∃ (m : ℤ), m + 1 = n ∧ ∃ (β : Cochain K L m), δ m n β = (↑x : Cochain K L n)
⊢ ∃ (m : ℤ), m + 1 = n ∧ ∃ (β : Cochain K L m), δ m n β = (↑x : Cochain K L n)

Tactic:
obtain ⟨γ, h⟩ := Cochain.equivHomotopy _ _ h.some

Premises used: Nonempty.some, CochainComplex.HomComplex.Cochain.equivHomotopy, DFunLike.coe
-- 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
h_1 :
  Nonempty.{max 1 (v + 1)}
    (Homotopy.{v, u, 0} (ι := ℤ) (V := C) (c := ComplexShape.up ℤ) (C := K) (D :=
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
        x)
      0)
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L) (-1)
h :
  Cochain.ofHom
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
        x) =
    δ (-1) 0 γ + Cochain.ofHom 0
⊢ (↑x : Cochain K L n).rightShift n 0 ⋯ = δ (-1) 0 γ

Tactic:
simp only [Cochain.ofHom_zero, add_zero, Cocycle.equivHomShift_symm_apply,
      Cocycle.cochain_ofHom_homOf_eq_coe, Cocycle.rightShift_coe] at h

Premises used: CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_apply, CochainComplex.HomComplex.Cochain.ofHom_zero, add_zero, CochainComplex.HomComplex.Cocycle.rightShift_coe
-- 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
h_1 :
  Nonempty.{max 1 (v + 1)}
    (Homotopy.{v, u, 0} (ι := ℤ) (V := C) (c := ComplexShape.up ℤ) (C := K) (D :=
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
        x)
      0)
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L) (-1)
h : (↑x : Cochain K L n).rightShift n 0 ⋯ = δ (-1) 0 γ
⊢ n - 1 + 1 = n

Tactic:
simp
-- 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
h_1 :
  Nonempty.{max 1 (v + 1)}
    (Homotopy.{v, u, 0} (ι := ℤ) (V := C) (c := ComplexShape.up ℤ) (C := K) (D :=
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
        x)
      0)
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L) (-1)
h : (↑x : Cochain K L n).rightShift n 0 ⋯ = δ (-1) 0 γ
⊢ -1 + n = n - 1

Tactic:
lia
-- 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
h_1 :
  Nonempty.{max 1 (v + 1)}
    (Homotopy.{v, u, 0} (ι := ℤ) (V := C) (c := ComplexShape.up ℤ) (C := K) (D :=
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
        x)
      0)
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L) (-1)
h : (↑x : Cochain K L n).rightShift n 0 ⋯ = δ (-1) 0 γ
⊢ δ (n - 1) n (n.negOnePow • γ.rightUnshift (n - 1) ⋯) = (↑x : Cochain K L n)

Tactic:
simp [Cochain.δ_rightUnshift _ _ _ _ _ (zero_add n), smul_smul, ← h]

Premises used: smul_smul, zero_add, CochainComplex.HomComplex.Cochain.δ_rightUnshift
-- 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
h_1 :
  Nonempty.{max 1 (v + 1)}
    (Homotopy.{v, u, 0} (ι := ℤ) (V := C) (c := ComplexShape.up ℤ) (C := K) (D :=
      Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
        x)
      0)
γ : Cochain K (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L) (-1)
h : (↑x : Cochain K L n).rightShift n 0 ⋯ = δ (-1) 0 γ
⊢ ∃ (m : ℤ), m + 1 = n ∧ ∃ (β : Cochain K L m), δ m n β = (↑x : Cochain K L n)

Tactic:
exact ⟨n - 1, by simp, n.negOnePow • γ.rightUnshift _ (by lia),
      by simp [Cochain.δ_rightUnshift _ _ _ _ _ (zero_add n), smul_smul, ← h]⟩
-- 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
h : x ∈ coboundaries K L n
⊢ mk x = 0

Tactic:
rw [← mk_eq_zero_iff] at h

Premises used: CochainComplex.HomComplex.CohomologyClass.mk_eq_zero_iff
-- 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
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
refine_2₁ 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
⊢ 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))

Tactic:
rw [h, map_zero]

Premises used: map_zero
-- 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 : ℤ
⊢ 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))

Tactic:
⟨fun x y h ↦ ?_, fun f ↦ ?_⟩

Premises used: And.intro, Function.Bijective
-- 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 : ℤ
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
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
⊢ 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))

Tactic:
refine ⟨fun x y h ↦ ?_, fun f ↦ ?_⟩