awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
x x_1 : C
f₁ f₂ : x ⟶ x_1
h :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C n) x)
      (Functor.obj (singleFunctor C n) x_1))
    (CategoryTheory.Functor.map (singleFunctor C n) f₁) (CategoryTheory.Functor.map (singleFunctor C n) f₂)
eq₁ :
  CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
      (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
      (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₁) ≫
        NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
    f₁
eq₂ :
  CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
      (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
      (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₂) ≫
        NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
    f₂
rw :
  CategoryStruct.comp (Y :=
      Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
      (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
      (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₁) ≫
        NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
    f₂
⊢ f₁ = f₂
have rw₁ : CategoryStruct.comp (Y :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
    (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
    (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₁) ≫
      NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1) =
  CategoryStruct.comp (Y :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) x))
    (NatTrans.app (Iso.inv (singleFunctorCompHomologyFunctorIso C n)) x)
    (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) f₂) ≫
      NatTrans.app (Iso.hom (singleFunctorCompHomologyFunctorIso C n)) x_1)
Tactic: rw [← eq₁, ← eq₂, h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
f :
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C n) A) (Functor.obj (singleFunctor C n) B)
⊢ ∃ (a : A ⟶ B), CategoryTheory.Functor.map (singleFunctor C n) a = f
have change : ∀
  (f :
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B))),
  ∃ (a : A ⟶ B), CategoryTheory.Functor.map (singleFunctor C n) a = f
Tactic: change Q.obj ((CochainComplex.singleFunctor C n).obj A) ⟶
      Q.obj ((CochainComplex.singleFunctor C n).obj B) at f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
f :
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
    (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B))
this :
  ∃ (f' :
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
      (Functor.obj (CochainComplex.singleFunctor C n) B)),
    f = CategoryTheory.Functor.map Q f'
⊢ ∃ (a : A ⟶ B), CategoryTheory.Functor.map (singleFunctor C n) a = f
have obtain : ∀
  (f' :
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
      (Functor.obj (CochainComplex.singleFunctor C n) B)),
  ∃ (a : A ⟶ B),
    Eq.{w + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C n) A)
        (Functor.obj (singleFunctor C n) B))
      (CategoryTheory.Functor.map (singleFunctor C n) a) (CategoryTheory.Functor.map Q f')
Tactic: obtain ⟨f', rfl⟩ := this
Cleared hypotheses: f, this
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
f' :
  Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
    (Functor.obj (CochainComplex.singleFunctor C n) B)
⊢ ∃ (a : A ⟶ B),
    Eq.{w + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C n) A)
        (Functor.obj (singleFunctor C n) B))
      (CategoryTheory.Functor.map (singleFunctor C n) a) (CategoryTheory.Functor.map Q f')
have obtain : ∀ (g : A ⟶ B),
  ∃ (a : A ⟶ B),
    Eq.{w + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj (singleFunctor C n) A)
        (Functor.obj (singleFunctor C n) B))
      (CategoryTheory.Functor.map (singleFunctor C n) a)
      (CategoryTheory.Functor.map Q (CategoryTheory.Functor.map (CochainComplex.singleFunctor C n) g))
Tactic: obtain ⟨g, rfl⟩ := (CochainComplex.singleFunctor C n).map_surjective f'
Cleared hypotheses: f'
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
f :
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
    (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B))
⊢ ∃ (a : A ⟶ B), CategoryTheory.Functor.map (singleFunctor C n) a = f
have suffices : ∃ (f' :
  Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
    (Functor.obj (CochainComplex.singleFunctor C n) B)),
  f = CategoryTheory.Functor.map Q f'
Tactic: suffices ∃ f', f = Q.map f' by
      obtain ⟨f', rfl⟩ := this
      obtain ⟨g, rfl⟩ := (CochainComplex.singleFunctor C n).map_surjective f'
      exact ⟨g, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
f :
  Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
    (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B))
⊢ ∃ (f' :
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
      (Functor.obj (CochainComplex.singleFunctor C n) B)),
    f = CategoryTheory.Functor.map Q f'
have obtain : ∀ (X : CochainComplex.{v, u, 0} C ℤ),
  X.IsStrictlyGE n →
    X.IsStrictlyLE n →
      ∀ (s : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) A)
        (w : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X) (CategoryTheory.Functor.map Q s))
        (g : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) B),
        ∃ (f' :
          Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
            (Functor.obj (CochainComplex.singleFunctor C n) B)),
          Eq.{w + 1} (α :=
            Quiver.Hom (V := DerivedCategory.{w, v, u} C)
              (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
              (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B)))
            (inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g) (CategoryTheory.Functor.map Q f')
Tactic: obtain ⟨X, _, _, s, _, g, rfl⟩ := right_fac_of_isStrictlyLE_of_isStrictlyGE n n f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
X : CochainComplex.{v, u, 0} C ℤ
w : X.IsStrictlyGE n
w_1 : X.IsStrictlyLE n
s : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) A
w_2 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X) (CategoryTheory.Functor.map Q s)
g : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) B
⊢ ∃ (f' :
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
      (Functor.obj (CochainComplex.singleFunctor C n) B)),
    Eq.{w + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B)))
      (inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g) (CategoryTheory.Functor.map Q f')
have obtain : ∀ (A₀ : C) (e : X ≅ Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) A₀),
  ∃ (f' :
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
      (Functor.obj (CochainComplex.singleFunctor C n) B)),
    Eq.{w + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B)))
      (inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g) (CategoryTheory.Functor.map Q f')
Tactic: obtain ⟨A₀, ⟨e⟩⟩ := X.exists_iso_single n
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
X : CochainComplex.{v, u, 0} C ℤ
w : X.IsStrictlyGE n
w_1 : X.IsStrictlyLE n
s : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) A
w_2 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X) (CategoryTheory.Functor.map Q s)
g : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) B
A₀ : C
e : X ≅ Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) A₀
⊢ ∃ (f' :
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
      (Functor.obj (CochainComplex.singleFunctor C n) B)),
    Eq.{w + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B)))
      (inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g) (CategoryTheory.Functor.map Q f')
have have : ∀ (φ : A₀ ⟶ A) (hφ : CategoryTheory.Functor.map (CochainComplex.singleFunctor C n) φ = e.inv ≫ s),
  ∃ (f' :
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
      (Functor.obj (CochainComplex.singleFunctor C n) B)),
    Eq.{w + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B)))
      (inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g) (CategoryTheory.Functor.map Q f')
Tactic: have ⟨φ, hφ⟩ := (CochainComplex.singleFunctor C n).map_surjective (e.inv ≫ s)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
X : CochainComplex.{v, u, 0} C ℤ
w : X.IsStrictlyGE n
w_1 : X.IsStrictlyLE n
s : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) A
w_2 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X) (CategoryTheory.Functor.map Q s)
g : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) B
A₀ : C
e : X ≅ Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) A₀
φ : A₀ ⟶ A
hφ : CategoryTheory.Functor.map (CochainComplex.singleFunctor C n) φ = e.inv ≫ s
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj (singleFunctor C n) A₀)
    (CategoryTheory.Functor.map (singleFunctor C n) φ)
have change : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A₀))
  (CategoryTheory.Functor.map Q (CategoryTheory.Functor.map (CochainComplex.singleFunctor C n) φ))
Tactic: change IsIso (Q.map ((CochainComplex.singleFunctor C n).map φ))
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
X : CochainComplex.{v, u, 0} C ℤ
w : X.IsStrictlyGE n
w_1 : X.IsStrictlyLE n
s : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) A
w_2 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X) (CategoryTheory.Functor.map Q s)
g : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) B
A₀ : C
e : X ≅ Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) A₀
φ : A₀ ⟶ A
hφ : CategoryTheory.Functor.map (CochainComplex.singleFunctor C n) φ = e.inv ≫ s
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A₀))
    (CategoryTheory.Functor.map Q (CategoryTheory.Functor.map (CochainComplex.singleFunctor C n) φ))
have rw : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A₀))
  (CategoryTheory.Functor.map Q e.inv ≫ CategoryTheory.Functor.map Q s)
Tactic: rw [hφ, Functor.map_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
X : CochainComplex.{v, u, 0} C ℤ
w : X.IsStrictlyGE n
w_1 : X.IsStrictlyLE n
s : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) A
w_2 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X) (CategoryTheory.Functor.map Q s)
g : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) B
A₀ : C
e : X ≅ Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) A₀
φ : A₀ ⟶ A
hφ : CategoryTheory.Functor.map (CochainComplex.singleFunctor C n) φ = e.inv ≫ s
⊢ ∃ (f' :
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
      (Functor.obj (CochainComplex.singleFunctor C n) B)),
    Eq.{w + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B)))
      (inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g) (CategoryTheory.Functor.map Q f')
have this : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj (singleFunctor C n) A₀)
  (CategoryTheory.Functor.map (singleFunctor C n) φ)
Tactic: have : IsIso ((singleFunctor C n).map φ) := by
      change IsIso (Q.map ((CochainComplex.singleFunctor C n).map φ))
      rw [hφ, Functor.map_comp]
      infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
X : CochainComplex.{v, u, 0} C ℤ
w : X.IsStrictlyGE n
w_1 : X.IsStrictlyLE n
s : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) A
w_2 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X) (CategoryTheory.Functor.map Q s)
g : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) B
A₀ : C
e : X ≅ Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) A₀
φ : A₀ ⟶ A
hφ : CategoryTheory.Functor.map (CochainComplex.singleFunctor C n) φ = e.inv ≫ s
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj (singleFunctor C n) A₀)
    (CategoryTheory.Functor.map (singleFunctor C n) φ)
⊢ IsIso (X :=
    Functor.obj.{v, v, u, u} (Functor.comp (D := DerivedCategory.{w, v, u} C) (singleFunctor C n) (homologyFunctor C n))
      A₀)
    (CategoryTheory.Functor.map
      (Functor.comp (D := DerivedCategory.{w, v, u} C) (singleFunctor C n) (homologyFunctor C n)) φ)
have dsimp : IsIso (X := Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj (singleFunctor C n) A₀))
  (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map (singleFunctor C n) φ))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
X : CochainComplex.{v, u, 0} C ℤ
w : X.IsStrictlyGE n
w_1 : X.IsStrictlyLE n
s : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) A
w_2 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X) (CategoryTheory.Functor.map Q s)
g : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) B
A₀ : C
e : X ≅ Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) A₀
φ : A₀ ⟶ A
hφ : CategoryTheory.Functor.map (CochainComplex.singleFunctor C n) φ = e.inv ≫ s
this :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj (singleFunctor C n) A₀)
    (CategoryTheory.Functor.map (singleFunctor C n) φ)
⊢ ∃ (f' :
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
      (Functor.obj (CochainComplex.singleFunctor C n) B)),
    Eq.{w + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B)))
      (inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g) (CategoryTheory.Functor.map Q f')
have this₁ : IsIso φ
Tactic: have : IsIso φ := (NatIso.isIso_map_iff (singleFunctorCompHomologyFunctorIso C n) φ).1
        (by dsimp; infer_instance)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
X : CochainComplex.{v, u, 0} C ℤ
w : X.IsStrictlyGE n
w_1 : X.IsStrictlyLE n
s : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) A
w_2 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X) (CategoryTheory.Functor.map Q s)
g : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) B
A₀ : C
e : X ≅ Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) A₀
φ : A₀ ⟶ A
hφ : CategoryTheory.Functor.map (CochainComplex.singleFunctor C n) φ = e.inv ≫ s
this_1 :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj (singleFunctor C n) A₀)
    (CategoryTheory.Functor.map (singleFunctor C n) φ)
this : IsIso φ
⊢ IsIso (e.inv ≫ s)
have rw : IsIso (C := CochainComplex.{v, u, 0} C ℤ) (X := Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) A₀)
  (CategoryTheory.Functor.map (CochainComplex.singleFunctor C n) φ)
Tactic: rw [← hφ]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
X : CochainComplex.{v, u, 0} C ℤ
w : X.IsStrictlyGE n
w_1 : X.IsStrictlyLE n
s : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) A
w_2 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X) (CategoryTheory.Functor.map Q s)
g : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) B
A₀ : C
e : X ≅ Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) A₀
φ : A₀ ⟶ A
hφ : CategoryTheory.Functor.map (CochainComplex.singleFunctor C n) φ = e.inv ≫ s
this_1 :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj (singleFunctor C n) A₀)
    (CategoryTheory.Functor.map (singleFunctor C n) φ)
this : IsIso φ
⊢ ∃ (f' :
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
      (Functor.obj (CochainComplex.singleFunctor C n) B)),
    Eq.{w + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B)))
      (inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g) (CategoryTheory.Functor.map Q f')
have this₁ : IsIso (e.inv ≫ s)
Tactic: have : IsIso (e.inv ≫ s) := by rw [← hφ]; infer_instance
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
n : ℤ
A B : C
X : CochainComplex.{v, u, 0} C ℤ
w : X.IsStrictlyGE n
w_1 : X.IsStrictlyLE n
s : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) A
w_2 : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q X) (CategoryTheory.Functor.map Q s)
g : X ⟶ Functor.obj (CochainComplex.singleFunctor C n) B
A₀ : C
e : X ≅ Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) A₀
φ : A₀ ⟶ A
hφ : CategoryTheory.Functor.map (CochainComplex.singleFunctor C n) φ = e.inv ≫ s
this_1 :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj (singleFunctor C n) A₀)
    (CategoryTheory.Functor.map (singleFunctor C n) φ)
this_2 : IsIso φ
this : IsIso (e.inv ≫ s)
⊢ ∃ (f' :
    Quiver.Hom (V := CochainComplex.{v, u, 0} C ℤ) (Functor.obj (CochainComplex.singleFunctor C n) A)
      (Functor.obj (CochainComplex.singleFunctor C n) B)),
    Eq.{w + 1} (α :=
      Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) A))
        (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C n) B)))
      (inv (CategoryTheory.Functor.map Q s) ≫ CategoryTheory.Functor.map Q g) (CategoryTheory.Functor.map Q f')
have this₁ : IsIso s
Tactic: have : IsIso s := IsIso.of_isIso_comp_left e.inv s
-- 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
X Y : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
f : X ⟶ Y
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f) ↔
    HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f
have mp : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f) →
  HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f
Tactic: constructor
-- 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
X Y : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
f : X ⟶ Y
mp :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f) →
    HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f) ↔
    HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f
have mpr : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f →
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f)
Tactic: constructor
-- 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
X Y : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
f : X ⟶ Y
hf : IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Qh X) (CategoryTheory.Functor.map Qh f)
n : ℤ
⊢ IsIso (X := Functor.obj (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n) X)
    (CategoryTheory.Functor.map (HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n) f)
have mp : IsIso (X := Functor.obj (Functor.comp (D := DerivedCategory.{w, v, u} C) Qh (homologyFunctor C n)) X)
  (CategoryTheory.Functor.map (Functor.comp (D := DerivedCategory.{w, v, u} C) Qh (homologyFunctor C n)) f)
Tactic: rw [← NatIso.isIso_map_iff (homologyFunctorFactorsh C n) f]