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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : c.Rel i j
rw : e.f i = c'.prev j'
rw₁ : e.f i = c'.prev (e.f j)
rw₂ rw₃ : e.f i = e.f i
⊢ e.f i = i'

Tactic:
rw [← hi', ← hj', c'.prev_eq' (e.rel hij)]

Premises used: ComplexShape.prev_eq', ComplexShape.Embedding.rel
-- 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' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : c.Rel i j
⊢ e.f i = i'

Tactic:
have hi'' : e.f i = i' := by rw [← hi', ← hj', c'.prev_eq' (e.rel hij)]
-- 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' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : c.Rel i j
hi'' : e.f i = i'
apply : (Iso.hom (K.extendXIso e hi'') ≫ f') ≫ Fork.ι cone = f'' ≫ Fork.ι cone
⊢ Iso.hom (K.extendXIso e hi'') ≫ f' = f''

Tactic:
apply Fork.IsLimit.hom_ext hcone

Premises used: CategoryTheory.Limits.Fork.IsLimit.hom_ext
-- 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' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : c.Rel i j
hi'' : e.f i = i'
rw : Iso.hom (K.extendXIso e hi'') ≫ f' ≫ Fork.ι cone = f'' ≫ Fork.ι cone
rw₁ : Iso.hom (K.extendXIso e hi'') ≫ K.d i j = f'' ≫ Fork.ι cone
rw₂ :
  Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j')
    ((Iso.hom (K.extendXIso e hi'') ≫ K.d i j) ≫ Iso.inv (K.extendXIso e hj'))
    ((f'' ≫ Fork.ι cone) ≫ Iso.inv (K.extendXIso e hj'))
rw₃ :
  Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j')
    (Iso.hom (K.extendXIso e hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj'))
    ((f'' ≫ Fork.ι cone) ≫ Iso.inv (K.extendXIso e hj'))
rw₄ :
  Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j')
    (Iso.hom (K.extendXIso e hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj'))
    (f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj'))
rw₅ : Iso.hom (K.extendXIso e hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
rw₆ rw₇ :
  Eq (α := (K.extend e).X i' ⟶ (K.extend e).X j')
    (Iso.hom (K.extendXIso e hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj'))
    (Iso.hom (K.extendXIso e hi'') ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj'))
⊢ (Iso.hom (K.extendXIso e hi'') ≫ f') ≫ Fork.ι cone = f'' ≫ Fork.ι cone

Tactic:
rw [assoc, hf', ← cancel_mono (extendXIso K e hj').inv, assoc, assoc, hf'',
        K.extend_d_eq e hi'' hj']

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, HomologicalComplex.extend_d_eq, HomologicalComplex.extendXIso, 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'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : c.Rel i j
hi'' : e.f i = i'
⊢ Iso.hom (K.extendXIso e hi'') ≫ f' = f''

Tactic:
have : (K.extendXIso e hi'').hom ≫ f' = f'' := by
      apply Fork.IsLimit.hom_ext hcone
      rw [assoc, hf', ← cancel_mono (extendXIso K e hj').inv, assoc, assoc, hf'',
        K.extend_d_eq e hi'' hj']
-- 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' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : c.Rel i j
hi'' : e.f i = i'
this : Iso.hom (K.extendXIso e hi'') ≫ f' = f''
pos :
  Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) (Iso.hom (K.extendXIso e hi'') ≫ 0) ↔
    f'' ≫ φ = 0
pos₁ : Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) 0 ↔ f'' ≫ φ = 0
pos₂ :
  Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W) ((Iso.hom (K.extendXIso e hi'') ≫ f') ≫ φ) 0
pos₃ pos₄ :
  Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi'') ≫ f' ≫ φ) 0
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0

Tactic:
rw [← cancel_epi (K.extendXIso e hi'').hom, comp_zero, ← this, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, HomologicalComplex.extendXIso
-- 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' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : ¬c.Rel i j
apply : f' ≫ Fork.ι cone = 0 ≫ Fork.ι cone
⊢ f' = 0

Tactic:
apply Fork.IsLimit.hom_ext hcone

Premises used: CategoryTheory.Limits.Fork.IsLimit.hom_ext
-- 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' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : ¬c.Rel i j
⊢ f' ≫ Fork.ι cone = 0 ≫ Fork.ι cone

Tactic:
simp only [zero_comp, hf', K.shape _ _ hij]

Premises used: CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- 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' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : ¬c.Rel i j
⊢ f' = 0

Tactic:
have h₁ : f' = 0 := by
      apply Fork.IsLimit.hom_ext hcone
      simp only [zero_comp, hf', K.shape _ _ hij]
-- 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' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : ¬c.Rel i j
h₁ : f' = 0
apply : f'' ≫ Fork.ι cone = 0 ≫ Fork.ι cone
⊢ f'' = 0

Tactic:
apply Fork.IsLimit.hom_ext hcone

Premises used: CategoryTheory.Limits.Fork.IsLimit.hom_ext
-- 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' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : ¬c.Rel i j
h₁ : f' = 0
rw : ¬c.Rel (c.prev j) j
⊢ f'' ≫ Fork.ι cone = 0 ≫ Fork.ι cone

Tactic:
rw [← cancel_mono (extendXIso K e hj').inv, assoc, hf'', zero_comp, zero_comp,
        K.extend_d_to_eq_zero e i' j' j hj']

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.extend_d_to_eq_zero, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp, HomologicalComplex.extendXIso, 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'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : ¬c.Rel i j
h₁ : f' = 0
rw : ¬c.Rel i j
⊢ ¬c.Rel (c.prev j) j

Tactic:
rw [hi]
-- 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' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : ¬c.Rel i j
h₁ : f' = 0
⊢ ¬c.Rel i j

Tactic:
hij
-- 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' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : ¬c.Rel i j
h₁ : f' = 0
⊢ ¬c.Rel i j

Tactic:
exact hij
-- 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' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : ¬c.Rel i j
h₁ : f' = 0
⊢ f'' = 0

Tactic:
have h₂ : f'' = 0 := by
      apply Fork.IsLimit.hom_ext hcone
      dsimp
      rw [← cancel_mono (extendXIso K e hj').inv, assoc, hf'', zero_comp, zero_comp,
        K.extend_d_to_eq_zero e i' j' j hj']
      rw [hi]
      exact hij
-- 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' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : ¬c.Rel i j
h₁ : f' = 0
h₂ : f'' = 0
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0

Tactic:
simp [h₁, h₂]
-- 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'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
φ : cone.pt ⟶ W
⊢ Eq (α := (KernelFork.ofι (K.d i j) ⋯).pt ⟶ W) (hcone.lift (KernelFork.ofι (K.d i j) ⋯) ≫ φ) 0 ↔
    IsLimit.lift (isLimitKernelFork K e hj' hk hk' cone hcone) (KernelFork.ofι ((K.extend e).d i' j') ⋯) ≫ φ = 0

Tactic:
lift_d_comp_eq_zero_iff' K e hj' hi hi' cone hcone _ (hcone.fac _ _) _
    (IsLimit.fac _ _ WalkingParallelPair.zero) _

Premises used: HomologicalComplex.extend.d, HomologicalComplex.extend.leftHomologyData.lift_d_comp_eq_zero_iff', CategoryTheory.Limits.parallelPair, HomologicalComplex.extend.X
-- 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'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
cocone : CokernelCofork (X := (KernelFork.ofι (K.d i j) ⋯).pt) (hcone.lift (KernelFork.ofι (K.d i j) ⋯))
hcocone : IsColimit cocone
rw : Eq (α := (KernelFork.ofι (K.d i j) ⋯).pt ⟶ cocone.pt) (hcone.lift (KernelFork.ofι (K.d i j) ⋯) ≫ Cofork.π cocone) 0
⊢ IsLimit.lift (isLimitKernelFork K e hj' hk hk' cone hcone) (KernelFork.ofι ((K.extend e).d i' j') ⋯) ≫
      Cofork.π cocone =
    0

Tactic:
rw [← lift_d_comp_eq_zero_iff K e hj' hi hi' hk hk' cone hcone]

Premises used: HomologicalComplex.extend.leftHomologyData.lift_d_comp_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'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
cocone : CokernelCofork (X := (KernelFork.ofι (K.d i j) ⋯).pt) (hcone.lift (KernelFork.ofι (K.d i j) ⋯))
hcocone : IsColimit cocone
⊢ Eq (α := (KernelFork.ofι (K.d i j) ⋯).pt ⟶ cocone.pt) (hcone.lift (KernelFork.ofι (K.d i j) ⋯) ≫ Cofork.π cocone) 0

Tactic:
cocone.condition

Premises used: CategoryTheory.Limits.CokernelCofork.condition
-- 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'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
cocone : CokernelCofork (X := (KernelFork.ofι (K.d i j) ⋯).pt) (hcone.lift (KernelFork.ofι (K.d i j) ⋯))
hcocone : IsColimit cocone
⊢ Eq (α := (KernelFork.ofι (K.d i j) ⋯).pt ⟶ cocone.pt) (hcone.lift (KernelFork.ofι (K.d i j) ⋯) ≫ Cofork.π cocone) 0

Tactic:
exact cocone.condition

Premises used: CategoryTheory.Limits.CokernelCofork.condition
-- 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).LeftHomologyData
dsimp : (h.i ≫ Iso.inv (K.extendXIso e hj')) ≫ (K.extend e).d j' k' = 0
⊢ (h.i ≫ Iso.inv (K.extendXIso e hj')) ≫ ((K.extend e).sc' i' j' k').g = 0

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 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).LeftHomologyData
rw : h.i ≫ K.d j k = 0
⊢ (h.i ≫ Iso.inv (K.extendXIso e hj')) ≫ (K.extend e).d j' k' = 0

Tactic:
rw [assoc, ← comp_d_eq_zero_iff K e hj' hk hk']

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.extend.comp_d_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).LeftHomologyData
⊢ h.i ≫ K.d j k = 0

Tactic:
h.wi

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.wi
-- 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).LeftHomologyData
⊢ h.i ≫ K.d j k = 0

Tactic:
exact h.wi

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.wi
-- 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).LeftHomologyData
dsimp :
  IsLimit.lift (isLimitKernelFork K e hj' hk hk' (KernelFork.ofι h.i ⋯) h.hi)
        (KernelFork.ofι ((K.extend e).d i' j') ⋯) ≫
      h.π =
    0
⊢ IsLimit.lift (isLimitKernelFork K e hj' hk hk' (KernelFork.ofι h.i ⋯) h.hi)
        (KernelFork.ofι ((K.extend e).sc' i' j' k').f ⋯) ≫
      h.π =
    0

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 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).LeftHomologyData
rw : Eq (α := (KernelFork.ofι (K.d i j) ⋯).pt ⟶ h.H) (h.hi.lift (KernelFork.ofι (K.d i j) ⋯) ≫ h.π) 0
⊢ IsLimit.lift (isLimitKernelFork K e hj' hk hk' (KernelFork.ofι h.i ⋯) h.hi)
        (KernelFork.ofι ((K.extend e).d i' j') ⋯) ≫
      h.π =
    0

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

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.hi, HomologicalComplex.extend.leftHomologyData.lift_d_comp_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).LeftHomologyData
⊢ Eq (α := (KernelFork.ofι (K.d i j) ⋯).pt ⟶ h.H) (h.hi.lift (KernelFork.ofι (K.d i j) ⋯) ≫ h.π) 0

Tactic:
h.wπ

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.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).LeftHomologyData
⊢ Eq (α := (KernelFork.ofι (K.d i j) ⋯).pt ⟶ h.H) (h.hi.lift (KernelFork.ofι (K.d i j) ⋯) ≫ h.π) 0

Tactic:
exact h.wπ

Premises used: CategoryTheory.ShortComplex.LeftHomologyData.wπ