awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
I : C
inst_3 : Injective.{v, u} I
K : CochainComplex.{v, u, 0} C ℤ
i n : ℤ
hn : i < n
inst_4 : K.IsStrictlyGE n
L : CochainComplex.{v, u, 0} C ℤ
w : L.IsStrictlyGE i
g : K ⟶ L
ι : Functor.obj (CochainComplex.singleFunctor C i) I ⟶ L
h :
  IsIso (C := DerivedCategory.{w, v, u} C) (X := Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I))
    (CategoryTheory.Functor.map Q ι)
hπ : IsSplitMono ι
h₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q L)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (inv (CategoryTheory.Functor.map Q ι)) (CategoryTheory.Functor.map Q (retraction ι))
h₂ : g ≫ retraction ι = 0
rw :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q K)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (CategoryTheory.Functor.map Q g ≫ CategoryTheory.Functor.map Q (retraction ι)) 0
rw₁ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q K)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (CategoryTheory.Functor.map Q (g ≫ retraction ι)) 0
rw₂ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q K)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (CategoryTheory.Functor.map Q 0) 0
rw₃ rw₄ :
  Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q K)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    0 0
⊢ Eq.{w + 1} (α :=
    Quiver.Hom (V := DerivedCategory.{w, v, u} C) (Functor.obj Q K)
      (Functor.obj Q (Functor.obj (CochainComplex.singleFunctor C i) I)))
    (CategoryTheory.Functor.map Q g ≫ inv (CategoryTheory.Functor.map Q ι)) 0

Tactic:
rw [h₁, ← Q.map_comp, h₂, Q.map_zero]

Premises used: DerivedCategory.Q, CategoryTheory.Functor.map_zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X I : C
n : ℕ
inst_3 : Injective.{v, u} I
e : Ext.{w, v, u} X I (n + 1)
K : CochainComplex.{v, u, 0} C ℤ := Functor.obj (CochainComplex.singleFunctor C 0) X
⊢ LE.le (α := ℤ) (-(↑n : ℤ)) 0

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X I : C
n : ℕ
inst_3 : Injective.{v, u} I
e : Ext.{w, v, u} X I (n + 1)
K : CochainComplex.{v, u, 0} C ℤ := Functor.obj (CochainComplex.singleFunctor C 0) X
⊢ K.IsStrictlyGE (-(↑n : ℤ))

Tactic:
have := K.isStrictlyGE_of_ge (-n) 0 (by lia)
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X I : C
n : ℕ
inst_3 : Injective.{v, u} I
e : Ext.{w, v, u} X I (n + 1)
K : CochainComplex.{v, u, 0} C ℤ := Functor.obj (CochainComplex.singleFunctor C 0) X
this_1 : K.IsStrictlyGE (-(↑n : ℤ))
this : HasDerivedCategory C := HasDerivedCategory.standard C
a :
  Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) I)
      (↑(n + 1) : ℤ))
    ((homEquiv :
          (a : Ext X I (n + 1)) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj I) (↑(n + 1) : ℤ))
        e :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) I) (↑(n + 1) : ℤ))
    ((homEquiv :
          (a : Ext X I (n + 1)) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj I) (↑(n + 1) : ℤ))
        0 :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) I) (↑(n + 1) : ℤ))
⊢ e = 0

Tactic:
apply homEquiv.injective

Premises used: CategoryTheory.Abelian.Ext.homEquiv, Equiv.injective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X I : C
n : ℕ
inst_3 : Injective.{v, u} I
e : Ext.{w, v, u} X I (n + 1)
K : CochainComplex.{v, u, 0} C ℤ := Functor.obj (CochainComplex.singleFunctor C 0) X
this_1 : K.IsStrictlyGE (-(↑n : ℤ))
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 + -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 = 0

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X I : C
n : ℕ
inst_3 : Injective.{v, u} I
e : Ext.{w, v, u} X I (n + 1)
K : CochainComplex.{v, u, 0} C ℤ := Functor.obj (CochainComplex.singleFunctor C 0) X
this_1 : K.IsStrictlyGE (-(↑n : ℤ))
this : HasDerivedCategory C := HasDerivedCategory.standard C
a :
  Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) I))
    ((homEquiv :
            (a : Ext X I (n + 1)) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj I) (↑(n + 1) : ℤ))
          e ≫
        NatTrans.app
          (Iso.hom
            (SingleFunctors.shiftIso (singleFunctors C) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
              0 ⋯))
          I :
      Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) I))
    (0 :
      Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) I))
⊢ Eq (α :=
    ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X) (Functor.obj (singleFunctor C 0) I)
      (↑(n + 1) : ℤ))
    ((homEquiv :
          (a : Ext X I (n + 1)) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj I) (↑(n + 1) : ℤ))
        e :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) I) (↑(n + 1) : ℤ))
    ((homEquiv :
          (a : Ext X I (n + 1)) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj I) (↑(n + 1) : ℤ))
        0 :
      ShiftedHom (C := DerivedCategory C) (M := ℤ) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (singleFunctor C 0) I) (↑(n + 1) : ℤ))

Tactic:
simp only [← cancel_mono (((singleFunctors C).shiftIso (n + 1) (-(n + 1)) 0
    (by lia)).hom.app _), zero_hom, Limits.zero_comp]

Premises used: DerivedCategory.singleFunctors, CategoryTheory.cancel_mono, Nat.cast, CategoryTheory.Abelian.Ext.zero_hom, HAdd.hAdd, CategoryTheory.SingleFunctors.shiftIso, CategoryTheory.Limits.zero_comp, OfNat.ofNat, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, Neg.neg
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X I : C
n : ℕ
inst_3 : Injective.{v, u} I
e : Ext.{w, v, u} X I (n + 1)
K : CochainComplex.{v, u, 0} C ℤ := Functor.obj (CochainComplex.singleFunctor C 0) X
this_1 : K.IsStrictlyGE (-(↑n : ℤ))
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 < -(↑n : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X I : C
n : ℕ
inst_3 : Injective.{v, u} I
e : Ext.{w, v, u} X I (n + 1)
K : CochainComplex.{v, u, 0} C ℤ := Functor.obj (CochainComplex.singleFunctor C 0) X
this_1 : K.IsStrictlyGE (-(↑n : ℤ))
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ Eq (α :=
    Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) X)
      (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) I))
    ((homEquiv :
            (a : Ext X I (n + 1)) → ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj I) (↑(n + 1) : ℤ))
          e ≫
        NatTrans.app
          (Iso.hom
            (SingleFunctors.shiftIso (singleFunctors C) (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
              0 ⋯))
          I :
      Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) I))
    (0 :
      Quiver.Hom (V := DerivedCategory C) (Functor.obj (singleFunctor C 0) X)
        (Functor.obj (SingleFunctors.functor (singleFunctors C) (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) I))

Tactic:
exact to_singleFunctor_obj_eq_zero_of_injective (K := K) (n := -n) _ (by lia)

Premises used: DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective, Nat.cast, Neg.neg
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasExt.{w, v, u} C
X I : C
inst_3 : Injective.{v, u} I
n : ℕ
⊢ Subsingleton.{w + 1} (Ext.{w, v, u} X I (n + 1))

Tactic:
subsingleton_of_forall_eq 0 Ext.eq_zero_of_injective

Premises used: subsingleton_of_forall_eq, OfNat.ofNat, CategoryTheory.Abelian.Ext.eq_zero_of_injective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ HasExt C

Tactic:
have := hasExt_of_hasDerivedCategory C
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
rw : ∀ (X Y : C) (n : ℕ), Small.{w, max u v} (Ext X Y n)
⊢ HasExt.{w, v, u} C

Tactic:
rw [hasExt_iff_small_ext.{w}]
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
zero : Small.{w, v} (X ⟶ Y)
⊢ Small.{w, max u v} (Ext X Y 0)

Tactic:
rw [small_congr Ext.homEquiv₀]

Premises used: small_congr, CategoryTheory.Abelian.Ext.homEquiv₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
⊢ Small.{w, v} (X ⟶ Y)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex.{v, u} C :=
  ShortComplex.mk (X₂ := Injective.under.{v, u} Y) (X₃ :=
    cokernel.{v, u} (Y := Injective.under.{v, u} Y) (Injective.ι Y)) (Injective.ι Y) (cokernel.π (Injective.ι Y)) ⋯
⊢ S.ShortExact

Tactic:
have hS : S.ShortExact :=
        { exact := ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel S.f) }
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex.{v, u} C :=
  ShortComplex.mk (X₂ := Injective.under.{v, u} Y) (X₃ :=
    cokernel.{v, u} (Y := Injective.under.{v, u} Y) (Injective.ι Y)) (Injective.ι Y) (cokernel.π (Injective.ι Y)) ⋯
hS : S.ShortExact
⊢ Function.Surjective (α := Ext X S.X₃ n) (β := Ext X S.X₁ (n + 1))
    (⇑(Ext.postcomp hS.extClass X ⋯) : (a : Ext X S.X₃ n) → Ext X S.X₁ (n + 1))

Tactic:
have : Function.Surjective (Ext.postcomp hS.extClass X (rfl : n + 1 = _)) :=
        fun y₁ ↦ Ext.covariant_sequence_exact₁ X hS y₁ (Ext.eq_zero_of_injective _) rfl
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this_2 : HasExt C
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex.{v, u} C :=
  ShortComplex.mk (X₂ := Injective.under.{v, u} Y) (X₃ :=
    cokernel.{v, u} (Y := Injective.under.{v, u} Y) (Injective.ι Y)) (Injective.ι Y) (cokernel.π (Injective.ι Y)) ⋯
hS : S.ShortExact
this :
  Function.Surjective (α := Ext X S.X₃ n) (β := Ext X S.X₁ (n + 1))
    (⇑(Ext.postcomp hS.extClass X ⋯) : (a : Ext X S.X₃ n) → Ext X S.X₁ (n + 1))
⊢ Small.{w, max u v} (Ext X Y (n + 1))

Tactic:
small_of_surjective.{w} this

Premises used: small_of_surjective
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this_2 : HasExt C
n : ℕ
hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)
X Y : C
S : ShortComplex.{v, u} C :=
  ShortComplex.mk (X₂ := Injective.under.{v, u} Y) (X₃ :=
    cokernel.{v, u} (Y := Injective.under.{v, u} Y) (Injective.ι Y)) (Injective.ι Y) (cokernel.π (Injective.ι Y)) ⋯
hS : S.ShortExact
this :
  Function.Surjective (α := Ext X S.X₃ n) (β := Ext X S.X₁ (n + 1))
    (⇑(Ext.postcomp hS.extClass X ⋯) : (a : Ext X S.X₃ n) → Ext X S.X₁ (n + 1))
⊢ Small.{w, max u v} (Ext X Y (n + 1))

Tactic:
exact small_of_surjective.{w} this
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : EnoughInjectives.{v, u} C
this_1 : HasDerivedCategory C := HasDerivedCategory.standard C
this : HasExt C
X Y : C
n : ℕ
zero : ∀ (X Y : C), Small.{w, max u v} (Ext X Y 0)
succ : ∀ (n : ℕ) (hn : ∀ (X Y : C), Small.{w, max u v} (Ext X Y n)) (X Y : C), Small.{w, max u v} (Ext X Y (n + 1))
⊢ Small.{w, max u v} (Ext X Y n)

Tactic:
induction n generalizing X Y with
    | zero =>
      rw [small_congr Ext.homEquiv₀]
      infer_instance
    | succ n hn =>
      let S := ShortComplex.mk _ _ (cokernel.condition (Injective.ι Y))
      have hS : S.ShortExact :=
        { exact := ShortComplex.exact_of_g_is_cokernel _ (cokernelIsCokernel S.f) }
      have : Function.Surjective (Ext.postcomp hS.extClass X (rfl : n + 1 = _)) :=
        fun y₁ ↦ Ext.covariant_sequence_exact₁ X hS y₁ (Ext.eq_zero_of_injective _) rfl
      exact small_of_surjective.{w} this

Premises used: small_congr, CategoryTheory.Abelian.Ext.homEquiv₀
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
⊢ (ComplexShape.up ℤ).next i = i + 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
⊢ i < i + 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)
rw : e.hom ≫ π.f i = e.hom ≫ α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P)
⊢ π.f i = α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P)

Tactic:
rw [← cancel_epi e.hom]

Premises used: CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)
dsimp :
  Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (singleFunctor C i) P) i) (iCycles K i ≫ π.f i)
    (iCycles K i ≫
      CategoryStruct.comp (Y := cycles K i) (Iso.inv (iCyclesIso K i (i + 1) ⋯ ⋯))
          (homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)) ≫
        Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
⊢ e.hom ≫ π.f i = e.hom ≫ α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P)

Tactic:
dsimp [α, e]
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)
rw :
  Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (singleFunctor C i) P) i) (iCycles K i ≫ π.f i)
    (cyclesMap π i ≫
      homologyπ (Functor.obj (singleFunctor C i) P) i ≫
        Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
⊢ Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (singleFunctor C i) P) i) (iCycles K i ≫ π.f i)
    (iCycles K i ≫
      CategoryStruct.comp (Y := cycles K i) (Iso.inv (iCyclesIso K i (i + 1) ⋯ ⋯))
          (homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)) ≫
        Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))

Tactic:
rw [assoc, assoc, assoc, iCyclesIso_hom_inv_id_assoc,
      homologyπ_naturality_assoc]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.homologyπ_naturality_assoc, HomologicalComplex.iCyclesIso_hom_inv_id_assoc
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)
dsimp :
  Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
    (cyclesMap π i ≫
      homologyπ (Functor.obj (single C (ComplexShape.up ℤ) i) P) i ≫
        Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
⊢ Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (singleFunctor C i) P) i) (iCycles K i ≫ π.f i)
    (cyclesMap π i ≫
      homologyπ (Functor.obj (singleFunctor C i) P) i ≫
        Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))

Tactic:
dsimp [singleFunctor, singleFunctors]

Premises used: CochainComplex.singleFunctor, CochainComplex.singleFunctors
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)
rw :
  Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
    (cyclesMap π i ≫
      Iso.hom (singleObjCyclesSelfIso (ComplexShape.up ℤ) i P) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))
rw₁ :
  Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
    (cyclesMap π i ≫
      Iso.hom (singleObjCyclesSelfIso (ComplexShape.up ℤ) i P) ≫
        Iso.inv (singleObjCyclesSelfIso (ComplexShape.up ℤ) i P) ≫
          iCycles (Functor.obj (single C (ComplexShape.up ℤ) i) P) i)
rw₂ :
  Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
    (CategoryStruct.comp (Y := cycles.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (cyclesMap π i)
      (iCycles (Functor.obj (single C (ComplexShape.up ℤ) i) P) i))
rw₃ rw₄ :
  Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i)
    (CategoryStruct.comp (Y := cycles.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (cyclesMap π i)
      (iCycles (Functor.obj (single C (ComplexShape.up ℤ) i) P) i))
    (CategoryStruct.comp (Y := cycles.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (cyclesMap π i)
      (iCycles (Functor.obj (single C (ComplexShape.up ℤ) i) P) i))
⊢ Eq (α := cycles K i ⟶ X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) P) i) (iCycles K i ≫ π.f i)
    (cyclesMap π i ≫
      homologyπ (Functor.obj (single C (ComplexShape.up ℤ) i) P) i ≫
        Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P) ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P))

Tactic:
rw [homologyπ_singleObjHomologySelfIso_hom_assoc,
      ← singleObjCyclesSelfIso_inv_iCycles, Iso.hom_inv_id_assoc, ← cyclesMap_i]

Premises used: HomologicalComplex.singleObjCyclesSelfIso_inv_iCycles, HomologicalComplex.homologyπ_singleObjHomologySelfIso_hom_assoc, CategoryTheory.Iso.hom_inv_id_assoc, HomologicalComplex.cyclesMap_i
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)
⊢ π.f i = α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P)

Tactic:
have : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv := by
    rw [← cancel_epi e.hom]
    dsimp [α, e]
    rw [assoc, assoc, assoc, iCyclesIso_hom_inv_id_assoc,
      homologyπ_naturality_assoc]
    dsimp [singleFunctor, singleFunctors]
    rw [homologyπ_singleObjHomologySelfIso_hom_assoc,
      ← singleObjCyclesSelfIso_inv_iCycles, Iso.hom_inv_id_assoc, ← cyclesMap_i]
-- Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
P : C
inst_2 : Projective.{v, u} P
K : CochainComplex.{v, u, 0} C ℤ
i : ℤ
π : K ⟶ Functor.obj (singleFunctor C i) P
inst_3 : K.IsStrictlyLE i
inst_4 : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ Iso.hom (singleObjHomologySelfIso (ComplexShape.up ℤ) i P)
this : π.f i = α ≫ Iso.inv (singleObjXSelf (ComplexShape.up ℤ) i P)
⊢ i < i + 1

Tactic:
simp