awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ImageToKernel
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasKernels.{v, u} V
inst_3 : HasZeroObject.{v, u} V
inst_4 : Mono g
⊢ Eq (α := A ⟶ C) (0 ≫ g) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ImageToKernel
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasKernels.{v, u} V
inst_3 : HasZeroObject.{v, u} V
inst_4 : Mono g
⊢ Epi (X := Functor.obj (C := Subobject.{v, u} B) Subobject.underlying (imageSubobject (X := A) 0)) (Y :=
    Functor.obj Subobject.underlying (kernelSubobject g)) (imageToKernel 0 g ⋯)

Tactic:
epi_of_target_iso_zero _ (kernelSubobjectIso g ≪≫ kernel.ofMono g)

Premises used: CategoryTheory.Limits.kernel.ofMono, CategoryTheory.Iso.trans, CategoryTheory.Limits.epi_of_target_iso_zero, CategoryTheory.Limits.kernelSubobjectIso
-- Module: Mathlib.Algebra.Homology.ImageToKernel
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasImages.{v, u} V
inst_3 : Epi f
⊢ Eq (α := A ⟶ C) (f ≫ 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ImageToKernel
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasImages.{v, u} V
inst_3 : Epi f
simp :
  Epi (Y := Functor.obj (C := Subobject.{v, u} B) Subobject.underlying (kernelSubobject (Y := C) 0))
    ((imageSubobject f).arrow ≫ inv (Subobject.arrow (kernelSubobject (Y := C) 0)))
⊢ Epi (X := Functor.obj Subobject.underlying (imageSubobject f)) (Y :=
    Functor.obj (C := Subobject.{v, u} B) Subobject.underlying (kernelSubobject (Y := C) 0)) (imageToKernel f 0 ⋯)

Tactic:
simp only [imageToKernel_zero_right]

Premises used: imageToKernel_zero_right
-- Module: Mathlib.Algebra.Homology.ImageToKernel
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasImages.{v, u} V
inst_3 : Epi f
⊢ Epi (X := image f) (image.ι f)

Tactic:
haveI := epi_image_of_epi f
-- Module: Mathlib.Algebra.Homology.ImageToKernel
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasImages.{v, u} V
inst_3 : Epi f
this : Epi (X := image f) (image.ι f)
rw :
  Epi (X := Functor.obj Subobject.underlying (imageSubobject f)) (Y :=
    Functor.obj (C := Subobject.{v, u} B) Subobject.underlying (kernelSubobject (Y := C) 0))
    ((Iso.hom (imageSubobjectIso f) ≫ image.ι f) ≫ inv (Subobject.arrow (kernelSubobject (Y := C) 0)))
⊢ Epi (Y := Functor.obj (C := Subobject.{v, u} B) Subobject.underlying (kernelSubobject (Y := C) 0))
    ((imageSubobject f).arrow ≫ inv (Subobject.arrow (kernelSubobject (Y := C) 0)))

Tactic:
rw [← imageSubobject_arrow]

Premises used: CategoryTheory.Limits.imageSubobject_arrow
-- Module: Mathlib.Algebra.Homology.ImageToKernel
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasImages.{v, u} V
inst_3 : Epi f
this : Epi (X := image f) (image.ι f)
⊢ Epi (X := Functor.obj Subobject.underlying (imageSubobject f)) (Y :=
    Functor.obj (C := Subobject.{v, u} B) Subobject.underlying (kernelSubobject (Y := C) 0))
    ((Iso.hom (imageSubobjectIso f) ≫ image.ι f) ≫ inv (Subobject.arrow (kernelSubobject (Y := C) 0)))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.ImageToKernel
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
w_1 : f ≫ g = 0
inst_2 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
w : f ≫ g = 0
w₁ :
  CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f ≫ g) =
    CategoryStruct.comp (Y := image f) (factorThruImage f) 0
⊢ Eq (α := image f ⟶ C) (image.ι f ≫ g) 0

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ImageToKernel
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
w_1 : f ≫ g = 0
inst_2 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
w : f ≫ g = 0
⊢ CategoryStruct.comp (Y := image f) (factorThruImage f) (image.ι f ≫ g) =
    CategoryStruct.comp (Y := image f) (factorThruImage f) 0

Tactic:
simpa using w
-- Module: Mathlib.Algebra.Homology.ImageToKernel
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
w : f ≫ g = 0
h :
  Eq (α := Functor.obj Subobject.underlying (imageSubobject f) ⟶ B)
    (CategoryStruct.comp (Y := equalizer g 0)
        (Iso.hom (imageSubobjectIso f) ≫ imageToKernel' f g w :
          Functor.obj Subobject.underlying (imageSubobject f) ⟶ kernel g)
        (equalizer.ι g 0 : equalizer g 0 ⟶ B) :
      Functor.obj Subobject.underlying (imageSubobject f) ⟶ B)
    (CategoryStruct.comp (Y := equalizer g 0) (imageToKernel f g w ≫ Iso.hom (kernelSubobjectIso g)) (equalizer.ι g 0) :
      Functor.obj Subobject.underlying (imageSubobject f) ⟶ B)
⊢ Eq (α := Functor.obj Subobject.underlying (imageSubobject f) ⟶ kernel g)
    (Iso.hom (imageSubobjectIso f) ≫ imageToKernel' f g w :
      Functor.obj Subobject.underlying (imageSubobject f) ⟶ kernel g)
    (imageToKernel f g w ≫ Iso.hom (kernelSubobjectIso g) :
      Functor.obj Subobject.underlying (imageSubobject f) ⟶ kernel g)

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ImageToKernel
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
w : f ≫ g = 0
⊢ Eq (α := Functor.obj Subobject.underlying (imageSubobject f) ⟶ B)
    (CategoryStruct.comp (Y := equalizer g 0)
        (Iso.hom (imageSubobjectIso f) ≫ imageToKernel' f g w :
          Functor.obj Subobject.underlying (imageSubobject f) ⟶ kernel g)
        (equalizer.ι g 0 : equalizer g 0 ⟶ B) :
      Functor.obj Subobject.underlying (imageSubobject f) ⟶ B)
    (CategoryStruct.comp (Y := equalizer g 0) (imageToKernel f g w ≫ Iso.hom (kernelSubobjectIso g)) (equalizer.ι g 0) :
      Functor.obj Subobject.underlying (imageSubobject f) ⟶ B)

Tactic:
simp [imageToKernel']

Premises used: imageToKernel'
-- Module: Mathlib.Algebra.Homology.ImageToKernel
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
w : f ≫ g = 0
h :
  Eq (α := image f ⟶ B)
    (CategoryStruct.comp (Y := kernel g) (imageToKernel' f g w : image f ⟶ kernel g)
          (Iso.inv (kernelSubobjectIso g) : kernel g ⟶ Functor.obj Subobject.underlying (kernelSubobject g)) ≫
        (kernelSubobject g).arrow :
      image f ⟶ B)
    ((Iso.inv (imageSubobjectIso f) ≫ imageToKernel f g w) ≫ (kernelSubobject g).arrow : image f ⟶ B)
⊢ Eq (α := image f ⟶ Functor.obj Subobject.underlying (kernelSubobject g))
    (CategoryStruct.comp (Y := kernel g) (imageToKernel' f g w : image f ⟶ kernel g)
        (Iso.inv (kernelSubobjectIso g) : kernel g ⟶ Functor.obj Subobject.underlying (kernelSubobject g)) :
      image f ⟶ Functor.obj Subobject.underlying (kernelSubobject g))
    (Iso.inv (imageSubobjectIso f) ≫ imageToKernel f g w :
      image f ⟶ Functor.obj Subobject.underlying (kernelSubobject g))

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.ImageToKernel
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst_2 : HasKernels.{v, u} V
inst_3 : HasImages.{v, u} V
w : f ≫ g = 0
⊢ Eq (α := image f ⟶ B)
    (CategoryStruct.comp (Y := kernel g) (imageToKernel' f g w : image f ⟶ kernel g)
          (Iso.inv (kernelSubobjectIso g) : kernel g ⟶ Functor.obj Subobject.underlying (kernelSubobject g)) ≫
        (kernelSubobject g).arrow :
      image f ⟶ B)
    ((Iso.inv (imageSubobjectIso f) ≫ imageToKernel f g w) ≫ (kernelSubobject g).arrow : image f ⟶ B)

Tactic:
simp [imageToKernel']

Premises used: imageToKernel'
-- Module: Mathlib.Algebra.Homology.LeftResolution.Basic
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X Y : A
f : X ⟶ Y
⊢ ι.map (Λ.F.map f) ≫ Λ.π.app Y = Λ.π.app X ≫ f

Tactic:
Λ.π.naturality f

Premises used: CategoryTheory.Abelian.LeftResolution.π, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.Algebra.Homology.LeftResolution.Basic
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X Y Z : A
f_1 : X ⟶ Y
g : Y ⟶ Z
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
X₀ X₁ : C
f : X₁ ⟶ X₀
⊢ Eq (α := ι.obj (Λ.F.obj (kernel (ι.map f))) ⟶ ι.obj X₀)
    (ι.map (ι.preimage (Λ.π.app (kernel (ι.map f)) ≫ kernel.ι (ι.map f)) ≫ f)) (ι.map 0)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.LeftResolution.Basic
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
⊢ Eq (α := ι.obj (HomologicalComplex.X (Λ.chainComplex X) 1) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex X) 0))
    (ι.map (HomologicalComplex.d (Λ.chainComplex X) 1 0))
    (ι.map (Iso.hom (Λ.chainComplexXOneIso X)) ≫
      Λ.π.app (kernel (Λ.π.app X)) ≫ kernel.ι (Λ.π.app X) ≫ ι.map (Iso.inv (Λ.chainComplexXZeroIso X)))

Tactic:
simp [chainComplexXOneIso, chainComplexXZeroIso, chainComplex]

Premises used: CategoryTheory.Abelian.LeftResolution.chainComplex, CategoryTheory.Abelian.LeftResolution.chainComplexXOneIso, CategoryTheory.Abelian.LeftResolution.chainComplexXZeroIso
-- Module: Mathlib.Algebra.Homology.LeftResolution.Basic
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X Y Z : A
f : X ⟶ Y
g : Y ⟶ Z
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
⊢ HomologicalComplex.X (Λ.chainComplex X) (n + 2) ≅
    Λ.F.obj
      (kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
        (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))

Tactic:
apply ChainComplex.mk'XIso

Premises used: ChainComplex.mk'XIso
-- Module: Mathlib.Algebra.Homology.LeftResolution.Basic
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
⊢ Eq (α :=
    ι.obj
        (Λ.F.obj
          (limit.cone
              (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
                (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)).1) ⟶
      ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
    (ι.map
      (ι.preimage
        (Λ.π.app
            (limit.cone
                (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
                  (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)).1 ≫
          kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))))
    (Λ.π.app
        (limit.cone
            (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
              (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)).1 ≫
      kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))

Tactic:
have := ι.map_preimage (Λ.π.app _ ≫ kernel.ι (ι.map ((Λ.chainComplex X).d (n + 1) n)))
-- Module: Mathlib.Algebra.Homology.LeftResolution.Basic
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
this :
  Eq (α :=
    ι.obj
        (Λ.F.obj
          (limit
            (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
              (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0))) ⟶
      ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
    (ι.map
      (ι.preimage
        (Λ.π.app
            (limit
              (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
                (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)) ≫
          kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))))
    (Λ.π.app
        (limit
          (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
            (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)) ≫
      kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))
rw :
  Eq (α :=
    ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 2)) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
    (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 2) (n + 1)))
    (ι.map
      (Iso.hom (Λ.chainComplexXIso X n) ≫
        ι.preimage
          (Λ.π.app
              (limit
                (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
                  (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)) ≫
            kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))))
⊢ Eq (α :=
    ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 2)) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
    (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 2) (n + 1)))
    (ι.map (Iso.hom (Λ.chainComplexXIso X n)) ≫
      Λ.π.app
          (kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
            (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))) ≫
        kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))

Tactic:
rw [← this, ← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.LeftResolution.Basic
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
this :
  Eq (α :=
    ι.obj
        (Λ.F.obj
          (limit
            (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
              (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0))) ⟶
      ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
    (ι.map
      (ι.preimage
        (Λ.π.app
            (limit
              (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
                (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)) ≫
          kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))))
    (Λ.π.app
        (limit
          (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
            (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)) ≫
      kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))
e_a :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 2) ⟶ HomologicalComplex.X (Λ.chainComplex X) (n + 1))
    (HomologicalComplex.d (Λ.chainComplex X) (n + 2) (n + 1))
    (Iso.hom (Λ.chainComplexXIso X n) ≫
      ι.preimage
        (Λ.π.app
            (limit
              (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
                (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)) ≫
          kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))))
⊢ Eq (α :=
    ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 2)) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
    (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 2) (n + 1)))
    (ι.map
      (Iso.hom (Λ.chainComplexXIso X n) ≫
        ι.preimage
          (Λ.π.app
              (limit
                (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
                  (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)) ≫
            kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))))

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.LeftResolution.Basic
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
this :
  Eq (α :=
    ι.obj
        (Λ.F.obj
          (limit
            (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
              (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0))) ⟶
      ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
    (ι.map
      (ι.preimage
        (Λ.π.app
            (limit
              (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
                (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)) ≫
          kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))))
    (Λ.π.app
        (limit
          (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
            (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)) ≫
      kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 2) ⟶ HomologicalComplex.X (Λ.chainComplex X) (n + 1))
    (HomologicalComplex.d (Λ.chainComplex X) (n + 2) (n + 1))
    (Iso.hom (Λ.chainComplexXIso X n) ≫
      ι.preimage
        (Λ.π.app
            (limit
              (parallelPair (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
                (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)) 0)) ≫
          kernel.ι (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))))

Tactic:
apply ChainComplex.mk'_d

Premises used: ChainComplex.mk'_d
-- Module: Mathlib.Algebra.Homology.LeftResolution.Basic
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
⊢ n + 1 + 1 = n + 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.LeftResolution.Basic
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
⊢ (ComplexShape.down ℕ).next (n + 1) = n

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.LeftResolution.Basic
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
rw :
  Epi (X :=
    ShortComplex.X₁
      (HomologicalComplex.sc'
        (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
          (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
        (n + 2) (n + 1) n))
    (Y :=
    kernel (X :=
      ShortComplex.X₂
        (HomologicalComplex.sc'
          (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
            (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
          (n + 2) (n + 1) n))
      (ShortComplex.g
        (HomologicalComplex.sc'
          (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
            (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
          (n + 2) (n + 1) n)))
    (kernel.lift
      (ShortComplex.g
        (HomologicalComplex.sc'
          (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
            (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
          (n + 2) (n + 1) n))
      (ShortComplex.f
        (HomologicalComplex.sc'
          (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
            (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
          (n + 2) (n + 1) n))
      ⋯)
⊢ HomologicalComplex.ExactAt
    (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
      (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
    (n + 1)

Tactic:
rw [HomologicalComplex.exactAt_iff' _ (n + 2) (n + 1) n
    (ComplexShape.prev_eq' _ (by dsimp; lia)) (by simp),
    ShortComplex.exact_iff_epi_kernel_lift]

Premises used: ComplexShape.prev_eq', HAdd.hAdd, CategoryTheory.ShortComplex.exact_iff_epi_kernel_lift, OfNat.ofNat, HomologicalComplex.exactAt_iff'
-- Module: Mathlib.Algebra.Homology.LeftResolution.Basic
Goal:
A : Type u_1
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Category.{v_2, u_1} A
ι : Functor.{v_1, v_2, u_2, u_1} C A
Λ : LeftResolution ι
X : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
⊢ Epi (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 2)))
    (ι.map (Iso.hom (Λ.chainComplexXIso X n)) ≫
      Λ.π.app
        (kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
          (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))))

Tactic:
epi_comp (ι.map (Λ.chainComplexXIso X n).hom) (Λ.π.app _)

Premises used: CategoryTheory.epi_comp, CategoryTheory.Abelian.LeftResolution.chainComplexXIso, CategoryTheory.Abelian.LeftResolution.π, CategoryTheory.Functor.map, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app