awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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
⊢ 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
have rw₄ : Eq (α := (K.restriction e).X i ⟶ K.opcycles j') (Iso.hom (K.restrictionXIso e hi') ≫ 0) 0
Tactic: rw [restriction_d_eq _ _ hi' hj', assoc, assoc, Iso.inv_hom_id_assoc,
        d_pOpcycles, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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
⊢ 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
have rw₅ : Eq.{v_1 + 1} (α := (K.restriction e).X i ⟶ K.opcycles j') 0 0
Tactic: rw [restriction_d_eq _ _ hi' hj', assoc, assoc, Iso.inv_hom_id_assoc,
        d_pOpcycles, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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
⊢ 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
have 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)
Tactic: rw [← cancel_epi (K.restrictionXIso e hi').hom, ← restriction_d_eq_assoc,
        comp_zero, d_pOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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)
⊢ 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
have 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)
Tactic: rw [← cancel_epi (K.restrictionXIso e hi').hom, ← restriction_d_eq_assoc,
        comp_zero, d_pOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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)
⊢ 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
have rw₂ : Eq (α := (K.restriction e).X i ⟶ (K.restriction e).opcycles j) ((K.restriction e).d i j ≫ (K.restriction e).pOpcycles j)
  0
Tactic: rw [← cancel_epi (K.restrictionXIso e hi').hom, ← restriction_d_eq_assoc,
        comp_zero, d_pOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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
⊢ 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
have rw₃ : Eq.{v_1 + 1} (α := (K.restriction e).X i ⟶ (K.restriction e).opcycles j) 0 0
Tactic: rw [← cancel_epi (K.restrictionXIso e hi').hom, ← restriction_d_eq_assoc,
        comp_zero, d_pOpcycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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
have 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
Tactic: subst hi hk
Cleared hypotheses: i, k, hi, hk, hi', hk'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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
have 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
Tactic: subst hi'' hk''
Cleared hypotheses: i', k', hi', hk', hi'', hk''
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (hypothesis)
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
⊢ 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')
have this : ((K.restriction e).sc' i j k).HasHomology
Tactic: have : ((K.restriction e).sc' i j k).HasHomology := by subst hi hk; assumption
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (hypothesis)
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
⊢ 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')
have this₁ : (K.sc' i' j' k').HasHomology
Tactic: have : (K.sc' i' j' k').HasHomology := by subst hi'' hk''; assumption
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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.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')
have 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')
Tactic: dsimp [restrictionHomologyIso, homologyIsoSc']
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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.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')
have 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)
Tactic: rw [← ShortComplex.homologyMap_comp, ← ShortComplex.homologyMap_comp,
    ← cancel_mono (K.sc j').homologyι, assoc, assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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.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)
have 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)
Tactic: apply (ShortComplex.π_homologyMap_ι _).trans
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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.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)
have 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)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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.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)
have 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)
Tactic: rw [comp_id, id_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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.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)
have 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)
Tactic: apply (K.restrictionCyclesIso_hom_iCycles_assoc e j k hk hj' hk' hk'' _).symm.trans
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.RestrictionHomology (goal)
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_2} C c'
e : c.Embedding c'
inst_2 : e.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.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)
have e_a : Eq (α := K.cycles j' ⟶ (K.sc j').opcycles) (K.iCycles j' ≫ (K.sc j').pOpcycles) (K.homologyπ j' ≫ (K.sc j').homologyι)
Tactic: congr 1