awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.DifferentialObject
Goal:
β : Type u_1
inst : AddCommGroup β
b : β
V : Type u_2
inst_1 : Category.{v_1, u_2} V
inst_2 : HasZeroMorphisms.{v_1, u_2} V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x y : β
h : x = y
refl : X.objEqToHom ⋯ ≫ X.d x = X.d x ≫ X.objEqToHom ⋯
⊢ X.objEqToHom h ≫ X.d y = X.d x ≫ X.objEqToHom ⋯

Tactic:
cases h
-- Module: Mathlib.Algebra.Homology.DifferentialObject
Goal:
β : Type u_1
inst : AddCommGroup β
b : β
V : Type u_2
inst_1 : Category.{v_1, u_2} V
inst_2 : HasZeroMorphisms.{v_1, u_2} V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ X.objEqToHom ⋯ ≫ X.d x = X.d x ≫ X.objEqToHom ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DifferentialObject
Goal:
β : Type u_1
inst : AddCommGroup β
b : β
V : Type u_2
inst_1 : Category.{v_1, u_2} V
inst_2 : HasZeroMorphisms.{v_1, u_2} V
X : DifferentialObject ℤ (GradedObjectWithShift b V)
x : β
⊢ Eq.{v_1 + 1} (α :=
    X.obj x ⟶
      Functor.obj (CategoryTheory.shiftFunctor (GradedObjectWithShift b V) (A := ℤ) 1) X.obj
        ((fun (b_1 : β) ↦ b_1 + HSMul.hSMul (α := ℤ) (Discrete.as { as := 1 : Discrete ℤ }) b) x))
    (X.d x ≫ X.d ((fun (b_1 : β) ↦ b_1 + HSMul.hSMul (α := ℤ) (Discrete.as { as := 1 : Discrete ℤ }) b) x) :
      X.obj x ⟶
        Functor.obj (CategoryTheory.shiftFunctor (GradedObjectWithShift b V) (A := ℤ) 1) X.obj
          ((fun (b_1 : β) ↦ b_1 + HSMul.hSMul (α := ℤ) (Discrete.as { as := 1 : Discrete ℤ }) b) x))
    (0 :
      X.obj x ⟶
        Functor.obj (CategoryTheory.shiftFunctor (GradedObjectWithShift b V) (A := ℤ) 1) X.obj
          ((fun (b_1 : β) ↦ b_1 + HSMul.hSMul (α := ℤ) (Discrete.as { as := 1 : Discrete ℤ }) b) x))

Tactic:
congr_fun X.d_squared _

Premises used: CategoryTheory.DifferentialObject.d_squared, congr_fun
-- Module: Mathlib.Algebra.Homology.DifferentialObject
Goal:
β : Type u_1
inst : AddCommGroup β
b : β
V : Type u_2
inst_1 : Category.{v_1, u_2} V
inst_2 : HasZeroMorphisms.{v_1, u_2} V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
x y : β
h : x = y
refl : X.objEqToHom ⋯ ≫ f.f x = f.f x ≫ Y.objEqToHom ⋯
⊢ X.objEqToHom h ≫ f.f y = f.f x ≫ Y.objEqToHom h

Tactic:
cases h
-- Module: Mathlib.Algebra.Homology.DifferentialObject
Goal:
β : Type u_1
inst : AddCommGroup β
b : β
V : Type u_2
inst_1 : Category.{v_1, u_2} V
inst_2 : HasZeroMorphisms.{v_1, u_2} V
X Y : DifferentialObject ℤ (GradedObjectWithShift b V)
f : X ⟶ Y
x : β
⊢ X.objEqToHom ⋯ ≫ f.f x = f.f x ≫ Y.objEqToHom ⋯

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.DifferentialObject
Goal:
β : Type u_1
inst : AddCommGroup β
b : β
V : Type u_2
inst_1 : Category.{v_1, u_2} V
inst_2 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V (ComplexShape.up' b)
x y z : β
h : y = z
refl : X.d x y ≫ eqToHom ⋯ = X.d x y
⊢ X.d x y ≫ eqToHom ⋯ = X.d x z

Tactic:
cases h
-- Module: Mathlib.Algebra.Homology.DifferentialObject
Goal:
β : Type u_1
inst : AddCommGroup β
b : β
V : Type u_2
inst_1 : Category.{v_1, u_2} V
inst_2 : HasZeroMorphisms.{v_1, u_2} V
X : HomologicalComplex.{v_1, u_2, u_1} V (ComplexShape.up' b)
x y : β
⊢ X.d x y ≫ eqToHom ⋯ = X.d x y

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k k' : ι
hk : k = i₀ ∧ k' = i₁ ∧ i₀ ≠ i₁
hnc : ¬k' = i₀
⊢ X₁ = if k' = i₀ then X₀ else if k' = i₁ then X₁ else 0

Tactic:
rw [if_neg, if_pos hk.2.1]

Premises used: if_pos, And.right, And.left, if_neg
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k k' : ι
hk : k = i₀ ∧ k' = i₁ ∧ i₀ ≠ i₁
⊢ ¬k' = i₀

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
i j : ι
hij : ¬c.Rel i j
⊢ ¬(i = i₀ ∧ j = i₁ ∧ i₀ ≠ i₁)

Tactic:
aesop
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
dsimp :
  Eq.{v_1 + 1} (α :=
    (if i = i₀ then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i₀ then X₀ else if k = i₁ then X₁ else 0)
    (CategoryStruct.comp (Y := if j = i₀ then X₀ else if j = i₁ then X₁ else 0)
      (if hk : i = i₀ ∧ j = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
      (if hk : j = i₀ ∧ k = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
    0
⊢ Eq.{v_1 + 1} (α :=
    (if i = i₀ then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i₀ then X₀ else if k = i₁ then X₁ else 0)
    (CategoryStruct.comp (Y := if j = i₀ then X₀ else if j = i₁ then X₁ else 0)
      (if hk : i = i₀ ∧ j = i₁ ∧ i₀ ≠ i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
      (if hk : j = i₀ ∧ k = i₁ ∧ i₀ ≠ i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
    0

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
pos :
  ∀ (hi : i = i₀),
    Eq.{v_1 + 1} (α :=
      (if i = i₀ then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i₀ then X₀ else if k = i₁ then X₁ else 0)
      (CategoryStruct.comp (Y := if j = i₀ then X₀ else if j = i₁ then X₁ else 0)
        (if hk : i = i₀ ∧ j = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
        (if hk : j = i₀ ∧ k = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
      0
neg :
  ∀ (hi : ¬i = i₀),
    Eq.{v_1 + 1} (α :=
      (if i = i₀ then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i₀ then X₀ else if k = i₁ then X₁ else 0)
      (CategoryStruct.comp (Y := if j = i₀ then X₀ else if j = i₁ then X₁ else 0)
        (if hk : i = i₀ ∧ j = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
        (if hk : j = i₀ ∧ k = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
      0
⊢ Eq.{v_1 + 1} (α :=
    (if i = i₀ then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i₀ then X₀ else if k = i₁ then X₁ else 0)
    (CategoryStruct.comp (Y := if j = i₀ then X₀ else if j = i₁ then X₁ else 0)
      (if hk : i = i₀ ∧ j = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
      (if hk : j = i₀ ∧ k = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
    0

Tactic:
by_cases hi : i = i₀
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi : i = i₀
pos :
  ∀ (hi₀₁ : c.Rel i i₁),
    Eq.{v_1 + 1} (α :=
      (if i = i then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i then X₀ else if k = i₁ then X₁ else 0)
      (CategoryStruct.comp (Y := if j = i then X₀ else if j = i₁ then X₁ else 0)
        (if hk : i = i ∧ j = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
        (if hk : j = i ∧ k = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
      0
⊢ Eq.{v_1 + 1} (α :=
    (if i = i₀ then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i₀ then X₀ else if k = i₁ then X₁ else 0)
    (CategoryStruct.comp (Y := if j = i₀ then X₀ else if j = i₁ then X₁ else 0)
      (if hk : i = i₀ ∧ j = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
      (if hk : j = i₀ ∧ k = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
    0

Tactic:
subst hi
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₁ i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi₀₁ : c.Rel i i₁
pos :
  ∀ (hj : j = i₁),
    Eq.{v_1 + 1} (α :=
      (if i = i then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i then X₀ else if k = i₁ then X₁ else 0)
      (CategoryStruct.comp (Y := if j = i then X₀ else if j = i₁ then X₁ else 0)
        (if hk : i = i ∧ j = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
        (if hk : j = i ∧ k = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
      0
neg :
  ∀ (hj : ¬j = i₁),
    Eq.{v_1 + 1} (α :=
      (if i = i then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i then X₀ else if k = i₁ then X₁ else 0)
      (CategoryStruct.comp (Y := if j = i then X₀ else if j = i₁ then X₁ else 0)
        (if hk : i = i ∧ j = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
        (if hk : j = i ∧ k = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
      0
⊢ Eq.{v_1 + 1} (α := (if i = i then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i then X₀ else if k = i₁ then X₁ else 0)
    (CategoryStruct.comp (Y := if j = i then X₀ else if j = i₁ then X₁ else 0)
      (if hk : i = i ∧ j = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
      (if hk : j = i ∧ k = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
    0

Tactic:
by_cases hj : j = i₁
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₁ i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi₀₁ : c.Rel i i₁
hj : j = i₁
pos :
  ∀ (hi₀₁ : c.Rel i j),
    Eq.{v_1 + 1} (α := (if i = i then X₀ else if i = j then X₁ else 0) ⟶ if k = i then X₀ else if k = j then X₁ else 0)
      (CategoryStruct.comp (Y := if j = i then X₀ else if j = j then X₁ else 0)
        (if hk : i = i ∧ j = j ∧ ¬i = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
        (if hk : j = i ∧ k = j ∧ ¬i = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
      0
⊢ Eq.{v_1 + 1} (α := (if i = i then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i then X₀ else if k = i₁ then X₁ else 0)
    (CategoryStruct.comp (Y := if j = i then X₀ else if j = i₁ then X₁ else 0)
      (if hk : i = i ∧ j = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
      (if hk : j = i ∧ k = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
    0

Tactic:
subst hj
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi₀₁ : c.Rel i j
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : j = i → k = j → ¬i = j → False
⊢ ¬(j = i ∧ k = j ∧ ¬i = j)

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi₀₁ : c.Rel i j
pos :
  Eq.{v_1 + 1} (α := (if i = i then X₀ else if i = j then X₁ else 0) ⟶ if k = i then X₀ else if k = j then X₁ else 0)
    (CategoryStruct.comp (Y := if j = i then X₀ else if j = j then X₁ else 0)
      (if hk : i = i ∧ j = j ∧ ¬i = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) 0)
    0
⊢ Eq.{v_1 + 1} (α := (if i = i then X₀ else if i = j then X₁ else 0) ⟶ if k = i then X₀ else if k = j then X₁ else 0)
    (CategoryStruct.comp (Y := if j = i then X₀ else if j = j then X₁ else 0)
      (if hk : i = i ∧ j = j ∧ ¬i = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
      (if hk : j = i ∧ k = j ∧ ¬i = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
    0

Tactic:
nth_rw 2 [dif_neg (by tauto)]

Premises used: dif_neg
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi₀₁ : c.Rel i j
pos pos₁ :
  Eq.{v_1 + 1} (α := (if i = i then X₀ else if i = j then X₁ else 0) ⟶ if k = i then X₀ else if k = j then X₁ else 0) 0
    0
⊢ Eq.{v_1 + 1} (α := (if i = i then X₀ else if i = j then X₁ else 0) ⟶ if k = i then X₀ else if k = j then X₁ else 0)
    (CategoryStruct.comp (Y := if j = i then X₀ else if j = j then X₁ else 0)
      (if hk : i = i ∧ j = j ∧ ¬i = j then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0) 0)
    0

Tactic:
rw [comp_zero]

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₁ i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi₀₁ : c.Rel i i₁
hj : ¬j = i₁
tauto : i = i → j = i₁ → ¬i = i₁ → False
⊢ ¬(i = i ∧ j = i₁ ∧ ¬i = i₁)

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₁ i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi₀₁ : c.Rel i i₁
hj : ¬j = i₁
neg :
  Eq.{v_1 + 1} (α := (if i = i then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i then X₀ else if k = i₁ then X₁ else 0)
    (CategoryStruct.comp (Y := if j = i then X₀ else if j = i₁ then X₁ else 0) 0
      (if hk : j = i ∧ k = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
    0
neg₁ neg₂ :
  Eq.{v_1 + 1} (α := (if i = i then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i then X₀ else if k = i₁ then X₁ else 0)
    0 0
⊢ Eq.{v_1 + 1} (α := (if i = i then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i then X₀ else if k = i₁ then X₁ else 0)
    (CategoryStruct.comp (Y := if j = i then X₀ else if j = i₁ then X₁ else 0)
      (if hk : i = i ∧ j = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
      (if hk : j = i ∧ k = i₁ ∧ ¬i = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
    0

Tactic:
rw [dif_neg (by tauto), zero_comp]

Premises used: dif_neg, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi : ¬i = i₀
tauto : i = i₀ → j = i₁ → ¬i₀ = i₁ → False
⊢ ¬(i = i₀ ∧ j = i₁ ∧ ¬i₀ = i₁)

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi : ¬i = i₀
neg :
  Eq.{v_1 + 1} (α :=
    (if i = i₀ then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i₀ then X₀ else if k = i₁ then X₁ else 0)
    (CategoryStruct.comp (Y := if j = i₀ then X₀ else if j = i₁ then X₁ else 0) 0
      (if hk : j = i₀ ∧ k = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
    0
neg₁ neg₂ :
  Eq.{v_1 + 1} (α :=
    (if i = i₀ then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i₀ then X₀ else if k = i₁ then X₁ else 0) 0 0
⊢ Eq.{v_1 + 1} (α :=
    (if i = i₀ then X₀ else if i = i₁ then X₁ else 0) ⟶ if k = i₀ then X₀ else if k = i₁ then X₁ else 0)
    (CategoryStruct.comp (Y := if j = i₀ then X₀ else if j = i₁ then X₁ else 0)
      (if hk : i = i₀ ∧ j = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0)
      (if hk : j = i₀ ∧ k = i₁ ∧ ¬i₀ = i₁ then eqToHom ⋯ ≫ f ≫ eqToHom ⋯ else 0))
    0

Tactic:
rw [dif_neg (by tauto), zero_comp]

Premises used: dif_neg, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
dsimp : IsZero.{v_1, u_1} (if k = i₀ then X₀ else if k = i₁ then X₁ else 0)
⊢ IsZero.{v_1, u_1} (X (double f hi₀₁) k)

Tactic:
dsimp [double]

Premises used: HomologicalComplex.double
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
rw : IsZero.{v_1, u_1} (C := C) 0
⊢ IsZero.{v_1, u_1} (if k = i₀ then X₀ else if k = i₁ then X₁ else 0)

Tactic:
rw [if_neg h₀, if_neg h₁]

Premises used: if_neg
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
⊢ IsZero.{v_1, u_1} (C := C) 0

Tactic:
Limits.isZero_zero C

Premises used: CategoryTheory.Limits.isZero_zero
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
⊢ IsZero.{v_1, u_1} (C := C) 0

Tactic:
exact Limits.isZero_zero C

Premises used: CategoryTheory.Limits.isZero_zero
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
dsimp : (if i₁ = i₀ then X₀ else if i₁ = i₁ then X₁ else 0) = X₁
⊢ X (double f hi₀₁) i₁ = X₁

Tactic:
dsimp [double]

Premises used: HomologicalComplex.double
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
rw : (if i₁ = i₁ then X₁ else 0) = X₁
rw₁ rw₂ : X₁ = X₁
⊢ (if i₁ = i₀ then X₀ else if i₁ = i₁ then X₁ else 0) = X₁

Tactic:
rw [if_neg h.symm, if_pos rfl]

Premises used: Ne.symm, if_pos, if_neg, rfl
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
⊢ Eq (α := X (double f hi₀₁) i₀ ⟶ X (double f hi₀₁) i₁) (d (double f hi₀₁) i₀ i₁)
    (Iso.hom (doubleXIso₀ f hi₀₁) ≫ f ≫ Iso.inv (doubleXIso₁ f hi₀₁ h))

Tactic:
dif_pos ⟨rfl, rfl, h⟩

Premises used: Eq.mpr, CategoryTheory.eqToHom, dif_pos, dite, ite
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
a b : ι
ha : a ≠ i₀
tauto : a = i₀ → b = i₁ → i₀ ≠ i₁ → False
⊢ ¬(a = i₀ ∧ b = i₁ ∧ i₀ ≠ i₁)

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
a b : ι
hb : b ≠ i₁
tauto : a = i₀ → b = i₁ → i₀ ≠ i₁ → False
⊢ ¬(a = i₀ ∧ b = i₁ ∧ i₀ ≠ i₁)

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
h : ∀ (k : ι), φ.f k = φ'.f k
⊢ φ = φ'

Tactic:
ext k
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
k : ι
pos : ∀ (h : k = i₀ ∨ k = i₁), φ.f k = φ'.f k
neg : ∀ (h : ¬(k = i₀ ∨ k = i₁)), φ.f k = φ'.f k
⊢ φ.f k = φ'.f k

Tactic:
by_cases h : k = i₀ ∨ k = i₁
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
k : ι
h : k = i₀ ∨ k = i₁
pos : ∀ {hi₀₁ : c.Rel k i₁} {φ φ' : double f hi₀₁ ⟶ K} (h₀ : φ.f k = φ'.f k) (h₁ : φ.f i₁ = φ'.f i₁), φ.f k = φ'.f k
pos₁ : ∀ {hi₀₁ : c.Rel i₀ k} {φ φ' : double f hi₀₁ ⟶ K} (h₀ : φ.f i₀ = φ'.f i₀) (h₁ : φ.f k = φ'.f k), φ.f k = φ'.f k
⊢ φ.f k = φ'.f k

Tactic:
obtain rfl | rfl := h

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₁ : ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
k : ι
hi₀₁ : c.Rel k i₁
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f k = φ'.f k
h₁ : φ.f i₁ = φ'.f i₁
⊢ φ.f k = φ'.f k

Tactic:
assumption
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ : ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
k : ι
hi₀₁ : c.Rel i₀ k
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f k = φ'.f k
⊢ φ.f k = φ'.f k

Tactic:
assumption
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
k : ι
h : ¬(k = i₀ ∨ k = i₁)
⊢ ¬k = i₀ ∧ ¬k = i₁

Tactic:
simp only [not_or] at h

Premises used: not_or
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
k : ι
h : ¬k = i₀ ∧ ¬k = i₁
⊢ φ.f k = φ'.f k

Tactic:
apply (isZero_double_X f hi₀₁ k h.1 h.2).eq_of_src

Premises used: HomologicalComplex.isZero_double_X, And.right, And.left, CategoryTheory.Limits.IsZero.eq_of_src
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ φ' : K ⟶ double f hi₀₁
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
h : ∀ (k : ι), φ.f k = φ'.f k
⊢ φ = φ'

Tactic:
ext k
-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ φ' : K ⟶ double f hi₀₁
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
k : ι
pos : ∀ (h : k = i₀ ∨ k = i₁), φ.f k = φ'.f k
neg : ∀ (h : ¬(k = i₀ ∨ k = i₁)), φ.f k = φ'.f k
⊢ φ.f k = φ'.f k

Tactic:
by_cases h : k = i₀ ∨ k = i₁