awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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)
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))
⊢ ∃ (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 ⟨g, rfl⟩ := (CochainComplex.singleFunctor C n).map_surjective f'

Premises used: CochainComplex.singleFunctor, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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
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:
⟨g, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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
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:
exact ⟨g, rfl⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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))
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'
⊢ ∃ (a : A ⟶ B), CategoryTheory.Functor.map (singleFunctor C n) a = 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⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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))
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')
⊢ ∃ (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:
obtain ⟨X, _, _, s, _, g, rfl⟩ := right_fac_of_isStrictlyLE_of_isStrictlyGE n n f

Premises used: DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE, rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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
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')
⊢ ∃ (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

Premises used: CochainComplex.exists_iso_single
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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₀
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')
⊢ ∃ (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)
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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
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) φ))
⊢ IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj (singleFunctor C n) A₀)
    (CategoryTheory.Functor.map (singleFunctor C n) φ)

Tactic:
change IsIso (Q.map ((CochainComplex.singleFunctor C n).map φ))

Premises used: CategoryTheory.IsIso, CochainComplex.singleFunctor, DerivedCategory.Q, CategoryTheory.Functor.map
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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
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)
⊢ 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:
rw [hφ, Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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 e.inv ≫ CategoryTheory.Functor.map Q s)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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) φ)

Tactic:
have : IsIso ((singleFunctor C n).map φ) := by
      change IsIso (Q.map ((CochainComplex.singleFunctor C n).map φ))
      rw [hφ, Functor.map_comp]
      infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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) φ)
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) φ))
⊢ 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)) φ)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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 (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:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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 φ

Tactic:
have : IsIso φ := (NatIso.isIso_map_iff (singleFunctorCompHomologyFunctorIso C n) φ).1
        (by dsimp; infer_instance)
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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 φ
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) φ)
⊢ IsIso (e.inv ≫ s)

Tactic:
rw [← hφ]
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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 (C := CochainComplex.{v, u, 0} C ℤ) (X := Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) A₀)
    (CategoryTheory.Functor.map (CochainComplex.singleFunctor C n) φ)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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)

Tactic:
have : IsIso (e.inv ≫ s) := by rw [← hφ]; infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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)
⊢ IsIso s

Tactic:
have : IsIso s := IsIso.of_isIso_comp_left e.inv s
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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_3 : IsIso (e.inv ≫ s)
this : IsIso s
⊢ 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 (inv s ≫ g))

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
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_3 : IsIso (e.inv ≫ s)
this : IsIso 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:
exact ⟨inv s ≫ g, by simp⟩
-- Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K L : CochainComplex.{v, u, 0} C ℤ
f : K ⟶ L
n : ℤ
⊢ Eq (α :=
    Functor.obj (C := DerivedCategory.{w, v, u} C) (homologyFunctor C n) (Functor.obj Q K) ⟶
      Functor.obj (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) n) L)
    (CategoryTheory.Functor.map (homologyFunctor C n) (CategoryTheory.Functor.map Q f) ≫
      NatTrans.app (Iso.hom (homologyFunctorFactors C n)) L)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C n)) K ≫ HomologicalComplex.homologyMap f n)

Tactic:
(homologyFunctorFactors C n).hom.naturality f

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.homology, CategoryTheory.ShortComplex.homologyMap', DerivedCategory.homologyFunctorFactors, CategoryTheory.NatTrans.naturality, HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.LeftHomologyData.descH, CategoryTheory.Iso.hom, HomologicalComplex.homology, CategoryTheory.ShortComplex.homologyMap