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
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.iCycles j' ≫ (K.sc j').pOpcycles) (K.homologyπ j' ≫ (K.sc j').homologyι)
have e_a : Eq (α := K.cycles j' ⟶ (K.sc j').opcycles) (K.homologyπ j' ≫ (K.sc j').homologyι) (K.iCycles j' ≫ (K.sc j').pOpcycles)
Tactic: symm
-- 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.cycles j' ⟶ (K.restriction e).homology j)
    (K.homologyπ j' ≫ Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
    (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
have rw : Eq (α := K.cycles j' ⟶ K.homology j')
  (CategoryStruct.comp (Y := (K.restriction e).homology j)
    (K.homologyπ j' ≫ Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
    (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
  (CategoryStruct.comp (Y := (K.restriction e).homology j)
    (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
    (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
Tactic: rw [← cancel_mono (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom,
    assoc, assoc, Iso.inv_hom_id, homologyπ_restrictionHomologyIso_hom, comp_id,
    Iso.inv_hom_id_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
rw :
  Eq (α := K.cycles j' ⟶ K.homology j')
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (K.homologyπ j' ≫ Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
⊢ Eq (α := K.cycles j' ⟶ (K.restriction e).homology j)
    (K.homologyπ j' ≫ Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
    (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
have rw₁ : Eq (α := K.cycles j' ⟶ K.homology j')
  (K.homologyπ j' ≫
    CategoryStruct.comp (Y := (K.restriction e).homology j)
      (Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
  (CategoryStruct.comp (Y := (K.restriction e).homology j)
    (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
    (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
Tactic: rw [← cancel_mono (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom,
    assoc, assoc, Iso.inv_hom_id, homologyπ_restrictionHomologyIso_hom, comp_id,
    Iso.inv_hom_id_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
rw :
  Eq (α := K.cycles j' ⟶ K.homology j')
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (K.homologyπ j' ≫ Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
rw₁ :
  Eq (α := K.cycles j' ⟶ K.homology j')
    (K.homologyπ j' ≫
      CategoryStruct.comp (Y := (K.restriction e).homology j)
        (Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
        (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
⊢ Eq (α := K.cycles j' ⟶ (K.restriction e).homology j)
    (K.homologyπ j' ≫ Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
    (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
have rw₂ : Eq (α := K.cycles j' ⟶ K.homology j')
  (K.homologyπ j' ≫
    CategoryStruct.comp (Y := (K.restriction e).homology j)
      (Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
  (CategoryStruct.comp (Y := (K.restriction e).cycles j) (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk''))
    ((K.restriction e).homologyπ j ≫ Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
Tactic: rw [← cancel_mono (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom,
    assoc, assoc, Iso.inv_hom_id, homologyπ_restrictionHomologyIso_hom, comp_id,
    Iso.inv_hom_id_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
rw :
  Eq (α := K.cycles j' ⟶ K.homology j')
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (K.homologyπ j' ≫ Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
rw₁ :
  Eq (α := K.cycles j' ⟶ K.homology j')
    (K.homologyπ j' ≫
      CategoryStruct.comp (Y := (K.restriction e).homology j)
        (Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
        (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
rw₂ :
  Eq (α := K.cycles j' ⟶ K.homology j')
    (K.homologyπ j' ≫
      CategoryStruct.comp (Y := (K.restriction e).homology j)
        (Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
        (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
    (CategoryStruct.comp (Y := (K.restriction e).cycles j) (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk''))
      ((K.restriction e).homologyπ j ≫ Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
⊢ Eq (α := K.cycles j' ⟶ (K.restriction e).homology j)
    (K.homologyπ j' ≫ Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
    (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
have rw₃ : K.homologyπ j' ≫ 𝟙 (K.homology j') =
  CategoryStruct.comp (Y := (K.restriction e).cycles j) (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk''))
    ((K.restriction e).homologyπ j ≫ Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
Tactic: rw [← cancel_mono (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom,
    assoc, assoc, Iso.inv_hom_id, homologyπ_restrictionHomologyIso_hom, comp_id,
    Iso.inv_hom_id_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
rw :
  Eq (α := K.cycles j' ⟶ K.homology j')
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (K.homologyπ j' ≫ Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
rw₁ :
  Eq (α := K.cycles j' ⟶ K.homology j')
    (K.homologyπ j' ≫
      CategoryStruct.comp (Y := (K.restriction e).homology j)
        (Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
        (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
    (CategoryStruct.comp (Y := (K.restriction e).homology j)
      (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
      (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
rw₂ :
  Eq (α := K.cycles j' ⟶ K.homology j')
    (K.homologyπ j' ≫
      CategoryStruct.comp (Y := (K.restriction e).homology j)
        (Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
        (Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
    (CategoryStruct.comp (Y := (K.restriction e).cycles j) (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk''))
      ((K.restriction e).homologyπ j ≫ Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'')))
rw₃ :
  K.homologyπ j' ≫ 𝟙 (K.homology j') =
    CategoryStruct.comp (Y := (K.restriction e).cycles j) (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk''))
      ((K.restriction e).homologyπ j ≫ Iso.hom (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
⊢ Eq (α := K.cycles j' ⟶ (K.restriction e).homology j)
    (K.homologyπ j' ≫ Iso.inv (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk''))
    (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ (K.restriction e).homologyπ j)
have rw₄ : K.homologyπ j' ≫ 𝟙 (K.homology j') =
  CategoryStruct.comp (Y := (K.restriction e).cycles j) (Iso.inv (K.restrictionCyclesIso e j k hk hj' hk' hk''))
    (Iso.hom (K.restrictionCyclesIso e j k hk hj' hk' hk'') ≫ K.homologyπ j')
Tactic: rw [← cancel_mono (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom,
    assoc, assoc, Iso.inv_hom_id, homologyπ_restrictionHomologyIso_hom, comp_id,
    Iso.inv_hom_id_assoc]
-- 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.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''))
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.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''))
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.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''))
have 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''))
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.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''))
have 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)
Tactic: rw [← ShortComplex.homologyMap_comp, ← ShortComplex.homologyMap_comp, assoc,
    ← cancel_epi (K.sc j').homologyπ]
-- 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.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)
have 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)
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.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)
have dsimp : Eq (α := (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
  ((K.sc j').iCycles ≫
      (𝟙 (K.X j') ≫
          CategoryStruct.comp (Y := K.X (e.f j)) (Iso.inv (K.restrictionXIso e hj') : K.X j' ⟶ K.X (e.f j))
            (𝟙 (K.X (e.f j)) : K.X (e.f j) ⟶ K.X (e.f j))) ≫
        ((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)
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.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
    ((K.sc j').iCycles ≫
        (𝟙 (K.X j') ≫
            CategoryStruct.comp (Y := K.X (e.f j)) (Iso.inv (K.restrictionXIso e hj') : K.X j' ⟶ K.X (e.f j))
              (𝟙 (K.X (e.f j)) : K.X (e.f j) ⟶ K.X (e.f j))) ≫
          ((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)
have rw : Eq (α := (K.sc j').cycles ⟶ ((K.restriction e).sc j).opcycles)
  ((K.sc j').iCycles ≫
      CategoryStruct.comp (Y := K.X (e.f j)) (Iso.inv (K.restrictionXIso e hj') : K.X j' ⟶ K.X (e.f j))
        (((K.restriction e).sc j).pOpcycles : ((K.restriction e).sc j).X₂ ⟶ ((K.restriction e).sc j).opcycles) :
    (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)
Tactic: rw [comp_id, id_comp]