awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
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 ≫ φ₁
⊢ 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)
have pos : Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) ((eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry) ≫ K.d k₀ k₁)
  (d (double f hi₀₁) k₀ k₁ ≫
    if hk₀ : k₁ = k₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
    else if hk₁ : k₁ = i₁ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0)
Tactic: rw [dif_pos rfl]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
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 ≫ φ₁
⊢ 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)
have 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 sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = k₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
      else if hk₁ : k₁ = k₁ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0)
Tactic: obtain rfl := c.next_eq hk hi₀₁
Cleared hypotheses: i₁, φ₁, hφ, hi₀₁, h, comm
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
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₀
⊢ 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)
have neg : Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
  ((if hk₁ : k₀ = i₁ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0) ≫ K.d k₀ k₁)
  (d (double f hi₀₁) k₀ k₁ ≫
    if hk₀ : k₁ = i₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
    else if hk₁ : k₁ = i₁ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0)
Tactic: rw [dif_neg h₀]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
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₀
⊢ 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)
have pos : ∀ (h₁ : k₀ = i₁),
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
    ((if hk₁ : k₀ = i₁ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
      else if hk₁ : k₁ = i₁ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0)
Tactic: by_cases h₁ : k₀ = i₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
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)
⊢ 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)
have neg : ∀ (h₁ : ¬k₀ = i₁),
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁)
    ((if hk₁ : k₀ = i₁ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
      else if hk₁ : k₁ = i₁ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0)
Tactic: by_cases h₁ : k₀ = i₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
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)
have 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 sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
      else if hk₁ : k₁ = k₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0)
Tactic: subst h₁
Cleared hypotheses: i₁, hi₀₁, h, φ₁, comm, hφ, h₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
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
⊢ 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)
have 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 sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
    else if hk₁ : k₁ = k₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
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
⊢ (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
have pos : (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X k₀)) ≫ K.d k₀ k₁ =
  d (double f hi₀₁) k₀ k₁ ≫
    if hk₀ : k₁ = i₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
    else if hk₁ : k₁ = k₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0
Tactic: rw [if_pos rfl, comp_id, id_comp, assoc, hφ k₁ hk, comp_zero,
          double_d_eq_zero₀ _ _ _ _ h.symm, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
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 :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X k₀)) ≫ 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
⊢ (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
have pos₁ : (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ K.d k₀ k₁ =
  d (double f hi₀₁) k₀ k₁ ≫
    if hk₀ : k₁ = i₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
    else if hk₁ : k₁ = k₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0
Tactic: rw [if_pos rfl, comp_id, id_comp, assoc, hφ k₁ hk, comp_zero,
          double_d_eq_zero₀ _ _ _ _ h.symm, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
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 :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X k₀)) ≫ 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
pos₁ :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ 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
⊢ (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
have pos₂ : Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) ((Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ K.d k₀ k₁)
  (d (double f hi₀₁) k₀ k₁ ≫
    if hk₀ : k₁ = i₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
    else if hk₁ : k₁ = k₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0)
Tactic: rw [if_pos rfl, comp_id, id_comp, assoc, hφ k₁ hk, comp_zero,
          double_d_eq_zero₀ _ _ _ _ h.symm, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
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 :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X k₀)) ≫ 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
pos₁ :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ 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
pos₂ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) ((Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ 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)
⊢ (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
have pos₃ : Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ K.d k₀ k₁)
  (d (double f hi₀₁) k₀ k₁ ≫
    if hk₀ : k₁ = i₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
    else if hk₁ : k₁ = k₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0)
Tactic: rw [if_pos rfl, comp_id, id_comp, assoc, hφ k₁ hk, comp_zero,
          double_d_eq_zero₀ _ _ _ _ h.symm, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
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 :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X k₀)) ≫ 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
pos₁ :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ 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
pos₂ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) ((Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ 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)
pos₃ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 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)
⊢ (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
have pos₄ : Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ 0)
  (d (double f hi₀₁) k₀ k₁ ≫
    if hk₀ : k₁ = i₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
    else if hk₁ : k₁ = k₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0)
Tactic: rw [if_pos rfl, comp_id, id_comp, assoc, hφ k₁ hk, comp_zero,
          double_d_eq_zero₀ _ _ _ _ h.symm, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (goal)
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 :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X k₀)) ≫ 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
pos₁ :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ 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
pos₂ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) ((Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ 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)
pos₃ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 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)
pos₄ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ 0)
    (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)
⊢ (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
have pos₅ : Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) 0
  (d (double f hi₀₁) k₀ k₁ ≫
    if hk₀ : k₁ = i₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom sorry
    else if hk₁ : k₁ = k₀ then eqToHom sorry ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom sorry else 0)
Tactic: rw [if_pos rfl, comp_id, id_comp, assoc, hφ k₁ hk, comp_zero,
          double_d_eq_zero₀ _ _ _ _ h.symm, zero_comp]