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 : 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 (α :=
    ι.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)))
have 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)))))
Tactic: rw [← this, ← Functor.map_comp]
-- 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 : 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 (α :=
    ι.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)))))
have 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))))
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 : A
inst_2 : ι.Full
inst_3 : ι.Faithful
inst_4 : HasZeroMorphisms.{v_1, u_2} C
inst_5 : Abelian.{v_2, u_1} A
n : ℕ
⊢ HomologicalComplex.ExactAt
    (Functor.obj (C := HomologicalComplex.{v_1, u_2, 0} C (ComplexShape.down ℕ))
      (ι.mapHomologicalComplex (ComplexShape.down ℕ)) (Λ.chainComplex X))
    (n + 1)
have 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))
    sorry)
Tactic: rw [HomologicalComplex.exactAt_iff' _ (n + 2) (n + 1) n
    (ComplexShape.prev_eq' _ (by dsimp; lia)) (by simp),
    ShortComplex.exact_iff_epi_kernel_lift]
-- 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 (α := ι.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)))
have 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 sorry) ≫ 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
-- 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 (α := ι.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)))
have 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 sorry)) ≫
      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 [Category.assoc, Functor.map_comp, map_chainComplex_d_1_0]
-- 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 (α := ι.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))))
have 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 sorry) ≫
          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 only [← ι.map_comp, ← ι.map_comp_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 (α := ι.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))
have 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))
Tactic: rw [← ι.map_comp, ← ι.map_comp, HomologicalComplex.Hom.comm]
-- 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 : ℕ
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))
⊢ 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))
have 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))
Tactic: rw [← ι.map_comp, ← ι.map_comp, HomologicalComplex.Hom.comm]
-- 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 : ℕ
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))
⊢ 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))
have 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))
Tactic: rw [← ι.map_comp, ← ι.map_comp, HomologicalComplex.Hom.comm]
-- 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 : A
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 X))
    (Λ.chainComplexMap (𝟙 X)) (𝟙 (Λ.chainComplex X))
have 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)
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 : 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)
⊢ 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))
have 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))
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 : 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))
⊢ 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))
have 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))
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 : 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 (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex X) n)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) n) (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) n)
have h : Eq (α := HomologicalComplex.X (Λ.chainComplex X) 0 ⟶ HomologicalComplex.X (Λ.chainComplex X) 0)
  (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) 0) (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) 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 : 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)
⊢ Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex X) n)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap (𝟙 X)) n) (HomologicalComplex.Hom.f (𝟙 (Λ.chainComplex X)) n)
have 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))
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
⊢ Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_2, 0} C ℕ) (Λ.chainComplex X) (Λ.chainComplex Y)) (Λ.chainComplexMap 0)
    0
have h : ∀ (n : ℕ),
  Eq (α := HomologicalComplex.X (Λ.chainComplex X) n ⟶ HomologicalComplex.X (Λ.chainComplex Y) n)
    (HomologicalComplex.Hom.f (Λ.chainComplexMap 0) n) (HomologicalComplex.Hom.f 0 n)
Tactic: ext n