mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : ¬c.Rel j k
h₁ : f' = 0
⊢ 0 = 0

pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : ¬c.Rel j k
h₁ : f' = 0
⊢ ¬c.Rel j (c.next j)

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : ¬c.Rel j k
h₁ : f' = 0
⊢ ¬c.Rel j (c.next j)
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : ¬c.Rel j k
h₁ : f' = 0
⊢ ¬c.Rel j k

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : ¬c.Rel j k
h₁ : f' = 0
⊢ ¬c.Rel j k
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
cone : KernelFork (hcocone.desc (CokernelCofork.ofπ (K.d j k) ⋯))
hcone : IsLimit cone
⊢ Fork.ι cone ≫ hcocone.desc (CokernelCofork.ofπ (K.d j k) ⋯) = 0

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
cone : KernelFork (hcocone.desc (CokernelCofork.ofπ (K.d j k) ⋯))
hcone : IsLimit cone
⊢ Fork.ι cone ≫ hcocone.desc (CokernelCofork.ofπ (K.d j k) ⋯) = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
⊢ K.d i j ≫ h.p = 0

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
⊢ K.d i j ≫ h.p = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
⊢ h.ι ≫ h.hp.desc (CokernelCofork.ofπ (K.d j k) ⋯) = 0

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
⊢ h.ι ≫ h.hp.desc (CokernelCofork.ofπ (K.d j k) ⋯) = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
hk'' : e.f k = k'
⊢ (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' =
    (K.extendXIso e hj').hom ≫ h.p ≫ h.g' ≫ (K.extendXIso e hk'').inv

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
hk'' : e.f k = k'
⊢ (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' =
    (K.extendXIso e hj').hom ≫ h.p ≫ h.g' ≫ (K.extendXIso e hk'').inv
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
⊢ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv =
    (K.restrictionXIso e hi').hom ≫ K.pOpcycles i' ≫ (K.truncGE'XIsoOpcycles e hi' hi).inv

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
⊢ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv =
    (K.restrictionXIso e hi').hom ≫ K.pOpcycles i' ≫ (K.truncGE'XIsoOpcycles e hi' hi).inv
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i j k : ι
j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hk : c.next j = k
hj : e.BoundaryGE j
⊢ e.f k = e.f k

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
hk'' : e.f k = k'
this : (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' = (K.extend e).d j' k'
⊢ (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' =
    (K.extendXIso e hj').hom ≫ h.p ≫ h.g' ≫ (K.extendXIso e hk'').inv

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
hk'' : e.f k = k'
this : (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' = (K.extend e).d j' k'
⊢ (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' =
    (K.extendXIso e hj').hom ≫ h.p ≫ h.g' ≫ (K.extendXIso e hk'').inv
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryGE i
⊢ (K.truncGE'XIso e ⋯ hi).inv = (K.restrictionXIso e hi').hom ≫ (K.truncGE'XIso e hi' hi).inv

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : ¬e.BoundaryGE i
⊢ (K.truncGE'XIso e ⋯ hi).inv = (K.restrictionXIso e hi').hom ≫ (K.truncGE'XIso e hi' hi).inv
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : 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✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.restriction e).homologyπ j ≫
      ShortComplex.homologyMap
          ((natIsoSc' C c i j k hi hk).hom.app (K.restriction e) ≫
            (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom ≫ (natIsoSc' C c' i' j' k' hi'' hk'').inv.app K) ≫
        (K.sc j').homologyι =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j' ≫ (K.sc j').homologyι

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : 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✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.restriction e).homologyπ j ≫
      ShortComplex.homologyMap
          ((natIsoSc' C c i j k hi hk).hom.app (K.restriction e) ≫
            (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom ≫ (natIsoSc' C c' i' j' k' hi'' hk'').inv.app K) ≫
        (K.sc j').homologyι =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j' ≫ (K.sc j').homologyι
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject 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'
⊢ (K.truncGE'XIsoOpcycles e hj' hj).inv ≫ (K.truncGE' e).d j k ≫ ((K.truncGE' e).extendXIso e hk').inv =
    ((shortComplexFunctor C c' j').obj K).fromOpcycles ≫
      (K.restrictionXIso e hk').inv ≫ (K.restrictionToTruncGE' e).f k ≫ ((K.truncGE' e).extendXIso e hk').inv

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject 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'
⊢ (K.truncGE'XIsoOpcycles e hj' hj).inv ≫ (K.truncGE' e).d j k ≫ ((K.truncGE' e).extendXIso e hk').inv =
    ((shortComplexFunctor C c' j').obj K).fromOpcycles ≫
      (K.restrictionXIso e hk').inv ≫ (K.restrictionToTruncGE' e).f k ≫ ((K.truncGE' e).extendXIso e hk').inv
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : 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✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ ((K.restriction e).sc j).iCycles ≫ (K.restrictionXIso e hj').hom ≫ (K.sc j').pOpcycles =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j' ≫ (K.sc j').homologyι

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : 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✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ ((K.restriction e).sc j).iCycles ≫ (K.restrictionXIso e hj').hom ≫ (K.sc j').pOpcycles =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j' ≫ (K.sc j').homologyι
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).RightHomologyData
hk'' : e.f k = k'
this : (K.extendXIso e hj').hom ≫ h.p ≫ (rightHomologyData K e hj' hi hi' hk hk' h).g' = (K.extend e).d j' k'
⊢ (K.extendXIso e hj').hom ≫ K.d j k ≫ (K.extendXIso e hk'').inv =
    (K.extendXIso e hj').hom ≫ K.d j k ≫ (K.extendXIso e hk'').inv

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
hi : e.BoundaryGE i
⊢ ((K.restrictionXIso e ⋯).hom ≫ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv) ≫
      (K.truncGE'XIsoOpcycles e ⋯ hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (K.truncGE'XIso e ⋯ ⋯).inv =
    (K.restriction e).d i j ≫ (K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ ⋯).inv

Tactic:
]

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
hi : e.BoundaryGE i
⊢ ((K.restrictionXIso e ⋯).hom ≫ K.pOpcycles (e.f i) ≫ (K.truncGE'XIsoOpcycles e ⋯ hi).inv) ≫
      (K.truncGE'XIsoOpcycles e ⋯ hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (K.truncGE'XIso e ⋯ ⋯).inv =
    (K.restriction e).d i j ≫ (K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ ⋯).inv
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : 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✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ K.homologyπ j' = K.homologyπ j'

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
hi : ¬e.BoundaryGE i
⊢ ((K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ hi).inv) ≫
      (K.truncGE'XIso e ⋯ hi).hom ≫ K.d (e.f i) (e.f j) ≫ (K.truncGE'XIso e ⋯ ⋯).inv =
    (K.restriction e).d i j ≫ (K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ ⋯).inv

Tactic:
]

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
hi : ¬e.BoundaryGE i
⊢ ((K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ hi).inv) ≫
      (K.truncGE'XIso e ⋯ hi).hom ≫ K.d (e.f i) (e.f j) ≫ (K.truncGE'XIso e ⋯ ⋯).inv =
    (K.restriction e).d i j ≫ (K.restrictionXIso e ⋯).hom ≫ (K.truncGE'XIso e ⋯ ⋯).inv
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject 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 = k

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ K.iCycles j = (K.extendCyclesIso e hj').inv ≫ (K.extend e).iCycles j' ≫ (K.extendXIso e hj').hom

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ K.iCycles j = (K.extendCyclesIso e hj').inv ≫ (K.extend e).iCycles j' ≫ (K.extendXIso e hj').hom
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : 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✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.sc j').homologyπ ≫
      ShortComplex.homologyMap
          ((natIsoSc' C c' i' j' k' hi'' hk'').hom.app K ≫
            (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv ≫
              (natIsoSc' C c i j k hi hk).inv.app (K.restriction e)) ≫
        (K.restriction e).homologyι j =
    (K.sc j').homologyπ ≫ K.homologyι j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv

Tactic:
]

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : 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✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.sc j').homologyπ ≫
      ShortComplex.homologyMap
          ((natIsoSc' C c' i' j' k' hi'' hk'').hom.app K ≫
            (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv ≫
              (natIsoSc' C c i j k hi hk).inv.app (K.restriction e)) ≫
        (K.restriction e).homologyι j =
    (K.sc j').homologyπ ≫ K.homologyι j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv