awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
pos :
  ∀ (hjk : c.Rel j k),
    Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
      (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) ≫ (K.truncGE' e).d j k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
      ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫
        Iso.inv (K.restrictionXIso e hk') ≫
          Hom.f (K.restrictionToTruncGE' e) k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
⊢ Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
    (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) ≫ (K.truncGE' e).d j k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
    ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫
      Iso.inv (K.restrictionXIso e hk') ≫
        Hom.f (K.restrictionToTruncGE' e) k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
have neg : ∀ (hjk : ¬c.Rel j k),
  Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
    (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) ≫ (K.truncGE' e).d j k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
    ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫
      Iso.inv (K.restrictionXIso e hk') ≫
        Hom.f (K.restrictionToTruncGE' e) k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
Tactic: by_cases hjk : c.Rel j k
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
hjk : c.Rel j k
⊢ Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
    (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) ≫ (K.truncGE' e).d j k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
    ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫
      Iso.inv (K.restrictionXIso e hk') ≫
        Hom.f (K.restrictionToTruncGE' e) k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
have pos : Eq (α := K.opcycles j' ⟶ K.X (c'.next j')) (K.fromOpcycles j' (c'.next j'))
  (Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles
Tactic: simp [K.truncGE'_d_eq_fromOpcycles e hjk hj' hk' hj,
        K.restrictionToTruncGE'_f_eq_iso_hom_iso_inv e hk' (e.not_boundaryGE_next hjk)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
hjk : ¬c.Rel j k
⊢ k = j
have rw : k = c.next j
Tactic: rw [← c.next_eq_self j (by simpa only [hk] using hjk), hk]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
hjk : ¬c.Rel j k
rw : k = c.next j
⊢ k = j
have rw₁ : k = k
Tactic: rw [← c.next_eq_self j (by simpa only [hk] using hjk), hk]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
hk' : e.f k = c'.next j'
hjk : ¬c.Rel j k
⊢ Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
    (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) ≫ (K.truncGE' e).d j k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
    ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫
      Iso.inv (K.restrictionXIso e hk') ≫
        Hom.f (K.restrictionToTruncGE' e) k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
have neg : ∀ (hj' : e.f k = j') (hi : c.prev k = i) (hk : c.next k = k) (hj : e.BoundaryGE k) (hjk : ¬c.Rel k k),
  Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
    (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) ≫ (K.truncGE' e).d k k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
    ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫
      Iso.inv (K.restrictionXIso e hk') ≫
        Hom.f (K.restrictionToTruncGE' e) k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
Tactic: obtain rfl : k = j := by rw [← c.next_eq_self j (by simpa only [hk] using hjk), hk]
Cleared hypotheses: j, hj', hi, hk, hj, hjk
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
⊢ Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
    (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) ≫ (K.truncGE' e).d k k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
    ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫
      Iso.inv (K.restrictionXIso e hk') ≫
        Hom.f (K.restrictionToTruncGE' e) k ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
have neg : Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j')) 0
  ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫
    CategoryStruct.comp (Y := (K.restriction e).X k) (Iso.inv (K.restrictionXIso e hk'))
      ((Iso.hom (K.restrictionXIso e hk') ≫ K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj)) ≫
        Iso.inv ((K.truncGE' e).extendXIso e hk')))
Tactic: rw [shape _ _ _ hjk, zero_comp, comp_zero,
        K.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv e hk' hj]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
⊢ Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j')) 0
    ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫
      CategoryStruct.comp (Y := (K.restriction e).X k) (Iso.inv (K.restrictionXIso e hk'))
        ((Iso.hom (K.restrictionXIso e hk') ≫ K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj)) ≫
          Iso.inv ((K.truncGE' e).extendXIso e hk')))
have neg : Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j')) 0
  ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫
    K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
Tactic: simp only [restriction_X, restrictionXIso, eqToIso.inv, eqToIso.hom, assoc,
        eqToHom_trans_assoc, eqToHom_refl, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
⊢ Eq (α := (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j')) 0
    ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫
      K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
have neg : Eq (α := K.opcycles j' ⟶ (K.truncGE e).X (c'.next j')) 0
  (K.fromOpcycles j' (c'.next j') ≫
    K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
Tactic: change 0 = K.fromOpcycles _ _ ≫ _
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
⊢ Eq (α := K.opcycles j' ⟶ (K.truncGE e).X (c'.next j')) 0
    (K.fromOpcycles j' (c'.next j') ≫
      K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
have neg : Eq (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j') 0)
  (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j')
    (K.fromOpcycles j' (c'.next j') ≫
      K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk')))
Tactic: rw [← cancel_epi (K.pOpcycles _), comp_zero, p_fromOpcycles_assoc,
        d_pOpcycles_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
neg :
  Eq (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j') 0)
    (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j')
      (K.fromOpcycles j' (c'.next j') ≫
        K.pOpcycles (c'.next j') ≫
          Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk')))
⊢ Eq (α := K.opcycles j' ⟶ (K.truncGE e).X (c'.next j')) 0
    (K.fromOpcycles j' (c'.next j') ≫
      K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
have neg₁ : Eq (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) 0
  (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j')
    (K.fromOpcycles j' (c'.next j') ≫
      K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk')))
Tactic: rw [← cancel_epi (K.pOpcycles _), comp_zero, p_fromOpcycles_assoc,
        d_pOpcycles_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
neg :
  Eq (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j') 0)
    (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j')
      (K.fromOpcycles j' (c'.next j') ≫
        K.pOpcycles (c'.next j') ≫
          Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk')))
neg₁ :
  Eq (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) 0
    (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j')
      (K.fromOpcycles j' (c'.next j') ≫
        K.pOpcycles (c'.next j') ≫
          Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk')))
⊢ Eq (α := K.opcycles j' ⟶ (K.truncGE e).X (c'.next j')) 0
    (K.fromOpcycles j' (c'.next j') ≫
      K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
have neg₂ : Eq (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) 0
  (K.d j' (c'.next j') ≫
    K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
Tactic: rw [← cancel_epi (K.pOpcycles _), comp_zero, p_fromOpcycles_assoc,
        d_pOpcycles_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
neg :
  Eq (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j') 0)
    (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j')
      (K.fromOpcycles j' (c'.next j') ≫
        K.pOpcycles (c'.next j') ≫
          Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk')))
neg₁ :
  Eq (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) 0
    (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j')
      (K.fromOpcycles j' (c'.next j') ≫
        K.pOpcycles (c'.next j') ≫
          Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk')))
neg₂ :
  Eq (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) 0
    (K.d j' (c'.next j') ≫
      K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
⊢ Eq (α := K.opcycles j' ⟶ (K.truncGE e).X (c'.next j')) 0
    (K.fromOpcycles j' (c'.next j') ≫
      K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
have neg₃ : Eq (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) 0
  (0 ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
Tactic: rw [← cancel_epi (K.pOpcycles _), comp_zero, p_fromOpcycles_assoc,
        d_pOpcycles_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : ∀ (i' : ι'), L.HasHomology i'
inst_5 : HasZeroObject.{v_1, u_3} C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
neg :
  Eq (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j') 0)
    (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j')
      (K.fromOpcycles j' (c'.next j') ≫
        K.pOpcycles (c'.next j') ≫
          Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk')))
neg₁ :
  Eq (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) 0
    (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j')
      (K.fromOpcycles j' (c'.next j') ≫
        K.pOpcycles (c'.next j') ≫
          Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk')))
neg₂ :
  Eq (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) 0
    (K.d j' (c'.next j') ≫
      K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
neg₃ :
  Eq (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) 0
    (0 ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
⊢ Eq (α := K.opcycles j' ⟶ (K.truncGE e).X (c'.next j')) 0
    (K.fromOpcycles j' (c'.next j') ≫
      K.pOpcycles (c'.next j') ≫ Iso.inv (K.truncGE'XIsoOpcycles e hk' hj) ≫ Iso.inv ((K.truncGE' e).extendXIso e hk'))
have neg₄ : Eq.{v_1 + 1} (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) 0 0
Tactic: rw [← cancel_epi (K.pOpcycles _), comp_zero, p_fromOpcycles_assoc,
        d_pOpcycles_assoc, zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
j : ι
j' : ι'
hj' : e.f j = j'
⊢ QuasiIsoAt (L := K.truncGE e) (K.πTruncGE e) j'
have rw : ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c' j') K) (S₂ :=
  Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
  (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e))
Tactic: rw [quasiIsoAt_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
j : ι
j' : ι'
hj' : e.f j = j'
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c' j') K) (S₂ :=
    Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
    (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e))
have pos : ∀ (hj : e.BoundaryGE j),
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c' j') K) (S₂ :=
    Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
    (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e))
Tactic: by_cases hj : e.BoundaryGE j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
j : ι
j' : ι'
hj' : e.f j = j'
pos :
  ∀ (hj : e.BoundaryGE j),
    ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c' j') K) (S₂ :=
      Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
      (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e))
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c' j') K) (S₂ :=
    Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
    (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e))
have neg : ∀ (hj : ¬e.BoundaryGE j),
  ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c' j') K) (S₂ :=
    Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
    (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e))
Tactic: by_cases hj : e.BoundaryGE j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
j : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
⊢ ShortComplex.QuasiIso (S₁ := Functor.obj (shortComplexFunctor C c' j') K) (S₂ :=
    Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
    (CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e))
have pos : IsIso (X := (ShortComplex.RightHomologyData.canonical (K.sc j')).H) (Y :=
  ShortComplex.RightHomologyData.H (S := Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
    (extend.rightHomologyData (K.truncGE' e) e hj' sorry sorry sorry sorry
      (ShortComplex.HomologyData.right (truncGE'.homologyData K e (c.prev j) j (c.next j) sorry hj' hj))))
  (ShortComplex.RightHomologyMapData.φH (truncGE.rightHomologyMapData K e hj' sorry sorry hj))
Tactic: rw [(truncGE.rightHomologyMapData K e hj' rfl rfl hj).quasiIso_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.TruncGEHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.IsTruncGE
inst_3 : ∀ (i' : ι'), K.HasHomology i'
inst_4 : HasZeroObject.{v_1, u_3} C
j : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
⊢ IsIso (X := (ShortComplex.RightHomologyData.canonical (K.sc j')).H) (Y :=
    ShortComplex.RightHomologyData.H (S := Functor.obj (shortComplexFunctor C c' j') (K.truncGE e))
      (extend.rightHomologyData (K.truncGE' e) e hj' ⋯ ⋯ ⋯ ⋯
        (ShortComplex.HomologyData.right (truncGE'.homologyData K e (c.prev j) j (c.next j) ⋯ hj' hj))))
    (ShortComplex.RightHomologyMapData.φH (truncGE.rightHomologyMapData K e hj' ⋯ ⋯ hj))
have pos : IsIso.{v_1, u_3} (𝟙 (Functor.obj (shortComplexFunctor C c' j') K).homology)
Tactic: dsimp