awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Single
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
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 := ⋯, 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)
⊢ 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' := ⋯ })

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.Single
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 :
  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))
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Single
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)
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))
⊢ 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))

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Homology.Single
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
pos :
  Eq.{v + 1} (α := (if i = i then A else 0) ⟶ if i = i then A else 0)
    (eqToHom ⋯ ≫ 𝟙 A ≫ eqToHom ⋯ : (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)
⊢ 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)

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.Single
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 ι
A : V
i : ι
⊢ Eq.{v + 1} (α := (if i = i then A else 0) ⟶ if i = i then A else 0)
    (eqToHom ⋯ ≫ 𝟙 A ≫ eqToHom ⋯ : (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:
simp
-- Module: Mathlib.Algebra.Homology.Single
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} (α := Quiver.Hom.{v, u} (V := V) 0 0) 0 (𝟙 0)

Tactic:
(id_zero (C := V)).symm

Premises used: CategoryTheory.Limits.id_zero, Eq.symm
-- Module: Mathlib.Algebra.Homology.Single
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
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
⊢ 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:
convert! (id_zero (C := V)).symm

Premises used: CategoryTheory.Limits.id_zero, Eq.symm
-- Module: Mathlib.Algebra.Homology.Single
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
⊢ (if i = j then A else 0) = 0

Tactic:
simp [if_neg h]

Premises used: if_neg
-- Module: Mathlib.Algebra.Homology.Single
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
e_1 : ((if i = j then A else 0) ⟶ if i = j then A else 0) = Quiver.Hom.{v, u} (V := V) 0 0
e_1_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' := ⋯ :
          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

Tactic:
simp [if_neg h]

Premises used: if_neg
-- Module: Mathlib.Algebra.Homology.Single
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
e_1 : ((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:
simp [if_neg h]

Premises used: if_neg
-- Module: Mathlib.Algebra.Homology.Single
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
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 := ⋯, 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)
⊢ 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' := ⋯ })

Tactic:
ext
-- Module: Mathlib.Algebra.Homology.Single
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 :
  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))
⊢ 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)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Single
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)
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)
⊢ 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))

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Homology.Single
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
pos :
  Eq (α := (if i = i then X else 0) ⟶ if i = i then Z else 0)
    (eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ : (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 ⋯ ≫ f ≫ eqToHom ⋯ : (if i = i then X else 0) ⟶ if i = i then Y else 0)
        (eqToHom ⋯ ≫ g ≫ eqToHom ⋯ : (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)
⊢ 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)

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.Single
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 ι
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
i : ι
⊢ Eq (α := (if i = i then X else 0) ⟶ if i = i then Z else 0)
    (eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯ : (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 ⋯ ≫ f ≫ eqToHom ⋯ : (if i = i then X else 0) ⟶ if i = i then Y else 0)
        (eqToHom ⋯ ≫ g ≫ eqToHom ⋯ : (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:
simp
-- Module: Mathlib.Algebra.Homology.Single
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.{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:
simp
-- Module: Mathlib.Algebra.Homology.Single
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
⊢ X.{v, u, u_1} (Functor.obj (single V c j) A) j = A

Tactic:
if_pos rfl

Premises used: if_pos, rfl, ite
-- Module: Mathlib.Algebra.Homology.Single
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
dsimp : IsZero.{v, u} (if i = j then A else 0)
⊢ IsZero.{v, u} (X.{v, u, u_1} (Functor.obj (single V c j) A) i)

Tactic:
dsimp [single]

Premises used: HomologicalComplex.single
-- Module: Mathlib.Algebra.Homology.Single
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
rw : IsZero.{v, u} (C := V) 0
⊢ IsZero.{v, u} (if i = j then A else 0)

Tactic:
rw [if_neg hi]

Premises used: if_neg
-- Module: Mathlib.Algebra.Homology.Single
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} (C := V) 0

Tactic:
Limits.isZero_zero V

Premises used: CategoryTheory.Limits.isZero_zero
-- Module: Mathlib.Algebra.Homology.Single
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} (C := V) 0

Tactic:
exact Limits.isZero_zero V

Premises used: CategoryTheory.Limits.isZero_zero
-- Module: Mathlib.Algebra.Homology.Single
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
subst : X.{v, u, u_1} (Functor.obj (single V c i) A) i = A
⊢ X.{v, u, u_1} (Functor.obj (single V c j) A) i = A

Tactic:
subst hi
-- Module: Mathlib.Algebra.Homology.Single
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 ι
A : V
i : ι
⊢ X.{v, u, u_1} (Functor.obj (single V c i) A) i = A

Tactic:
simp [single]

Premises used: HomologicalComplex.single
-- Module: Mathlib.Algebra.Homology.Single
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
k l : ι
⊢ Eq.{v + 1} (α := X.{v, u, u_1} (Functor.obj (single V c j) A) k ⟶ X.{v, u, u_1} (Functor.obj (single V c j) A) l)
    (d (Functor.obj (single V c j) A) k l) 0

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Algebra.Homology.Single
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
dsimp :
  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)
⊢ 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))

Tactic:
dsimp [single]

Premises used: HomologicalComplex.single
-- Module: Mathlib.Algebra.Homology.Single
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
rw :
  Eq (α := (if j = j then A else 0) ⟶ if j = j then B else 0)
    (eqToHom ⋯ ≫ f ≫ eqToHom ⋯ : (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)
⊢ 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)

Tactic:
rw [dif_pos rfl]

Premises used: dif_pos, rfl
-- Module: Mathlib.Algebra.Homology.Single
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)
    (eqToHom ⋯ ≫ f ≫ eqToHom ⋯ : (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:
rfl
-- Module: Mathlib.Algebra.Homology.Single
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 (α :=
    Functor.obj.{v, v, u, u} (Functor.comp (D := HomologicalComplex.{v, u, u_1} V c) (single V c j) (eval V c j)) A ⟶
      Functor.obj.{v, v, u, u} (𝟭 V) B)
    (CategoryTheory.Functor.map (Functor.comp (D := HomologicalComplex.{v, u, u_1} V c) (single V c j) (eval V c j)) f ≫
      Iso.hom (singleObjXSelf c j B))
    (Iso.hom (singleObjXSelf c j A) ≫ CategoryTheory.Functor.map (𝟭 V) f)

Tactic:
simp [single_map_f_self]

Premises used: HomologicalComplex.single_map_f_self
-- Module: Mathlib.Algebra.Homology.Single
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 i : ι
hi : i ≠ j
⊢ IsZero (C := CategoryTheory.Functor.{v, v, u, u} V V)
    (Functor.comp (D := HomologicalComplex.{v, u, u_1} V c) (single V c j) (eval V c i))

Tactic:
Functor.isZero _ (fun _ ↦ isZero_single_obj_X c _ _ _ hi)

Premises used: CategoryTheory.Functor.isZero, HomologicalComplex.isZero_single_obj_X
-- Module: Mathlib.Algebra.Homology.Single
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
h : ∀ (i : ι), f.f i = g.f i
⊢ f = g

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.Single
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
neg : ∀ (h : ¬i = j), f.f i = g.f i
⊢ f.f i = g.f i

Tactic:
by_cases h : i = j
-- Module: Mathlib.Algebra.Homology.Single
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
pos : ∀ {f g : Functor.obj (single V c i) A ⟶ K} (hfg : f.f i = g.f i), f.f i = g.f i
⊢ f.f i = g.f i

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.Single
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
A : V
i : ι
f g : Functor.obj (single V c i) A ⟶ K
hfg : f.f i = g.f i
⊢ f.f i = g.f i

Tactic:
hfg
-- Module: Mathlib.Algebra.Homology.Single
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
A : V
i : ι
f g : Functor.obj (single V c i) A ⟶ K
hfg : f.f i = g.f i
⊢ f.f i = g.f i

Tactic:
exact hfg
-- Module: Mathlib.Algebra.Homology.Single
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

Tactic:
apply (isZero_single_obj_X c j A i h).eq_of_src

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.Algebra.Homology.Single
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
h : ∀ (i : ι), f.f i = g.f i
⊢ f = g

Tactic:
ext i