awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
S₁ S₂ : ShortComplex.{v, u} C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
dsimp :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
    (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
      triangleOfSESδ ⋯ ≫
        Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (Functor.map Q (Functor.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0) f.τ₁)) ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
    (Functor.map (singleFunctor C 0) f.τ₃ ≫
      NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
    (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
      triangleOfSESδ ⋯ ≫
        Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (Functor.map (SingleFunctors.functor (CochainComplex.singleFunctors C) 0 ⋙ Q) f.τ₁) ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))
    (Functor.map (singleFunctor C 0) f.τ₃ ≫
      NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))

Tactic:
dsimp [CochainComplex.singleFunctors]

Premises used: CochainComplex.singleFunctors
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
S : ShortComplex.{v, u} C
hS : S.ShortExact
S₁ S₂ : ShortComplex.{v, u} C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₁.X₃)
      (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁)))
    (NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₁.X₃ ≫
      CategoryStruct.comp (Y := Functor.obj (singleFunctor C 0) S₂.X₃)
        (Functor.map Q (Functor.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0) f.τ₃) :
          Quiver.Hom (V := DerivedCategory.{w, v, u} C)
            (Functor.obj Q (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) 0) S₁.X₃))
            (Functor.obj Q (Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) 0) S₂.X₃)))
        (CategoryStruct.comp (Y :=
            Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1) (Functor.obj (singleFunctor C 0) S₂.X₁))
            (triangleOfSESδ ⋯ :
              Quiver.Hom (V := DerivedCategory.{w, v, u} C)
                (Functor.obj Q (X₃ (S₂.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))))
                (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
                  (Functor.obj Q (X₁ (S₂.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0))))))
            (Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
              (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁)) :
          Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C 0) S₂.X₃)
            (Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
              (Functor.obj (singleFunctor C 0) S₂.X₁))))
    (Functor.map (singleFunctor C 0) f.τ₃ ≫
      NatTrans.app (SingleFunctors.Hom.hom (Iso.hom (singleFunctorsPostcompQIso C)) 0) S₂.X₃ ≫
        triangleOfSESδ ⋯ ≫
          Functor.map (shiftFunctor (DerivedCategory.{w, v, u} C) (A := ℤ) 1)
            (NatTrans.app (SingleFunctors.Hom.hom (Iso.inv (singleFunctorsPostcompQIso C)) 0) S₂.X₁))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
⊢ Eq.{w + 1} (α := SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n)
    ((fun (y : Cocycle K L n) ↦
        (SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
            ((AddEquiv.symm Cocycle.equivHomShift :
                (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
              y) :
          SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n))
      y₁)
    ((fun (y : Cocycle K L n) ↦
        (SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
            ((AddEquiv.symm Cocycle.equivHomShift :
                (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
              y) :
          SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n))
      y₂)

Tactic:
(SmallShiftedHom.equiv _ DerivedCategory.Q).injective ?_

Premises used: DerivedCategory.Q, Equiv.injective, CategoryTheory.Localization.SmallShiftedHom.equiv
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
refine :
  Eq (α := ShiftedHom (C := DerivedCategory C) (Functor.obj DerivedCategory.Q K) (Functor.obj DerivedCategory.Q L) n)
    ((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q :
        (a : SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) →
          ShiftedHom (DerivedCategory.Q.obj K) (DerivedCategory.Q.obj L) n)
      ((fun (y : Cocycle K L n) ↦
          (SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
              ((AddEquiv.symm Cocycle.equivHomShift :
                  (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
                y) :
            SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n))
        y₁))
    ((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q :
        (a : SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) →
          ShiftedHom (DerivedCategory.Q.obj K) (DerivedCategory.Q.obj L) n)
      ((fun (y : Cocycle K L n) ↦
          (SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
              ((AddEquiv.symm Cocycle.equivHomShift :
                  (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
                y) :
            SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n))
        y₂))
⊢ Eq.{w + 1} (α := SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n)
    ((fun (y : Cocycle K L n) ↦
        (SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
            ((AddEquiv.symm Cocycle.equivHomShift :
                (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
              y) :
          SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n))
      y₁)
    ((fun (y : Cocycle K L n) ↦
        (SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
            ((AddEquiv.symm Cocycle.equivHomShift :
                (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
              y) :
          SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n))
      y₂)

Tactic:
refine (SmallShiftedHom.equiv _ DerivedCategory.Q).injective ?_

Premises used: DerivedCategory.Q, Equiv.injective, CategoryTheory.Localization.SmallShiftedHom.equiv
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
h₁ :
  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)
      y₁)
    ((AddEquiv.symm Cocycle.equivHomShift :
        (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
      y₂)
⊢ Eq (α := ShiftedHom (C := DerivedCategory C) (Functor.obj DerivedCategory.Q K) (Functor.obj DerivedCategory.Q L) n)
    (CategoryStruct.comp (Y :=
        Functor.obj DerivedCategory.Q (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L))
        (CategoryTheory.Functor.map DerivedCategory.Q
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
            y₁))
        (NatTrans.app (Iso.hom (Functor.commShiftIso DerivedCategory.Q n)) L) :
      Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q K)
        (Functor.obj (CategoryTheory.shiftFunctor (DerivedCategory C) n) (Functor.obj DerivedCategory.Q L)))
    (CategoryStruct.comp (Y :=
        Functor.obj DerivedCategory.Q (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L))
        (CategoryTheory.Functor.map DerivedCategory.Q
          ((AddEquiv.symm Cocycle.equivHomShift :
              (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
            y₂))
        (NatTrans.app (Iso.hom (Functor.commShiftIso DerivedCategory.Q n)) L) :
      Quiver.Hom (V := DerivedCategory C) (Functor.obj DerivedCategory.Q K)
        (Functor.obj (CategoryTheory.shiftFunctor (DerivedCategory C) n) (Functor.obj DerivedCategory.Q L)))

Tactic:
rw [cancel_mono, DerivedCategory.Q_map_eq_of_homotopy]

Premises used: CategoryTheory.cancel_mono, DerivedCategory.Q_map_eq_of_homotopy
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
h₁ :
  Eq.{max 1 (v + 1)} (α :=
    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))
    (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)
        y₁))
    (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)
        y₂))
⊢ 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)
      y₁)
    ((AddEquiv.symm Cocycle.equivHomShift :
        (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
      y₂)

Tactic:
apply HomotopyCategory.homotopyOfEq

Premises used: HomotopyCategory.homotopyOfEq
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
h₁ :
  Eq (α :=
    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))
    ((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))
    ((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))
⊢ Eq.{max 1 (v + 1)} (α :=
    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))
    (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)
        y₁))
    (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)
        y₂))

Tactic:
rw [← toHom_mk, ← toHom_mk]

Premises used: CochainComplex.HomComplex.CohomologyClass.toHom_mk
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
h₁ : mk y₁ = mk y₂
⊢ Eq (α :=
    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))
    ((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))
    ((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))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
⊢ mk y₁ = mk y₂

Tactic:
Quotient.sound h

Premises used: CochainComplex.HomComplex.CohomologyClass.mk, CochainComplex.HomComplex.CohomologyClass, Quotient.sound
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := HasDerivedCategory.standard C
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
⊢ mk y₁ = mk y₂

Tactic:
exact Quotient.sound h

Premises used: Quotient.sound
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : Cocycle K L n
⊢ Eq.{w + 1} (α := SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) (mk x).toSmallShiftedHom
    (SmallShiftedHom.mk (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))
      ((AddEquiv.symm Cocycle.equivHomShift :
          (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
        x))

Tactic:
rfl

Premises used: CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom, rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.SmallShiftedHom
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
n : ℤ
inst_2 : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
inst_3 : HasDerivedCategory.{u_1, v, u} C
x : Cocycle K L n
⊢ Eq.{u_1 + 1} (α :=
    ShiftedHom (C := DerivedCategory.{u_1, v, u} C) (Functor.obj DerivedCategory.Q K) (Functor.obj DerivedCategory.Q L)
      n)
    ((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q :
          (a : SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) →
            ShiftedHom (DerivedCategory.Q.obj K) (DerivedCategory.Q.obj L) n)
        (mk x).toSmallShiftedHom :
      ShiftedHom (C := DerivedCategory.{u_1, v, u} C) (Functor.obj DerivedCategory.Q K)
        (Functor.obj DerivedCategory.Q L) n)
    (ShiftedHom.map
        ((AddEquiv.symm Cocycle.equivHomShift :
            (a : Cocycle K L n) → K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)
          x)
        DerivedCategory.Q :
      ShiftedHom (C := DerivedCategory.{u_1, v, u} C) (Functor.obj DerivedCategory.Q K)
        (Functor.obj DerivedCategory.Q L) n)

Tactic:
simp [toSmallShiftedHom_mk]

Premises used: CochainComplex.HomComplex.CohomologyClass.toSmallShiftedHom_mk
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X Y : DerivedCategory.{w, v, u} C
e : X ≅ Y
K : CochainComplex.{v, u, 0} C ℤ
e' : X ≅ Functor.obj Q K
h : K.IsStrictlyLE n
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x : Y ≅ Functor.obj Q K), K.IsStrictlyLE n

Tactic:
⟨K, e.symm ≪≫ e', inferInstance⟩

Premises used: inferInstance, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X Y : DerivedCategory.{w, v, u} C
e : X ≅ Y
K : CochainComplex.{v, u, 0} C ℤ
e' : X ≅ Functor.obj Q K
h : K.IsStrictlyLE n
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x : Y ≅ Functor.obj Q K), K.IsStrictlyLE n

Tactic:
exact ⟨K, e.symm ≪≫ e', inferInstance⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X Y : DerivedCategory.{w, v, u} C
e : X ≅ Y
K : CochainComplex.{v, u, 0} C ℤ
e' : X ≅ Functor.obj Q K
h : K.IsStrictlyGE n
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x : Y ≅ Functor.obj Q K), K.IsStrictlyGE n

Tactic:
⟨K, e.symm ≪≫ e', inferInstance⟩

Premises used: inferInstance, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Iso.symm
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
X Y : DerivedCategory.{w, v, u} C
e : X ≅ Y
K : CochainComplex.{v, u, 0} C ℤ
e' : X ≅ Functor.obj Q K
h : K.IsStrictlyGE n
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x : Y ≅ Functor.obj Q K), K.IsStrictlyGE n

Tactic:
exact ⟨K, e.symm ≪≫ e', inferInstance⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n a n' : ℤ
h : a + n' = n
X : DerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
e : X ≅ Functor.obj Q K
h_1 : K.IsStrictlyLE n
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x :
    Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) a) X ≅ Functor.obj Q K), K.IsStrictlyLE n'

Tactic:
⟨(shiftFunctor (CochainComplex C ℤ) a).obj K,
      (shiftFunctor (DerivedCategory C) a).mapIso e ≪≫ (Q.commShiftIso a).symm.app K,
      K.isStrictlyLE_shift n a n' h⟩

Premises used: DerivedCategory, DerivedCategory.Q, CategoryTheory.shiftFunctor, Int, CochainComplex, CategoryTheory.Iso.trans, CochainComplex.isStrictlyLE_shift, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Functor.mapIso, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n a n' : ℤ
h : a + n' = n
X : DerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
e : X ≅ Functor.obj Q K
h_1 : K.IsStrictlyLE n
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (x :
    Functor.obj (shiftFunctor (DerivedCategory.{w, v, u} C) a) X ≅ Functor.obj Q K), K.IsStrictlyLE n'

Tactic:
exact ⟨(shiftFunctor (CochainComplex C ℤ) a).obj K,
      (shiftFunctor (DerivedCategory C) a).mapIso e ≪≫ (Q.commShiftIso a).symm.app K,
      K.isStrictlyLE_shift n a n' h⟩