awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
e_3 :
  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) =
    ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 2))
e_4 :
  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)) =
    Functor.obj.{v_2, v_2, u_1, u_1} (𝟭 A)
      (kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
        (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n)))
⊢ Eq (α :=
    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.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.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))
    ((ι.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.ι
        (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)))

Tactic:
simp [map_chainComplex_d]

Premises used: CategoryTheory.Abelian.LeftResolution.map_chainComplex_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 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
dsimp :
  Eq (α := ι.obj (HomologicalComplex.X (Λ.chainComplex X) 1) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex Y) 0))
    (ι.map
      ((Iso.hom (Λ.chainComplexXOneIso X) ≫
          Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯) ≫ Iso.inv (Λ.chainComplexXOneIso Y)) ≫
        HomologicalComplex.d (Λ.chainComplex Y) 1 0))
    (ι.map
      (HomologicalComplex.d (Λ.chainComplex X) 1 0 ≫
        Iso.hom (Λ.chainComplexXZeroIso X) ≫ Λ.F.map f ≫ Iso.inv (Λ.chainComplexXZeroIso Y)))
⊢ Eq (α := ι.obj (HomologicalComplex.X (Λ.chainComplex X) 1) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex Y) 0))
    (ι.map
      ((Iso.hom (Λ.chainComplexXOneIso X) ≫
          Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯) ≫ Iso.inv (Λ.chainComplexXOneIso Y)) ≫
        HomologicalComplex.d (Λ.chainComplex Y) 1 0))
    (ι.map
      (HomologicalComplex.d (Λ.chainComplex X) 1 0 ≫
        Iso.hom (Λ.chainComplexXZeroIso X) ≫ Λ.F.map f ≫ Iso.inv (Λ.chainComplexXZeroIso Y)))

Tactic:
dsimp
-- 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
simp :
  Eq (α := ι.obj (HomologicalComplex.X (Λ.chainComplex X) 1) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex Y) 0))
    (ι.map (Iso.hom (Λ.chainComplexXOneIso X)) ≫
      ι.map (Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯)) ≫
        CategoryStruct.comp (Y := ι.obj (HomologicalComplex.X (Λ.chainComplex Y) 1))
          (ι.map (Iso.inv (Λ.chainComplexXOneIso Y)))
          (ι.map (Iso.hom (Λ.chainComplexXOneIso Y)) ≫
            Λ.π.app (kernel (Λ.π.app Y)) ≫ kernel.ι (Λ.π.app Y) ≫ ι.map (Iso.inv (Λ.chainComplexXZeroIso Y))))
    (ι.map (Iso.hom (Λ.chainComplexXOneIso X)) ≫
      Λ.π.app (kernel (Λ.π.app X)) ≫
        kernel.ι (Λ.π.app X) ≫
          CategoryStruct.comp (Y := ι.obj (HomologicalComplex.X (Λ.chainComplex X) 0))
            (ι.map (Iso.inv (Λ.chainComplexXZeroIso X)))
            (ι.map (Iso.hom (Λ.chainComplexXZeroIso X)) ≫
              ι.map (Λ.F.map f) ≫ ι.map (Iso.inv (Λ.chainComplexXZeroIso Y))))
⊢ Eq (α := ι.obj (HomologicalComplex.X (Λ.chainComplex X) 1) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex Y) 0))
    (ι.map
      ((Iso.hom (Λ.chainComplexXOneIso X) ≫
          Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯) ≫ Iso.inv (Λ.chainComplexXOneIso Y)) ≫
        HomologicalComplex.d (Λ.chainComplex Y) 1 0))
    (ι.map
      (HomologicalComplex.d (Λ.chainComplex X) 1 0 ≫
        Iso.hom (Λ.chainComplexXZeroIso X) ≫ Λ.F.map f ≫ Iso.inv (Λ.chainComplexXZeroIso Y)))

Tactic:
simp only [Category.assoc, Functor.map_comp, map_chainComplex_d_1_0]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0
-- 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
simp :
  Eq (α := ι.obj (HomologicalComplex.X (Λ.chainComplex X) 1) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex Y) 0))
    (ι.map
        (Iso.hom (Λ.chainComplexXOneIso X) ≫
          Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯) ≫
            CategoryStruct.comp (Y := HomologicalComplex.X (Λ.chainComplex Y) 1) (Iso.inv (Λ.chainComplexXOneIso Y))
              (Iso.hom (Λ.chainComplexXOneIso Y))) ≫
      Λ.π.app (kernel (Λ.π.app Y)) ≫ kernel.ι (Λ.π.app Y) ≫ ι.map (Iso.inv (Λ.chainComplexXZeroIso Y)))
    (ι.map (Iso.hom (Λ.chainComplexXOneIso X)) ≫
      Λ.π.app (kernel (Λ.π.app X)) ≫
        kernel.ι (Λ.π.app X) ≫
          CategoryStruct.comp (Y := ι.obj (HomologicalComplex.X (Λ.chainComplex X) 0))
            (ι.map (Iso.inv (Λ.chainComplexXZeroIso X)))
            (ι.map (Iso.hom (Λ.chainComplexXZeroIso X) ≫ Λ.F.map f ≫ Iso.inv (Λ.chainComplexXZeroIso Y))))
⊢ Eq (α := ι.obj (HomologicalComplex.X (Λ.chainComplex X) 1) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex Y) 0))
    (ι.map (Iso.hom (Λ.chainComplexXOneIso X)) ≫
      ι.map (Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯)) ≫
        CategoryStruct.comp (Y := ι.obj (HomologicalComplex.X (Λ.chainComplex Y) 1))
          (ι.map (Iso.inv (Λ.chainComplexXOneIso Y)))
          (ι.map (Iso.hom (Λ.chainComplexXOneIso Y)) ≫
            Λ.π.app (kernel (Λ.π.app Y)) ≫ kernel.ι (Λ.π.app Y) ≫ ι.map (Iso.inv (Λ.chainComplexXZeroIso Y))))
    (ι.map (Iso.hom (Λ.chainComplexXOneIso X)) ≫
      Λ.π.app (kernel (Λ.π.app X)) ≫
        kernel.ι (Λ.π.app X) ≫
          CategoryStruct.comp (Y := ι.obj (HomologicalComplex.X (Λ.chainComplex X) 0))
            (ι.map (Iso.inv (Λ.chainComplexXZeroIso X)))
            (ι.map (Iso.hom (Λ.chainComplexXZeroIso X)) ≫
              ι.map (Λ.F.map f) ≫ ι.map (Iso.inv (Λ.chainComplexXZeroIso Y))))

Tactic:
simp only [← ι.map_comp, ← ι.map_comp_assoc]

Premises used: CategoryTheory.Functor.map_comp_assoc, 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 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
⊢ Eq (α := ι.obj (HomologicalComplex.X (Λ.chainComplex X) 1) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex Y) 0))
    (ι.map
        (Iso.hom (Λ.chainComplexXOneIso X) ≫
          Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯) ≫
            CategoryStruct.comp (Y := HomologicalComplex.X (Λ.chainComplex Y) 1) (Iso.inv (Λ.chainComplexXOneIso Y))
              (Iso.hom (Λ.chainComplexXOneIso Y))) ≫
      Λ.π.app (kernel (Λ.π.app Y)) ≫ kernel.ι (Λ.π.app Y) ≫ ι.map (Iso.inv (Λ.chainComplexXZeroIso Y)))
    (ι.map (Iso.hom (Λ.chainComplexXOneIso X)) ≫
      Λ.π.app (kernel (Λ.π.app X)) ≫
        kernel.ι (Λ.π.app X) ≫
          CategoryStruct.comp (Y := ι.obj (HomologicalComplex.X (Λ.chainComplex X) 0))
            (ι.map (Iso.inv (Λ.chainComplexXZeroIso X)))
            (ι.map (Iso.hom (Λ.chainComplexXZeroIso X) ≫ Λ.F.map f ≫ Iso.inv (Λ.chainComplexXZeroIso Y))))

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 Y : A
f : X ⟶ Y
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex Y) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f) 0)
    (Iso.hom (Λ.chainComplexXZeroIso X) ≫ Λ.F.map f ≫ Iso.inv (Λ.chainComplexXZeroIso Y))

Tactic:
rfl

Premises used: rfl
-- 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
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) 1 ⟶ HomologicalComplex.X (Λ.chainComplex Y) 1)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f) 1)
    (Iso.hom (Λ.chainComplexXOneIso X) ≫
      Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯) ≫ Iso.inv (Λ.chainComplexXOneIso Y))

Tactic:
rfl

Premises used: rfl
-- 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 : ℕ
rw :
  Eq (α := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex Y) n))
    (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ HomologicalComplex.Hom.f (Λ.chainComplexMap f) n))
    (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap f) (n + 1)) ≫
      ι.map (HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n))
rw₁ :
  Eq (α := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex Y) n))
    (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ HomologicalComplex.Hom.f (Λ.chainComplexMap f) n))
    (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap f) (n + 1) ≫ HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n))
rw₂ rw₃ :
  Eq (α := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex Y) n))
    (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ HomologicalComplex.Hom.f (Λ.chainComplexMap f) n))
    (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n ≫ HomologicalComplex.Hom.f (Λ.chainComplexMap f) n))
⊢ Eq (α := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)) ⟶ ι.obj (HomologicalComplex.X (Λ.chainComplex Y) n))
    (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n) ≫
      ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap f) n))
    (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap f) (n + 1)) ≫
      ι.map (HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n))

Tactic:
rw [← ι.map_comp, ← ι.map_comp, HomologicalComplex.Hom.comm]

Premises used: CategoryTheory.Functor.map_comp, HomologicalComplex.Hom.comm
-- 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
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 2) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 2))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f) (n + 2))
    (Iso.hom (Λ.chainComplexXIso X n) ≫
      Λ.F.map
          (kernel.map (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))
            (ι.map (HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n))
            (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap f) (n + 1)))
            (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap f) n)) ⋯) ≫
        Iso.inv (Λ.chainComplexXIso Y n))

Tactic:
apply ChainComplex.mkHom_f_succ_succ

Premises used: ChainComplex.mkHom_f_succ_succ
-- 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
h :
  ∀ (n : ℕ),
    Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex X) n)
      (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) n) (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) n)
⊢ Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_2, 0} C ℕ) (Λ.chainComplex X) (Λ.chainComplex X))
    (Λ.chainComplexMap (𝟙 X)) (𝟙 (Λ.chainComplex X))

Tactic:
ext 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
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex X) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) 0) (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) 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
n : ℕ
hn :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex X) n)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) n) (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) n)
h :
  ∀
    (hn :
      Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex X) 0)
        (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) 0) (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) 0)),
    Eq (α :=
      HomologicalComplex.X (Λ.chainComplex X) (HAdd.hAdd (α := ℕ) 0 1) ⟶
        HomologicalComplex.X (Λ.chainComplex X) (HAdd.hAdd (α := ℕ) 0 1))
      (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) (HAdd.hAdd (α := ℕ) 0 1))
      (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) (HAdd.hAdd (α := ℕ) 0 1))
h₁ :
  ∀ (n : ℕ)
    (hn :
      Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex X) (n + 1))
        (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) (n + 1))
        (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) (n + 1))),
    Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1 + 1) ⟶ HomologicalComplex.X (Λ.chainComplex X) (n + 1 + 1))
      (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) (n + 1 + 1))
      (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) (n + 1 + 1))
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex X) (n + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) (n + 1))
    (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) (n + 1))

Tactic:
obtain _ | n := 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
hn :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex X) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) 0) (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) 0)
⊢ Eq (α :=
    HomologicalComplex.X (Λ.chainComplex X) (HAdd.hAdd (α := ℕ) 0 1) ⟶
      HomologicalComplex.X (Λ.chainComplex X) (HAdd.hAdd (α := ℕ) 0 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) (HAdd.hAdd (α := ℕ) 0 1))
    (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
simp [hn]
-- 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 : ℕ
hn :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex X) (n + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) (n + 1))
    (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) (n + 1))
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1 + 1) ⟶ HomologicalComplex.X (Λ.chainComplex X) (n + 1 + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) (n + 1 + 1))
    (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) (n + 1 + 1))

Tactic:
simp [hn]
-- 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 : ℕ
h :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex X) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) 0) (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) 0)
h₁ :
  ∀ (n : ℕ)
    (hn :
      Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex X) n)
        (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) n) (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) n)),
    Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex X) (n + 1))
      (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) (n + 1))
      (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) (n + 1))
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex X) n)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) n) (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) n)

Tactic:
induction n with
  | zero => simp
  | succ n hn => obtain _ | n := n <;> simp [hn]
-- 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
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
inst_6 : Λ.F.PreservesZeroMorphisms
h :
  ∀ (n : ℕ),
    Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n)
      (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) n) (HomologicalComplex.Hom.f 0 n)
⊢ Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_2, 0} C ℕ) (Λ.chainComplex X) (Λ.chainComplex Y)) (Λ.chainComplexMap 0)
    0

Tactic:
ext 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 Y : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
inst_6 : Λ.F.PreservesZeroMorphisms
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex Y) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) 0) (HomologicalComplex.Hom.f 0 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 Y : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
inst_6 : Λ.F.PreservesZeroMorphisms
n : ℕ
hn :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) n) (HomologicalComplex.Hom.f 0 n)
h :
  ∀
    (hn :
      Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex Y) 0)
        (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) 0) (HomologicalComplex.Hom.f 0 0)),
    Eq (α :=
      HomologicalComplex.X (Λ.chainComplex X) (HAdd.hAdd (α := ℕ) 0 1) ⟶
        HomologicalComplex.X (Λ.chainComplex Y) (HAdd.hAdd (α := ℕ) 0 1))
      (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) (HAdd.hAdd (α := ℕ) 0 1))
      (HomologicalComplex.Hom.f 0 (HAdd.hAdd (α := ℕ) 0 1))
h₁ :
  ∀ (n : ℕ)
    (hn :
      Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1))
        (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) (n + 1)) (HomologicalComplex.Hom.f 0 (n + 1))),
    Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1 + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1 + 1))
      (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) (n + 1 + 1)) (HomologicalComplex.Hom.f 0 (n + 1 + 1))
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Y) (n + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) (n + 1)) (HomologicalComplex.Hom.f 0 (n + 1))

Tactic:
obtain _ | n := 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 Y : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
inst_6 : Λ.F.PreservesZeroMorphisms
hn :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex Y) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) 0) (HomologicalComplex.Hom.f 0 0)
⊢ Eq (α :=
    HomologicalComplex.X (Λ.chainComplex X) (HAdd.hAdd (α := ℕ) 0 1) ⟶
      HomologicalComplex.X (Λ.chainComplex Y) (HAdd.hAdd (α := ℕ) 0 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) (HAdd.hAdd (α := ℕ) 0 1))
    (HomologicalComplex.Hom.f 0 (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
simp [hn]