awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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
rw : Eq (α := h.H ⟶ (CokernelCofork.ofπ (K.d j k) ⋯).pt) (h.ι ≫ h.hp.desc (CokernelCofork.ofπ (K.d j k) ⋯)) 0
⊢ h.ι ≫
      IsColimit.desc (isColimitCokernelCofork K e hj' hi hi' (CokernelCofork.ofπ h.p ⋯) h.hp)
        (CokernelCofork.ofπ ((K.extend e).d j' k') ⋯) =
    0

Tactic:
rw [← d_comp_desc_eq_zero_iff K e hj' hi hi' hk hk' _ h.hp]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.hp, HomologicalComplex.extend.rightHomologyData.d_comp_desc_eq_zero_iff
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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
⊢ Eq (α := h.H ⟶ (CokernelCofork.ofπ (K.d j k) ⋯).pt) (h.ι ≫ h.hp.desc (CokernelCofork.ofπ (K.d j k) ⋯)) 0

Tactic:
h.wι

Premises used: CategoryTheory.ShortComplex.RightHomologyData.wι
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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
⊢ Eq (α := h.H ⟶ (CokernelCofork.ofπ (K.d j k) ⋯).pt) (h.ι ≫ h.hp.desc (CokernelCofork.ofπ (K.d j k) ⋯)) 0

Tactic:
exact h.wι

Premises used: CategoryTheory.ShortComplex.RightHomologyData.wι
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
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''))
⊢ 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''))

Tactic:
rw [← cancel_epi h.p, ← cancel_epi (extendXIso K e hj').hom]

Premises used: CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, HomologicalComplex.extendXIso, CategoryTheory.ShortComplex.RightHomologyData.p
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
⊢ 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'
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
⊢ 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

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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''))
rw₃ 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''))
⊢ 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 [this, K.extend_d_eq e hj' hk'', h.p_g'_assoc, shortComplexFunctor'_obj_g]

Premises used: CategoryTheory.ShortComplex.RightHomologyData.p_g'_assoc, HomologicalComplex.shortComplexFunctor'_obj_g, HomologicalComplex.extend_d_eq
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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
⊢ (K.extend e).HasHomology j'

Tactic:
ShortComplex.HasHomology.mk'
    (homologyData' K e hj' rfl rfl ((K.sc j).homologyData))

Premises used: HomologicalComplex.extend.homologyData', HomologicalComplex.sc, CategoryTheory.ShortComplex.HasHomology.mk', rfl, CategoryTheory.ShortComplex.homologyData
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
j : ι
inst_3 : K.HasHomology j
⊢ (K.extend e).HasHomology (e.f j)

Tactic:
hasHomology K e rfl

Premises used: HomologicalComplex.extend.hasHomology, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
neg : ∀ (h : ¬∃ (j : ι), e.f j = j'), (K.extend e).HasHomology j'
⊢ (K.extend e).HasHomology j'

Tactic:
by_cases h : ∃ j, e.f j = j'
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
pos : ∀ (j : ι), (K.extend e).HasHomology (e.f j)
⊢ (K.extend e).HasHomology j'

Tactic:
obtain ⟨j, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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 (e.f j)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
tauto tauto₁ : ∀ (i : ι), e.f i ≠ j'
tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : ∀ (i : ι), e.f i = j' → False
⊢ ∀ (i : ι), e.f i ≠ j'

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
⊢ IsZero.{v_1, u_3} ((K.extend e).X j')

Tactic:
have hj := isZero_extend_X K e j' (by tauto)
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
hj : IsZero.{v_1, u_3} ((K.extend e).X j')
⊢ (K.extend e).HasHomology j'

Tactic:
ShortComplex.HasHomology.mk'
      (ShortComplex.HomologyData.ofZeros _ (hj.eq_of_tgt _ _) (hj.eq_of_src _ _))

Premises used: CategoryTheory.ShortComplex.HasHomology.mk', CategoryTheory.ShortComplex.HomologyData.ofZeros, CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
hj : IsZero.{v_1, u_3} ((K.extend e).X j')
⊢ (K.extend e).HasHomology j'

Tactic:
exact ShortComplex.HasHomology.mk'
      (ShortComplex.HomologyData.ofZeros _ (hj.eq_of_tgt _ _) (hj.eq_of_src _ _))

Premises used: CategoryTheory.ShortComplex.HasHomology.mk', CategoryTheory.ShortComplex.HomologyData.ofZeros
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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' : ι'
hj' : ∀ (j : ι), e.f j ≠ j'
⊢ (K.extend e).ExactAt j'

Tactic:
exactAt_of_isSupported _ e j' hj'

Premises used: HomologicalComplex.exactAt_of_isSupported
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
simp : IsZero.{v_1, u_3} ((K.extend e).homology j') ↔ IsZero.{v_1, u_3} (K.homology j)
⊢ (K.extend e).ExactAt j' ↔ K.ExactAt j

Tactic:
simp only [HomologicalComplex.exactAt_iff_isZero_homology]

Premises used: HomologicalComplex.exactAt_iff_isZero_homology
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
⊢ IsZero.{v_1, u_3} ((K.extend e).homology j') ↔ IsZero.{v_1, u_3} (K.homology j)

Tactic:
(K.extendHomologyIso e hj').isZero_iff

Premises used: HomologicalComplex.extendHomologyIso, CategoryTheory.Iso.isZero_iff
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
⊢ IsZero.{v_1, u_3} ((K.extend e).homology j') ↔ IsZero.{v_1, u_3} (K.homology j)

Tactic:
exact (K.extendHomologyIso e hj').isZero_iff

Premises used: HomologicalComplex.extendHomologyIso, CategoryTheory.Iso.isZero_iff
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
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')))
⊢ 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'))

Tactic:
rw [← cancel_epi (K.extendCyclesIso e hj').inv, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Iso.inv_hom_id_assoc, HomologicalComplex.extendCyclesIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
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' ⋯ ⋯ (K.sc j).homologyData))))
      (((K.extend e).sc j').iCycles ≫ Iso.hom (K.extendXIso e hj')))
⊢ 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:
dsimp [extendCyclesIso, iCycles]

Premises used: HomologicalComplex.iCycles, HomologicalComplex.extendCyclesIso
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
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' ⋯ ⋯ (K.sc j).homologyData)) ≫
        Iso.hom (K.extendXIso e hj'))
⊢ 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')))

Tactic:
rw [assoc, ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles_assoc
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
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')))
⊢ 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'))

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
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')))
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 ≫ 𝟙 (K.X j))
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)
rw₃ rw₄ : Eq (α := K.cycles j ⟶ K.X j) (K.sc j).iCycles (K.sc j).iCycles
⊢ 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:
rw [assoc, Iso.inv_hom_id, comp_id,
    ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.Category.comp_id, CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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.extend e).X j')
    (CategoryStruct.comp (Y := (K.extend e).cycles j') (Iso.inv (K.extendCyclesIso e hj')) ((K.extend e).iCycles j'))
    (K.iCycles j ≫ Iso.inv (K.extendXIso e hj'))

Tactic:
simp only [← cancel_epi (K.extendCyclesIso e hj').hom, Iso.hom_inv_id_assoc,
    extendCyclesIso_hom_iCycles_assoc, Iso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, CategoryTheory.Iso.hom_inv_id_assoc, HomologicalComplex.extendCyclesIso, HomologicalComplex.extendCyclesIso_hom_iCycles_assoc, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
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'
dsimp :
  Eq (α := (K.extend e).cycles j' ⟶ K.homology j)
    (CategoryStruct.comp (Y := (K.extend e).homology j') ((K.extend e).sc j').homologyπ
        (CategoryStruct.comp (Y := (K.sc j).homologyData.left.H)
          (Iso.hom
              (ShortComplex.LeftHomologyData.homologyIso
                (ShortComplex.HomologyData.left (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData))) :
            (K.extend e).homology j' ⟶ (K.sc j).homologyData.left.H)
          (Iso.inv (K.sc j).homologyData.left.homologyIso)) :
      (K.extend e).cycles j' ⟶ K.homology j)
    (CategoryStruct.comp (Y := K.cycles j) (Iso.hom (K.extendCyclesIso e hj')) (K.sc j).homologyπ :
      (K.extend e).cycles j' ⟶ K.homology j)
⊢ Eq (α := (K.extend e).cycles j' ⟶ K.homology j) ((K.extend e).homologyπ j' ≫ Iso.hom (K.extendHomologyIso e hj'))
    (Iso.hom (K.extendCyclesIso e hj') ≫ K.homologyπ j)

Tactic:
dsimp [extendHomologyIso, homologyπ]

Premises used: HomologicalComplex.homologyπ, HomologicalComplex.extendHomologyIso