awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKInjective
inst_3 : L.IsKInjective
f : K ⟶ L
h : QuasiIso f
obtain :
  ∀
    (g :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
    (hg :
      CategoryTheory.Functor.map Qh g =
        NatTrans.app (Iso.hom (quotientCompQhIso C)) L ≫
          inv (CategoryTheory.Functor.map Q f) ≫ NatTrans.app (Iso.inv (quotientCompQhIso C)) K),
    IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
⊢ IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)

Tactic:
obtain ⟨g, hg⟩ := (Qh_map_bijective _ _).surjective
    ((quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K)

Premises used: CochainComplex.IsKInjective.Qh_map_bijective, DerivedCategory.Q, CategoryTheory.Functor.map, Function.Bijective.surjective, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, DerivedCategory.quotientCompQhIso, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKInjective
inst_3 : L.IsKInjective
f : K ⟶ L
h : QuasiIso f
g :
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K
hg :
  CategoryTheory.Functor.map Qh g =
    NatTrans.app (Iso.hom (quotientCompQhIso C)) L ≫
      inv (CategoryTheory.Functor.map Q f) ≫ NatTrans.app (Iso.inv (quotientCompQhIso C)) K
⊢ IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)

Tactic:
⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩

Premises used: CochainComplex.IsKInjective.Qh_map_bijective, Function.Bijective.injective, And.intro, Exists.intro, CategoryTheory.IsIso.mk
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKInjective
inst_3 : L.IsKInjective
f : K ⟶ L
h : QuasiIso f
g :
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K
hg :
  CategoryTheory.Functor.map Qh g =
    NatTrans.app (Iso.hom (quotientCompQhIso C)) L ≫
      inv (CategoryTheory.Functor.map Q f) ≫ NatTrans.app (Iso.inv (quotientCompQhIso C)) K
refine_1 :
  Eq (α :=
    Quiver.Hom (V := DerivedCategory C)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)))
    (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f ≫ g))
    (CategoryTheory.Functor.map Qh (𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)))
refine_2 :
  Eq (α :=
    Quiver.Hom (V := DerivedCategory C)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L))
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)))
    (CategoryTheory.Functor.map Qh (g ≫ CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f))
    (CategoryTheory.Functor.map Qh (𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)))
⊢ IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)

Tactic:
refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKInjective
inst_3 : L.IsKInjective
f : K ⟶ L
h : QuasiIso f
g :
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K
hg :
  CategoryTheory.Functor.map Qh g =
    NatTrans.app (Iso.hom (quotientCompQhIso C)) L ≫
      inv (CategoryTheory.Functor.map Q f) ≫ NatTrans.app (Iso.inv (quotientCompQhIso C)) K
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)))
    (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f ≫ g))
    (CategoryTheory.Functor.map Qh (𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)))

Tactic:
simp [hg]
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKInjective
inst_3 : L.IsKInjective
f : K ⟶ L
h : QuasiIso f
g :
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K
hg :
  CategoryTheory.Functor.map Qh g =
    NatTrans.app (Iso.hom (quotientCompQhIso C)) L ≫
      inv (CategoryTheory.Functor.map Q f) ≫ NatTrans.app (Iso.inv (quotientCompQhIso C)) K
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L))
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)))
    (CategoryTheory.Functor.map Qh (g ≫ CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f))
    (CategoryTheory.Functor.map Qh (𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)))

Tactic:
simp [hg, ← quotientCompQhIso_inv_naturality, -NatTrans.naturality]

Premises used: DerivedCategory.quotientCompQhIso_inv_naturality, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective
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 : L.IsKInjective
this : HasDerivedCategory C := HasDerivedCategory.standard C
rw :
  Function.Bijective (α := CohomologyClass K L n) (β :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh) K)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)))
    (Function.comp (β :=
      Quiver.Hom (V := DerivedCategory C) (Functor.obj Q K)
        (Functor.obj (Q ⋙ CategoryTheory.shiftFunctor (DerivedCategory C) n) L))
      (⇑(Iso.homCongr (Iso.app (Iso.symm (quotientCompQhIso C)) K)
            (Iso.trans (Y := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n ⋙ Q) L)
              (Iso.app (Iso.symm (Functor.commShiftIso Q n)) L)
              (Iso.app (Iso.symm (quotientCompQhIso C))
                (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)))) :
        (a : Q.obj K ⟶ (Q ⋙ CategoryTheory.shiftFunctor (DerivedCategory C) n).obj L) →
          (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj K ⟶
            (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj
              ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L))
      (Function.comp (β := SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n)
        (⇑(SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) Q) :
          (a : SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) →
            ShiftedHom (Q.obj K) (Q.obj L) n)
        toSmallShiftedHom))
⊢ Function.Bijective.{v + 1, w + 1} (α := CohomologyClass K L n) (β :=
    SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) toSmallShiftedHom

Tactic:
rw [← Function.Bijective.of_comp_iff'
      (SmallShiftedHom.equiv _ DerivedCategory.Q).bijective,
    ← Function.Bijective.of_comp_iff' (Iso.homCongr ((quotientCompQhIso C).symm.app K)
      ((Q.commShiftIso n).symm.app L ≪≫ (quotientCompQhIso C).symm.app (L⟦n⟧))).bijective]

Premises used: Equiv.bijective, DerivedCategory.Q, CategoryTheory.shiftFunctor, CategoryTheory.Iso.homCongr, CategoryTheory.Iso.trans, Function.Bijective.of_comp_iff', CategoryTheory.Iso.symm, DerivedCategory.quotientCompQhIso, CategoryTheory.Localization.SmallShiftedHom.equiv, CategoryTheory.Iso.app, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective
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 : L.IsKInjective
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Function.Bijective (α := CohomologyClass K L n) (β :=
    Quiver.Hom (V := DerivedCategory C)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
      (Functor.obj Qh
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))))
    (CategoryTheory.Functor.map Qh ∘
      (⇑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:
(CochainComplex.IsKInjective.Qh_map_bijective _ _).comp (toHom_bijective K L n)

Premises used: CochainComplex.IsKInjective.Qh_map_bijective, CochainComplex.HomComplex.CohomologyClass.toHom_bijective, Function.Bijective.comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℕ
inst_2 : ∀ (n : ℕ), Injective.{v, u} (K.X n)
inst_3 : ∀ (n : ℕ), Injective.{v, u} (L.X n)
f : K ⟶ L
rw :
  QuasiIso (K := extend K ComplexShape.embeddingUpNat) (extendMap f ComplexShape.embeddingUpNat) ↔
    homotopyEquivalences C (ComplexShape.up ℕ) f
rw₁ :
  homotopyEquivalences C (ComplexShape.up ℤ) (X := extend K ComplexShape.embeddingUpNat)
      (extendMap f ComplexShape.embeddingUpNat) ↔
    homotopyEquivalences C (ComplexShape.up ℕ) f
rw₂ rw₃ : homotopyEquivalences C (ComplexShape.up ℕ) f ↔ homotopyEquivalences C (ComplexShape.up ℕ) f
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.up ℕ) f

Tactic:
rw [← quasiIso_extendMap_iff _ ComplexShape.embeddingUpNat,
    CochainComplex.IsKInjective.quasiIso_iff,
    homotopyEquivalences_extendMap_iff]

Premises used: HomologicalComplex.quasiIso_extendMap_iff, CochainComplex.IsKInjective.quasiIso_iff, HomologicalComplex.homotopyEquivalences_extendMap_iff, ComplexShape.embeddingUpNat
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{u_1, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
L : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
inst_3 : K.IsKProjective
⊢ Function.Bijective.{v + 1, u_1 + 1} (α := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K ⟶ L) (β :=
    Quiver.Hom (V := DerivedCategory.{u_1, v, u} C)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)) (Functor.obj Qh L))
    (CategoryTheory.Functor.map Qh)

Tactic:
(CochainComplex.IsKProjective.leftOrthogonal K).map_bijective_of_isTriangulated _ _

Premises used: CategoryTheory.ObjectProperty.leftOrthogonal.map_bijective_of_isTriangulated, CochainComplex.IsKProjective.leftOrthogonal
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKProjective
inst_3 : L.IsKProjective
f : K ⟶ L
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.up ℤ) f

Tactic:
⟨fun _ ↦ ?_, fun hf ↦ homotopyEquivalences_le_quasiIso _ _ _ hf⟩

Premises used: homotopyEquivalences_le_quasiIso, Int, Iff.intro, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKProjective
inst_3 : L.IsKProjective
f : K ⟶ L
refine : QuasiIso f → homotopyEquivalences C (ComplexShape.up ℤ) f
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.up ℤ) f

Tactic:
refine ⟨fun _ ↦ ?_, fun hf ↦ homotopyEquivalences_le_quasiIso _ _ _ hf⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKProjective
inst_3 : L.IsKProjective
f : K ⟶ L
h : QuasiIso f
rw :
  IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
⊢ homotopyEquivalences C (ComplexShape.up ℤ) f

Tactic:
rw [← HomotopyCategory.inverseImage_quotient_isomorphisms,
    MorphismProperty.inverseImage_iff, MorphismProperty.isomorphisms.iff]

Premises used: CategoryTheory.MorphismProperty.isomorphisms.iff, CategoryTheory.MorphismProperty.inverseImage_iff, HomotopyCategory.inverseImage_quotient_isomorphisms
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKProjective
inst_3 : L.IsKProjective
f : K ⟶ L
h : QuasiIso f
obtain :
  ∀
    (g :
      Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L ⟶
        Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
    (hg :
      CategoryTheory.Functor.map Qh g =
        NatTrans.app (Iso.hom (quotientCompQhIso C)) L ≫
          inv (CategoryTheory.Functor.map Q f) ≫ NatTrans.app (Iso.inv (quotientCompQhIso C)) K),
    IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
      (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
⊢ IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)

Tactic:
obtain ⟨g, hg⟩ := (Qh_map_bijective _ _).surjective
    ((quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K)

Premises used: DerivedCategory.Q, CategoryTheory.Functor.map, CochainComplex.IsKProjective.Qh_map_bijective, Function.Bijective.surjective, CategoryTheory.CategoryStruct.comp, CategoryTheory.inv, DerivedCategory.quotientCompQhIso, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKProjective
inst_3 : L.IsKProjective
f : K ⟶ L
h : QuasiIso f
g :
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K
hg :
  CategoryTheory.Functor.map Qh g =
    NatTrans.app (Iso.hom (quotientCompQhIso C)) L ≫
      inv (CategoryTheory.Functor.map Q f) ≫ NatTrans.app (Iso.inv (quotientCompQhIso C)) K
⊢ IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)

Tactic:
⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩

Premises used: Function.Bijective.injective, CochainComplex.IsKProjective.Qh_map_bijective, And.intro, Exists.intro, CategoryTheory.IsIso.mk
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKProjective
inst_3 : L.IsKProjective
f : K ⟶ L
h : QuasiIso f
g :
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K
hg :
  CategoryTheory.Functor.map Qh g =
    NatTrans.app (Iso.hom (quotientCompQhIso C)) L ≫
      inv (CategoryTheory.Functor.map Q f) ≫ NatTrans.app (Iso.inv (quotientCompQhIso C)) K
refine_1 :
  Eq (α :=
    Quiver.Hom (V := DerivedCategory C)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)))
    (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f ≫ g))
    (CategoryTheory.Functor.map Qh (𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)))
refine_2 :
  Eq (α :=
    Quiver.Hom (V := DerivedCategory C)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L))
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)))
    (CategoryTheory.Functor.map Qh (g ≫ CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f))
    (CategoryTheory.Functor.map Qh (𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)))
⊢ IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)

Tactic:
refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKProjective
inst_3 : L.IsKProjective
f : K ⟶ L
h : QuasiIso f
g :
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K
hg :
  CategoryTheory.Functor.map Qh g =
    NatTrans.app (Iso.hom (quotientCompQhIso C)) L ≫
      inv (CategoryTheory.Functor.map Q f) ≫ NatTrans.app (Iso.inv (quotientCompQhIso C)) K
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)))
    (CategoryTheory.Functor.map Qh (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f ≫ g))
    (CategoryTheory.Functor.map Qh (𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)))

Tactic:
simp [hg]
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
inst_2 : K.IsKProjective
inst_3 : L.IsKProjective
f : K ⟶ L
h : QuasiIso f
g :
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K
hg :
  CategoryTheory.Functor.map Qh g =
    NatTrans.app (Iso.hom (quotientCompQhIso C)) L ≫
      inv (CategoryTheory.Functor.map Q f) ≫ NatTrans.app (Iso.inv (quotientCompQhIso C)) K
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L))
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)))
    (CategoryTheory.Functor.map Qh (g ≫ CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f))
    (CategoryTheory.Functor.map Qh (𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) L)))

Tactic:
simp [hg, ← quotientCompQhIso_inv_naturality f, -NatTrans.naturality]

Premises used: DerivedCategory.quotientCompQhIso_inv_naturality, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective
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 : K.IsKProjective
this : HasDerivedCategory C := HasDerivedCategory.standard C
rw :
  Function.Bijective (α := CohomologyClass K L n) (β :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh) K)
      (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh)
        (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)))
    (Function.comp (β :=
      Quiver.Hom (V := DerivedCategory C) (Functor.obj Q K)
        (Functor.obj (Q ⋙ CategoryTheory.shiftFunctor (DerivedCategory C) n) L))
      (⇑(Iso.homCongr (Iso.app (Iso.symm (quotientCompQhIso C)) K)
            (Iso.trans (Y := Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n ⋙ Q) L)
              (Iso.app (Iso.symm (Functor.commShiftIso Q n)) L)
              (Iso.app (Iso.symm (quotientCompQhIso C))
                (Functor.obj (CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) L)))) :
        (a : Q.obj K ⟶ (Q ⋙ CategoryTheory.shiftFunctor (DerivedCategory C) n).obj L) →
          (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj K ⟶
            (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj
              ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L))
      (Function.comp (β := SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n)
        (⇑(SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) Q) :
          (a : SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) →
            ShiftedHom (Q.obj K) (Q.obj L) n)
        toSmallShiftedHom))
⊢ Function.Bijective.{v + 1, w + 1} (α := CohomologyClass K L n) (β :=
    SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) toSmallShiftedHom

Tactic:
rw [← Function.Bijective.of_comp_iff'
      (SmallShiftedHom.equiv _ DerivedCategory.Q).bijective,
    ← Function.Bijective.of_comp_iff' (Iso.homCongr ((quotientCompQhIso C).symm.app K)
      ((Q.commShiftIso n).symm.app L ≪≫ (quotientCompQhIso C).symm.app (L⟦n⟧))).bijective]

Premises used: Equiv.bijective, DerivedCategory.Q, CategoryTheory.shiftFunctor, CategoryTheory.Iso.homCongr, CategoryTheory.Iso.trans, Function.Bijective.of_comp_iff', CategoryTheory.Iso.symm, DerivedCategory.quotientCompQhIso, CategoryTheory.Localization.SmallShiftedHom.equiv, CategoryTheory.Iso.app, CategoryTheory.Functor.CommShift.commShiftIso, CategoryTheory.Functor.obj
-- Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective
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 : K.IsKProjective
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Function.Bijective (α := CohomologyClass K L n) (β :=
    Quiver.Hom (V := DerivedCategory C)
      (Functor.obj Qh (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K))
      (Functor.obj Qh
        (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ))
          (Functor.obj (CategoryTheory.shiftFunctor (HomologicalComplex.{v, u, 0} C (ComplexShape.up ℤ)) n) L))))
    (CategoryTheory.Functor.map Qh ∘
      (⇑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:
(CochainComplex.IsKProjective.Qh_map_bijective _ _).comp (toHom_bijective K L n)

Premises used: CochainComplex.IsKProjective.Qh_map_bijective, CochainComplex.HomComplex.CohomologyClass.toHom_bijective, Function.Bijective.comp