awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasInjectiveResolutions.{v, u} C
X Y : C
f : X ⟶ Y
I : InjectiveResolution.{v, u} X
J : InjectiveResolution.{v, u} Y
φ : I.cocomplex ⟶ J.cocomplex
comm :
  Eq (α := HomologicalComplex.X.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) X) 0 ⟶ J.cocomplex.X 0)
    (I.ι.f 0 ≫ φ.f 0) (f ≫ J.ι.f 0)
rw :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f) (Iso.hom J.iso) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₁ :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) X) (Iso.inv I.iso)
      (Functor.map (injectiveResolutions C) f ≫ Iso.hom J.iso) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₂ :
  CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) X) (Iso.inv I.iso)
      (Iso.hom I.iso ≫ Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ) =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₃ :
  Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ =
    CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y)
      (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso) (Iso.hom J.iso)
rw₄ :
  Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ =
    Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫
      CategoryStruct.comp (Y := Functor.obj (injectiveResolutions C) Y) (Iso.inv J.iso) (Iso.hom J.iso)
rw₅ :
  Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ =
    Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫
      𝟙 (Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) J.cocomplex)
⊢ Eq (α :=
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex ⟶ Functor.obj (injectiveResolutions C) Y)
    (Iso.inv I.iso ≫ Functor.map (injectiveResolutions C) f)
    (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ ≫ Iso.inv J.iso)
have rw₆ : Eq (α :=
  Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) I.cocomplex ⟶
    Functor.obj (HomotopyCategory.quotient C (ComplexShape.up ℕ)) J.cocomplex)
  (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ)
  (Functor.map (HomotopyCategory.quotient C (ComplexShape.up ℕ)) φ)
Tactic: rw [← cancel_mono (J.iso).hom, Category.assoc, iso_hom_naturality f I J φ comm,
    Iso.inv_hom_id_assoc, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯ ⟶ ShortComplex.mk (X₃ := syzygies f) f (d f) ⋯ :=
  { τ₁ := 𝟙 (ShortComplex.X₁ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)),
    τ₂ := 𝟙 (ShortComplex.X₂ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)),
    τ₃ := ι (ShortComplex.X₃ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)), comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ ShortComplex.Exact (ShortComplex.mk (X₃ := syzygies f) f (d f) ⋯)
have rw : ShortComplex.Exact (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) sorry)
Tactic: rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono α]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
X Y : C
f : X ⟶ Y
α : ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯ ⟶ ShortComplex.mk (X₃ := syzygies f) f (d f) ⋯ :=
  { τ₁ := 𝟙 (ShortComplex.X₁ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)),
    τ₂ := 𝟙 (ShortComplex.X₂ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)),
    τ₃ := ι (ShortComplex.X₃ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)), comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ ShortComplex.Exact (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) ⋯)
have hS : IsColimit (F :=
  parallelPair (X := ShortComplex.X₁ (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) sorry))
    (ShortComplex.f (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) sorry)) 0)
  (CokernelCofork.ofπ (ShortComplex.g (ShortComplex.mk (X₃ := cokernel f) f (cokernel.π f) sorry)) sorry)
Tactic: apply ShortComplex.exact_of_g_is_cokernel
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
⊢ HomologicalComplex.ExactAt.{v, u, 0} (ofCocomplex Z) (n + 1)
have rw : ShortComplex.Exact.{v, u} (HomologicalComplex.sc' (ofCocomplex Z) n (n + 1) (n + 1 + 1))
Tactic: rw [HomologicalComplex.exactAt_iff' _ n (n + 1) (n + 1 + 1) (by simp) (by simp)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
⊢ ShortComplex.Exact.{v, u} (HomologicalComplex.sc' (ofCocomplex Z) n (n + 1) (n + 1 + 1))
have simp : ShortComplex.Exact
  (ShortComplex.mk (X₁ :=
    ShortComplex.X₁
      (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
        (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (d (Injective.ι Z)))
        (d (Injective.ι Z)) (d (d (Injective.ι Z))) sorry
        (fun (S : ShortComplex.{v, u} C) ↦
          PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
            (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) sorry))
        n))
    (X₃ :=
    ShortComplex.X₁
      (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
        (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (d (Injective.ι Z)))
        (d (Injective.ι Z)) (d (d (Injective.ι Z))) sorry
        (fun (S : ShortComplex.{v, u} C) ↦
          PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
            (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) sorry))
        (n + 1 + 1)))
    (ShortComplex.f
      (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
        (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (d (Injective.ι Z)))
        (d (Injective.ι Z)) (d (d (Injective.ι Z))) sorry
        (fun (S : ShortComplex.{v, u} C) ↦
          PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
            (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) sorry))
        n))
    (ShortComplex.f
      (CochainComplex.mkAux (under.{v, u} Z) (syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
        (syzygies.{v, u} (X := under.{v, u} Z) (Y := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
          (d (Injective.ι Z)))
        (d (Injective.ι Z)) (d (d (Injective.ι Z))) sorry
        (fun (S : ShortComplex.{v, u} C) ↦
          PSigma.mk (β := fun (X₂ : C) ↦ (d : S.X₃ ⟶ X₂) ×' S.g ≫ d = 0) (syzygies S.g)
            (PSigma.mk (β := fun (d : S.X₃ ⟶ syzygies S.g) ↦ S.g ≫ d = 0) (d S.g) sorry))
        (n + 1)))
    sorry)
Tactic: simp only [HomologicalComplex.sc', HomologicalComplex.shortComplexFunctor', ofCocomplex,
    CochainComplex.mk', CochainComplex.mk, CochainComplex.of_d]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
⊢ Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) n)
have zero : Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0)
Tactic: obtain (_ | _ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
zero : Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0)
⊢ Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) n)
have succ : Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) (HAdd.hAdd (α := ℕ) 0 1))
Tactic: obtain (_ | _ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
zero : Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0)
succ : Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) (HAdd.hAdd (α := ℕ) 0 1))
⊢ Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) n)
have succ₁ : Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) (HAdd.hAdd (α := ℕ) 0 1 + 1))
Tactic: obtain (_ | _ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
zero : Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0)
succ : Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) (HAdd.hAdd (α := ℕ) 0 1))
succ₁ : Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) (HAdd.hAdd (α := ℕ) 0 1 + 1))
⊢ Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) n)
have succ₂ : ∀ (n : ℕ), Injective.{v, u} (HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) (n + 1 + 1 + 1))
Tactic: obtain (_ | _ | _ | n) := n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
⊢ Eq.{v + 1} (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) (Injective.ι Z : Z ⟶ under.{v, u} Z)
      (HomologicalComplex.d (ofCocomplex Z) 0 1))
    0
have rw : Eq.{v + 1} (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
  (Injective.ι Z ≫ d (Injective.ι Z) : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
  (0 : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
Tactic: rw [ofCocomplex_d_0_1, cokernel.condition_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
rw :
  Eq.{v + 1} (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (Injective.ι Z ≫ d (Injective.ι Z) : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (0 : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
⊢ Eq.{v + 1} (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) (Injective.ι Z : Z ⟶ under.{v, u} Z)
      (HomologicalComplex.d (ofCocomplex Z) 0 1))
    0
have rw₁ : Eq.{v + 1} (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
  (0 ≫ Injective.ι (cokernel.{v, u} (Y := under.{v, u} Z) (Injective.ι Z)) :
    Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
  (0 : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
Tactic: rw [ofCocomplex_d_0_1, cokernel.condition_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
rw :
  Eq.{v + 1} (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (Injective.ι Z ≫ d (Injective.ι Z) : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (0 : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
rw₁ :
  Eq.{v + 1} (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (0 ≫ Injective.ι (cokernel.{v, u} (Y := under.{v, u} Z) (Injective.ι Z)) :
      Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (0 : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
⊢ Eq.{v + 1} (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1)
    (CategoryStruct.comp (Y := HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) (Injective.ι Z : Z ⟶ under.{v, u} Z)
      (HomologicalComplex.d (ofCocomplex Z) 0 1))
    0
have rw₂ : Eq.{v + 1} (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) 0 0
Tactic: rw [ofCocomplex_d_0_1, cokernel.condition_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
⊢ QuasiIsoAt.{v, u, 0} (C := C) (c := ComplexShape.up ℕ) (K := Functor.obj (CochainComplex.single₀ C) Z) (L :=
    ofCocomplex Z)
    ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
        (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
          (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
      (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0)
          (Injective.ι Z) ⋯ :
        { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0 }))
    n
have zero : QuasiIsoAt.{v, u, 0} (ι := ℕ) (C := C) (c := ComplexShape.up ℕ) (K := Functor.obj (CochainComplex.single₀ C) Z) (L :=
  ofCocomplex Z)
  ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
      (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
        (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
    (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
        Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1) 0)
        (Injective.ι Z) sorry :
      { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
        Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
          0 }))
  0
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
zero :
  QuasiIsoAt.{v, u, 0} (ι := ℕ) (C := C) (c := ComplexShape.up ℕ) (K := Functor.obj (CochainComplex.single₀ C) Z) (L :=
    ofCocomplex Z)
    ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
        (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
          (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
      (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0)
          (Injective.ι Z) ⋯ :
        { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0 }))
    0
⊢ QuasiIsoAt.{v, u, 0} (C := C) (c := ComplexShape.up ℕ) (K := Functor.obj (CochainComplex.single₀ C) Z) (L :=
    ofCocomplex Z)
    ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
        (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
          (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
      (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0)
          (Injective.ι Z) ⋯ :
        { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0 }))
    n
have succ : ∀ (n : ℕ),
  QuasiIsoAt.{v, u, 0} (C := C) (c := ComplexShape.up ℕ) (K := Functor.obj (CochainComplex.single₀ C) Z) (L :=
    ofCocomplex Z)
    ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
        (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
          (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
      (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0)
          (Injective.ι Z) sorry :
        { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0 }))
    (n + 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
⊢ Mono.{v, u} (X :=
    ShortComplex.X₁.{v, u}
      (ShortComplex.mk (X₂ := under.{v, u} Z) (X₃ := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
        (Injective.ι Z) (d (Injective.ι Z)) ⋯))
    (ShortComplex.f
      (ShortComplex.mk (X₂ := under.{v, u} Z) (X₃ := syzygies.{v, u} (Y := under.{v, u} Z) (Injective.ι Z))
        (Injective.ι Z) (d (Injective.ι Z)) ⋯))
have dsimp : Mono.{v, u} (Y := under.{v, u} Z) (Injective.ι Z)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
⊢ QuasiIsoAt.{v, u, 0} (C := C) (c := ComplexShape.up ℕ) (K := Functor.obj (CochainComplex.single₀ C) Z) (L :=
    ofCocomplex Z)
    ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
        (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
          (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
      (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0)
          (Injective.ι Z) ⋯ :
        { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0 }))
    (n + 1)
have succ : HomologicalComplex.ExactAt.{v, u, 0} (ofCocomplex Z) (n + 1)
Tactic: rw [quasiIsoAt_iff_exactAt]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Injective.Resolution (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : EnoughInjectives.{v, u} C
Z : C
n : ℕ
succ : HomologicalComplex.ExactAt.{v, u, 0} (ofCocomplex Z) (n + 1)
⊢ QuasiIsoAt.{v, u, 0} (C := C) (c := ComplexShape.up ℕ) (K := Functor.obj (CochainComplex.single₀ C) Z) (L :=
    ofCocomplex Z)
    ((Equiv.symm (CochainComplex.fromSingle₀Equiv (ofCocomplex Z) Z) :
        (a : { f : Z ⟶ (ofCocomplex Z).X 0 // f ≫ (ofCocomplex Z).d 0 1 = 0 }) →
          (CochainComplex.single₀ C).obj Z ⟶ ofCocomplex Z)
      (Subtype.mk (p := fun (f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0) ↦
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0)
          (Injective.ι Z) ⋯ :
        { f : Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 0 //
          Eq (α := Z ⟶ HomologicalComplex.X.{v, u, 0} (ofCocomplex Z) 1) (f ≫ HomologicalComplex.d (ofCocomplex Z) 0 1)
            0 }))
    (n + 1)
have succ₁ : HomologicalComplex.ExactAt.{v, u, 0} (Functor.obj (CochainComplex.single₀ C) Z) (n + 1)
Tactic: rw [quasiIsoAt_iff_exactAt]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.LeftDerived (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
inst_2 : Abelian.{v, u} C
inst_3 : HasProjectiveResolutions.{v, u} C
inst_4 : Abelian.{v_1, u_1} D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution.{v, u} X
Q : ProjectiveResolution.{v, u} Y
φ : P.complex ⟶ Q.complex
comm :
  Eq (α := P.complex.X 0 ⟶ HomologicalComplex.X.{v, u, 0} (Functor.obj (ChainComplex.single₀ C) Y) 0) (φ.f 0 ≫ Q.π.f 0)
    (P.π.f 0 ≫ f)
F : Functor.{v, v_1, u, u_1} C D
inst_5 : F.Additive
⊢ Eq (α :=
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj F.leftDerivedToHomotopyCategory X)
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
    (Functor.map F.leftDerivedToHomotopyCategory f ≫ Iso.hom (Q.isoLeftDerivedToHomotopyCategoryObj F))
    (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F) ≫
      Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ))
have rw : Eq (α :=
  Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
    (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
      P.complex)
    (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
      (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
  (CategoryStruct.comp (Y := Functor.obj F.leftDerivedToHomotopyCategory X)
      (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj F))
      (Functor.map F.leftDerivedToHomotopyCategory f ≫ Iso.hom (Q.isoLeftDerivedToHomotopyCategoryObj F)) :
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
        P.complex)
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
  (CategoryStruct.comp (Y := Functor.obj F.leftDerivedToHomotopyCategory X)
      (Iso.inv (P.isoLeftDerivedToHomotopyCategoryObj F))
      (Iso.hom (P.isoLeftDerivedToHomotopyCategoryObj F) ≫
        Functor.map (HomotopyCategory.quotient D (ComplexShape.down ℕ))
          (Functor.map (F.mapHomologicalComplex (ComplexShape.down ℕ)) φ)) :
    Quiver.Hom (V := HomotopyCategory.{v_1, u_1, 0} D (ComplexShape.down ℕ))
      (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ))
        P.complex)
      (Functor.obj (HomotopyCategory.quotient D (ComplexShape.down ℕ))
        (Functor.obj (F.mapHomologicalComplex (ComplexShape.down ℕ)) Q.complex)))
Tactic: rw [← cancel_epi (P.isoLeftDerivedToHomotopyCategoryObj F).inv, Iso.inv_hom_id_assoc,
      isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc f P Q φ comm F,
      Iso.inv_hom_id, comp_id]