awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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' j' : ι'
i j : ι
hi : e.f i = i'
hj : e.f j = j'
⊢ (K.extend e).d i' j' = Iso.hom (K.extendXIso e hi) ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj)

Tactic:
apply extend.d_eq

Premises used: HomologicalComplex.extend.d_eq
-- 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' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
inl : ∀ (hj' : e.r j' = none), (K.extend e).d i' j' = 0
inr : ∀ (j : ι) (hj : e.r j' = some j), (K.extend e).d i' j' = 0
⊢ (K.extend e).d i' 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
hj' : e.r j' = none
⊢ (K.extend e).d i' j' = 0

Tactic:
extend.d_none_eq_zero' _ _ _ hj'

Premises used: HomologicalComplex.extend.d, HomologicalComplex.extend.d_none_eq_zero', 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' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
hj' : e.r j' = none
⊢ (K.extend e).d i' j' = 0

Tactic:
exact extend.d_none_eq_zero' _ _ _ 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
inr : ¬c.Rel i j
⊢ (K.extend e).d i' j' = 0

Tactic:
rw [extend_d_eq K e hi (e.f_eq_of_r_eq_some hj), K.shape, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, ComplexShape.Embedding.f_eq_of_r_eq_some, CategoryTheory.Limits.zero_comp, HomologicalComplex.extend_d_eq, 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
hij : c.Rel i j
⊢ e.r j' = some (c.next i)

Tactic:
obtain rfl := c.next_eq' hij

Premises used: rfl, ComplexShape.next_eq'
-- 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' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
j : ι
hj : e.r j' = some j
hij : c.Rel i j
hj₁ : e.r j' = some (c.next i)
⊢ c.Rel i (c.next i)

Tactic:
obtain rfl := c.next_eq' hij

Premises used: rfl, ComplexShape.next_eq'
-- 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' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
hj : e.r j' = some (c.next i)
hij : c.Rel i (c.next i)
⊢ False

Tactic:
hi' hij
-- 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' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
hj : e.r j' = some (c.next i)
hij : c.Rel i (c.next i)
⊢ False

Tactic:
exact hi' hij
-- 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' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
inl : ∀ (hi' : e.r i' = none), (K.extend e).d i' j' = 0
inr : ∀ (i : ι) (hi : e.r i' = some i), (K.extend e).d i' j' = 0
⊢ (K.extend e).d i' 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
hi' : e.r i' = none
⊢ (K.extend e).d i' j' = 0

Tactic:
extend.d_none_eq_zero _ _ _ hi'

Premises used: HomologicalComplex.extend.d, HomologicalComplex.extend.d_none_eq_zero, 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' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
hi' : e.r i' = none
⊢ (K.extend e).d i' j' = 0

Tactic:
exact extend.d_none_eq_zero _ _ _ 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
i : ι
hi : e.r i' = some i
inr : ¬c.Rel i j
⊢ (K.extend e).d i' j' = 0

Tactic:
rw [extend_d_eq K e (e.f_eq_of_r_eq_some hi) hj, K.shape, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, ComplexShape.Embedding.f_eq_of_r_eq_some, CategoryTheory.Limits.zero_comp, HomologicalComplex.extend_d_eq, 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
i : ι
hi : e.r i' = some i
hij : c.Rel i j
⊢ e.r i' = some (c.prev j)

Tactic:
obtain rfl := c.prev_eq' hij

Premises used: ComplexShape.prev_eq', 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
i : ι
hi : e.r i' = some i
hij : c.Rel i j
hi₁ : e.r i' = some (c.prev j)
⊢ c.Rel (c.prev j) j

Tactic:
obtain rfl := c.prev_eq' hij

Premises used: ComplexShape.prev_eq', 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
hi : e.r i' = some (c.prev j)
hij : c.Rel (c.prev j) j
⊢ False

Tactic:
hj' hij
-- 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' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
hi : e.r i' = some (c.prev j)
hij : c.Rel (c.prev j) j
⊢ False

Tactic:
exact hj' hij
-- 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'
pos :
  ∀ (hi : ∃ (i : ι), e.f i = i'),
    extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
neg :
  ∀ (hi : ¬∃ (i : ι), e.f i = i'),
    extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

Tactic:
by_cases hi : ∃ i, e.f i = i'
-- 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 : ∃ (i : ι), e.f i = i'
pos :
  ∀ (i : ι) (hi : e.f i = i'),
    extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

Tactic:
obtain ⟨i, hi⟩ := hi
-- 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.f i = i'
pos :
  ∀ (hj : ∃ (j : ι), e.f j = j'),
    extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
neg :
  ∀ (hj : ¬∃ (j : ι), e.f j = j'),
    extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

Tactic:
by_cases hj : ∃ j, e.f j = j'
-- 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.f i = i'
hj : ∃ (j : ι), e.f j = j'
pos :
  ∀ (j : ι) (hj : e.f j = j'),
    extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

Tactic:
obtain ⟨j, hj⟩ := hj
-- 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.f i = i'
j : ι
hj : e.f j = j'
pos :
  Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j')
    (CategoryStruct.comp (Y := (L.extend e).X i') (Iso.hom (extend.XIso K ⋯) ≫ φ.f i ≫ Iso.inv (extend.XIso L ⋯))
      (Iso.hom (L.extendXIso e hi) ≫ L.d i j ≫ Iso.inv (L.extendXIso e hj)))
    (CategoryStruct.comp (Y := (K.extend e).X j') (Iso.hom (K.extendXIso e hi) ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj))
      (Iso.hom (extend.XIso K ⋯) ≫ φ.f j ≫ Iso.inv (extend.XIso L ⋯)))
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

Tactic:
rw [K.extend_d_eq e hi hj, L.extend_d_eq e hi hj,
          extend.mapX_some φ (e.r_eq_some hi),
          extend.mapX_some φ (e.r_eq_some hj)]

Premises used: ComplexShape.Embedding.r_eq_some, HomologicalComplex.extend.mapX_some, HomologicalComplex.extend_d_eq
-- 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.f i = i'
j : ι
hj : e.f j = j'
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X j')
    (CategoryStruct.comp (Y := (L.extend e).X i') (Iso.hom (extend.XIso K ⋯) ≫ φ.f i ≫ Iso.inv (extend.XIso L ⋯))
      (Iso.hom (L.extendXIso e hi) ≫ L.d i j ≫ Iso.inv (L.extendXIso e hj)))
    (CategoryStruct.comp (Y := (K.extend e).X j') (Iso.hom (K.extendXIso e hi) ≫ K.d i j ≫ Iso.inv (K.extendXIso e hj))
      (Iso.hom (extend.XIso K ⋯) ≫ φ.f j ≫ Iso.inv (extend.XIso L ⋯)))

Tactic:
simp only [extendXIso, assoc, Iso.inv_hom_id_assoc, Hom.comm_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id_assoc, HomologicalComplex.Hom.comm_assoc, HomologicalComplex.extendXIso
-- 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.f i = i'
hj : ¬∃ (j : ι), e.f j = j'
⊢ e.r j' = none

Tactic:
have hj' := e.r_eq_none j' (fun j'' hj'' => hj ⟨j'', hj''⟩)
-- 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.f i = i'
hj : ¬∃ (j : ι), e.f j = j'
hj' : e.r j' = none
neg :
  Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j'))
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

Tactic:
dsimp [extend]

Premises used: HomologicalComplex.extend
-- 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.f i = i'
hj : ¬∃ (j : ι), e.f j = j'
hj' : e.r j' = none
neg :
  Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0)
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
neg₁ : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0) (0 ≫ extend.mapX φ (e.r j'))
neg₂ : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) 0 (0 ≫ extend.mapX φ (e.r j'))
neg₃ neg₄ : Eq.{v_1 + 1} (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) 0 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j'))
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))

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

Premises used: HomologicalComplex.extend.d_none_eq_zero', CategoryTheory.Limits.comp_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' : ι'
h : c'.Rel i' j'
hi : ¬∃ (i : ι), e.f i = i'
⊢ e.r i' = none

Tactic:
have hi' := e.r_eq_none i' (fun i'' hi'' => hi ⟨i'', hi''⟩)
-- 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 : ¬∃ (i : ι), e.f i = i'
hi' : e.r i' = none
neg :
  Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j'))
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

Tactic:
dsimp [extend]

Premises used: HomologicalComplex.extend
-- 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 : ¬∃ (i : ι), e.f i = i'
hi' : e.r i' = none
neg :
  Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0)
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))
neg₁ : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ 0) (0 ≫ extend.mapX φ (e.r j'))
neg₂ : Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) 0 (0 ≫ extend.mapX φ (e.r j'))
neg₃ neg₄ : Eq.{v_1 + 1} (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) 0 0
⊢ Eq (α := extend.X K (e.r i') ⟶ extend.X L (e.r j')) (extend.mapX φ (e.r i') ≫ extend.d L (e.r i') (e.r j'))
    (extend.d K (e.r i') (e.r j') ≫ extend.mapX φ (e.r j'))

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

Premises used: HomologicalComplex.extend.d_none_eq_zero, CategoryTheory.Limits.comp_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 : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
i : ι
i' : ι'
h : e.f i = i'
rw :
  Eq (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Iso.hom (extend.XIso K ⋯) ≫ φ.f i ≫ Iso.inv (extend.XIso L ⋯))
    (Iso.hom (K.extendXIso e h) ≫ φ.f i ≫ Iso.inv (L.extendXIso e h))
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X i') (extend.mapX φ (e.r i'))
    (Iso.hom (K.extendXIso e h) ≫ φ.f i ≫ Iso.inv (L.extendXIso e h))

Tactic:
rw [extend.mapX_some φ (e.r_eq_some h)]

Premises used: ComplexShape.Embedding.r_eq_some, HomologicalComplex.extend.mapX_some
-- 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 : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
i : ι
i' : ι'
h : e.f i = i'
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Iso.hom (extend.XIso K ⋯) ≫ φ.f i ≫ Iso.inv (extend.XIso L ⋯))
    (Iso.hom (K.extendXIso e h) ≫ φ.f i ≫ Iso.inv (L.extendXIso e h))

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 : HomologicalComplex.{v_1, u_3, u_1} C c
φ : K ⟶ L
e : c.Embedding c'
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
rw rw₁ : Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') 0 0
⊢ Eq (α := (K.extend e).X i' ⟶ (L.extend e).X i') (extend.mapX φ (e.r i')) 0

Tactic:
rw [extend.mapX_none φ (e.r_eq_none i' hi')]

Premises used: ComplexShape.Embedding.r_eq_none, HomologicalComplex.extend.mapX_none
-- 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'
h :
  ∀ (i' : ι'),
    Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
      (Hom.f (extendMap φ e ≫ extendMap φ' e) i')
⊢ Eq (α := K.extend e ⟶ M.extend e) (extendMap (φ ≫ φ') e) (extendMap φ e ≫ extendMap φ' e)

Tactic:
ext i'
-- 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' : ι'
pos :
  ∀ (hi' : ∃ (i : ι), e.f i = i'),
    Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
      (Hom.f (extendMap φ e ≫ extendMap φ' e) i')
neg :
  ∀ (hi' : ¬∃ (i : ι), e.f i = i'),
    Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
      (Hom.f (extendMap φ e ≫ extendMap φ' e) i')
⊢ Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
    (Hom.f (extendMap φ e ≫ extendMap φ' e) i')

Tactic:
by_cases hi' : ∃ i, e.f i = i'
-- 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' : ι'
hi' : ∃ (i : ι), e.f i = i'
pos :
  ∀ (i : ι) (hi : e.f i = i'),
    Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
      (Hom.f (extendMap φ e ≫ extendMap φ' e) i')
⊢ Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
    (Hom.f (extendMap φ e ≫ extendMap φ' e) i')

Tactic:
obtain ⟨i, hi⟩ := hi'
-- 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' : ι'
i : ι
hi : e.f i = i'
⊢ Eq (α := (K.extend e).X i' ⟶ (M.extend e).X i') (Hom.f (extendMap (φ ≫ φ') e) i')
    (Hom.f (extendMap φ e ≫ extendMap φ' e) i')

Tactic:
simp [extendMap_f _ e hi]

Premises used: HomologicalComplex.extendMap_f