awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
rw :
  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'))
    (CategoryStruct.comp (Y :=
        ShortComplex.RightHomologyData.Q (S := (K.truncGE' e).sc' i j k)
          (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj)))
        (Iso.inv (K.truncGE'XIsoOpcycles e hj' hj) : K.opcycles j' ⟶ (K.truncGE' e).X j)
        (ShortComplex.RightHomologyData.g'
          (extend.rightHomologyData (K.truncGE' e) e hj' hi ⋯ hk ⋯
            (ShortComplex.HomologyData.right (truncGE'.homologyData K e i j k hk hj' hj)))) :
      (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))
    ((Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles ≫ Hom.f (K.πTruncGE e) (c'.next j') :
      (Functor.obj (shortComplexFunctor C c' j') K).opcycles ⟶ (K.truncGE e).X (c'.next j'))

Tactic:
rw [extend.rightHomologyData_g' _ _ _ _ _ _ _ _ hk', πTruncGE,
        e.liftExtend_f _ _ hk', truncGE'.homologyData_right_g']

Premises used: HomologicalComplex.truncGE'.homologyData_right_g', HomologicalComplex.extend.rightHomologyData_g', ComplexShape.Embedding.liftExtend_f, HomologicalComplex.πTruncGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'))
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'))
⊢ 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

Premises used: ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
pos :
  Eq (α := K.opcycles j' ⟶ K.X (c'.next j')) (K.fromOpcycles j' (c'.next j'))
    (Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles
⊢ 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:
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)]

Premises used: HomologicalComplex.truncGE'_d_eq_fromOpcycles, HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_iso_inv, ComplexShape.Embedding.not_boundaryGE_next
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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 (α := K.opcycles j' ⟶ K.X (c'.next j')) (K.fromOpcycles j' (c'.next j'))
    (Functor.obj (shortComplexFunctor C c' j') K).fromOpcycles

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
⊢ ¬c.Rel j (c.next j)

Tactic:
simpa only [hk] using hjk
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
rw₁ rw₂ : k = k
⊢ k = j

Tactic:
rw [← c.next_eq_self j (by simpa only [hk] using hjk), hk]

Premises used: ComplexShape.next_eq_self
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
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'))
⊢ 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:
obtain rfl : k = j := by rw [← c.next_eq_self j (by simpa only [hk] using hjk), hk]

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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 (α := (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')))
⊢ 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:
rw [shape _ _ _ hjk, zero_comp, comp_zero,
        K.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv e hk' hj]

Premises used: HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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 (α := (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'))
⊢ 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:
simp only [restriction_X, restrictionXIso, eqToIso.inv, eqToIso.hom, assoc,
        eqToHom_trans_assoc, eqToHom_refl, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.eqToIso.hom, HomologicalComplex.restriction_X, CategoryTheory.eqToHom_refl, HomologicalComplex.restrictionXIso, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.eqToIso.inv, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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.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'))
⊢ 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:
change 0 = K.fromOpcycles _ _ ≫ _

Premises used: HomologicalComplex.fromOpcycles
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'))
neg₄ neg₅ : Eq.{v_1 + 1} (α := K.X j' ⟶ (K.truncGE e).X (c'.next j')) 0 0
⊢ 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:
rw [← cancel_epi (K.pOpcycles _), comp_zero, p_fromOpcycles_assoc,
        d_pOpcycles_assoc, zero_comp]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.d_pOpcycles_assoc, HomologicalComplex.pOpcycles, CategoryTheory.Limits.zero_comp, HomologicalComplex.p_fromOpcycles_assoc, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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'
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))
⊢ QuasiIsoAt (L := K.truncGE e) (K.πTruncGE e) j'

Tactic:
rw [quasiIsoAt_iff]

Premises used: quasiIsoAt_iff
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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))
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))
⊢ 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

Premises used: ComplexShape.Embedding.BoundaryGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
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' ⋯ ⋯ ⋯ ⋯
        (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))
⊢ 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 [(truncGE.rightHomologyMapData K e hj' rfl rfl hj).quasiIso_iff]

Premises used: rfl, HomologicalComplex.truncGE.rightHomologyMapData, CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
pos : IsIso.{v_1, u_3} (𝟙 (Functor.obj (shortComplexFunctor C c' j') K).homology)
⊢ 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))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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.{v_1, u_3} (𝟙 (Functor.obj (shortComplexFunctor C c' j') K).homology)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
pos : ∀ (hi : ∃ (i : ι), e.f i = c'.prev j'), Epi φ.τ₁
neg : ∀ (hi : ¬∃ (i : ι), e.f i = c'.prev j'), Epi φ.τ₁
⊢ Epi φ.τ₁

Tactic:
by_cases hi : ∃ i, e.f i = c'.prev j'

Premises used: ComplexShape.prev
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
hi : ∃ (i : ι), e.f i = c'.prev j'
pos : ∀ (i : ι) (hi : e.f i = c'.prev j'), Epi φ.τ₁
⊢ Epi φ.τ₁

Tactic:
obtain ⟨i, hi⟩ := hi
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
i : ι
hi : e.f i = c'.prev j'
pos :
  Epi (X := K.X (c'.prev j')) (Y := (K.truncGE e).X (c'.prev j'))
    (Hom.f (e.liftExtend (K.restrictionToTruncGE' e) ⋯) (c'.prev j'))
⊢ Epi φ.τ₁

Tactic:
dsimp [φ, πTruncGE]

Premises used: HomologicalComplex.πTruncGE
-- Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology
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
φ : Functor.obj (shortComplexFunctor C c' j') K ⟶ Functor.obj (shortComplexFunctor C c' j') (K.truncGE e) :=
  CategoryTheory.Functor.map (shortComplexFunctor C c' j') (K.πTruncGE e)
i : ι
hi : e.f i = c'.prev j'
pos : Epi (X := (K.restriction e).X i) (Y := (K.truncGE' e).X i) (Hom.f (K.restrictionToTruncGE' e) i)
⊢ Epi (X := K.X (c'.prev j')) (Y := (K.truncGE e).X (c'.prev j'))
    (Hom.f (e.liftExtend (K.restrictionToTruncGE' e) ⋯) (c'.prev j'))

Tactic:
rw [e.epi_liftExtend_f_iff _ _ hi]

Premises used: ComplexShape.Embedding.epi_liftExtend_f_iff