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 j k : ι
hij : c.Rel i j
hjk : c.Rel j k
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
have 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 sorry ≫ f ≫ eqToHom sorry else 0) 0)
  0
Tactic: nth_rw 2 [dif_neg (by tauto)]
-- 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 j k : ι
hij : c.Rel i j
hjk : c.Rel j k
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) 0)
    0
have 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
Tactic: rw [comp_zero]
-- 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 j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi₀₁ : c.Rel i i₁
hj : ¬j = i₁
⊢ ¬(i = i ∧ j = i₁ ∧ ¬i = i₁)
have tauto : i = i → j = i₁ → ¬i = i₁ → False
Tactic: tauto
-- 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 j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi₀₁ : c.Rel i i₁
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
have 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 sorry ≫ f ≫ eqToHom sorry else 0))
  0
Tactic: rw [dif_neg (by tauto), 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₁ 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
⊢ 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
have 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
Tactic: rw [dif_neg (by tauto), 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₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
hi : ¬i = i₀
⊢ ¬(i = i₀ ∧ j = i₁ ∧ ¬i₀ = i₁)
have tauto : i = i₀ → j = i₁ → ¬i₀ = i₁ → False
Tactic: tauto
-- 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₁
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
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
have 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 sorry ≫ f ≫ eqToHom sorry else 0))
  0
Tactic: rw [dif_neg (by tauto), 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₀ 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
⊢ 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
have 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
Tactic: rw [dif_neg (by tauto), 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₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
⊢ IsZero.{v_1, u_1} (X (double f hi₀₁) k)
have dsimp : IsZero.{v_1, u_1} (if k = i₀ then X₀ else if k = i₁ then X₁ else 0)
Tactic: dsimp [double]
-- 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₁
k : ι
h₀ : k ≠ i₀
h₁ : k ≠ i₁
⊢ IsZero.{v_1, u_1} (if k = i₀ then X₀ else if k = i₁ then X₁ else 0)
have rw : IsZero.{v_1, u_1} (C := C) 0
Tactic: rw [if_neg h₀, if_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₁
⊢ X (double f hi₀₁) i₁ = X₁
have dsimp : (if i₁ = i₀ then X₀ else if i₁ = i₁ then X₁ else 0) = X₁
Tactic: dsimp [double]
-- 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₁
⊢ (if i₁ = i₀ then X₀ else if i₁ = i₁ then X₁ else 0) = X₁
have rw : (if i₁ = i₁ then X₁ else 0) = X₁
Tactic: rw [if_neg h.symm, if_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₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
rw : (if i₁ = i₁ then X₁ else 0) = X₁
⊢ (if i₁ = i₀ then X₀ else if i₁ = i₁ then X₁ else 0) = X₁
have rw₁ : X₁ = X₁
Tactic: rw [if_neg h.symm, if_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₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
a b : ι
ha : a ≠ i₀
⊢ ¬(a = i₀ ∧ b = i₁ ∧ i₀ ≠ i₁)
have tauto : a = i₀ → b = i₁ → i₀ ≠ i₁ → False
Tactic: tauto
-- 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₁
a b : ι
hb : b ≠ i₁
⊢ ¬(a = i₀ ∧ b = i₁ ∧ i₀ ≠ i₁)
have tauto : a = i₀ → b = i₁ → i₀ ≠ i₁ → False
Tactic: tauto
-- 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₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ φ' : double f hi₀₁ ⟶ K
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
⊢ φ = φ'
have h : ∀ (k : ι), φ.f k = φ'.f k
Tactic: ext k
-- 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₁
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 : ι
⊢ φ.f k = φ'.f k
have pos : ∀ (h : k = i₀ ∨ k = i₁), φ.f k = φ'.f k
Tactic: by_cases h : k = i₀ ∨ 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₁
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
⊢ φ.f k = φ'.f k
have neg : ∀ (h : ¬(k = i₀ ∨ k = i₁)), φ.f k = φ'.f k
Tactic: by_cases h : k = i₀ ∨ 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₁
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
have pos : ∀ {hi₀₁ : c.Rel k i₁} {φ φ' : double f hi₀₁ ⟶ K} (h₀ : φ.f k = φ'.f k) (h₁ : φ.f i₁ = φ'.f i₁), φ.f k = φ'.f k
Tactic: obtain rfl | rfl := h
Cleared hypotheses: i₀, hi₀₁, φ, φ', h₀, 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₀ 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
⊢ φ.f k = φ'.f k
have pos₁ : ∀ {hi₀₁ : c.Rel i₀ k} {φ φ' : double f hi₀₁ ⟶ K} (h₀ : φ.f i₀ = φ'.f i₀) (h₁ : φ.f k = φ'.f k), φ.f k = φ'.f k
Tactic: obtain rfl | rfl := h
Cleared hypotheses: i₁, hi₀₁, φ, φ', h₀, h₁, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (hypothesis)
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
have h₂ : ¬k = i₀ ∧ ¬k = i₁
Tactic: simp only [not_or] at h
Cleared hypotheses: 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₁
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ φ' : K ⟶ double f hi₀₁
h₀ : φ.f i₀ = φ'.f i₀
h₁ : φ.f i₁ = φ'.f i₁
⊢ φ = φ'
have h : ∀ (k : ι), φ.f k = φ'.f k
Tactic: ext k
-- 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₁
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 : ι
⊢ φ.f k = φ'.f k
have pos : ∀ (h : k = i₀ ∨ k = i₁), φ.f k = φ'.f k
Tactic: by_cases h : k = i₀ ∨ 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₁
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
⊢ φ.f k = φ'.f k
have neg : ∀ (h : ¬(k = i₀ ∨ k = i₁)), φ.f k = φ'.f k
Tactic: by_cases h : k = i₀ ∨ 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₁
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
have pos : ∀ {hi₀₁ : c.Rel k i₁} {φ φ' : K ⟶ double f hi₀₁} (h₀ : φ.f k = φ'.f k) (h₁ : φ.f i₁ = φ'.f i₁), φ.f k = φ'.f k
Tactic: obtain rfl | rfl := h
Cleared hypotheses: i₀, hi₀₁, φ, φ', h₀, 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₀ 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
⊢ φ.f k = φ'.f k
have pos₁ : ∀ {hi₀₁ : c.Rel i₀ k} {φ φ' : K ⟶ double f hi₀₁} (h₀ : φ.f i₀ = φ'.f i₀) (h₁ : φ.f k = φ'.f k), φ.f k = φ'.f k
Tactic: obtain rfl | rfl := h
Cleared hypotheses: i₁, hi₀₁, φ, φ', h₀, h₁, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Double (hypothesis)
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
have h₂ : ¬k = i₀ ∧ ¬k = i₁
Tactic: simp only [not_or] at h
Cleared hypotheses: 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 : ι
hk₀ : k = i₀
⊢ X (double f hi₀₁) k = X (double f hi₀₁) i₀
have rw : X (double f hi₀₁) i₀ = X (double f hi₀₁) i₀
Tactic: rw [hk₀]
-- 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 : ι
hk₀ : k = i₀
⊢ K.X i₀ = K.X k
have rw : K.X i₀ = K.X i₀
Tactic: rw [hk₀]
-- 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 : ι
hk₀ : ¬k = i₀
hk₁ : k = i₁
⊢ X (double f hi₀₁) k = X (double f hi₀₁) i₁
have rw : X (double f hi₀₁) i₁ = X (double f hi₀₁) i₁
Tactic: rw [hk₁]
-- 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 : ι
hk₀ : ¬k = i₀
hk₁ : k = i₁
⊢ K.X i₁ = K.X k
have rw : K.X i₁ = K.X i₁
Tactic: rw [hk₁]
-- 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₁
⊢ 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 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₀₁) ≫ φ₀ ≫ eqToHom sorry
      else 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₁
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)
⊢ 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 : ∀ (h₀ : ¬k₀ = i₀),
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X 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) ≫
      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₀
⊢ 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 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 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) ≫
      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: subst h₀
Cleared hypotheses: i₀, hi₀₁, h, φ₀, comm, h₀