awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.GrothendieckAbelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type t
c : ComplexShape ι
inst_1 : Abelian.{v, u} C
inst_2 : IsGrothendieckAbelian.{w, v, u} C
inst_3 : c.HasNoLoop
inst_4 : Small.{w, t} ι
⊢ HasSeparator (HomologicalComplex.{v, u, t} C c)
have this : HasCoproductsOfShape.{t, u, v} ι C
Tactic: have : HasCoproductsOfShape ι C :=
      hasColimitsOfShape_of_equivalence (Discrete.equivalence (equivShrink.{w} ι)).symm
-- Lean 4 proof step from Mathlib.Algebra.Homology.HasNoLoop (goal)
Goal:
ι : Type u_1
c : ComplexShape ι
inst : c.HasNoLoop
j j' : ι
h : j = j'
⊢ ¬c.Rel j j'
have subst : ¬c.Rel j j
Tactic: subst h
Cleared hypotheses: j', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HasNoLoop (goal)
Goal:
α : Type u_2
inst : AddZeroClass α
inst_1 : IsRightCancelAdd α
inst_2 : IsLeftCancelAdd α
a : α
ha : a ≠ 0
i : α
hi rw : i + a = i
⊢ i + a = i + 0
have rw₁ : i = i
Tactic: rw [add_zero, hi]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HasNoLoop (hypothesis)
Goal:
α : Type u_2
inst : AddZeroClass α
inst_1 : IsRightCancelAdd α
inst_2 : IsLeftCancelAdd α
a : α
ha : a ≠ 0
⊢ (down' a).HasNoLoop
have this : (up' a).HasNoLoop
Tactic: have := hasNoLoop_up' a ha
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalBicomplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
x x_1 : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
φ₁ φ₂ : x ⟶ x_1
h :
  Eq (α := Functor.obj (toGradedObjectFunctor C c₁ c₂) x ⟶ Functor.obj (toGradedObjectFunctor C c₁ c₂) x_1)
    (CategoryTheory.Functor.map (toGradedObjectFunctor C c₁ c₂) φ₁)
    (CategoryTheory.Functor.map (toGradedObjectFunctor C c₁ c₂) φ₂)
⊢ φ₁ = φ₂
have h₁ : ∀ (i₁ : I₁) (i₂ : I₂), (φ₁.f i₁).f i₂ = (φ₂.f i₁).f i₂
Tactic: ext i₁ i₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalBicomplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' : I₁
h : ¬c₁.Rel i₁ i₁'
⊢ Eq (α :=
    { X := fun (i₂ : I₂) ↦ X (i₁, i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁ i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
        HomologicalComplex.{v_1, u_1, u_3} C c₂ } ⟶
      { X := fun (i₂ : I₂) ↦ X (i₁', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ })
    { f := fun (i₂ : I₂) ↦ d₁ i₁ i₁' i₂, comm' := ⋯ } 0
have h₁ : ∀ (i₂ : I₂),
  Eq.{v_1 + 1} (α :=
    { X := fun (i₂ : I₂) ↦ X (i₁, i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁ i₂ i₂', shape := sorry, d_comp_d' := sorry :
            HomologicalComplex.{v_1, u_1, u_3} C c₂ }.X
        i₂ ⟶
      { X := fun (i₂ : I₂) ↦ X (i₁', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁' i₂ i₂', shape := sorry, d_comp_d' := sorry :
            HomologicalComplex.{v_1, u_1, u_3} C c₂ }.X
        i₂)
    (Hom.f { f := fun (i₂ : I₂) ↦ d₁ i₁ i₁' i₂, comm' := sorry } i₂) (Hom.f 0 i₂)
Tactic: ext i₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalBicomplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
X : GradedObject (I₁ × I₂) C
d₁ : (i₁ i₁' : I₁) → (i₂ : I₂) → X (i₁, i₂) ⟶ X (i₁', i₂)
d₂ : (i₁ : I₁) → (i₂ i₂' : I₂) → X (i₁, i₂) ⟶ X (i₁, i₂')
shape₁ : ∀ (i₁ i₁' : I₁), ¬c₁.Rel i₁ i₁' → ∀ (i₂ : I₂), d₁ i₁ i₁' i₂ = 0
shape₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), ¬c₂.Rel i₂ i₂' → d₂ i₁ i₂ i₂' = 0
d₁_comp_d₁ : ∀ (i₁ i₁' i₁'' : I₁) (i₂ : I₂), d₁ i₁ i₁' i₂ ≫ d₁ i₁' i₁'' i₂ = 0
d₂_comp_d₂ : ∀ (i₁ : I₁) (i₂ i₂' i₂'' : I₂), d₂ i₁ i₂ i₂' ≫ d₂ i₁ i₂' i₂'' = 0
comm : ∀ (i₁ i₁' : I₁) (i₂ i₂' : I₂), d₁ i₁ i₁' i₂ ≫ d₂ i₁' i₂ i₂' = d₂ i₁ i₂ i₂' ≫ d₁ i₁ i₁' i₂'
i₁ i₁' i₁'' : I₁
h : c₁.Rel i₁ i₁'
h_1 : c₁.Rel i₁' i₁''
⊢ Eq (α :=
    { X := fun (i₂ : I₂) ↦ X (i₁, i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁ i₂ i₂', shape := ⋯, d_comp_d' := ⋯ :
        HomologicalComplex.{v_1, u_1, u_3} C c₂ } ⟶
      { X := fun (i₂ : I₂) ↦ X (i₁'', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁'' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ })
    (CategoryStruct.comp (Y :=
      { X := fun (i₂ : I₂) ↦ X (i₁', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁' i₂ i₂', shape := ⋯, d_comp_d' := ⋯ })
      { f := fun (i₂ : I₂) ↦ d₁ i₁ i₁' i₂, comm' := ⋯ } { f := fun (i₂ : I₂) ↦ d₁ i₁' i₁'' i₂, comm' := ⋯ })
    0
have h : ∀ (i₂ : I₂),
  Eq.{v_1 + 1} (α :=
    { X := fun (i₂ : I₂) ↦ X (i₁, i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁ i₂ i₂', shape := sorry, d_comp_d' := sorry :
            HomologicalComplex.{v_1, u_1, u_3} C c₂ }.X
        i₂ ⟶
      { X := fun (i₂ : I₂) ↦ X (i₁'', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁'' i₂ i₂', shape := sorry, d_comp_d' := sorry :
            HomologicalComplex.{v_1, u_1, u_3} C c₂ }.X
        i₂)
    (Hom.f
      (CategoryStruct.comp (Y :=
        { X := fun (i₂ : I₂) ↦ X (i₁', i₂), d := fun (i₂ i₂' : I₂) ↦ d₂ i₁' i₂ i₂', shape := sorry, d_comp_d' := sorry })
        { f := fun (i₂ : I₂) ↦ d₁ i₁ i₁' i₂, comm' := sorry } { f := fun (i₂ : I₂) ↦ d₁ i₁' i₁'' i₂, comm' := sorry })
      i₂)
    (Hom.f 0 i₂)
Tactic: ext i₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalBicomplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
f : K.toGradedObject ⟶ L.toGradedObject
comm₁ :
  ∀ (i₁ i₁' : I₁) (i₂ : I₂),
    c₁.Rel i₁ i₁' →
      Eq.{v_1 + 1} (α := K.toGradedObject (i₁, i₂) ⟶ (L.X i₁').X i₂) (f (i₁, i₂) ≫ (L.d i₁ i₁').f i₂)
        ((K.d i₁ i₁').f i₂ ≫ f (i₁', i₂))
comm₂ :
  ∀ (i₁ : I₁) (i₂ i₂' : I₂),
    c₂.Rel i₂ i₂' →
      Eq.{v_1 + 1} (α := K.toGradedObject (i₁, i₂) ⟶ (L.X i₁).X i₂') (f (i₁, i₂) ≫ (L.X i₁).d i₂ i₂')
        ((K.X i₁).d i₂ i₂' ≫ f (i₁, i₂'))
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
⊢ { f := fun (i₂ : I₂) ↦ f (i₁, i₂), comm' := ⋯ : (K.X i₁).Hom (L.X i₁) } ≫ L.d i₁ i₁' =
    K.d i₁ i₁' ≫ { f := fun (i₂ : I₂) ↦ f (i₁', i₂), comm' := ⋯ : (K.X i₁').Hom (L.X i₁') }
have h : ∀ (i₂ : I₂),
  Hom.f ({ f := fun (i₂ : I₂) ↦ f (i₁, i₂), comm' := sorry : (K.X i₁).Hom (L.X i₁) } ≫ L.d i₁ i₁') i₂ =
    (K.d i₁ i₁' ≫ { f := fun (i₂ : I₂) ↦ f (i₁', i₂), comm' := sorry : (K.X i₁').Hom (L.X i₁') }).f i₂
Tactic: ext i₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalBicomplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
i₁ i₁' : I₁
h : ¬c₁.Rel i₁ i₁'
i₂ : I₂
⊢ (K.d i₁ i₁').f i₂ = 0
have rw : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ (K.X i₁').X i₂) (Hom.f 0 i₂) 0
Tactic: rw [K.shape _ _ h, zero_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalBicomplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
i₁ i₁' : I₁
h : ¬c₁.Rel i₁ i₁'
i₂ : I₂
rw : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ (K.X i₁').X i₂) (Hom.f 0 i₂) 0
⊢ (K.d i₁ i₁').f i₂ = 0
have rw₁ : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ (K.X i₁').X i₂) 0 0
Tactic: rw [K.shape _ _ h, zero_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalBicomplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
⊢ (K.d i₁ i₁').f i₂ ≫ (K.d i₁' i₁'').f i₂ = 0
have rw : (K.d i₁ i₁' ≫ K.d i₁' i₁'').f i₂ = 0
Tactic: rw [← comp_f, d_comp_d, zero_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalBicomplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
rw : (K.d i₁ i₁' ≫ K.d i₁' i₁'').f i₂ = 0
⊢ (K.d i₁ i₁').f i₂ ≫ (K.d i₁' i₁'').f i₂ = 0
have rw₁ : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ (K.X i₁'').X i₂) (Hom.f 0 i₂) 0
Tactic: rw [← comp_f, d_comp_d, zero_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalBicomplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
i₁ i₁' i₁'' : I₁
i₂ : I₂
rw : (K.d i₁ i₁' ≫ K.d i₁' i₁'').f i₂ = 0
rw₁ : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ (K.X i₁'').X i₂) (Hom.f 0 i₂) 0
⊢ (K.d i₁ i₁').f i₂ ≫ (K.d i₁' i₁'').f i₂ = 0
have rw₂ : Eq.{v_1 + 1} (α := (K.X i₁).X i₂ ⟶ (K.X i₁'').X i₂) 0 0
Tactic: rw [← comp_f, d_comp_d, zero_f]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalBicomplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
i i' : I₂
w : ¬c₂.Rel i i'
⊢ Eq (α :=
    { X := fun (j : I₁) ↦ (K.X j).X i, d := fun (j j' : I₁) ↦ (K.d j j').f i, shape := ⋯, d_comp_d' := ⋯ :
        HomologicalComplex.{v_1, u_1, u_2} C c₁ } ⟶
      { X := fun (j : I₁) ↦ (K.X j).X i', d := fun (j j' : I₁) ↦ (K.d j j').f i', shape := ⋯, d_comp_d' := ⋯ })
    { f := fun (j : I₁) ↦ (K.X j).d i i', comm' := ⋯ } 0
have h : ∀ (j : I₁),
  Eq.{v_1 + 1} (α :=
    { X := fun (j : I₁) ↦ (K.X j).X i, d := fun (j j' : I₁) ↦ (K.d j j').f i, shape := sorry, d_comp_d' := sorry :
            HomologicalComplex.{v_1, u_1, u_2} C c₁ }.X
        j ⟶
      { X := fun (j : I₁) ↦ (K.X j).X i', d := fun (j j' : I₁) ↦ (K.d j j').f i', shape := sorry, d_comp_d' := sorry :
            HomologicalComplex.{v_1, u_1, u_2} C c₁ }.X
        j)
    (Hom.f { f := fun (j : I₁) ↦ (K.X j).d i i', comm' := sorry } j) (Hom.f 0 j)
Tactic: ext j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalBicomplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
f : K ⟶ L
i j : I₂
h : c₂.Rel i j
⊢ { f := fun (j : I₁) ↦ (f.f j).f i, comm' := ⋯ } ≫ L.flip.d i j =
    K.flip.d i j ≫ { f := fun (j_1 : I₁) ↦ (f.f j_1).f j, comm' := ⋯ : (K.flip.X j).Hom (L.flip.X j) }
have h : ∀ (i_1 : I₁),
  Hom.f ({ f := fun (j : I₁) ↦ (f.f j).f i, comm' := sorry } ≫ L.flip.d i j) i_1 =
    Hom.f (K.flip.d i j ≫ { f := fun (j_1 : I₁) ↦ (f.f j_1).f j, comm' := sorry : (K.flip.X j).Hom (L.flip.X j) }) i_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalBicomplex (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂.{v_1, u_1, u_2, u_3} C c₁ c₂
x₁ y₁ : I₁
h₁ : x₁ = y₁
x₂ y₂ : I₂
h₂ : x₂ = y₂
⊢ (K.X x₁).X x₂ = (K.X y₁).X y₂
have subst : (K.X x₁).X x₂ = (K.X x₁).X x₂
Tactic: subst h₁ h₂
Cleared hypotheses: y₁, h₁, y₂, h₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j k : ι
⊢ C.d i j ≫ C.d j k = 0
have pos : ∀ (hij : c.Rel i j), C.d i j ≫ C.d j k = 0
Tactic: by_cases hij : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j k : ι
pos : ∀ (hij : c.Rel i j), C.d i j ≫ C.d j k = 0
⊢ C.d i j ≫ C.d j k = 0
have neg : ∀ (hij : ¬c.Rel i j), C.d i j ≫ C.d j k = 0
Tactic: by_cases hij : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j k : ι
hij : c.Rel i j
⊢ C.d i j ≫ C.d j k = 0
have pos : ∀ (hjk : c.Rel j k), C.d i j ≫ C.d j k = 0
Tactic: by_cases hjk : c.Rel j k
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j k : ι
hij : c.Rel i j
pos : ∀ (hjk : c.Rel j k), C.d i j ≫ C.d j k = 0
⊢ C.d i j ≫ C.d j k = 0
have neg : ∀ (hjk : ¬c.Rel j k), C.d i j ≫ C.d j k = 0
Tactic: by_cases hjk : c.Rel j k
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j k : ι
hij : c.Rel i j
hjk : ¬c.Rel j k
⊢ C.d i j ≫ C.d j k = 0
have neg : Eq (α := C.X i ⟶ C.X k) (C.d i j ≫ 0) 0
Tactic: rw [C.shape j k hjk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j k : ι
hij : c.Rel i j
hjk : ¬c.Rel j k
neg : Eq (α := C.X i ⟶ C.X k) (C.d i j ≫ 0) 0
⊢ C.d i j ≫ C.d j k = 0
have neg₁ : Eq.{v + 1} (α := C.X i ⟶ C.X k) 0 0
Tactic: rw [C.shape j k hjk, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j k : ι
hij : ¬c.Rel i j
⊢ C.d i j ≫ C.d j k = 0
have neg : Eq (α := C.X i ⟶ C.X k) (0 ≫ C.d j k) 0
Tactic: rw [C.shape i j hij, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C : HomologicalComplex.{v, u, u_1} V c
i j k : ι
hij : ¬c.Rel i j
neg : Eq (α := C.X i ⟶ C.X k) (0 ≫ C.d j k) 0
⊢ C.d i j ≫ C.d j k = 0
have neg₁ : Eq.{v + 1} (α := C.X i ⟶ C.X k) 0 0
Tactic: rw [C.shape i j hij, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C₁ C₂ : HomologicalComplex.{v, u, u_1} V c
h_X : C₁.X = C₂.X
h_d : ∀ (i j : ι), c.Rel i j → C₁.d i j ≫ eqToHom ⋯ = eqToHom ⋯ ≫ C₂.d i j
⊢ C₁ = C₂
have obtain : ∀ (X₁ : ι → V) (d₁ : (i j : ι) → X₁ i ⟶ X₁ j) (s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0)
  (h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0)
  (h_X : { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.X = C₂.X)
  (h_d :
    ∀ (i j : ι),
      c.Rel i j →
        { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom sorry =
          eqToHom sorry ≫ C₂.d i j),
  { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c } = C₂
Tactic: obtain ⟨X₁, d₁, s₁, h₁⟩ := C₁
Cleared hypotheses: C₁, h_X, h_d
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
C₂ : HomologicalComplex.{v, u, u_1} V c
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
h_X : { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.X = C₂.X
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ C₂.d i j
⊢ { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c } = C₂
have obtain : ∀ (X₂ : ι → V) (d₂ : (i j : ι) → X₂ i ⟶ X₂ j) (s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0)
  (h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0)
  (h_X :
    { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.X =
      { X := X₂, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.X)
  (h_d :
    ∀ (i j : ι),
      c.Rel i j →
        { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom sorry =
          eqToHom sorry ≫ { X := X₂, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j),
  { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c } =
    { X := X₂, d := d₂, shape := s₂, d_comp_d' := h₂ }
Tactic: obtain ⟨X₂, d₂, s₂, h₂⟩ := C₂
Cleared hypotheses: C₂, h_X, h_d
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
X₂ : ι → V
d₂ : (i j : ι) → X₂ i ⟶ X₂ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_X : X₁ = X₂
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₂, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j
⊢ { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c } =
    { X := X₂, d := d₂, shape := s₂, d_comp_d' := h₂ }
have subst : ∀ (d₂ : (i j : ι) → X₁ i ⟶ X₁ j) (s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0)
  (h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0)
  (h_d :
    ∀ (i j : ι),
      c.Rel i j →
        { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom sorry =
          eqToHom sorry ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j),
  { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c } =
    { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }
Tactic: subst h_X
Cleared hypotheses: X₂, d₂, s₂, h₂, h_X, h_d
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j
⊢ { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c } =
    { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ }
have simp : d₁ = d₂
Tactic: simp only [mk.injEq, heq_eq_eq, true_and]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j
⊢ d₁ = d₂
have h : ∀ (i j : ι), d₁ i j = d₂ i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j
i j : ι
⊢ d₁ i j = d₂ i j
have pos : ∀ (hij : c.Rel i j), d₁ i j = d₂ i j
Tactic: by_cases hij : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j
i j : ι
pos : ∀ (hij : c.Rel i j), d₁ i j = d₂ i j
⊢ d₁ i j = d₂ i j
have neg : ∀ (hij : ¬c.Rel i j), d₁ i j = d₂ i j
Tactic: by_cases hij : c.Rel i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j
i j : ι
hij : ¬c.Rel i j
⊢ d₁ i j = d₂ i j
have neg : 0 = d₂ i j
Tactic: rw [s₁ i j hij, s₂ i j hij]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplex (goal)
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
c : ComplexShape ι
X₁ : ι → V
d₁ : (i j : ι) → X₁ i ⟶ X₁ j
s₁ : ∀ (i j : ι), ¬c.Rel i j → d₁ i j = 0
h₁ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₁ i j ≫ d₁ j k = 0
d₂ : (i j : ι) → X₁ i ⟶ X₁ j
s₂ : ∀ (i j : ι), ¬c.Rel i j → d₂ i j = 0
h₂ : ∀ (i j k : ι), c.Rel i j → c.Rel j k → d₂ i j ≫ d₂ j k = 0
h_d :
  ∀ (i j : ι),
    c.Rel i j →
      { X := X₁, d := d₁, shape := s₁, d_comp_d' := h₁ : HomologicalComplex.{v, u, u_1} V c }.d i j ≫ eqToHom ⋯ =
        eqToHom ⋯ ≫ { X := X₁, d := d₂, shape := s₂, d_comp_d' := h₂ : HomologicalComplex.{v, u, u_1} V c }.d i j
i j : ι
hij : ¬c.Rel i j
neg : 0 = d₂ i j
⊢ d₁ i j = d₂ i j
have neg₁ : Eq.{v + 1} (α := X₁ i ⟶ X₁ j) 0 0
Tactic: rw [s₁ i j hij, s₂ i j hij]