awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
hX : ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
⊢ (Functor.objPreimage Q X).IsGE n
have rw : ∀ i < n, HomologicalComplex.ExactAt (Functor.objPreimage Q X) i
Tactic: rw [CochainComplex.isGE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
hX : ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
i : ℤ
hi : i < n
⊢ HomologicalComplex.ExactAt (Functor.objPreimage Q X) i
have rw : IsZero.{v, u} (HomologicalComplex.homology (Functor.objPreimage Q X) i)
Tactic: rw [HomologicalComplex.exactAt_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
hX : ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
i : ℤ
hi : i < n
⊢ IsZero.{v, u} (HomologicalComplex.homology (Functor.objPreimage Q X) i)
have apply : HomologicalComplex.homology (Functor.objPreimage Q X) i ≅ Functor.obj (homologyFunctor C i) X
Tactic: apply (hX i hi).of_iso
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
hX : ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
⊢ X.IsGE n
have this : (Functor.objPreimage Q X).IsGE n
Tactic: have : (Q.objPreimage X).IsGE n := by
      rw [CochainComplex.isGE_iff]
      intro i hi
      rw [HomologicalComplex.exactAt_iff_isZero_homology]
      apply (hX i hi).of_iso
      exact (homologyFunctorFactors C i).symm.app _ ≪≫
        (homologyFunctor C i).mapIso (Q.objObjPreimageIso X)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
⊢ X.IsLE n ↔ ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
have mp : X.IsLE n → ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
mp : X.IsLE n → ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
⊢ X.IsLE n ↔ ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
have mpr : (∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)) → X.IsLE n
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
K : CochainComplex.{v, u, 0} C ℤ
e : X ≅ Functor.obj Q K
h : K.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
have mp : Functor.obj (homologyFunctor C i) X ≅ HomologicalComplex.homology K i
Tactic: apply ((K.exactAt_of_isLE n i hi).isZero_homology).of_iso
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
hX : ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
⊢ (Functor.objPreimage Q X).IsLE n
have rw : ∀ (i : ℤ), n < i → HomologicalComplex.ExactAt (Functor.objPreimage Q X) i
Tactic: rw [CochainComplex.isLE_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
hX : ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
i : ℤ
hi : n < i
⊢ HomologicalComplex.ExactAt (Functor.objPreimage Q X) i
have rw : IsZero.{v, u} (HomologicalComplex.homology (Functor.objPreimage Q X) i)
Tactic: rw [HomologicalComplex.exactAt_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
hX : ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
i : ℤ
hi : n < i
⊢ IsZero.{v, u} (HomologicalComplex.homology (Functor.objPreimage Q X) i)
have apply : HomologicalComplex.homology (Functor.objPreimage Q X) i ≅ Functor.obj (homologyFunctor C i) X
Tactic: apply (hX i hi).of_iso
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
hX : ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
⊢ X.IsLE n
have this : (Functor.objPreimage Q X).IsLE n
Tactic: have : (Q.objPreimage X).IsLE n := by
      rw [CochainComplex.isLE_iff]
      intro i hi
      rw [HomologicalComplex.exactAt_iff_isZero_homology]
      apply (hX i hi).of_iso
      exact (homologyFunctorFactors C i).symm.app _ ≪≫
        (homologyFunctor C i).mapIso (Q.objObjPreimageIso X)
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n i : ℤ
hi : i < n
hX : X.IsGE n
⊢ IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
have hX₁ : ∀ i < n, IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
Tactic: rw [isGE_iff] at hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n i : ℤ
hi : n < i
hX : X.IsLE n
⊢ IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
have hX₁ : ∀ (i : ℤ), n < i → IsZero.{v, u} (Functor.obj (homologyFunctor C i) X)
Tactic: rw [isLE_iff] at hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ IsGE.{w, v, u} (Functor.obj Q K) n ↔ K.IsGE n
have eq : ∀ (i : ℤ),
  IsZero.{v, u} (Functor.obj (Functor.comp (D := DerivedCategory.{w, v, u} C) Q (homologyFunctor C i)) K) ↔
    IsZero.{v, u} (Functor.obj (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) i) K)
Tactic: have eq := fun i ↦ ((homologyFunctorFactors C i).app K).isZero_iff
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ IsLE.{w, v, u} (Functor.obj Q K) n ↔ K.IsLE n
have eq : ∀ (i : ℤ),
  IsZero.{v, u} (Functor.obj (Functor.comp (D := DerivedCategory.{w, v, u} C) Q (homologyFunctor C i)) K) ↔
    IsZero.{v, u} (Functor.obj (HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) i) K)
Tactic: have eq := fun i ↦ ((homologyFunctorFactors C i).app K).isZero_iff
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
hX : X.IsLE n
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyLE n), Nonempty.{w + 1} (X ≅ Functor.obj Q K)
have obtain : ∀ (K : CochainComplex.{v, u, 0} C ℤ) (e : X ≅ Functor.obj Q K),
  K.IsStrictlyLE n → ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyLE n), Nonempty.{w + 1} (X ≅ Functor.obj Q K)
Tactic: obtain ⟨K, e, _⟩ := hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
hX : X.IsGE n
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyGE n), Nonempty.{w + 1} (X ≅ Functor.obj Q K)
have obtain : ∀ (K : CochainComplex.{v, u, 0} C ℤ) (e : X ≅ Functor.obj Q K),
  K.IsStrictlyGE n → ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyGE n), Nonempty.{w + 1} (X ≅ Functor.obj Q K)
Tactic: obtain ⟨K, e, _⟩ := hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
a b : ℤ
inst_3 : X.IsGE a
inst_4 : X.IsLE b
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyGE a) (_ : K.IsStrictlyLE b),
    Nonempty.{w + 1} (X ≅ Functor.obj Q K)
have obtain : ∀ (K : CochainComplex.{v, u, 0} C ℤ) (hK : K.IsStrictlyLE b) (e : X ≅ Functor.obj Q K),
  ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyGE a) (_ : K.IsStrictlyLE b),
    Nonempty.{w + 1} (X ≅ Functor.obj Q K)
Tactic: obtain ⟨K, hK, ⟨e⟩⟩ := X.exists_iso_Q_obj_of_isLE b
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
a b : ℤ
inst_3 : X.IsGE a
inst_4 : X.IsLE b
K : CochainComplex.{v, u, 0} C ℤ
hK : K.IsStrictlyLE b
e : X ≅ Functor.obj Q K
⊢ K.IsGE a
have rw : IsGE.{w, v, u} (Functor.obj Q K) a
Tactic: rw [← isGE_Q_obj_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
a b : ℤ
inst_3 : X.IsGE a
inst_4 : X.IsLE b
K : CochainComplex.{v, u, 0} C ℤ
hK : K.IsStrictlyLE b
e : X ≅ Functor.obj Q K
⊢ ∃ (K : CochainComplex.{v, u, 0} C ℤ) (_ : K.IsStrictlyGE a) (_ : K.IsStrictlyLE b),
    Nonempty.{w + 1} (X ≅ Functor.obj Q K)
have this : K.IsGE a
Tactic: have : K.IsGE a := by
    rw [← isGE_Q_obj_iff]
    exact TStructure.t.isGE_of_iso e a
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
inst_3 : X.IsGE n
inst_4 : X.IsLE n
⊢ ∃ (Y : C), Nonempty.{w + 1} (X ≅ Functor.obj (singleFunctor C n) Y)
have obtain : ∀ (K : CochainComplex.{v, u, 0} C ℤ),
  K.IsStrictlyGE n →
    K.IsStrictlyLE n → ∀ (e : X ≅ Functor.obj Q K), ∃ (Y : C), Nonempty.{w + 1} (X ≅ Functor.obj (singleFunctor C n) Y)
Tactic: obtain ⟨K, _, _, ⟨e⟩⟩ := exists_iso_Q_obj_of_isGE_of_isLE X n n
-- Lean 4 proof step from Mathlib.Algebra.Homology.DerivedCategory.TStructure (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasDerivedCategory.{w, v, u} C
X : DerivedCategory.{w, v, u} C
n : ℤ
inst_3 : X.IsGE n
inst_4 : X.IsLE n
K : CochainComplex.{v, u, 0} C ℤ
w : K.IsStrictlyGE n
w_1 : K.IsStrictlyLE n
e : X ≅ Functor.obj Q K
⊢ ∃ (Y : C), Nonempty.{w + 1} (X ≅ Functor.obj (singleFunctor C n) Y)
have obtain : ∀ (Y : C) (e' : K ≅ Functor.obj (HomologicalComplex.single C (ComplexShape.up ℤ) n) Y),
  ∃ (Y : C), Nonempty.{w + 1} (X ≅ Functor.obj (singleFunctor C n) Y)
Tactic: obtain ⟨Y, ⟨e'⟩⟩ := CochainComplex.exists_iso_single K n
-- Lean 4 proof step from Mathlib.Algebra.Homology.DifferentialObject (goal)
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
⊢ Eq.{u_1 + 1} (α := β) ((fun (b_1 : β) ↦ b_1 + HSMul.hSMul (α := ℤ) (Discrete.as { as := 1 : Discrete ℤ }) b) x)
    ((fun (b_1 : β) ↦ b_1 + HSMul.hSMul (α := ℤ) (Discrete.as { as := 1 : Discrete ℤ }) b) y)
have refl : Eq.{u_1 + 1} (α := β) ((fun (b_1 : β) ↦ b_1 + HSMul.hSMul (α := ℤ) (Discrete.as { as := 1 : Discrete ℤ }) b) x)
  ((fun (b_1 : β) ↦ b_1 + HSMul.hSMul (α := ℤ) (Discrete.as { as := 1 : Discrete ℤ }) b) x)
Tactic: cases h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.DifferentialObject (goal)
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
⊢ X.objEqToHom h ≫ X.d y = X.d x ≫ X.objEqToHom ⋯
have refl : X.objEqToHom sorry ≫ X.d x = X.d x ≫ X.objEqToHom sorry
Tactic: cases h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.DifferentialObject (goal)
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
⊢ X.objEqToHom h ≫ f.f y = f.f x ≫ Y.objEqToHom h
have refl : X.objEqToHom sorry ≫ f.f x = f.f x ≫ Y.objEqToHom sorry
Tactic: cases h
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.DifferentialObject (goal)
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
⊢ X.d x y ≫ eqToHom ⋯ = X.d x z
have refl : X.d x y ≫ eqToHom sorry = X.d x y
Tactic: cases h
Cleared hypotheses: z, 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 k' : ι
hk : k = i₀ ∧ k' = i₁ ∧ i₀ ≠ i₁
⊢ X₁ = if k' = i₀ then X₀ else if k' = i₁ then X₁ else 0
have hnc : ¬k' = i₀
Tactic: rw [if_neg, if_pos hk.2.1]
-- 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
⊢ 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 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 sorry ≫ f ≫ eqToHom sorry else 0)
    (if hk : j = i₀ ∧ k = i₁ ∧ ¬i₀ = i₁ then eqToHom sorry ≫ f ≫ eqToHom sorry else 0))
  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₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ 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 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 sorry ≫ f ≫ eqToHom sorry else 0)
      (if hk : j = i₀ ∧ k = i₁ ∧ ¬i₀ = i₁ then eqToHom sorry ≫ f ≫ eqToHom sorry else 0))
    0
Tactic: by_cases hi : i = 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₁
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
⊢ 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 : ∀ (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 sorry ≫ f ≫ eqToHom sorry else 0)
      (if hk : j = i₀ ∧ k = i₁ ∧ ¬i₀ = i₁ then eqToHom sorry ≫ f ≫ eqToHom sorry else 0))
    0
Tactic: by_cases hi : i = 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₁
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 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 sorry ≫ f ≫ eqToHom sorry else 0)
      (if hk : j = i ∧ k = i₁ ∧ ¬i = i₁ then eqToHom sorry ≫ f ≫ eqToHom sorry else 0))
    0
Tactic: subst hi
Cleared hypotheses: i₀, hi₀₁, hi
-- 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₁
⊢ 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 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 sorry ≫ f ≫ eqToHom sorry else 0)
      (if hk : j = i ∧ k = i₁ ∧ ¬i = i₁ then eqToHom sorry ≫ f ≫ eqToHom sorry else 0))
    0
Tactic: by_cases hj : j = 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 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
⊢ 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 : ∀ (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 sorry ≫ f ≫ eqToHom sorry else 0)
      (if hk : j = i ∧ k = i₁ ∧ ¬i = i₁ then eqToHom sorry ≫ f ≫ eqToHom sorry else 0))
    0
Tactic: by_cases hj : j = 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 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 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 sorry ≫ f ≫ eqToHom sorry else 0)
      (if hk : j = i ∧ k = j ∧ ¬i = j then eqToHom sorry ≫ f ≫ eqToHom sorry else 0))
    0
Tactic: subst hj
Cleared hypotheses: i₁, hi₀₁, hj
-- 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
⊢ ¬(j = i ∧ k = j ∧ ¬i = j)
have tauto : j = i → k = j → ¬i = j → False
Tactic: tauto