awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ { X₁ := homology T.obj₃ n₀, X₂ := homology T.obj₁ n₁, X₃ := homology T.obj₂ n₁, f := homologyδOfTriangle T n₀ n₁ h,
      g := homologyMap T.mor₁ n₁, zero := ⋯ : ShortComplex.{v, u} C }.Exact
have refine : { X₁ := (DerivedCategory.homologyFunctor C n₀).obj (DerivedCategory.Q.mapTriangle.obj T).obj₃,
    X₂ := (DerivedCategory.homologyFunctor C n₁).obj (DerivedCategory.Q.mapTriangle.obj T).obj₁,
    X₃ := (DerivedCategory.homologyFunctor C n₁).obj (DerivedCategory.Q.mapTriangle.obj T).obj₂,
    f := DerivedCategory.HomologySequence.δ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T) n₀ n₁ h,
    g :=
      CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n₁)
        (Triangle.mor₁ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)),
    zero := sorry : ShortComplex.{v, u} C } ≅
  { X₁ := homology T.obj₃ n₀, X₂ := homology T.obj₁ n₁, X₃ := homology T.obj₂ n₁, f := homologyδOfTriangle T n₀ n₁ h,
    g := homologyMap T.mor₁ n₁, zero := sorry }
Tactic: refine ShortComplex.exact_of_iso ?_ (DerivedCategory.HomologySequence.exact₁ _ hT n₀ n₁ h)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n : ℤ
⊢ { X₁ := homology T.obj₁ n, X₂ := homology T.obj₂ n, X₃ := homology T.obj₃ n, f := homologyMap T.mor₁ n,
      g := homologyMap T.mor₂ n, zero := ⋯ : ShortComplex.{v, u} C }.Exact
have refine : { X₁ := (DerivedCategory.homologyFunctor C n).obj (DerivedCategory.Q.mapTriangle.obj T).obj₁,
    X₂ := (DerivedCategory.homologyFunctor C n).obj (DerivedCategory.Q.mapTriangle.obj T).obj₂,
    X₃ := (DerivedCategory.homologyFunctor C n).obj (DerivedCategory.Q.mapTriangle.obj T).obj₃,
    f :=
      CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
        (Triangle.mor₁ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)),
    g :=
      CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n)
        (Triangle.mor₂ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)),
    zero := sorry : ShortComplex.{v, u} C } ≅
  { X₁ := homology T.obj₁ n, X₂ := homology T.obj₂ n, X₃ := homology T.obj₃ n, f := homologyMap T.mor₁ n,
    g := homologyMap T.mor₂ n, zero := sorry }
Tactic: refine ShortComplex.exact_of_iso ?_ (DerivedCategory.HomologySequence.exact₂ _ hT n)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.HomologySequence (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
T : Triangle (CochainComplex.{v, u, 0} C ℤ)
hT :
  Membership.mem (γ := Set (Triangle (DerivedCategory.{w, v, u} C)))
    (@distinguishedTriangles _ _ ⋯ _ DerivedCategory.instPreadditive ⋯ _)
    (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ { X₁ := homology T.obj₂ n₀, X₂ := homology T.obj₃ n₀, X₃ := homology T.obj₁ n₁, f := homologyMap T.mor₂ n₀,
      g := homologyδOfTriangle T n₀ n₁ h, zero := ⋯ : ShortComplex.{v, u} C }.Exact
have refine : { X₁ := (DerivedCategory.homologyFunctor C n₀).obj (DerivedCategory.Q.mapTriangle.obj T).obj₂,
    X₂ := (DerivedCategory.homologyFunctor C n₀).obj (DerivedCategory.Q.mapTriangle.obj T).obj₃,
    X₃ := (DerivedCategory.homologyFunctor C n₁).obj (DerivedCategory.Q.mapTriangle.obj T).obj₁,
    f :=
      CategoryTheory.Functor.map (DerivedCategory.homologyFunctor C n₀)
        (Triangle.mor₂ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T)),
    g := DerivedCategory.HomologySequence.δ (Functor.obj (Functor.mapTriangle DerivedCategory.Q) T) n₀ n₁ h, zero := sorry :
    ShortComplex.{v, u} C } ≅
  { X₁ := homology T.obj₂ n₀, X₂ := homology T.obj₃ n₀, X₃ := homology T.obj₁ n₁, f := homologyMap T.mor₂ n₀,
    g := homologyδOfTriangle T n₀ n₁ h, zero := sorry }
Tactic: refine ShortComplex.exact_of_iso ?_ (DerivedCategory.HomologySequence.exact₃ _ hT n₀ n₁ h)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KInjective (goal)
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
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.up ℤ) f
have refine : QuasiIso f → homotopyEquivalences C (ComplexShape.up ℤ) f
Tactic: refine ⟨fun _ ↦ ?_, fun hf ↦ homotopyEquivalences_le_quasiIso _ _ _ hf⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KInjective (goal)
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
⊢ homotopyEquivalences C (ComplexShape.up ℤ) f
have rw : IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
  (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
Tactic: rw [← HomotopyCategory.inverseImage_quotient_isomorphisms,
    MorphismProperty.inverseImage_iff, MorphismProperty.isomorphisms.iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KInjective (goal)
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
⊢ IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
have 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)
Tactic: obtain ⟨g, hg⟩ := (Qh_map_bijective _ _).surjective
    ((quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KInjective (goal)
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)
have 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)))
Tactic: refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KInjective (goal)
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)))
⊢ IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
have 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)))
Tactic: refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KInjective (goal)
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.{v + 1, w + 1} (α := CohomologyClass K L n) (β :=
    SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) toSmallShiftedHom
have 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))
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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KInjective (goal)
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
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.up ℕ) f
have rw : QuasiIso (K := extend K ComplexShape.embeddingUpNat) (extendMap f ComplexShape.embeddingUpNat) ↔
  homotopyEquivalences C (ComplexShape.up ℕ) f
Tactic: rw [← quasiIso_extendMap_iff _ ComplexShape.embeddingUpNat,
    CochainComplex.IsKInjective.quasiIso_iff,
    homotopyEquivalences_extendMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KInjective (goal)
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
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.up ℕ) f
have rw₁ : homotopyEquivalences C (ComplexShape.up ℤ) (X := extend K ComplexShape.embeddingUpNat)
    (extendMap f ComplexShape.embeddingUpNat) ↔
  homotopyEquivalences C (ComplexShape.up ℕ) f
Tactic: rw [← quasiIso_extendMap_iff _ ComplexShape.embeddingUpNat,
    CochainComplex.IsKInjective.quasiIso_iff,
    homotopyEquivalences_extendMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KInjective (goal)
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
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.up ℕ) f
have rw₂ : homotopyEquivalences C (ComplexShape.up ℕ) f ↔ homotopyEquivalences C (ComplexShape.up ℕ) f
Tactic: rw [← quasiIso_extendMap_iff _ ComplexShape.embeddingUpNat,
    CochainComplex.IsKInjective.quasiIso_iff,
    homotopyEquivalences_extendMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KProjective (goal)
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
have refine : QuasiIso f → homotopyEquivalences C (ComplexShape.up ℤ) f
Tactic: refine ⟨fun _ ↦ ?_, fun hf ↦ homotopyEquivalences_le_quasiIso _ _ _ hf⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KProjective (goal)
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
⊢ homotopyEquivalences C (ComplexShape.up ℤ) f
have rw : IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
  (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
Tactic: rw [← HomotopyCategory.inverseImage_quotient_isomorphisms,
    MorphismProperty.inverseImage_iff, MorphismProperty.isomorphisms.iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KProjective (goal)
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
⊢ IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
have 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)
Tactic: obtain ⟨g, hg⟩ := (Qh_map_bijective _ _).surjective
    ((quotientCompQhIso C).hom.app L ≫ inv (Q.map f) ≫ (quotientCompQhIso C).inv.app K)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KProjective (goal)
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)
have 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)))
Tactic: refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KProjective (goal)
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)))
⊢ IsIso (X := Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℤ)) K)
    (CategoryTheory.Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℤ)) f)
have 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)))
Tactic: refine ⟨g, (Qh_map_bijective _ _).injective ?_, (Qh_map_bijective _ _).injective ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KProjective (goal)
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.{v + 1, w + 1} (α := CohomologyClass K L n) (β :=
    SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n) toSmallShiftedHom
have 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))
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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KProjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : ChainComplex.{v, u, 0} C ℕ
inst_2 : ∀ (n : ℕ), Projective.{v, u} (K.X n)
inst_3 : ∀ (n : ℕ), Projective.{v, u} (L.X n)
f : K ⟶ L
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.down ℕ) f
have rw : QuasiIso (K := extend K ComplexShape.embeddingDownNat) (extendMap f ComplexShape.embeddingDownNat) ↔
  homotopyEquivalences C (ComplexShape.down ℕ) f
Tactic: rw [← quasiIso_extendMap_iff _ ComplexShape.embeddingDownNat,
    CochainComplex.IsKProjective.quasiIso_iff,
    homotopyEquivalences_extendMap_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.KProjective (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : ChainComplex.{v, u, 0} C ℕ
inst_2 : ∀ (n : ℕ), Projective.{v, u} (K.X n)
inst_3 : ∀ (n : ℕ), Projective.{v, u} (L.X n)
f : K ⟶ L
rw :
  QuasiIso (K := extend K ComplexShape.embeddingDownNat) (extendMap f ComplexShape.embeddingDownNat) ↔
    homotopyEquivalences C (ComplexShape.down ℕ) f
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.down ℕ) f
have rw₁ : homotopyEquivalences C (ComplexShape.up ℤ) (X := extend K ComplexShape.embeddingDownNat)
    (extendMap f ComplexShape.embeddingDownNat) ↔
  homotopyEquivalences C (ComplexShape.down ℕ) f
Tactic: rw [← quasiIso_extendMap_iff _ ComplexShape.embeddingDownNat,
    CochainComplex.IsKProjective.quasiIso_iff,
    homotopyEquivalences_extendMap_iff]