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 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 + 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))

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 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 : ℕ
h :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex Y) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) 0) (HomologicalComplex.Hom.f 0 0)
h₁ :
  ∀ (n : ℕ)
    (hn :
      Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n)
        (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) n) (HomologicalComplex.Hom.f 0 n)),
    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 ⟶ HomologicalComplex.X (Λ.chainComplex Y) n)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) n) (HomologicalComplex.Hom.f 0 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 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
h :
  ∀ (n : ℕ),
    Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Z) n)
      (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) n)
      (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) n)
⊢ Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_2, 0} C ℕ) (Λ.chainComplex X) (Λ.chainComplex Z))
    (Λ.chainComplexMap (f ≫ g)) (Λ.chainComplexMap f ≫ Λ.chainComplexMap g)

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 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 (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex Z) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) 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 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 : ℕ
hn :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Z) n)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) n)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) n)
h :
  ∀
    (hn :
      Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex Z) 0)
        (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) 0)
        (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) 0)),
    Eq (α :=
      HomologicalComplex.X (Λ.chainComplex X) (HAdd.hAdd (α := ℕ) 0 1) ⟶
        HomologicalComplex.X (Λ.chainComplex Z) (HAdd.hAdd (α := ℕ) 0 1))
      (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (HAdd.hAdd (α := ℕ) 0 1))
      (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) (HAdd.hAdd (α := ℕ) 0 1))
h₁ :
  ∀ (n : ℕ)
    (hn :
      Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Z) (n + 1))
        (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (n + 1))
        (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) (n + 1))),
    Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1 + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Z) (n + 1 + 1))
      (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (n + 1 + 1))
      (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) (n + 1 + 1))
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Z) (n + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (n + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) (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 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
hn :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex Z) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) 0)
h :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) 1 ⟶ HomologicalComplex.X (Λ.chainComplex Z) 1)
    (Iso.hom (Λ.chainComplexXOneIso X) ≫
      Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Z) (ι.map (Λ.F.map (f ≫ g))) (f ≫ g) ⋯) ≫
        Iso.inv (Λ.chainComplexXOneIso Z))
    (CategoryStruct.comp (Y := HomologicalComplex.X (Λ.chainComplex Y) 1)
      (Iso.hom (Λ.chainComplexXOneIso X) ≫
        Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯) ≫ Iso.inv (Λ.chainComplexXOneIso Y))
      (Iso.hom (Λ.chainComplexXOneIso Y) ≫
        Λ.F.map (kernel.map (Λ.π.app Y) (Λ.π.app Z) (ι.map (Λ.F.map g)) g ⋯) ≫ Iso.inv (Λ.chainComplexXOneIso Z)))
⊢ Eq (α :=
    HomologicalComplex.X (Λ.chainComplex X) (HAdd.hAdd (α := ℕ) 0 1) ⟶
      HomologicalComplex.X (Λ.chainComplex Z) (HAdd.hAdd (α := ℕ) 0 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (HAdd.hAdd (α := ℕ) 0 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) (HAdd.hAdd (α := ℕ) 0 1))

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
hn :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex Z) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) 0)
h :
  Eq (α := Λ.F.obj (kernel (Λ.π.app X)) ⟶ Λ.F.obj (kernel (Λ.π.app Z)))
    (Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Z) (ι.map (Λ.F.map (f ≫ g))) (f ≫ g) ⋯))
    (Λ.F.map
      (CategoryStruct.comp (Y := kernel (Λ.π.app Y)) (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯)
        (kernel.map (Λ.π.app Y) (Λ.π.app Z) (ι.map (Λ.F.map g)) g ⋯)))
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) 1 ⟶ HomologicalComplex.X (Λ.chainComplex Z) 1)
    (Iso.hom (Λ.chainComplexXOneIso X) ≫
      Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Z) (ι.map (Λ.F.map (f ≫ g))) (f ≫ g) ⋯) ≫
        Iso.inv (Λ.chainComplexXOneIso Z))
    (CategoryStruct.comp (Y := HomologicalComplex.X (Λ.chainComplex Y) 1)
      (Iso.hom (Λ.chainComplexXOneIso X) ≫
        Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯) ≫ Iso.inv (Λ.chainComplexXOneIso Y))
      (Iso.hom (Λ.chainComplexXOneIso Y) ≫
        Λ.F.map (kernel.map (Λ.π.app Y) (Λ.π.app Z) (ι.map (Λ.F.map g)) g ⋯) ≫ Iso.inv (Λ.chainComplexXOneIso Z)))

Tactic:
simp only [chainComplexMap_f_succ_succ, assoc, Iso.cancel_iso_hom_left,
        Iso.inv_hom_id_assoc, ← Λ.F.map_comp_assoc, Iso.cancel_iso_inv_right_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.LeftResolution.F, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.cancel_iso_hom_left, CategoryTheory.Iso.cancel_iso_inv_right_assoc, CategoryTheory.Abelian.LeftResolution.chainComplexMap_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 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
hn :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex Z) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) 0)
h :
  Eq (α := kernel (Λ.π.app X) ⟶ kernel (Λ.π.app Z))
    (kernel.map (Λ.π.app X) (Λ.π.app Z) (ι.map (Λ.F.map (f ≫ g))) (f ≫ g) ⋯)
    (CategoryStruct.comp (Y := kernel (Λ.π.app Y)) (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯)
      (kernel.map (Λ.π.app Y) (Λ.π.app Z) (ι.map (Λ.F.map g)) g ⋯))
⊢ Eq (α := Λ.F.obj (kernel (Λ.π.app X)) ⟶ Λ.F.obj (kernel (Λ.π.app Z)))
    (Λ.F.map (kernel.map (Λ.π.app X) (Λ.π.app Z) (ι.map (Λ.F.map (f ≫ g))) (f ≫ g) ⋯))
    (Λ.F.map
      (CategoryStruct.comp (Y := kernel (Λ.π.app Y)) (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f ⋯)
        (kernel.map (Λ.π.app Y) (Λ.π.app Z) (ι.map (Λ.F.map g)) g ⋯)))

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 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 : ℕ
hn :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Z) (n + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (n + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) (n + 1))
h :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1 + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Z) (n + 1 + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (n + 1 + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f) (n + 1 + 1) ≫
      HomologicalComplex.Hom.f (Λ.chainComplexMap g) (n + 1 + 1))
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1 + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Z) (n + 1 + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (n + 1 + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) (n + 1 + 1))

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
n : ℕ
hn :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Z) (n + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (n + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) (n + 1))
h :
  Eq (α :=
    Λ.F.obj
        (kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex X) (n + 1)))
          (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))) ⟶
      Λ.F.obj
        (kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex Z) (n + 1)))
          (ι.map (HomologicalComplex.d (Λ.chainComplex Z) (n + 1) n))))
    (Λ.F.map
      (kernel.map (ι.map (HomologicalComplex.d (Λ.chainComplex X) (n + 1) n))
        (ι.map (HomologicalComplex.d (Λ.chainComplex Z) (n + 1) n))
        (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (n + 1)))
        (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) n)) ⋯))
    (Λ.F.map
      (CategoryStruct.comp (Y :=
        kernel (X := ι.obj (HomologicalComplex.X (Λ.chainComplex Y) (n + 1)))
          (ι.map (HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n)))
        (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)) ⋯)
        (kernel.map (ι.map (HomologicalComplex.d (Λ.chainComplex Y) (n + 1) n))
          (ι.map (HomologicalComplex.d (Λ.chainComplex Z) (n + 1) n))
          (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap g) (n + 1)))
          (ι.map (HomologicalComplex.Hom.f (Λ.chainComplexMap g) n)) ⋯)))
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1 + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Z) (n + 1 + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (n + 1 + 1))
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f) (n + 1 + 1) ≫
      HomologicalComplex.Hom.f (Λ.chainComplexMap g) (n + 1 + 1))

Tactic:
simp only [chainComplexMap_f_succ_succ, assoc, Iso.cancel_iso_hom_left,
        Iso.inv_hom_id_assoc, ← Λ.F.map_comp_assoc, Iso.cancel_iso_inv_right_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.LeftResolution.F, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.cancel_iso_hom_left, CategoryTheory.Iso.cancel_iso_inv_right_assoc, CategoryTheory.Abelian.LeftResolution.chainComplexMap_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 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 : ℕ
h :
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex Z) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) 0)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) 0)
h₁ :
  ∀ (n : ℕ)
    (hn :
      Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Z) n)
        (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) n)
        (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) n)),
    Eq (α := HomologicalComplex.X (Λ.chainComplex X) (n + 1) ⟶ HomologicalComplex.X (Λ.chainComplex Z) (n + 1))
      (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) (n + 1))
      (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) (n + 1))
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Z) n)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (f ≫ g)) n)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap f ≫ Λ.chainComplexMap g) n)

Tactic:
induction n with
  | zero => simp
  | succ n hn =>
    obtain _ | n := n
    all_goals
      dsimp
      simp only [chainComplexMap_f_succ_succ, assoc, Iso.cancel_iso_hom_left,
        Iso.inv_hom_id_assoc, ← Λ.F.map_comp_assoc, Iso.cancel_iso_inv_right_assoc]
      congr 1
      cat_disch

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Abelian.LeftResolution.F, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Iso.cancel_iso_hom_left, CategoryTheory.Iso.cancel_iso_inv_right_assoc, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_succ_succ
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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 ι
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Preadditive.{v_2, u_1} A
inst_4 : ι.Additive
X : A
⊢ (𝟙 (Λ.F.obj X) - Λ.F.map 0) ≫ (𝟙 (Λ.F.obj X) - Λ.F.map 0) = 𝟙 (Λ.F.obj X) - Λ.F.map 0

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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 ι
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Preadditive.{v_2, u_1} A
inst_4 : ι.Additive
X Y : A
f : X ⟶ Y
⊢ { X := Λ.F.obj X, p := 𝟙 (Λ.F.obj X) - Λ.F.map 0, idem := ⋯ : Karoubi.{v_1, u_2} C }.p ≫
      (Λ.F.map f - Λ.F.map 0) ≫ { X := Λ.F.obj Y, p := 𝟙 (Λ.F.obj Y) - Λ.F.map 0, idem := ⋯ : Karoubi.{v_1, u_2} C }.p =
    Λ.F.map f - Λ.F.map 0

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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 ι
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Preadditive.{v_2, u_1} A
inst_4 : ι.Additive
X Y Z : A
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ { f := Λ.F.map (x ≫ x_1) - Λ.F.map 0, comm := ⋯ :
      { X := Λ.F.obj X, p := 𝟙 (Λ.F.obj X) - Λ.F.map 0, idem := ⋯ : Karoubi.{v_1, u_2} C }.Hom
        { X := Λ.F.obj Z, p := 𝟙 (Λ.F.obj Z) - Λ.F.map 0, idem := ⋯ : Karoubi.{v_1, u_2} C } } =
    { f := Λ.F.map x - Λ.F.map 0, comm := ⋯ :
        { X := Λ.F.obj X, p := 𝟙 (Λ.F.obj X) - Λ.F.map 0, idem := ⋯ : Karoubi.{v_1, u_2} C }.Hom
          { X := Λ.F.obj Y, p := 𝟙 (Λ.F.obj Y) - Λ.F.map 0, idem := ⋯ : Karoubi.{v_1, u_2} C } } ≫
      { f := Λ.F.map x_1 - Λ.F.map 0, comm := ⋯ }

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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 ι
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Preadditive.{v_2, u_1} A
inst_4 : ι.Additive
X : A
⊢ ((toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X).p ≫
      Λ.π.app X ≫ Karoubi.p (Functor.obj (toKaroubi A) X) =
    Λ.π.app X

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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 ι
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Preadditive.{v_2, u_1} A
inst_4 : ι.Additive
X : A
⊢ (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X) (NatTrans.app (π' Λ) X)).left.p ≫
      ι.map ((F' Λ).obj X).p ≫
        (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X)) (Functor.map (toKaroubi A) (Λ.π.app X))).left.p =
    ι.map ((F' Λ).obj X).p

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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 ι
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Preadditive.{v_2, u_1} A
inst_4 : ι.Additive
X : A
⊢ (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X)) (Functor.map (toKaroubi A) (Λ.π.app X))).left.p ≫
      ι.map ((F' Λ).obj X).p ≫
        (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
              (NatTrans.app (π' Λ) X)).left.p =
    ι.map ((F' Λ).obj X).p

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.LeftResolution.Reduced
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 ι
inst_2 : Preadditive.{v_1, u_2} C
inst_3 : Preadditive.{v_2, u_1} A
inst_4 : ι.Additive
X : A
h₁ :
  Karoubi.Hom.f
      (Arrow.Hom.left
        (Arrow.homMk
            { f := ι.map ((F' Λ).obj X).p, comm := ⋯ :
              (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
                      (NatTrans.app (π' Λ) X)).left.Hom
                (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X))
                    (Functor.map (toKaroubi A) (Λ.π.app X))).left }
            (𝟙
              (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
                  (NatTrans.app (π' Λ) X)).right)
            ⋯ ≫
          Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ }
            (𝟙
              (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X))
                  (Functor.map (toKaroubi A) (Λ.π.app X))).right)
            ⋯)) =
    (Arrow.Hom.left
        (𝟙
          (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
            (NatTrans.app (π' Λ) X)))).f
h₂ :
  Karoubi.Hom.f
      (Arrow.Hom.right
        (Arrow.homMk
            { f := ι.map ((F' Λ).obj X).p, comm := ⋯ :
              (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
                      (NatTrans.app (π' Λ) X)).left.Hom
                (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X))
                    (Functor.map (toKaroubi A) (Λ.π.app X))).left }
            (𝟙
              (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
                  (NatTrans.app (π' Λ) X)).right)
            ⋯ ≫
          Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ }
            (𝟙
              (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X))
                  (Functor.map (toKaroubi A) (Λ.π.app X))).right)
            ⋯)) =
    (Arrow.Hom.right
        (𝟙
          (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
            (NatTrans.app (π' Λ) X)))).f
⊢ Arrow.homMk
        { f := ι.map ((F' Λ).obj X).p, comm := ⋯ :
          (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
                  (NatTrans.app (π' Λ) X)).left.Hom
            (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X)) (Functor.map (toKaroubi A) (Λ.π.app X))).left }
        (𝟙
          (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X)
              (NatTrans.app (π' Λ) X)).right)
        ⋯ ≫
      Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ }
        (𝟙 (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X)) (Functor.map (toKaroubi A) (Λ.π.app X))).right)
        ⋯ =
    𝟙 (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X) (NatTrans.app (π' Λ) X))

Tactic:
ext