awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
X Y : V
f : X ⟶ Y
i : ι
h : i = j
⊢ HomologicalComplex.X.{v, u, u_1}
      { X := fun (i : ι) ↦ if i = j then X else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
        HomologicalComplex.{v, u, u_1} V c }
      i =
    X
have dsimp : (if i = j then X else 0) = X
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
X Y : V
f : X ⟶ Y
i : ι
h : i = j
⊢ (if i = j then X else 0) = X
have rw : X = X
Tactic: rw [if_pos h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
X Y : V
f : X ⟶ Y
i : ι
h : i = j
⊢ Y =
    HomologicalComplex.X.{v, u, u_1}
      { X := fun (i : ι) ↦ if i = j then Y else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ } i
have dsimp : Y = if i = j then Y else 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
X Y : V
f : X ⟶ Y
i : ι
h : i = j
⊢ Y = if i = j then Y else 0
have rw : Y = Y
Tactic: rw [if_pos h]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v, u, u_1} V c)
      { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ }
      { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ })
    { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ ≫ 𝟙 A ≫ eqToHom ⋯ else 0, comm' := ⋯ }
    (𝟙 { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ })
have h : ∀ (i : ι),
  Eq.{v + 1} (α :=
    X.{v, u, u_1}
        { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := sorry, d_comp_d' := sorry :
          HomologicalComplex.{v, u, u_1} V c }
        i ⟶
      X.{v, u, u_1} { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := sorry, d_comp_d' := sorry }
        i)
    (Hom.f { f := fun (i : ι) ↦ if h : i = j then eqToHom sorry ≫ 𝟙 A ≫ eqToHom sorry else 0, comm' := sorry } i)
    (Hom.f (𝟙 { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := sorry, d_comp_d' := sorry }) i)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
⊢ Eq.{v + 1} (α :=
    X.{v, u, u_1}
        { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
          HomologicalComplex.{v, u, u_1} V c }
        i ⟶
      X.{v, u, u_1} { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ }
        i)
    (Hom.f { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ ≫ 𝟙 A ≫ eqToHom ⋯ else 0, comm' := ⋯ } i)
    (Hom.f (𝟙 { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ }) i)
have h : Eq.{v + 1} (α := (if i = j then A else 0) ⟶ if i = j then A else 0)
  (if h : i = j then eqToHom sorry ≫ 𝟙 A ≫ eqToHom sorry else 0) (𝟙 (if i = j then A else 0))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
⊢ Eq.{v + 1} (α := (if i = j then A else 0) ⟶ if i = j then A else 0)
    (if h : i = j then eqToHom ⋯ ≫ 𝟙 A ≫ eqToHom ⋯ else 0) (𝟙 (if i = j then A else 0))
have pos : ∀ (h : i = j),
  Eq.{v + 1} (α := (if i = j then A else 0) ⟶ if i = j then A else 0)
    (eqToHom sorry ≫ 𝟙 A ≫ eqToHom sorry : (if i = j then A else 0) ⟶ if i = j then A else 0)
    (𝟙 (if i = j then A else 0) : (if i = j then A else 0) ⟶ if i = j then A else 0)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
pos :
  ∀ (h : i = j),
    Eq.{v + 1} (α := (if i = j then A else 0) ⟶ if i = j then A else 0)
      (eqToHom ⋯ ≫ 𝟙 A ≫ eqToHom ⋯ : (if i = j then A else 0) ⟶ if i = j then A else 0)
      (𝟙 (if i = j then A else 0) : (if i = j then A else 0) ⟶ if i = j then A else 0)
⊢ Eq.{v + 1} (α := (if i = j then A else 0) ⟶ if i = j then A else 0)
    (if h : i = j then eqToHom ⋯ ≫ 𝟙 A ≫ eqToHom ⋯ else 0) (𝟙 (if i = j then A else 0))
have neg : ∀ (h : ¬i = j), Eq.{v + 1} (α := (if i = j then A else 0) ⟶ if i = j then A else 0) 0 (𝟙 (if i = j then A else 0))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
h : i = j
⊢ Eq.{v + 1} (α := (if i = j then A else 0) ⟶ if i = j then A else 0)
    (eqToHom ⋯ ≫ 𝟙 A ≫ eqToHom ⋯ : (if i = j then A else 0) ⟶ if i = j then A else 0)
    (𝟙 (if i = j then A else 0) : (if i = j then A else 0) ⟶ if i = j then A else 0)
have pos : Eq.{v + 1} (α := (if i = i then A else 0) ⟶ if i = i then A else 0)
  (eqToHom sorry ≫ 𝟙 A ≫ eqToHom sorry : (if i = i then A else 0) ⟶ if i = i then A else 0)
  (𝟙 (if i = i then A else 0) : (if i = i then A else 0) ⟶ if i = i then A else 0)
Tactic: subst h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
h : ¬i = j
⊢ Eq.{v + 1} (α := (if i = j then A else 0) ⟶ if i = j then A else 0) 0 (𝟙 (if i = j then A else 0))
have h₁ : (if i = j then A else 0) = 0
Tactic: convert! (id_zero (C := V)).symm
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
h : ¬i = j
h₁ h₂ : (if i = j then A else 0) = 0
⊢ Eq.{v + 1} (α := (if i = j then A else 0) ⟶ if i = j then A else 0) 0 (𝟙 (if i = j then A else 0))
have h₃ : ((if i = j then A else 0) ⟶ if i = j then A else 0) = Quiver.Hom.{v, u} (V := V) 0 0 →
  (X.{v, u, u_1}
          { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := sorry, d_comp_d' := sorry :
            HomologicalComplex.{v, u, u_1} V c }
          i ⟶
        X.{v, u, u_1}
          { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := sorry, d_comp_d' := sorry :
            HomologicalComplex.{v, u, u_1} V c }
          i) =
      Quiver.Hom.{v, u} (V := V) 0 0 →
    X.{v, u, u_1}
        { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := sorry, d_comp_d' := sorry :
          HomologicalComplex.{v, u, u_1} V c }
        i =
      0
Tactic: convert! (id_zero (C := V)).symm
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
h : ¬i = j
h₁ h₂ : (if i = j then A else 0) = 0
h₃ h₄ :
  ((if i = j then A else 0) ⟶ if i = j then A else 0) = Quiver.Hom.{v, u} (V := V) 0 0 →
    (X.{v, u, u_1}
            { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
              HomologicalComplex.{v, u, u_1} V c }
            i ⟶
          X.{v, u, u_1}
            { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
              HomologicalComplex.{v, u, u_1} V c }
            i) =
        Quiver.Hom.{v, u} (V := V) 0 0 →
      X.{v, u, u_1}
          { X := fun (i : ι) ↦ if i = j then A else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v, u, u_1} V c }
          i =
        0
⊢ Eq.{v + 1} (α := (if i = j then A else 0) ⟶ if i = j then A else 0) 0 (𝟙 (if i = j then A else 0))
have h₅ : ((if i = j then A else 0) ⟶ if i = j then A else 0) = Quiver.Hom.{v, u} (V := V) 0 0 → (if i = j then A else 0) = 0
Tactic: convert! (id_zero (C := V)).symm
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v, u, u_1} V c)
      { X := fun (i : ι) ↦ if i = j then X else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ }
      { X := fun (i : ι) ↦ if i = j then Z else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ })
    { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ else 0, comm' := ⋯ }
    ({ f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0, comm' := ⋯ :
        Hom.{v, u, u_1}
          { X := fun (i : ι) ↦ if i = j then X else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v, u, u_1} V c }
          { X := fun (i : ι) ↦ if i = j then Y else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
            HomologicalComplex.{v, u, u_1} V c } } ≫
      { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ ≫ g ≫ eqToHom ⋯ else 0, comm' := ⋯ })
have h : ∀ (i : ι),
  Eq (α :=
    HomologicalComplex.X.{v, u, u_1}
        { X := fun (i : ι) ↦ if i = j then X else 0, d := fun (x x_1 : ι) ↦ 0, shape := sorry, d_comp_d' := sorry :
          HomologicalComplex.{v, u, u_1} V c }
        i ⟶
      HomologicalComplex.X.{v, u, u_1}
        { X := fun (i : ι) ↦ if i = j then Z else 0, d := fun (x x_1 : ι) ↦ 0, shape := sorry, d_comp_d' := sorry } i)
    (Hom.f { f := fun (i : ι) ↦ if h : i = j then eqToHom sorry ≫ (f ≫ g) ≫ eqToHom sorry else 0, comm' := sorry } i)
    (Hom.f
      ({ f := fun (i : ι) ↦ if h : i = j then eqToHom sorry ≫ f ≫ eqToHom sorry else 0, comm' := sorry :
          Hom.{v, u, u_1}
            { X := fun (i : ι) ↦ if i = j then X else 0, d := fun (x x_1 : ι) ↦ 0, shape := sorry, d_comp_d' := sorry :
              HomologicalComplex.{v, u, u_1} V c }
            { X := fun (i : ι) ↦ if i = j then Y else 0, d := fun (x x_1 : ι) ↦ 0, shape := sorry, d_comp_d' := sorry :
              HomologicalComplex.{v, u, u_1} V c } } ≫
        { f := fun (i : ι) ↦ if h : i = j then eqToHom sorry ≫ g ≫ eqToHom sorry else 0, comm' := sorry })
      i)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
i : ι
⊢ Eq (α :=
    HomologicalComplex.X.{v, u, u_1}
        { X := fun (i : ι) ↦ if i = j then X else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
          HomologicalComplex.{v, u, u_1} V c }
        i ⟶
      HomologicalComplex.X.{v, u, u_1}
        { X := fun (i : ι) ↦ if i = j then Z else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ } i)
    (Hom.f { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ else 0, comm' := ⋯ } i)
    (Hom.f
      ({ f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0, comm' := ⋯ :
          Hom.{v, u, u_1}
            { X := fun (i : ι) ↦ if i = j then X else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
              HomologicalComplex.{v, u, u_1} V c }
            { X := fun (i : ι) ↦ if i = j then Y else 0, d := fun (x x_1 : ι) ↦ 0, shape := ⋯, d_comp_d' := ⋯ :
              HomologicalComplex.{v, u, u_1} V c } } ≫
        { f := fun (i : ι) ↦ if h : i = j then eqToHom ⋯ ≫ g ≫ eqToHom ⋯ else 0, comm' := ⋯ })
      i)
have h : Eq.{v + 1} (α := (if i = j then X else 0) ⟶ if i = j then Z else 0)
  (if h : i = j then eqToHom sorry ≫ (f ≫ g) ≫ eqToHom sorry else 0)
  (CategoryStruct.comp (Y := if i = j then Y else 0) (if h : i = j then eqToHom sorry ≫ f ≫ eqToHom sorry else 0)
    (if h : i = j then eqToHom sorry ≫ g ≫ eqToHom sorry else 0))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
i : ι
⊢ Eq.{v + 1} (α := (if i = j then X else 0) ⟶ if i = j then Z else 0)
    (if h : i = j then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ else 0)
    (CategoryStruct.comp (Y := if i = j then Y else 0) (if h : i = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
      (if h : i = j then eqToHom ⋯ ≫ g ≫ eqToHom ⋯ else 0))
have pos : ∀ (h : i = j),
  Eq (α := (if i = j then X else 0) ⟶ if i = j then Z else 0)
    (eqToHom sorry ≫ (f ≫ g) ≫ eqToHom sorry : (if i = j then X else 0) ⟶ if i = j then Z else 0)
    (CategoryStruct.comp (Y := if i = j then Y else 0)
        (eqToHom sorry ≫ f ≫ eqToHom sorry : (if i = j then X else 0) ⟶ if i = j then Y else 0)
        (eqToHom sorry ≫ g ≫ eqToHom sorry : (if i = j then Y else 0) ⟶ if i = j then Z else 0) :
      (if i = j then X else 0) ⟶ if i = j then Z else 0)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
i : ι
pos :
  ∀ (h : i = j),
    Eq (α := (if i = j then X else 0) ⟶ if i = j then Z else 0)
      (eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ : (if i = j then X else 0) ⟶ if i = j then Z else 0)
      (CategoryStruct.comp (Y := if i = j then Y else 0)
          (eqToHom ⋯ ≫ f ≫ eqToHom ⋯ : (if i = j then X else 0) ⟶ if i = j then Y else 0)
          (eqToHom ⋯ ≫ g ≫ eqToHom ⋯ : (if i = j then Y else 0) ⟶ if i = j then Z else 0) :
        (if i = j then X else 0) ⟶ if i = j then Z else 0)
⊢ Eq.{v + 1} (α := (if i = j then X else 0) ⟶ if i = j then Z else 0)
    (if h : i = j then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ else 0)
    (CategoryStruct.comp (Y := if i = j then Y else 0) (if h : i = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
      (if h : i = j then eqToHom ⋯ ≫ g ≫ eqToHom ⋯ else 0))
have neg : ∀ (h : ¬i = j),
  Eq.{v + 1} (α := (if i = j then X else 0) ⟶ if i = j then Z else 0) 0
    (CategoryStruct.comp (Y := if i = j then Y else 0) 0 0)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
i : ι
h : i = j
⊢ Eq (α := (if i = j then X else 0) ⟶ if i = j then Z else 0)
    (eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ : (if i = j then X else 0) ⟶ if i = j then Z else 0)
    (CategoryStruct.comp (Y := if i = j then Y else 0)
        (eqToHom ⋯ ≫ f ≫ eqToHom ⋯ : (if i = j then X else 0) ⟶ if i = j then Y else 0)
        (eqToHom ⋯ ≫ g ≫ eqToHom ⋯ : (if i = j then Y else 0) ⟶ if i = j then Z else 0) :
      (if i = j then X else 0) ⟶ if i = j then Z else 0)
have pos : Eq (α := (if i = i then X else 0) ⟶ if i = i then Z else 0)
  (eqToHom sorry ≫ (f ≫ g) ≫ eqToHom sorry : (if i = i then X else 0) ⟶ if i = i then Z else 0)
  (CategoryStruct.comp (Y := if i = i then Y else 0)
      (eqToHom sorry ≫ f ≫ eqToHom sorry : (if i = i then X else 0) ⟶ if i = i then Y else 0)
      (eqToHom sorry ≫ g ≫ eqToHom sorry : (if i = i then Y else 0) ⟶ if i = i then Z else 0) :
    (if i = i then X else 0) ⟶ if i = i then Z else 0)
Tactic: subst h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
hi : i ≠ j
⊢ IsZero.{v, u} (X.{v, u, u_1} (Functor.obj (single V c j) A) i)
have dsimp : IsZero.{v, u} (if i = j then A else 0)
Tactic: dsimp [single]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
hi : i ≠ j
⊢ IsZero.{v, u} (if i = j then A else 0)
have rw : IsZero.{v, u} (C := V) 0
Tactic: rw [if_neg hi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A : V
i : ι
hi : i = j
⊢ X.{v, u, u_1} (Functor.obj (single V c j) A) i = A
have subst : X.{v, u, u_1} (Functor.obj (single V c i) A) i = A
Tactic: subst hi
Cleared hypotheses: j, hi
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f : A ⟶ B
⊢ Eq (α := X.{v, u, u_1} (Functor.obj (single V c j) A) j ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j)
    (Hom.f (CategoryTheory.Functor.map (single V c j) f) j)
    (Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B))
have dsimp : Eq (α := (if j = j then A else 0) ⟶ if j = j then B else 0)
  (if h : j = j then eqToHom sorry ≫ f ≫ eqToHom sorry else 0 : (if j = j then A else 0) ⟶ if j = j then B else 0)
  (Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B) :
    (if j = j then A else 0) ⟶ if j = j then B else 0)
Tactic: dsimp [single]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f : A ⟶ B
⊢ Eq (α := (if j = j then A else 0) ⟶ if j = j then B else 0)
    (if h : j = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0 : (if j = j then A else 0) ⟶ if j = j then B else 0)
    (Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B) :
      (if j = j then A else 0) ⟶ if j = j then B else 0)
have rw : Eq (α := (if j = j then A else 0) ⟶ if j = j then B else 0)
  (eqToHom sorry ≫ f ≫ eqToHom sorry : (if j = j then A else 0) ⟶ if j = j then B else 0)
  (Iso.hom (singleObjXSelf c j A) ≫ f ≫ Iso.inv (singleObjXSelf c j B) :
    (if j = j then A else 0) ⟶ if j = j then B else 0)
Tactic: rw [dif_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
f g : Functor.obj (single V c j) A ⟶ K
hfg : f.f j = g.f j
⊢ f = g
have h : ∀ (i : ι), f.f i = g.f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
f g : Functor.obj (single V c j) A ⟶ K
hfg : f.f j = g.f j
i : ι
⊢ f.f i = g.f i
have pos : ∀ (h : i = j), f.f i = g.f i
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
f g : Functor.obj (single V c j) A ⟶ K
hfg : f.f j = g.f j
i : ι
pos : ∀ (h : i = j), f.f i = g.f i
⊢ f.f i = g.f i
have neg : ∀ (h : ¬i = j), f.f i = g.f i
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
f g : Functor.obj (single V c j) A ⟶ K
hfg : f.f j = g.f j
i : ι
h : i = j
⊢ f.f i = g.f i
have pos : ∀ {f g : Functor.obj (single V c i) A ⟶ K} (hfg : f.f i = g.f i), f.f i = g.f i
Tactic: subst h
Cleared hypotheses: j, f, g, hfg, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
f g : K ⟶ Functor.obj (single V c j) A
hfg : f.f j = g.f j
⊢ f = g
have h : ∀ (i : ι), f.f i = g.f i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
f g : K ⟶ Functor.obj (single V c j) A
hfg : f.f j = g.f j
i : ι
⊢ f.f i = g.f i
have pos : ∀ (h : i = j), f.f i = g.f i
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
f g : K ⟶ Functor.obj (single V c j) A
hfg : f.f j = g.f j
i : ι
pos : ∀ (h : i = j), f.f i = g.f i
⊢ f.f i = g.f i
have neg : ∀ (h : ¬i = j), f.f i = g.f i
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
K : HomologicalComplex.{v, u, u_1} V c
j : ι
A : V
f g : K ⟶ Functor.obj (single V c j) A
hfg : f.f j = g.f j
i : ι
h : i = j
⊢ f.f i = g.f i
have pos : ∀ {f g : K ⟶ Functor.obj (single V c i) A} (hfg : f.f i = g.f i), f.f i = g.f i
Tactic: subst h
Cleared hypotheses: j, f, g, hfg, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Single (goal)
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
inst_2 : HasZeroObject.{v, u} V
ι : Type u_1
inst_3 : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f g : A ⟶ B
w :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v, u, u_1} V c) (Functor.obj (single V c j) A) (Functor.obj (single V c j) B))
    (CategoryTheory.Functor.map (single V c j) f) (CategoryTheory.Functor.map (single V c j) g)
⊢ f = g
have rw : Eq (α := A ⟶ X.{v, u, u_1} (Functor.obj (single V c j) B) j) (f ≫ Iso.inv (singleObjXSelf c j B))
  (g ≫ Iso.inv (singleObjXSelf c j B))
Tactic: rw [← cancel_mono (singleObjXSelf c j B).inv,
      ← cancel_epi (singleObjXSelf c j A).hom, ← single_map_f_self,
      ← single_map_f_self, w]