awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι
h : k = i₀ ∨ k = i₁
pos : ∀ {hi₀₁ : c.Rel k i₁} {φ φ' : K ⟶ double f hi₀₁} (h₀ : φ.f k = φ'.f k) (h₁ : φ.f i₁ = φ'.f i₁), φ.f k = φ'.f k
pos₁ : ∀ {hi₀₁ : c.Rel i₀ k} {φ φ' : K ⟶ double f hi₀₁} (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₁
φ φ' : K ⟶ double f hi₀₁
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
φ φ' : K ⟶ double f hi₀₁
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
φ φ' : K ⟶ double f hi₀₁
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
φ φ' : K ⟶ double f hi₀₁
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_tgt

Premises used: HomologicalComplex.isZero_double_X, And.right, And.left, CategoryTheory.Limits.IsZero.eq_of_tgt
-- 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₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : k = i₀
rw rw₁ : X (double f hi₀₁) i₀ = X (double f hi₀₁) i₀
⊢ X (double f hi₀₁) k = X (double f hi₀₁) i₀

Tactic:
rw [hk₀]
-- 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₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : k = i₀
rw rw₁ : K.X i₀ = K.X i₀
⊢ K.X i₀ = K.X k

Tactic:
rw [hk₀]
-- 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₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : ¬k = i₀
hk₁ : k = i₁
rw rw₁ : X (double f hi₀₁) i₁ = X (double f hi₀₁) i₁
⊢ X (double f hi₀₁) k = X (double f hi₀₁) i₁

Tactic:
rw [hk₁]
-- 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₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k : ι
hk₀ : ¬k = i₀
hk₁ : k = i₁
rw rw₁ : K.X i₁ = K.X i₁
⊢ K.X i₁ = K.X k

Tactic:
rw [hk₁]
-- 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₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
pos :
  ∀ (h₀ : k₀ = i₀),
    Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
      ((if hk₀ : k₀ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
        else if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫
        K.d k₀ k₁)
      (d (double f hi₀₁) k₀ k₁ ≫
        if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
        else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
neg :
  ∀ (h₀ : ¬k₀ = i₀),
    Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
      ((if hk₀ : k₀ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
        else if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫
        K.d k₀ k₁)
      (d (double f hi₀₁) k₀ k₁ ≫
        if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
        else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
⊢ Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
    ((if hk₀ : k₀ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫
      K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)

Tactic:
by_cases h₀ : 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₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : k₀ = i₀
pos :
  ∀ (hi₀₁ : c.Rel k₀ i₁) (h : k₀ ≠ i₁) (φ₀ : X₀ ⟶ K.X k₀) (comm : φ₀ ≫ K.d k₀ i₁ = f ≫ φ₁),
    Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
      ((if hk₀ : k₀ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
        else if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫
        K.d k₀ k₁)
      (d (double f hi₀₁) k₀ k₁ ≫
        if hk₀ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
        else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
⊢ Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
    ((if hk₀ : k₀ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫
      K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)

Tactic:
subst h₀
-- 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
φ₁ : X₁ ⟶ K.X i₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
hi₀₁ : c.Rel k₀ i₁
h : k₀ ≠ i₁
φ₀ : X₀ ⟶ K.X k₀
comm : φ₀ ≫ K.d k₀ i₁ = f ≫ φ₁
pos :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) ((eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
⊢ Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
    ((if hk₀ : k₀ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫
      K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)

Tactic:
rw [dif_pos rfl]

Premises used: dif_pos, 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
φ₁ : X₁ ⟶ K.X i₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
hi₀₁ : c.Rel k₀ i₁
h : k₀ ≠ i₁
φ₀ : X₀ ⟶ K.X k₀
comm : φ₀ ≫ K.d k₀ i₁ = f ≫ φ₁
pos :
  ∀ (φ₁ : X₁ ⟶ K.X k₁) (hφ : ∀ (k : ι), c.Rel k₁ k → φ₁ ≫ K.d k₁ k = 0) (hi₀₁ : c.Rel k₀ k₁) (h : k₀ ≠ k₁)
    (comm : φ₀ ≫ K.d k₀ k₁ = f ≫ φ₁),
    Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) ((eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯) ≫ K.d k₀ k₁)
      (d (double f hi₀₁) k₀ k₁ ≫
        if hk₀ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
        else if hk₁ : k₁ = k₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
⊢ Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) ((eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)

Tactic:
obtain rfl := c.next_eq hk hi₀₁

Premises used: ComplexShape.next_eq, 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 ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
k₀ k₁ : ι
hk : c.Rel k₀ k₁
φ₀ : X₀ ⟶ K.X k₀
φ₁ : X₁ ⟶ K.X k₁
hφ : ∀ (k : ι), c.Rel k₁ k → φ₁ ≫ K.d k₁ k = 0
hi₀₁ : c.Rel k₀ k₁
h : k₀ ≠ k₁
comm : φ₀ ≫ K.d k₀ k₁ = f ≫ φ₁
⊢ Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) ((eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)

Tactic:
simp [dif_neg h.symm, double_d f hi₀₁ h, comm]

Premises used: Ne.symm, dif_neg, HomologicalComplex.double_d
-- 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₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
neg :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
    ((if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
⊢ Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
    ((if hk₀ : k₀ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫
      K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)

Tactic:
rw [dif_neg h₀]

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₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
pos :
  ∀ (h₁ : k₀ = i₁),
    Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
      ((if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁)
      (d (double f hi₀₁) k₀ k₁ ≫
        if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
        else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
neg :
  ∀ (h₁ : ¬k₀ = i₁),
    Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
      ((if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁)
      (d (double f hi₀₁) k₀ k₁ ≫
        if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
        else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
⊢ Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
    ((if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)

Tactic:
by_cases h₁ : 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₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
h₁ : k₀ = i₁
pos :
  ∀ (hi₀₁ : c.Rel i₀ k₀) (h : i₀ ≠ k₀) (φ₁ : X₁ ⟶ K.X k₀) (comm : φ₀ ≫ K.d i₀ k₀ = f ≫ φ₁)
    (hφ : ∀ (k : ι), c.Rel k₀ k → φ₁ ≫ K.d k₀ k = 0),
    Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
      ((if hk₁ : k₀ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁)
      (d (double f hi₀₁) k₀ k₁ ≫
        if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
        else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
⊢ Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
    ((if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)

Tactic:
subst h₁
-- 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
φ₀ : X₀ ⟶ K.X i₀
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
hi₀₁ : c.Rel i₀ k₀
h : i₀ ≠ k₀
φ₁ : X₁ ⟶ K.X k₀
comm : φ₀ ≫ K.d i₀ k₀ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel k₀ k → φ₁ ≫ K.d k₀ k = 0
pos :
  (if k₀ = k₀ then 𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X k₀) else 0) ≫ K.d k₀ k₁ =
    d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0
⊢ Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
    ((if hk₁ : k₀ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 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₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
h₁ : ¬k₀ = i₁
⊢ Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
    ((if hk₁ : k₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)

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

Premises used: HomologicalComplex.isZero_double_X, 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₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
dsimp :
  (if i₀ = i₀ then 𝟙 (X (double f hi₀₁) i₀) ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ 𝟙 (K.X i₀)
    else if hk₁ : i₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) =
    Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀
⊢ Eq (α := X (double f hi₀₁) i₀ ⟶ K.X i₀) (Hom.f (mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ) i₀)
    (Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀)

Tactic:
dsimp [mkHomFromDouble]

Premises used: HomologicalComplex.mkHomFromDouble
-- 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₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
rw : 𝟙 (X (double f hi₀₁) i₀) ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ 𝟙 (K.X i₀) = Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀
rw₁ :
  Eq (α := X (double f hi₀₁) i₀ ⟶ K.X i₀) (Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ 𝟙 (K.X i₀))
    (Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀)
rw₂ rw₃ :
  Eq (α := X (double f hi₀₁) i₀ ⟶ K.X i₀) (Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀) (Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀)
⊢ (if i₀ = i₀ then 𝟙 (X (double f hi₀₁) i₀) ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ 𝟙 (K.X i₀)
    else if hk₁ : i₀ = i₁ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0) =
    Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀

Tactic:
rw [if_pos rfl, id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, if_pos, rfl, CategoryTheory.Category.id_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₁
h : i₀ ≠ i₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
dsimp :
  Eq (α := X (double f hi₀₁) i₁ ⟶ K.X i₁)
    (if hk₀ : i₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
    else if i₁ = i₁ then 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0)
    (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁)
⊢ Eq (α := X (double f hi₀₁) i₁ ⟶ K.X i₁) (Hom.f (mkHomFromDouble hi₀₁ h φ₀ φ₁ comm hφ) i₁)
    (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁)

Tactic:
dsimp [mkHomFromDouble]

Premises used: HomologicalComplex.mkHomFromDouble
-- 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₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
rw :
  (if i₁ = i₁ then 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0) =
    Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁
rw₁ : 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) = Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁
rw₂ :
  Eq (α := X (double f hi₀₁) i₁ ⟶ K.X i₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁))
    (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁)
rw₃ rw₄ :
  Eq (α := X (double f hi₀₁) i₁ ⟶ K.X i₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁)
⊢ Eq (α := X (double f hi₀₁) i₁ ⟶ K.X i₁)
    (if hk₀ : i₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
    else if i₁ = i₁ then 𝟙 (X (double f hi₀₁) i₁) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X i₁) else 0)
    (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁)

Tactic:
rw [dif_neg h.symm, if_pos rfl, id_comp, comp_id]

Premises used: Ne.symm, CategoryTheory.Category.comp_id, if_pos, dif_neg, rfl, CategoryTheory.Category.id_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₁
h : i₀ ≠ i₁
X : C
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) K
⊢ φ₀ ≫ K.d i₀ i₁ = 𝟙 X ≫ φ₀ ≫ K.d i₀ i₁

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₁
h : i₀ ≠ i₁
X : C
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : Functor.obj (eval C c i₀ ⋙ Functor.obj coyoneda (op X)) K
⊢ ∀ (k : ι), c.Rel i₁ k → (φ₀ ≫ K.d i₀ i₁) ≫ K.d i₁ k = 0

Tactic:
simp