awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
j : ι
i' j' k' : ι'
hj' : e.f j = j'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
hi' : e.f (c.prev j) = i'
hk' : e.f (c.next j) = k'
⊢ ((K.restriction e).sc' (c.prev j) j (c.next j)).HasHomology

Tactic:
assumption
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
subst : ∀ (hi' : e.f i = c'.prev j') (hk' : e.f k = c'.next j'), (K.sc' (c'.prev j') j' (c'.next j')).HasHomology
⊢ (K.sc' i' j' k').HasHomology

Tactic:
subst hi'' hk''
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
hi' : e.f i = c'.prev j'
hk' : e.f k = c'.next j'
⊢ (K.sc' (c'.prev j') j' (c'.next j')).HasHomology

Tactic:
assumption
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
⊢ ((K.restriction e).sc' i j k).HasHomology

Tactic:
have : ((K.restriction e).sc' i j k).HasHomology := by subst hi hk; assumption
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
⊢ (K.sc' i' j' k').HasHomology

Tactic:
have : (K.sc' i' j' k').HasHomology := by subst hi'' hk''; assumption
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
dsimp :
  Eq (α := (K.restriction e).cycles j ⟶ K.homology j')
    ((K.restriction e).homologyπ j ≫
      CategoryStruct.comp (Y := ((K.restriction e).sc' i j k).homology)
        (ShortComplex.homologyMap (NatTrans.app (Iso.hom (natIsoSc' C c i j k hi hk)) (K.restriction e)))
        (CategoryStruct.comp (Y := (K.sc' i' j' k').homology)
          (ShortComplex.homologyMap (Iso.hom (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'')))
          (ShortComplex.homologyMap (NatTrans.app (Iso.inv (natIsoSc' C c' i' j' k' hi'' hk'')) K))))
    (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ K.homologyπ j')
⊢ Eq (α := (K.restriction e).cycles j ⟶ K.homology j')
    ((K.restriction e).homologyπ j ≫ Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
    (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ K.homologyπ j')

Tactic:
dsimp [restrictionHomologyIso, homologyIsoSc']

Premises used: HomologicalComplex.restrictionHomologyIso, HomologicalComplex.homologyIsoSc'
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
rw :
  Eq (α := (K.restriction e).cycles j ⟶ (K.sc j').opcycles)
    ((K.restriction e).homologyπ j ≫
        CategoryStruct.comp (Y := (K.sc j').homology)
          (ShortComplex.homologyMap
            (NatTrans.app (Iso.hom (natIsoSc' C c i j k hi hk)) (K.restriction e) ≫
              Iso.hom (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'') ≫
                NatTrans.app (Iso.inv (natIsoSc' C c' i' j' k' hi'' hk'')) K))
          (K.sc j').homologyι :
      (K.restriction e).cycles j ⟶ (K.sc j').opcycles)
    (CategoryStruct.comp (Y := K.cycles j') (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk''))
        (K.homologyπ j' ≫ (K.sc j').homologyι) :
      (K.restriction e).cycles j ⟶ (K.sc j').opcycles)
⊢ Eq (α := (K.restriction e).cycles j ⟶ K.homology j')
    ((K.restriction e).homologyπ j ≫
      CategoryStruct.comp (Y := ((K.restriction e).sc' i j k).homology)
        (ShortComplex.homologyMap (NatTrans.app (Iso.hom (natIsoSc' C c i j k hi hk)) (K.restriction e)))
        (CategoryStruct.comp (Y := (K.sc' i' j' k').homology)
          (ShortComplex.homologyMap (Iso.hom (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'')))
          (ShortComplex.homologyMap (NatTrans.app (Iso.inv (natIsoSc' C c' i' j' k' hi'' hk'')) K))))
    (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ K.homologyπ j')

Tactic:
rw [← ShortComplex.homologyMap_comp, ← ShortComplex.homologyMap_comp,
    ← cancel_mono (K.sc j').homologyι, assoc, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, HomologicalComplex.sc, CategoryTheory.ShortComplex.homologyMap_comp, CategoryTheory.ShortComplex.homologyι
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
apply :
  Eq (α := ((K.restriction e).sc j).cycles ⟶ (K.sc j').opcycles)
    (((K.restriction e).sc j).iCycles ≫
        (NatTrans.app (Iso.hom (natIsoSc' C c i j k hi hk)) (K.restriction e) ≫
              Iso.hom (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'') ≫
                NatTrans.app (Iso.inv (natIsoSc' C c' i' j' k' hi'' hk'')) K).τ₂ ≫
          (K.sc j').pOpcycles :
      ((K.restriction e).sc j).cycles ⟶ (K.sc j').opcycles)
    (CategoryStruct.comp (Y := K.cycles j') (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk''))
        (K.homologyπ j' ≫ (K.sc j').homologyι) :
      (K.restriction e).cycles j ⟶ (K.sc j').opcycles)
⊢ Eq (α := (K.restriction e).cycles j ⟶ (K.sc j').opcycles)
    ((K.restriction e).homologyπ j ≫
        CategoryStruct.comp (Y := (K.sc j').homology)
          (ShortComplex.homologyMap
            (NatTrans.app (Iso.hom (natIsoSc' C c i j k hi hk)) (K.restriction e) ≫
              Iso.hom (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'') ≫
                NatTrans.app (Iso.inv (natIsoSc' C c' i' j' k' hi'' hk'')) K))
          (K.sc j').homologyι :
      (K.restriction e).cycles j ⟶ (K.sc j').opcycles)
    (CategoryStruct.comp (Y := K.cycles j') (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk''))
        (K.homologyπ j' ≫ (K.sc j').homologyι) :
      (K.restriction e).cycles j ⟶ (K.sc j').opcycles)

Tactic:
apply (ShortComplex.π_homologyMap_ι _).trans

Premises used: Eq.trans, CategoryTheory.ShortComplex.π_homologyMap_ι
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
dsimp :
  Eq (α := ((K.restriction e).sc j).cycles ⟶ (K.sc j').opcycles)
    (((K.restriction e).sc j).iCycles ≫
        (𝟙 (K.X (e.f j)) ≫ Iso.hom (K.restrictionXIso e hj') ≫ 𝟙 (K.X j')) ≫ (K.sc j').pOpcycles :
      ((K.restriction e).sc j).cycles ⟶ (K.sc j').opcycles)
    (CategoryStruct.comp (Y := K.cycles j') (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk''))
        (K.homologyπ j' ≫ (K.sc j').homologyι) :
      (K.restriction e).cycles j ⟶ (K.sc j').opcycles)
⊢ Eq (α := ((K.restriction e).sc j).cycles ⟶ (K.sc j').opcycles)
    (((K.restriction e).sc j).iCycles ≫
        (NatTrans.app (Iso.hom (natIsoSc' C c i j k hi hk)) (K.restriction e) ≫
              Iso.hom (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'') ≫
                NatTrans.app (Iso.inv (natIsoSc' C c' i' j' k' hi'' hk'')) K).τ₂ ≫
          (K.sc j').pOpcycles :
      ((K.restriction e).sc j).cycles ⟶ (K.sc j').opcycles)
    (CategoryStruct.comp (Y := K.cycles j') (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk''))
        (K.homologyπ j' ≫ (K.sc j').homologyι) :
      (K.restriction e).cycles j ⟶ (K.sc j').opcycles)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
rw :
  Eq (α := ((K.restriction e).sc j).cycles ⟶ (K.sc j').opcycles)
    (((K.restriction e).sc j).iCycles ≫ Iso.hom (K.restrictionXIso e hj') ≫ (K.sc j').pOpcycles :
      ((K.restriction e).sc j).cycles ⟶ (K.sc j').opcycles)
    (CategoryStruct.comp (Y := K.cycles j') (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk''))
        (K.homologyπ j' ≫ (K.sc j').homologyι) :
      (K.restriction e).cycles j ⟶ (K.sc j').opcycles)
⊢ Eq (α := ((K.restriction e).sc j).cycles ⟶ (K.sc j').opcycles)
    (((K.restriction e).sc j).iCycles ≫
        (𝟙 (K.X (e.f j)) ≫ Iso.hom (K.restrictionXIso e hj') ≫ 𝟙 (K.X j')) ≫ (K.sc j').pOpcycles :
      ((K.restriction e).sc j).cycles ⟶ (K.sc j').opcycles)
    (CategoryStruct.comp (Y := K.cycles j') (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk''))
        (K.homologyπ j' ≫ (K.sc j').homologyι) :
      (K.restriction e).cycles j ⟶ (K.sc j').opcycles)

Tactic:
rw [comp_id, id_comp]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
apply :
  Eq (α := (K.restriction e).cycles j ⟶ (K.sc j').opcycles)
    (CategoryStruct.comp (Y := K.cycles j') (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk''))
        (K.iCycles j' ≫ (K.sc j').pOpcycles) :
      (K.restriction e).cycles j ⟶ (K.sc j').opcycles)
    (CategoryStruct.comp (Y := K.cycles j') (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk''))
        (K.homologyπ j' ≫ (K.sc j').homologyι) :
      (K.restriction e).cycles j ⟶ (K.sc j').opcycles)
⊢ Eq (α := ((K.restriction e).sc j).cycles ⟶ (K.sc j').opcycles)
    (((K.restriction e).sc j).iCycles ≫ Iso.hom (K.restrictionXIso e hj') ≫ (K.sc j').pOpcycles :
      ((K.restriction e).sc j).cycles ⟶ (K.sc j').opcycles)
    (CategoryStruct.comp (Y := K.cycles j') (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk''))
        (K.homologyπ j' ≫ (K.sc j').homologyι) :
      (K.restriction e).cycles j ⟶ (K.sc j').opcycles)

Tactic:
apply (K.restrictionCyclesIso_hom_iCycles_assoc e j k hk hj' hk' hk'' _).symm.trans

Premises used: HomologicalComplex.restrictionCyclesIso_hom_iCycles_assoc, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
e_a :
  Eq (α := K.cycles j' ⟶ (K.sc j').opcycles) (K.iCycles j' ≫ (K.sc j').pOpcycles) (K.homologyπ j' ≫ (K.sc j').homologyι)
⊢ Eq (α := (K.restriction e).cycles j ⟶ (K.sc j').opcycles)
    (CategoryStruct.comp (Y := K.cycles j') (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk''))
        (K.iCycles j' ≫ (K.sc j').pOpcycles) :
      (K.restriction e).cycles j ⟶ (K.sc j').opcycles)
    (CategoryStruct.comp (Y := K.cycles j') (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk''))
        (K.homologyπ j' ≫ (K.sc j').homologyι) :
      (K.restriction e).cycles j ⟶ (K.sc j').opcycles)

Tactic:
congr 1
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
e_a :
  Eq (α := K.cycles j' ⟶ (K.sc j').opcycles) (K.homologyπ j' ≫ (K.sc j').homologyι) (K.iCycles j' ≫ (K.sc j').pOpcycles)
⊢ Eq (α := K.cycles j' ⟶ (K.sc j').opcycles) (K.iCycles j' ≫ (K.sc j').pOpcycles) (K.homologyπ j' ≫ (K.sc j').homologyι)

Tactic:
symm
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ Eq (α := K.cycles j' ⟶ (K.sc j').opcycles) (K.homologyπ j' ≫ (K.sc j').homologyι) (K.iCycles j' ≫ (K.sc j').pOpcycles)

Tactic:
apply ShortComplex.homology_π_ι

Premises used: CategoryTheory.ShortComplex.homology_π_ι
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
dsimp :
  Eq (α := K.homology j' ⟶ (K.restriction e).opcycles j)
    (CategoryStruct.comp (Y := ((K.restriction e).sc' i j k).homology)
        (CategoryStruct.comp (Y := (K.sc' i' j' k').homology)
          (ShortComplex.homologyMap (NatTrans.app (Iso.hom (natIsoSc' C c' i' j' k' hi'' hk'')) K))
          (ShortComplex.homologyMap (Iso.inv (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk''))))
        (ShortComplex.homologyMap (NatTrans.app (Iso.inv (natIsoSc' C c i j k hi hk)) (K.restriction e))) ≫
      (K.restriction e).homologyι j)
    (K.homologyι j' ≫ Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi''))
⊢ Eq (α := K.homology j' ⟶ (K.restriction e).opcycles j)
    (Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'') ≫ (K.restriction e).homologyι j)
    (K.homologyι j' ≫ Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi''))

Tactic:
dsimp [restrictionHomologyIso, homologyIsoSc']

Premises used: HomologicalComplex.restrictionHomologyIso, HomologicalComplex.homologyIsoSc'
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
rw :
  Eq (α := (K.sc j').cycles ⟶ (K.restriction e).opcycles j)
    (CategoryStruct.comp (Y := (K.sc j').homology) (K.sc j').homologyπ
        (ShortComplex.homologyMap
            (NatTrans.app (Iso.hom (natIsoSc' C c' i' j' k' hi'' hk'')) K ≫
              Iso.inv (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'') ≫
                NatTrans.app (Iso.inv (natIsoSc' C c i j k hi hk)) (K.restriction e)) ≫
          (K.restriction e).homologyι j) :
      (K.sc j').cycles ⟶ (K.restriction e).opcycles j)
    (CategoryStruct.comp (Y := (K.sc j').homology) (K.sc j').homologyπ
        (K.homologyι j' ≫ Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi'')) :
      (K.sc j').cycles ⟶ (K.restriction e).opcycles j)
⊢ Eq (α := K.homology j' ⟶ (K.restriction e).opcycles j)
    (CategoryStruct.comp (Y := ((K.restriction e).sc' i j k).homology)
        (CategoryStruct.comp (Y := (K.sc' i' j' k').homology)
          (ShortComplex.homologyMap (NatTrans.app (Iso.hom (natIsoSc' C c' i' j' k' hi'' hk'')) K))
          (ShortComplex.homologyMap (Iso.inv (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk''))))
        (ShortComplex.homologyMap (NatTrans.app (Iso.inv (natIsoSc' C c i j k hi hk)) (K.restriction e))) ≫
      (K.restriction e).homologyι j)
    (K.homologyι j' ≫ Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi''))

Tactic:
rw [← ShortComplex.homologyMap_comp, ← ShortComplex.homologyMap_comp, assoc,
    ← cancel_epi (K.sc j').homologyπ]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.homologyπ, HomologicalComplex.sc, CategoryTheory.ShortComplex.homologyMap_comp, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology
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.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
this_1 : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
apply :
  Eq (α := (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    ((K.sc j').iCycles ≫
        (NatTrans.app (Iso.hom (natIsoSc' C c' i' j' k' hi'' hk'')) K ≫
              Iso.inv (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'') ≫
                NatTrans.app (Iso.inv (natIsoSc' C c i j k hi hk)) (K.restriction e)).τ₂ ≫
          ((K.restriction e).sc j).pOpcycles :
      (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    (CategoryStruct.comp (Y := (K.sc j').homology) (K.sc j').homologyπ
        (K.homologyι j' ≫ Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi'')) :
      (K.sc j').cycles ⟶ (K.restriction e).opcycles j)
⊢ Eq (α := (K.sc j').cycles ⟶ (K.restriction e).opcycles j)
    (CategoryStruct.comp (Y := (K.sc j').homology) (K.sc j').homologyπ
        (ShortComplex.homologyMap
            (NatTrans.app (Iso.hom (natIsoSc' C c' i' j' k' hi'' hk'')) K ≫
              Iso.inv (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'') ≫
                NatTrans.app (Iso.inv (natIsoSc' C c i j k hi hk)) (K.restriction e)) ≫
          (K.restriction e).homologyι j) :
      (K.sc j').cycles ⟶ (K.restriction e).opcycles j)
    (CategoryStruct.comp (Y := (K.sc j').homology) (K.sc j').homologyπ
        (K.homologyι j' ≫ Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi'')) :
      (K.sc j').cycles ⟶ (K.restriction e).opcycles j)

Tactic:
apply (ShortComplex.π_homologyMap_ι _).trans

Premises used: Eq.trans, CategoryTheory.ShortComplex.π_homologyMap_ι