awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} 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'' : Iso.hom (K.extendXIso e hj') ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : ¬c.Rel j k
h₁ : f' = 0
⊢ Cofork.π cocone ≫ f'' = Cofork.π cocone ≫ 0
have rw : ¬c.Rel j (c.next j)
Tactic: rw [← cancel_epi (extendXIso K e hj').hom, hf'', comp_zero, comp_zero,
        K.extend_d_from_eq_zero e j' k' j hj']
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} 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'' : Iso.hom (K.extendXIso e hj') ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : ¬c.Rel j k
h₁ : f' = 0
⊢ φ ≫ f' = 0 ↔ φ ≫ f'' = 0
have h₂ : f'' = 0
Tactic: have h₂ : f'' = 0 := by
      apply Cofork.IsColimit.hom_ext hcocone
      rw [← cancel_epi (extendXIso K e hj').hom, hf'', comp_zero, comp_zero,
        K.extend_d_from_eq_zero e j' k' j hj']
      rw [hk]
      exact hjk
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_1} 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 (Y := (CokernelCofork.ofπ (K.d j k) ⋯).pt) (hcocone.desc (CokernelCofork.ofπ (K.d j k) ⋯))
hcone : IsLimit cone
⊢ Fork.ι cone ≫
      IsColimit.desc (isColimitCokernelCofork K e hj' hi hi' cocone hcocone)
        (CokernelCofork.ofπ ((K.extend e).d j' k') ⋯) =
    0
have rw : Eq (α := cone.pt ⟶ (CokernelCofork.ofπ (K.d j k) sorry).pt) (Fork.ι cone ≫ hcocone.desc (CokernelCofork.ofπ (K.d j k) sorry)) 0
Tactic: rw [← d_comp_desc_eq_zero_iff K e hj' hi hi' hk hk' cocone hcocone]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_1} 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.extend e).sc' i' j' k').f ≫ Iso.hom (K.extendXIso e hj') ≫ h.p = 0
have dsimp : (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ h.p = 0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_1} 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.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ h.p = 0
have rw : K.d i j ≫ h.p = 0
Tactic: rw [← d_comp_eq_zero_iff K e hj' hi hi']
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_1} 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.ι ≫
      IsColimit.desc (isColimitCokernelCofork K e hj' hi hi' (CokernelCofork.ofπ h.p ⋯) h.hp)
        (CokernelCofork.ofπ ((K.extend e).sc' i' j' k').g ⋯) =
    0
have dsimp : h.ι ≫
    IsColimit.desc (isColimitCokernelCofork K e hj' hi hi' (CokernelCofork.ofπ h.p sorry) h.hp)
      (CokernelCofork.ofπ ((K.extend e).d j' k') sorry) =
  0
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_1} 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.ι ≫
      IsColimit.desc (isColimitCokernelCofork K e hj' hi hi' (CokernelCofork.ofπ h.p ⋯) h.hp)
        (CokernelCofork.ofπ ((K.extend e).d j' k') ⋯) =
    0
have rw : Eq (α := h.H ⟶ (CokernelCofork.ofπ (K.d j k) sorry).pt) (h.ι ≫ h.hp.desc (CokernelCofork.ofπ (K.d j k) sorry)) 0
Tactic: rw [← d_comp_desc_eq_zero_iff K e hj' hi hi' hk hk' _ h.hp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} 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'
⊢ Eq (α :=
    ShortComplex.RightHomologyData.Q (S := (K.extend e).sc' i' j' k') (rightHomologyData K e hj' hi hi' hk hk' h) ⟶
      ((K.extend e).sc' i' j' k').X₃)
    (ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h))
    (h.g' ≫ Iso.inv (K.extendXIso e hk''))
have rw : Eq (α := (K.extend e).X j' ⟶ ((K.extend e).sc' i' j' k').X₃)
  (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h))
  (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ h.g' ≫ Iso.inv (K.extendXIso e hk''))
Tactic: rw [← cancel_epi h.p, ← cancel_epi (extendXIso K e hj').hom]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} 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'
⊢ Eq (α := (K.extend e).X j' ⟶ ((K.extend e).sc' i' j' k').X₃)
    (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h))
    (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ h.g' ≫ Iso.inv (K.extendXIso e hk''))
have this : CategoryStruct.comp (Y :=
    ShortComplex.RightHomologyData.Q (S := (K.extend e).sc' i' j' k') (rightHomologyData K e hj' hi hi' hk hk' h))
    (ShortComplex.RightHomologyData.p (rightHomologyData K e hj' hi hi' hk hk' h))
    (ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h)) =
  ((K.extend e).sc' i' j' k').g
Tactic: have := (rightHomologyData K e hj' hi hi' hk hk' h).p_g'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} 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 :
  (Iso.hom (K.extendXIso e hj') ≫ h.p) ≫ ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h) =
    (K.extend e).d j' k'
⊢ Eq (α := (K.extend e).X j' ⟶ ((K.extend e).sc' i' j' k').X₃)
    (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h))
    (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ h.g' ≫ Iso.inv (K.extendXIso e hk''))
have this₁ : Iso.hom (K.extendXIso e hj') ≫ h.p ≫ ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h) =
  (K.extend e).d j' k'
Tactic: rw [assoc] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} 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 :
  Iso.hom (K.extendXIso e hj') ≫ h.p ≫ ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h) =
    (K.extend e).d j' k'
⊢ Eq (α := (K.extend e).X j' ⟶ ((K.extend e).sc' i' j' k').X₃)
    (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h))
    (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ h.g' ≫ Iso.inv (K.extendXIso e hk''))
have rw : (K.extend e).d j' k' = Iso.hom (K.extendXIso e hj') ≫ h.p ≫ h.g' ≫ Iso.inv (K.extendXIso e hk'')
Tactic: rw [this, K.extend_d_eq e hj' hk'', h.p_g'_assoc, shortComplexFunctor'_obj_g]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} 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 :
  Iso.hom (K.extendXIso e hj') ≫ h.p ≫ ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h) =
    (K.extend e).d j' k'
rw : (K.extend e).d j' k' = Iso.hom (K.extendXIso e hj') ≫ h.p ≫ h.g' ≫ Iso.inv (K.extendXIso e hk'')
⊢ Eq (α := (K.extend e).X j' ⟶ ((K.extend e).sc' i' j' k').X₃)
    (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h))
    (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ h.g' ≫ Iso.inv (K.extendXIso e hk''))
have rw₁ : Eq (α := (K.extend e).X j' ⟶ ((K.extend e).sc' i' j' k').X₃)
  (Iso.hom (K.extendXIso e hj') ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk''))
  (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ h.g' ≫ Iso.inv (K.extendXIso e hk''))
Tactic: rw [this, K.extend_d_eq e hj' hk'', h.p_g'_assoc, shortComplexFunctor'_obj_g]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} 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 :
  Iso.hom (K.extendXIso e hj') ≫ h.p ≫ ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h) =
    (K.extend e).d j' k'
rw : (K.extend e).d j' k' = Iso.hom (K.extendXIso e hj') ≫ h.p ≫ h.g' ≫ Iso.inv (K.extendXIso e hk'')
rw₁ :
  Eq (α := (K.extend e).X j' ⟶ ((K.extend e).sc' i' j' k').X₃)
    (Iso.hom (K.extendXIso e hj') ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk''))
    (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ h.g' ≫ Iso.inv (K.extendXIso e hk''))
⊢ Eq (α := (K.extend e).X j' ⟶ ((K.extend e).sc' i' j' k').X₃)
    (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h))
    (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ h.g' ≫ Iso.inv (K.extendXIso e hk''))
have rw₂ : Eq (α := (K.extend e).X j' ⟶ ((K.extend e).sc' i' j' k').X₃)
  (Iso.hom (K.extendXIso e hj') ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk''))
  (Iso.hom (K.extendXIso e hj') ≫ (K.sc' i j k).g ≫ Iso.inv (K.extendXIso e hk''))
Tactic: rw [this, K.extend_d_eq e hj' hk'', h.p_g'_assoc, shortComplexFunctor'_obj_g]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} 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 :
  Iso.hom (K.extendXIso e hj') ≫ h.p ≫ ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h) =
    (K.extend e).d j' k'
rw : (K.extend e).d j' k' = Iso.hom (K.extendXIso e hj') ≫ h.p ≫ h.g' ≫ Iso.inv (K.extendXIso e hk'')
rw₁ :
  Eq (α := (K.extend e).X j' ⟶ ((K.extend e).sc' i' j' k').X₃)
    (Iso.hom (K.extendXIso e hj') ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk''))
    (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ h.g' ≫ Iso.inv (K.extendXIso e hk''))
rw₂ :
  Eq (α := (K.extend e).X j' ⟶ ((K.extend e).sc' i' j' k').X₃)
    (Iso.hom (K.extendXIso e hj') ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk''))
    (Iso.hom (K.extendXIso e hj') ≫ (K.sc' i j k).g ≫ Iso.inv (K.extendXIso e hk''))
⊢ Eq (α := (K.extend e).X j' ⟶ ((K.extend e).sc' i' j' k').X₃)
    (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ ShortComplex.RightHomologyData.g' (rightHomologyData K e hj' hi hi' hk hk' h))
    (Iso.hom (K.extendXIso e hj') ≫ h.p ≫ h.g' ≫ Iso.inv (K.extendXIso e hk''))
have rw₃ : Eq (α := (K.extend e).X j' ⟶ ((K.extend e).sc' i' j' k').X₃)
  (Iso.hom (K.extendXIso e hj') ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk''))
  (Iso.hom (K.extendXIso e hj') ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk''))
Tactic: rw [this, K.extend_d_eq e hj' hk'', h.p_g'_assoc, shortComplexFunctor'_obj_g]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
j' : ι'
⊢ (K.extend e).HasHomology j'
have pos : ∀ (h : ∃ (j : ι), e.f j = j'), (K.extend e).HasHomology j'
Tactic: by_cases h : ∃ j, e.f j = j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
j' : ι'
pos : ∀ (h : ∃ (j : ι), e.f j = j'), (K.extend e).HasHomology j'
⊢ (K.extend e).HasHomology j'
have neg : ∀ (h : ¬∃ (j : ι), e.f j = j'), (K.extend e).HasHomology j'
Tactic: by_cases h : ∃ j, e.f j = j'
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
j' : ι'
h : ∃ (j : ι), e.f j = j'
⊢ (K.extend e).HasHomology j'
have pos : ∀ (j : ι), (K.extend e).HasHomology (e.f j)
Tactic: obtain ⟨j, rfl⟩ := h
Cleared hypotheses: j', h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K L M : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst_3 : ∀ (j : ι), K.HasHomology j
j' : ι'
h : ¬∃ (j : ι), e.f j = j'
⊢ (K.extend e).HasHomology j'
have hj : IsZero.{v_1, u_3} ((K.extend e).X j')
Tactic: have hj := isZero_extend_X K e j' (by tauto)
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
⊢ (K.extend e).ExactAt j' ↔ K.ExactAt j
have simp : IsZero.{v_1, u_3} ((K.extend e).homology j') ↔ IsZero.{v_1, u_3} (K.homology j)
Tactic: simp only [HomologicalComplex.exactAt_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
⊢ Eq (α := (K.extend e).cycles j' ⟶ K.X j)
    (CategoryStruct.comp (Y := K.cycles j) (Iso.hom (K.extendCyclesIso e hj')) (K.iCycles j))
    ((K.extend e).iCycles j' ≫ Iso.hom (K.extendXIso e hj'))
have rw : Eq (α := K.cycles j ⟶ K.X j) (K.iCycles j)
  (CategoryStruct.comp (Y := (K.extend e).cycles j') (Iso.inv (K.extendCyclesIso e hj'))
    ((K.extend e).iCycles j' ≫ Iso.hom (K.extendXIso e hj')))
Tactic: rw [← cancel_epi (K.extendCyclesIso e hj').inv, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
⊢ Eq (α := K.cycles j ⟶ K.X j) (K.iCycles j)
    (CategoryStruct.comp (Y := (K.extend e).cycles j') (Iso.inv (K.extendCyclesIso e hj'))
      ((K.extend e).iCycles j' ≫ Iso.hom (K.extendXIso e hj')))
have dsimp : Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
  (CategoryStruct.comp (Y := (K.extend e).cycles j')
    (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫
      Iso.inv
        (ShortComplex.LeftHomologyData.cyclesIso
          (ShortComplex.HomologyData.left (extend.homologyData' K e hj' sorry sorry (K.sc j).homologyData))))
    (((K.extend e).sc j').iCycles ≫ Iso.hom (K.extendXIso e hj')))
Tactic: dsimp [extendCyclesIso, iCycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
⊢ Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
    (CategoryStruct.comp (Y := (K.extend e).cycles j')
      (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫
        Iso.inv
          (ShortComplex.LeftHomologyData.cyclesIso
            (ShortComplex.HomologyData.left (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData))))
      (((K.extend e).sc j').iCycles ≫ Iso.hom (K.extendXIso e hj')))
have rw : Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
  (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫
    ShortComplex.LeftHomologyData.i
        (ShortComplex.HomologyData.left (extend.homologyData' K e hj' sorry sorry (K.sc j).homologyData)) ≫
      Iso.hom (K.extendXIso e hj'))
Tactic: rw [assoc, ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
⊢ Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
    (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫
      ShortComplex.LeftHomologyData.i
          (ShortComplex.HomologyData.left (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData)) ≫
        Iso.hom (K.extendXIso e hj'))
have dsimp : Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
  (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫
    CategoryStruct.comp (Y := (K.extend e).X j') ((K.sc j).homologyData.left.i ≫ Iso.inv (K.extendXIso e hj'))
      (Iso.hom (K.extendXIso e hj')))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.Embedding.ExtendHomology (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
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst_3 : K.HasHomology j
inst_4 : (K.extend e).HasHomology j'
⊢ Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
    (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫
      CategoryStruct.comp (Y := (K.extend e).X j') ((K.sc j).homologyData.left.i ≫ Iso.inv (K.extendXIso e hj'))
        (Iso.hom (K.extendXIso e hj')))
have rw : Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles
  (Iso.hom (K.sc j).homologyData.left.cyclesIso ≫
    (K.sc j).homologyData.left.i ≫
      CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj')) (Iso.hom (K.extendXIso e hj')))
Tactic: rw [assoc, Iso.inv_hom_id, comp_id,
    ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i]