awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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)
⊢ 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))
have 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))
Tactic: obtain _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: obtain _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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 : ℕ
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) n) (HomologicalComplex.Hom.f 0 n)
have h : Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex Y) 0)
  (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) 0) (HomologicalComplex.Hom.f 0 0)
Tactic: induction n with
  | zero => simp
  | succ n hn => obtain _ | n := n <;> simp [hn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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)
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) n) (HomologicalComplex.Hom.f 0 n)
have 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))
Tactic: induction n with
  | zero => simp
  | succ n hn => obtain _ | n := n <;> simp [hn]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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 (α := Quiver.Hom (V := ChainComplex.{v_1, u_2, 0} C ℕ) (Λ.chainComplex X) (Λ.chainComplex Z))
    (Λ.chainComplexMap (f ≫ g)) (Λ.chainComplexMap f ≫ Λ.chainComplexMap g)
have 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)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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)
⊢ 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))
have 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))
Tactic: obtain _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: obtain _ | n := n
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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)
⊢ 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))
have 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) sorry) ≫
      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 sorry) ≫ Iso.inv (Λ.chainComplexXOneIso Y))
    (Iso.hom (Λ.chainComplexXOneIso Y) ≫
      Λ.F.map (kernel.map (Λ.π.app Y) (Λ.π.app Z) (ι.map (Λ.F.map g)) g sorry) ≫ Iso.inv (Λ.chainComplexXOneIso Z)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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)
⊢ 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)))
have 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) sorry))
  (Λ.F.map
    (CategoryStruct.comp (Y := kernel (Λ.π.app Y)) (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f sorry)
      (kernel.map (Λ.π.app Y) (Λ.π.app Z) (ι.map (Λ.F.map g)) g sorry)))
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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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)
⊢ 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 ⋯)))
have h : Eq (α := kernel (Λ.π.app X) ⟶ kernel (Λ.π.app Z))
  (kernel.map (Λ.π.app X) (Λ.π.app Z) (ι.map (Λ.F.map (f ≫ g))) (f ≫ g) sorry)
  (CategoryStruct.comp (Y := kernel (Λ.π.app Y)) (kernel.map (Λ.π.app X) (Λ.π.app Y) (ι.map (Λ.F.map f)) f sorry)
    (kernel.map (Λ.π.app Y) (Λ.π.app Z) (ι.map (Λ.F.map g)) g sorry))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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))
⊢ 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))
have 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))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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))
⊢ 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))
have 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)) sorry))
  (Λ.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)) sorry)
      (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)) sorry)))
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]
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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 : ℕ
⊢ 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)
have 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)
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Basic (goal)
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)
⊢ 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)
have 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))
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
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Homology.LeftResolution.Reduced (goal)
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.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))
have h₁ : Karoubi.Hom.f
    (Arrow.Hom.left
      (Arrow.homMk
          { f := ι.map ((F' Λ).obj X).p, comm := sorry :
            (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)
          sorry ≫
        Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := sorry }
          (𝟙
            (Arrow.mk (X := Functor.obj (toKaroubi A) ((Λ.F ⋙ ι).obj X)) (Functor.map (toKaroubi A) (Λ.π.app X))).right)
          sorry)) =
  (Arrow.Hom.left
      (𝟙 (Arrow.mk (X := (toKaroubi A ⋙ F Λ ⋙ Functor.obj (functorExtension₂ C A) ι).obj X) (NatTrans.app (π' Λ) X)))).f
Tactic: ext