awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i j : Option ι
a b : ι
hi : i = some a
hj : j = some b
subst :
  Eq (α := X K (some a) ⟶ X K (some b)) (d K (some a) (some b)) (Iso.hom (XIso K ⋯) ≫ K.d a b ≫ Iso.inv (XIso K ⋯))
⊢ Eq (α := X K i ⟶ X K j) (d K i j) (Iso.hom (XIso K hi) ≫ K.d a b ≫ Iso.inv (XIso K hj))

Tactic:
subst hi hj
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
a b : ι
⊢ Eq (α := X K (some a) ⟶ X K (some b)) (d K (some a) (some b)) (Iso.hom (XIso K ⋯) ≫ K.d a b ≫ Iso.inv (XIso K ⋯))

Tactic:
simp [XIso, X, d]

Premises used: HomologicalComplex.extend.d, HomologicalComplex.extend.XIso, HomologicalComplex.extend.X
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i j x : Option ι
⊢ Eq (α := X K.op none ⟶ Opposite.op (X K x)) (Iso.hom (XOpIso K none) ≫ Quiver.Hom.op (d K x none))
    (d K.op none x ≫ Iso.hom (XOpIso K x))

Tactic:
simp only [d_none_eq_zero, d_none_eq_zero', comp_zero, zero_comp, op_zero]

Premises used: HomologicalComplex.extend.d_none_eq_zero', HomologicalComplex.extend.d_none_eq_zero, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.op_zero
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i_1 j_1 : Option ι
i j : ι
dsimp : 𝟙 (X K.op (some i)) ≫ Quiver.Hom.op (d K (some j) (some i)) = d K.op (some i) (some j) ≫ 𝟙 (X K.op (some j))
⊢ Eq (α := X K.op (some i) ⟶ Opposite.op (X K (some j)))
    (Iso.hom (XOpIso K (some i)) ≫ Quiver.Hom.op (d K (some j) (some i)))
    (d K.op (some i) (some j) ≫ Iso.hom (XOpIso K (some j)))

Tactic:
dsimp [XOpIso]

Premises used: HomologicalComplex.extend.XOpIso
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i_1 j_1 : Option ι
i j : ι
simp :
  Eq (α := X K.op (some i) ⟶ Opposite.op (X K (some j)))
    (Quiver.Hom.op (Iso.inv (XIso K ⋯)) ≫ (K.d j i).op ≫ Quiver.Hom.op (Iso.hom (XIso K ⋯)) :
      Opposite.op (X K (some i)) ⟶ Opposite.op (X K (some j)))
    (Iso.hom (XIso K.op ⋯) ≫ K.op.d i j ≫ Iso.inv (XIso K.op ⋯) : X K.op (some i) ⟶ X K.op (some j))
⊢ 𝟙 (X K.op (some i)) ≫ Quiver.Hom.op (d K (some j) (some i)) = d K.op (some i) (some j) ≫ 𝟙 (X K.op (some j))

Tactic:
simp only [d_eq _ rfl rfl, op_comp, assoc, id_comp, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, CategoryTheory.Category.comp_id, HomologicalComplex.extend.d_eq, rfl, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i_1 j_1 : Option ι
i j : ι
⊢ Eq (α := X K.op (some i) ⟶ Opposite.op (X K (some j)))
    (Quiver.Hom.op (Iso.inv (XIso K ⋯)) ≫ (K.d j i).op ≫ Quiver.Hom.op (Iso.hom (XIso K ⋯)) :
      Opposite.op (X K (some i)) ⟶ Opposite.op (X K (some j)))
    (Iso.hom (XIso K.op ⋯) ≫ K.op.d i j ≫ Iso.inv (XIso K.op ⋯) : X K.op (some i) ⟶ X K.op (some j))

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
i j : Option ι
val : ι
⊢ Eq (α := X K.op (some val) ⟶ Opposite.op (X K none))
    (Iso.hom (XOpIso K (some val)) ≫ Quiver.Hom.op (d K none (some val)))
    (d K.op (some val) none ≫ Iso.hom (XOpIso K none))

Tactic:
simp only [d_none_eq_zero, d_none_eq_zero', comp_zero, zero_comp, op_zero]

Premises used: HomologicalComplex.extend.d_none_eq_zero', HomologicalComplex.extend.d_none_eq_zero, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp, CategoryTheory.Limits.op_zero
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
i : Option ι
a : ι
hi : i = some a
subst : Eq (α := X K (some a) ⟶ X L (some a)) (mapX φ (some a)) (Iso.hom (XIso K ⋯) ≫ φ.f a ≫ Iso.inv (XIso L ⋯))
⊢ Eq (α := X K i ⟶ X L i) (mapX φ i) (Iso.hom (XIso K hi) ≫ φ.f a ≫ Iso.inv (XIso L hi))

Tactic:
subst hi
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
a : ι
dsimp : mapX φ (some a) = 𝟙 (K.X a) ≫ φ.f a ≫ 𝟙 (L.X a)
⊢ Eq (α := X K (some a) ⟶ X L (some a)) (mapX φ (some a)) (Iso.hom (XIso K ⋯) ≫ φ.f a ≫ Iso.inv (XIso L ⋯))

Tactic:
dsimp [XIso, X]

Premises used: HomologicalComplex.extend.XIso, HomologicalComplex.extend.X
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
a : ι
rw : mapX φ (some a) = φ.f a
⊢ mapX φ (some a) = 𝟙 (K.X a) ≫ φ.f a ≫ 𝟙 (L.X a)

Tactic:
rw [id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
a : ι
⊢ mapX φ (some a) = φ.f a

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
i : Option ι
hi : i = none
subst : Eq (α := X K none ⟶ X L none) (mapX φ none) 0
⊢ Eq (α := X K i ⟶ X L i) (mapX φ i) 0

Tactic:
subst hi
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
⊢ Eq (α := X K none ⟶ X L none) (mapX φ none) 0

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
h : ¬c'.Rel i' j'
inl : ∀ (hi' : e.r i' = none), Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
inr :
  ∀ (i : ι) (hi : e.r i' = some i), Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0

Tactic:
obtain hi' | ⟨i, hi⟩ := (e.r i').eq_none_or_eq_some

Premises used: Option.eq_none_or_eq_some, ComplexShape.Embedding.r
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
h : ¬c'.Rel i' j'
hi' : e.r i' = none
inl inl₁ : Eq.{v_1 + 1} (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) 0 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0

Tactic:
rw [extend.d_none_eq_zero K _ _ hi']

Premises used: HomologicalComplex.extend.d_none_eq_zero
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
inr : ∀ (hj' : e.r j' = none), Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
inr₁ :
  ∀ (j : ι) (hj : e.r j' = some j), Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0

Tactic:
obtain hj' | ⟨j, hj⟩ := (e.r j').eq_none_or_eq_some

Premises used: Option.eq_none_or_eq_some, ComplexShape.Embedding.r
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
hj' : e.r j' = none
inr inr₁ : Eq.{v_1 + 1} (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) 0 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0

Tactic:
rw [extend.d_none_eq_zero' K _ _ hj']

Premises used: HomologicalComplex.extend.d_none_eq_zero'
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
inr : ¬c.Rel i j
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0

Tactic:
rw [extend.d_eq K hi hj, K.shape, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.extend.d_eq, CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
⊢ ¬c'.Rel (e.f i) j'

Tactic:
obtain rfl := e.f_eq_of_r_eq_some hi

Premises used: ComplexShape.Embedding.f_eq_of_r_eq_some, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
h : ¬c'.Rel i' j'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
h₁ : ¬c'.Rel (e.f i) j'
⊢ e.r (e.f i) = some i

Tactic:
obtain rfl := e.f_eq_of_r_eq_some hi

Premises used: ComplexShape.Embedding.f_eq_of_r_eq_some, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
i j : ι
hj : e.r j' = some j
h : ¬c'.Rel (e.f i) j'
hi : e.r (e.f i) = some i
⊢ e.r (e.f j) = some j

Tactic:
obtain rfl := e.f_eq_of_r_eq_some hj

Premises used: ComplexShape.Embedding.f_eq_of_r_eq_some, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
i j : ι
hj : e.r j' = some j
h : ¬c'.Rel (e.f i) j'
hi : e.r (e.f i) = some i
hj₁ : e.r (e.f j) = some j
⊢ ¬c'.Rel (e.f i) (e.f j)

Tactic:
obtain rfl := e.f_eq_of_r_eq_some hj

Premises used: ComplexShape.Embedding.f_eq_of_r_eq_some, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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 : ι
hi : e.r (e.f i) = some i
hj : e.r (e.f j) = some j
h : ¬c'.Rel (e.f i) (e.f j)
hij : c.Rel i j
⊢ False

Tactic:
h (e.rel hij)

Premises used: ComplexShape.Embedding.rel
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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 : ι
hi : e.r (e.f i) = some i
hj : e.r (e.f j) = some j
h : ¬c'.Rel (e.f i) (e.f j)
hij : c.Rel i j
⊢ False

Tactic:
exact h (e.rel hij)

Premises used: ComplexShape.Embedding.rel
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
h : c'.Rel i' j'
h_1 : c'.Rel j' k'
inl :
  ∀ (hi' : e.r i' = none),
    Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
      (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
inr :
  ∀ (i : ι) (hi : e.r i' = some i),
    Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
      (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0

Tactic:
obtain hi' | ⟨i, hi⟩ := (e.r i').eq_none_or_eq_some

Premises used: Option.eq_none_or_eq_some, ComplexShape.Embedding.r
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
h : c'.Rel i' j'
h_1 : c'.Rel j' k'
hi' : e.r i' = none
inl :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) 0 (extend.d K (e.r j') (e.r k'))) 0
inl₁ inl₂ : Eq.{v_1 + 1} (α := extend.X K (e.r i') ⟶ extend.X K (e.r k')) 0 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0

Tactic:
rw [extend.d_none_eq_zero K _ _ hi', zero_comp]

Premises used: HomologicalComplex.extend.d_none_eq_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
h : c'.Rel i' j'
h_1 : c'.Rel j' k'
i : ι
hi : e.r i' = some i
inr :
  ∀ (hj' : e.r j' = none),
    Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
      (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
inr₁ :
  ∀ (j : ι) (hj : e.r j' = some j),
    Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
      (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0

Tactic:
obtain hj' | ⟨j, hj⟩ := (e.r j').eq_none_or_eq_some

Premises used: Option.eq_none_or_eq_some, ComplexShape.Embedding.r
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
h : c'.Rel i' j'
h_1 : c'.Rel j' k'
i : ι
hi : e.r i' = some i
hj' : e.r j' = none
inr :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0) 0
inr₁ inr₂ : Eq.{v_1 + 1} (α := extend.X K (e.r i') ⟶ extend.X K (e.r k')) 0 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0

Tactic:
rw [extend.d_none_eq_zero K _ _ hj', comp_zero]

Premises used: HomologicalComplex.extend.d_none_eq_zero, CategoryTheory.Limits.comp_zero
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
h : c'.Rel i' j'
h_1 : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
inr :
  ∀ (hk' : e.r k' = none),
    Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
      (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
inr₁ :
  ∀ (k : ι) (hk : e.r k' = some k),
    Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
      (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0

Tactic:
obtain hk' | ⟨k, hk⟩ := (e.r k').eq_none_or_eq_some

Premises used: Option.eq_none_or_eq_some, ComplexShape.Embedding.r
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
h : c'.Rel i' j'
h_1 : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
hk' : e.r k' = none
inr :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) 0) 0
inr₁ inr₂ : Eq.{v_1 + 1} (α := extend.X K (e.r i') ⟶ extend.X K (e.r k')) 0 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0

Tactic:
rw [extend.d_none_eq_zero' K _ _ hk', comp_zero]

Premises used: HomologicalComplex.extend.d_none_eq_zero', CategoryTheory.Limits.comp_zero
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{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' : ι'
h : c'.Rel i' j'
h_1 : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
inr :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    ((Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj)) ≫ extend.d K (e.r j') (e.r k')) 0
inr₁ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ Iso.inv (extend.XIso K hj))
      (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₂ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫
      CategoryStruct.comp (Y := extend.X K (e.r j')) (K.d i j ≫ Iso.inv (extend.XIso K hj))
        (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₃ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫
      K.d i j ≫
        CategoryStruct.comp (Y := extend.X K (e.r j')) (Iso.inv (extend.XIso K hj))
          (Iso.hom (extend.XIso K hj) ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)))
    0
inr₄ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (Iso.hom (extend.XIso K hi) ≫ K.d i j ≫ K.d j k ≫ Iso.inv (extend.XIso K hk)) 0
inr₅ :
  Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k')) (Iso.hom (extend.XIso K hi) ≫ 0 ≫ Iso.inv (extend.XIso K hk)) 0
inr₆ : Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k')) (Iso.hom (extend.XIso K hi) ≫ 0) 0
inr₇ inr₈ : Eq.{v_1 + 1} (α := extend.X K (e.r i') ⟶ extend.X K (e.r k')) 0 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X K (e.r k'))
    (CategoryStruct.comp (Y := extend.X K (e.r j')) (extend.d K (e.r i') (e.r j')) (extend.d K (e.r j') (e.r k'))) 0

Tactic:
rw [extend.d_eq K hi hj, extend.d_eq K hj hk, assoc, assoc,
            Iso.inv_hom_id_assoc, K.d_comp_d_assoc, zero_comp, comp_zero]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.d_comp_d_assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Iso.inv_hom_id_assoc, HomologicalComplex.extend.d_eq, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' : ι'
hi' : e.r i' = none
⊢ IsZero.{v_1, u_3} ((K.extend e).X i')

Tactic:
extend.isZero_X K hi'

Premises used: HomologicalComplex.extend.isZero_X, HomologicalComplex.extend.X
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroObject.{v_1, u_3} C
inst_2 : HasZeroMorphisms.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ IsZero.{v_1, u_3} ((K.extend e).X i')

Tactic:
K.isZero_extend_X' e i' (ComplexShape.Embedding.r_eq_none e i' hi')

Premises used: ComplexShape.Embedding.r_eq_none, HomologicalComplex.isZero_extend_X'