awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.IsSupported
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
D : Type u_4
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_2, u_4} D
inst_2 : HasZeroMorphisms.{v_1, u_3} C
inst_3 : HasZeroMorphisms.{v_2, u_4} D
K : HomologicalComplex.{v_1, u_3, u_2} C c'
F : CategoryTheory.Functor.{v_1, v_2, u_3, u_4} C D
inst_4 : F.PreservesZeroMorphisms
e : c.Embedding c'
inst_5 : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
rw : F.map (𝟙 (K.X i')) = 0
rw₁ : Eq (α := F.obj (K.X i') ⟶ F.obj (K.X i')) (F.map 0) 0
rw₂ rw₃ : Eq.{v_2 + 1} (α := F.obj (K.X i') ⟶ F.obj (K.X i')) 0 0
⊢ Eq.{v_2 + 1} (α := F.obj (K.X i') ⟶ F.obj (K.X i')) (𝟙 (F.obj (K.X i'))) 0

Tactic:
rw [← F.map_id, (K.isZero_X_of_isStrictlySupported e i' hi').eq_of_src (𝟙 _) 0, F.map_zero]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map_id, CategoryTheory.Limits.IsZero.eq_of_src, HomologicalComplex.isZero_X_of_isStrictlySupported, OfNat.ofNat
-- Module: Mathlib.Algebra.Homology.Embedding.Restriction
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 M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsRelIff
i j : ι
hij : ¬c.Rel i j
⊢ ¬c'.Rel (e.f i) (e.f j)

Tactic:
simpa only [← e.rel_iff] using hij

Premises used: ComplexShape.Embedding.rel_iff
-- Module: Mathlib.Algebra.Homology.Embedding.Restriction
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 : ι
i' j' : ι'
hi : e.f i = i'
hj : e.f j = j'
subst :
  (K.restriction e).d i j = Iso.hom (K.restrictionXIso e ⋯) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (K.restrictionXIso e ⋯)
⊢ (K.restriction e).d i j = Iso.hom (K.restrictionXIso e hi) ≫ K.d i' j' ≫ Iso.inv (K.restrictionXIso e hj)

Tactic:
subst hi hj
-- Module: Mathlib.Algebra.Homology.Embedding.Restriction
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.restriction e).d i j = Iso.hom (K.restrictionXIso e ⋯) ≫ K.d (e.f i) (e.f j) ≫ Iso.inv (K.restrictionXIso e ⋯)

Tactic:
simp [restrictionXIso]

Premises used: HomologicalComplex.restrictionXIso
-- Module: Mathlib.Algebra.Homology.Embedding.Restriction
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.IsRelIff
i : ι
i' : ι'
hi : e.f i = i'
subst :
  Eq (α := (K.restriction e).X i ⟶ (L.restriction e).X i) (Hom.f (restrictionMap φ e) i)
    (Iso.hom (K.restrictionXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.inv (L.restrictionXIso e ⋯))
⊢ Eq (α := (K.restriction e).X i ⟶ (L.restriction e).X i) (Hom.f (restrictionMap φ e) i)
    (Iso.hom (K.restrictionXIso e hi) ≫ φ.f i' ≫ Iso.inv (L.restrictionXIso e hi))

Tactic:
subst hi
-- Module: Mathlib.Algebra.Homology.Embedding.Restriction
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.IsRelIff
i : ι
⊢ Eq (α := (K.restriction e).X i ⟶ (L.restriction e).X i) (Hom.f (restrictionMap φ e) i)
    (Iso.hom (K.restrictionXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.inv (L.restrictionXIso e ⋯))

Tactic:
simp [restrictionXIso]

Premises used: HomologicalComplex.restrictionXIso
-- Module: Mathlib.Algebra.Homology.Embedding.Restriction
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
⊢ restrictionMap (𝟙 K) e = 𝟙 (K.restriction e)

Tactic:
rfl

Premises used: HomologicalComplex.id, HomologicalComplex.restrictionMap, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Restriction
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 M : HomologicalComplex.{v_1, u_3, u_2} C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_2 : e.IsRelIff
⊢ Eq (α := K.restriction e ⟶ M.restriction e) (restrictionMap (φ ≫ φ') e) (restrictionMap φ e ≫ restrictionMap φ' e)

Tactic:
rfl

Premises used: HomologicalComplex.restrictionMap, HomologicalComplex.comp, rfl
-- 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'
subst :
  ∀ (hk'' : c'.next (e.f j) = k') (hi'' : c'.prev (e.f j) = e.f i),
    Iso.hom (K.restrictionXIso e ⋯) ≫ (K.sc' (e.f i) (e.f j) k').f =
      ((K.restriction e).sc' i j k).f ≫ Iso.hom (K.restrictionXIso e ⋯)
⊢ Iso.hom (K.restrictionXIso e hi') ≫ (K.sc' i' j' k').f =
    ((K.restriction e).sc' i j k).f ≫ Iso.hom (K.restrictionXIso e hj')

Tactic:
subst hi' hj'
-- 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
k' : ι'
hk' : e.f k = k'
hk'' : c'.next (e.f j) = k'
hi'' : c'.prev (e.f j) = e.f i
⊢ Iso.hom (K.restrictionXIso e ⋯) ≫ (K.sc' (e.f i) (e.f j) k').f =
    ((K.restriction e).sc' i j k).f ≫ Iso.hom (K.restrictionXIso e ⋯)

Tactic:
simp [restrictionXIso]

Premises used: HomologicalComplex.restrictionXIso
-- 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'
subst :
  ∀ (hi'' : c'.prev (e.f j) = i') (hk'' : c'.next (e.f j) = e.f k),
    Iso.hom (K.restrictionXIso e ⋯) ≫ (K.sc' i' (e.f j) (e.f k)).g =
      ((K.restriction e).sc' i j k).g ≫ Iso.hom (K.restrictionXIso e ⋯)
⊢ Iso.hom (K.restrictionXIso e hj') ≫ (K.sc' i' j' k').g =
    ((K.restriction e).sc' i j k).g ≫ Iso.hom (K.restrictionXIso e hk')

Tactic:
subst hj' 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
i' : ι'
hi' : e.f i = i'
hi'' : c'.prev (e.f j) = i'
hk'' : c'.next (e.f j) = e.f k
⊢ Iso.hom (K.restrictionXIso e ⋯) ≫ (K.sc' i' (e.f j) (e.f k)).g =
    ((K.restriction e).sc' i j k).g ≫ Iso.hom (K.restrictionXIso e ⋯)

Tactic:
simp [restrictionXIso]

Premises used: HomologicalComplex.restrictionXIso
-- 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'
⊢ (K.restriction e).HasHomology j

Tactic:
ShortComplex.hasHomology_of_iso (K.isoSc' i' j' k' hi'' hk'' ≪≫
    (sc'Iso K e i j k hi' hj' hk' hi'' hk'').symm ≪≫
    ((K.restriction e).isoSc' i j k hi hk).symm)

Premises used: HomologicalComplex.isoSc', HomologicalComplex.restriction, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, HomologicalComplex.restriction.sc'Iso, CategoryTheory.ShortComplex.hasHomology_of_iso
-- 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
rw :
  Eq (α := (K.restriction e).cycles j ⟶ K.X k')
    ((K.restriction e).iCycles j ≫ Iso.hom (K.restrictionXIso e hj') ≫ K.d j' k') 0
rw₁ :
  Eq (α := (K.restriction e).cycles j ⟶ (K.restriction e).X k)
    (((K.restriction e).iCycles j ≫ Iso.hom (K.restrictionXIso e hj') ≫ K.d j' k') ≫ Iso.inv (K.restrictionXIso e hk'))
    (0 ≫ Iso.inv (K.restrictionXIso e hk'))
rw₂ :
  Eq (α := (K.restriction e).cycles j ⟶ (K.restriction e).X k)
    ((K.restriction e).iCycles j ≫ (Iso.hom (K.restrictionXIso e hj') ≫ K.d j' k') ≫ Iso.inv (K.restrictionXIso e hk'))
    (0 ≫ Iso.inv (K.restrictionXIso e hk'))
rw₃ :
  Eq (α := (K.restriction e).cycles j ⟶ (K.restriction e).X k)
    ((K.restriction e).iCycles j ≫ Iso.hom (K.restrictionXIso e hj') ≫ K.d j' k' ≫ Iso.inv (K.restrictionXIso e hk'))
    (0 ≫ Iso.inv (K.restrictionXIso e hk'))
rw₄ :
  Eq (α := (K.restriction e).cycles j ⟶ (K.restriction e).X k) ((K.restriction e).iCycles j ≫ (K.restriction e).d j k)
    (0 ≫ Iso.inv (K.restrictionXIso e hk'))
rw₅ : Eq (α := (K.restriction e).cycles j ⟶ (K.restriction e).X k) 0 (0 ≫ Iso.inv (K.restrictionXIso e hk'))
rw₆ rw₇ : Eq.{v_1 + 1} (α := (K.restriction e).cycles j ⟶ (K.restriction e).X k) 0 0
⊢ Eq (α := (K.restriction e).cycles j ⟶ K.X k')
    (((K.restriction e).iCycles j ≫ Iso.hom (K.restrictionXIso e hj')) ≫ K.d j' k') 0

Tactic:
rw [assoc, ← cancel_mono (K.restrictionXIso e hk').inv, assoc, assoc, ← restriction_d_eq,
        iCycles_d, zero_comp]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.restriction_d_eq, HomologicalComplex.iCycles_d, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp, HomologicalComplex.restrictionXIso, CategoryTheory.Iso.inv
-- 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
rw :
  Eq (α := K.cycles j' ⟶ (K.restriction e).X k)
    (K.iCycles j' ≫ Iso.inv (K.restrictionXIso e hj') ≫ (K.restriction e).d j k) 0
rw₁ :
  Eq (α := K.cycles j' ⟶ (K.restriction e).X k)
    (K.iCycles j' ≫
      CategoryStruct.comp (Y := (K.restriction e).X j) (Iso.inv (K.restrictionXIso e hj'))
        (Iso.hom (K.restrictionXIso e hj') ≫ K.d j' k' ≫ Iso.inv (K.restrictionXIso e hk')))
    0
rw₂ : Eq (α := K.cycles j' ⟶ (K.restriction e).X k) (K.iCycles j' ≫ K.d j' k' ≫ Iso.inv (K.restrictionXIso e hk')) 0
rw₃ : Eq (α := K.cycles j' ⟶ (K.restriction e).X k) (0 ≫ Iso.inv (K.restrictionXIso e hk')) 0
rw₄ rw₅ : Eq.{v_1 + 1} (α := K.cycles j' ⟶ (K.restriction e).X k) 0 0
⊢ Eq (α := K.cycles j' ⟶ (K.restriction e).X k)
    ((K.iCycles j' ≫ Iso.inv (K.restrictionXIso e hj')) ≫ (K.restriction e).d j k) 0

Tactic:
rw [assoc, restriction_d_eq _ _ hj' hk', Iso.inv_hom_id_assoc,
        iCycles_d_assoc, zero_comp]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.restriction_d_eq, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Limits.zero_comp, HomologicalComplex.iCycles_d_assoc
-- 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
⊢ CategoryStruct.comp (Y := K.cycles j')
      (K.liftCycles ((K.restriction e).iCycles j ≫ Iso.hom (K.restrictionXIso e hj')) k' hk'' ⋯)
      ((K.restriction e).liftCycles (K.iCycles j' ≫ Iso.inv (K.restrictionXIso e hj')) k hk ⋯) =
    𝟙 ((K.restriction e).cycles j)

Tactic:
simp [← cancel_mono ((K.restriction e).iCycles j)]

Premises used: HomologicalComplex.iCycles, CategoryTheory.cancel_mono, HomologicalComplex.restriction
-- 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
⊢ CategoryStruct.comp (Y := (K.restriction e).cycles j)
      ((K.restriction e).liftCycles (K.iCycles j' ≫ Iso.inv (K.restrictionXIso e hj')) k hk ⋯)
      (K.liftCycles ((K.restriction e).iCycles j ≫ Iso.hom (K.restrictionXIso e hj')) k' hk'' ⋯) =
    𝟙 (K.cycles j')

Tactic:
simp [← cancel_mono (K.iCycles j')]

Premises used: HomologicalComplex.iCycles, CategoryTheory.cancel_mono
-- 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 k : ι
hk : c.next j = k
j' k' : ι'
hj' : e.f j = j'
hk' : e.f k = k'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
⊢ Eq (α := (K.restriction e).cycles j ⟶ K.X j')
    (CategoryStruct.comp (Y := K.cycles j') (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk'')) (K.iCycles j'))
    ((K.restriction e).iCycles j ≫ Iso.hom (K.restrictionXIso e hj'))

Tactic:
simp [restrictionCyclesIso]

Premises used: HomologicalComplex.restrictionCyclesIso
-- 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 k : ι
hk : c.next j = k
j' k' : ι'
hj' : e.f j = j'
hk' : e.f k = k'
hk'' : c'.next j' = k'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
⊢ Eq (α := K.cycles j' ⟶ (K.restriction e).X j)
    (CategoryStruct.comp (Y := (K.restriction e).cycles j) (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk''))
      ((K.restriction e).iCycles j))
    (K.iCycles j' ≫ Iso.inv (K.restrictionXIso e hj'))

Tactic:
simp [restrictionCyclesIso]

Premises used: HomologicalComplex.restrictionCyclesIso
-- 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
rw :
  Eq (α := (K.restriction e).X i ⟶ K.opcycles j')
    (CategoryStruct.comp (Y := (K.restriction e).X j)
      (Iso.hom (K.restrictionXIso e hi') ≫ K.d i' j' ≫ Iso.inv (K.restrictionXIso e hj'))
      (Iso.hom (K.restrictionXIso e hj') ≫ K.pOpcycles j'))
    0
rw₁ :
  Eq (α := (K.restriction e).X i ⟶ K.opcycles j')
    (Iso.hom (K.restrictionXIso e hi') ≫
      CategoryStruct.comp (Y := (K.restriction e).X j) (K.d i' j' ≫ Iso.inv (K.restrictionXIso e hj'))
        (Iso.hom (K.restrictionXIso e hj') ≫ K.pOpcycles j'))
    0
rw₂ :
  Eq (α := (K.restriction e).X i ⟶ K.opcycles j')
    (Iso.hom (K.restrictionXIso e hi') ≫
      K.d i' j' ≫
        CategoryStruct.comp (Y := (K.restriction e).X j) (Iso.inv (K.restrictionXIso e hj'))
          (Iso.hom (K.restrictionXIso e hj') ≫ K.pOpcycles j'))
    0
rw₃ : Eq (α := (K.restriction e).X i ⟶ K.opcycles j') (Iso.hom (K.restrictionXIso e hi') ≫ K.d i' j' ≫ K.pOpcycles j') 0
rw₄ : Eq (α := (K.restriction e).X i ⟶ K.opcycles j') (Iso.hom (K.restrictionXIso e hi') ≫ 0) 0
rw₅ rw₆ : Eq.{v_1 + 1} (α := (K.restriction e).X i ⟶ K.opcycles j') 0 0
⊢ Eq (α := (K.restriction e).X i ⟶ K.opcycles j')
    ((K.restriction e).d i j ≫ Iso.hom (K.restrictionXIso e hj') ≫ K.pOpcycles j') 0

Tactic:
rw [restriction_d_eq _ _ hi' hj', assoc, assoc, Iso.inv_hom_id_assoc,
        d_pOpcycles, comp_zero]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.restriction_d_eq, HomologicalComplex.d_pOpcycles, CategoryTheory.Limits.comp_zero, CategoryTheory.Iso.inv_hom_id_assoc
-- 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
rw :
  Eq (α := (K.restriction e).X i ⟶ (K.restriction e).opcycles j)
    (Iso.hom (K.restrictionXIso e hi') ≫ K.d i' j' ≫ Iso.inv (K.restrictionXIso e hj') ≫ (K.restriction e).pOpcycles j)
    (Iso.hom (K.restrictionXIso e hi') ≫ 0)
rw₁ :
  Eq (α := (K.restriction e).X i ⟶ (K.restriction e).opcycles j)
    ((K.restriction e).d i j ≫ (K.restriction e).pOpcycles j) (Iso.hom (K.restrictionXIso e hi') ≫ 0)
rw₂ :
  Eq (α := (K.restriction e).X i ⟶ (K.restriction e).opcycles j)
    ((K.restriction e).d i j ≫ (K.restriction e).pOpcycles j) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := (K.restriction e).X i ⟶ (K.restriction e).opcycles j) 0 0
⊢ Eq (α := K.X i' ⟶ (K.restriction e).opcycles j)
    (K.d i' j' ≫ Iso.inv (K.restrictionXIso e hj') ≫ (K.restriction e).pOpcycles j) 0

Tactic:
rw [← cancel_epi (K.restrictionXIso e hi').hom, ← restriction_d_eq_assoc,
        comp_zero, d_pOpcycles]

Premises used: HomologicalComplex.d_pOpcycles, CategoryTheory.Limits.comp_zero, HomologicalComplex.restrictionXIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, HomologicalComplex.restriction_d_eq_assoc
-- 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
⊢ CategoryStruct.comp (Y := K.opcycles j')
      ((K.restriction e).descOpcycles (Iso.hom (K.restrictionXIso e hj') ≫ K.pOpcycles j') i hi ⋯)
      (K.descOpcycles (Iso.inv (K.restrictionXIso e hj') ≫ (K.restriction e).pOpcycles j) i' hi'' ⋯) =
    𝟙 ((K.restriction e).opcycles j)

Tactic:
simp [← cancel_epi ((K.restriction e).pOpcycles j)]

Premises used: HomologicalComplex.restriction, HomologicalComplex.pOpcycles, 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
⊢ CategoryStruct.comp (Y := (K.restriction e).opcycles j)
      (K.descOpcycles (Iso.inv (K.restrictionXIso e hj') ≫ (K.restriction e).pOpcycles j) i' hi'' ⋯)
      ((K.restriction e).descOpcycles (Iso.hom (K.restrictionXIso e hj') ≫ K.pOpcycles j') i hi ⋯) =
    𝟙 (K.opcycles j')

Tactic:
simp [← cancel_epi (K.pOpcycles j')]

Premises used: HomologicalComplex.pOpcycles, 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 : ι
hi : c.prev j = i
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi'' : c'.prev j' = i'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
⊢ Eq (α := (K.restriction e).X j ⟶ K.opcycles j')
    (CategoryStruct.comp (Y := (K.restriction e).opcycles j) ((K.restriction e).pOpcycles j)
      (Iso.hom (K.restrictionOpcyclesIso e i j hi hi' hj' hi'')))
    (Iso.hom (K.restrictionXIso e hj') ≫ K.pOpcycles j')

Tactic:
simp [restrictionOpcyclesIso]

Premises used: HomologicalComplex.restrictionOpcyclesIso
-- 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 : ι
hi : c.prev j = i
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi'' : c'.prev j' = i'
inst_3 : K.HasHomology j'
inst_4 : (K.restriction e).HasHomology j
⊢ Eq (α := K.X j' ⟶ (K.restriction e).opcycles j)
    (CategoryStruct.comp (Y := K.opcycles j') (K.pOpcycles j')
      (Iso.inv (K.restrictionOpcyclesIso e i j hi hi' hj' hi'')))
    (Iso.inv (K.restrictionXIso e hj') ≫ (K.restriction e).pOpcycles j)

Tactic:
simp [restrictionOpcyclesIso]

Premises used: HomologicalComplex.restrictionOpcyclesIso
-- 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
subst :
  ∀ (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
⊢ ((K.restriction e).sc' i j k).HasHomology

Tactic:
subst hi hk