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'
⊢ 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')
have subst : ∀ (hi'' : c'.prev (e.f j) = i') (hk'' : c'.next (e.f j) = e.f k),
  Iso.hom (K.restrictionXIso e sorry) ≫ (K.sc' i' (e.f j) (e.f k)).g =
    ((K.restriction e).sc' i j k).g ≫ Iso.hom (K.restrictionXIso e sorry)
Tactic: subst hj' hk'
Cleared hypotheses: j', k', hj', 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
⊢ 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
have 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
Tactic: rw [assoc, ← cancel_mono (K.restrictionXIso e hk').inv, assoc, assoc, ← restriction_d_eq,
        iCycles_d, zero_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
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
⊢ 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
have 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'))
Tactic: rw [assoc, ← cancel_mono (K.restrictionXIso e hk').inv, assoc, assoc, ← restriction_d_eq,
        iCycles_d, zero_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
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'))
⊢ 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
have 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'))
Tactic: rw [assoc, ← cancel_mono (K.restrictionXIso e hk').inv, assoc, assoc, ← restriction_d_eq,
        iCycles_d, zero_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
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'))
⊢ 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
have 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'))
Tactic: rw [assoc, ← cancel_mono (K.restrictionXIso e hk').inv, assoc, assoc, ← restriction_d_eq,
        iCycles_d, zero_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
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'))
⊢ 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
have 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'))
Tactic: rw [assoc, ← cancel_mono (K.restrictionXIso e hk').inv, assoc, assoc, ← restriction_d_eq,
        iCycles_d, zero_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
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'))
⊢ 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
have rw₅ : Eq (α := (K.restriction e).cycles j ⟶ (K.restriction e).X k) 0 (0 ≫ Iso.inv (K.restrictionXIso e hk'))
Tactic: rw [assoc, ← cancel_mono (K.restrictionXIso e hk').inv, assoc, assoc, ← restriction_d_eq,
        iCycles_d, zero_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
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'))
⊢ 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
have rw₆ : Eq.{v_1 + 1} (α := (K.restriction e).cycles j ⟶ (K.restriction e).X k) 0 0
Tactic: rw [assoc, ← cancel_mono (K.restrictionXIso e hk').inv, assoc, assoc, ← restriction_d_eq,
        iCycles_d, zero_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
⊢ 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
have 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
Tactic: rw [assoc, restriction_d_eq _ _ hj' hk', Iso.inv_hom_id_assoc,
        iCycles_d_assoc, zero_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
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
⊢ 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
have 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
Tactic: rw [assoc, restriction_d_eq _ _ hj' hk', Iso.inv_hom_id_assoc,
        iCycles_d_assoc, zero_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
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
⊢ 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
have rw₂ : Eq (α := K.cycles j' ⟶ (K.restriction e).X k) (K.iCycles j' ≫ K.d j' k' ≫ Iso.inv (K.restrictionXIso e hk')) 0
Tactic: rw [assoc, restriction_d_eq _ _ hj' hk', Iso.inv_hom_id_assoc,
        iCycles_d_assoc, zero_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
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
⊢ 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
have rw₃ : Eq (α := K.cycles j' ⟶ (K.restriction e).X k) (0 ≫ Iso.inv (K.restrictionXIso e hk')) 0
Tactic: rw [assoc, restriction_d_eq _ _ hj' hk', Iso.inv_hom_id_assoc,
        iCycles_d_assoc, zero_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
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
⊢ 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
have rw₄ : Eq.{v_1 + 1} (α := K.cycles j' ⟶ (K.restriction e).X k) 0 0
Tactic: rw [assoc, restriction_d_eq _ _ hj' hk', Iso.inv_hom_id_assoc,
        iCycles_d_assoc, zero_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
⊢ 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')
  (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
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
⊢ 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') ≫
    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
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
⊢ 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') ≫
    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
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
⊢ 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') ≫ K.d i' j' ≫ K.pOpcycles j') 0
Tactic: rw [restriction_d_eq _ _ hi' hj', assoc, assoc, Iso.inv_hom_id_assoc,
        d_pOpcycles, comp_zero]