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 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'
⊢ 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_eq_zero _ e i' (fun i hi => hi' ⟨i, hi⟩)]

Premises used: Exists.intro, HomologicalComplex.extendMap_f_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' : ι'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Hom.f (extendMap (𝟙 K) e) i' = 𝟙 ((K.extend e).X i')
neg : ∀ (hi' : ¬∃ (i : ι), e.f i = i'), Hom.f (extendMap (𝟙 K) e) i' = 𝟙 ((K.extend e).X i')
⊢ Hom.f (extendMap (𝟙 K) e) i' = 𝟙 ((K.extend e).X 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
pos : ∀ (i : ι) (hi : e.f i = i'), Hom.f (extendMap (𝟙 K) e) i' = 𝟙 ((K.extend e).X i')
⊢ Hom.f (extendMap (𝟙 K) e) i' = 𝟙 ((K.extend e).X 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' : ι'
i : ι
hi : e.f i = i'
⊢ Hom.f (extendMap (𝟙 K) e) i' = 𝟙 ((K.extend e).X i')

Tactic:
simp [extendMap_f _ e hi]

Premises used: HomologicalComplex.extendMap_f
-- 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'
⊢ Hom.f (extendMap (𝟙 K) e) i' = 𝟙 ((K.extend e).X i')

Tactic:
apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.eq_of_src, Exists.intro
-- 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'
h : ∀ (i : ι'), Hom.f (extendMap (𝟙 K) e) i = Hom.f (𝟙 (K.extend e)) i
⊢ extendMap (𝟙 K) e = 𝟙 (K.extend e)

Tactic:
ext
-- 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 : ι'
⊢ Hom.f (extendMap (𝟙 K) e) i = Hom.f (𝟙 (K.extend e)) i

Tactic:
simpa using extendMap_id_f _ _ _

Premises used: HomologicalComplex.extendMap_id_f
-- 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
e : c.Embedding c'
h : ∀ (i' : ι'), Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 i')
⊢ Eq (α := K.extend e ⟶ L.extend e) (extendMap 0 e) 0

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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' : ι'
pos :
  ∀ (hi' : ∃ (i : ι), e.f i = i'),
    Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 i')
neg :
  ∀ (hi' : ¬∃ (i : ι), e.f i = i'),
    Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 i')
⊢ Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
pos :
  ∀ (i : ι) (hi : e.f i = i'),
    Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 i')
⊢ Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' : ι'
i : ι
hi : e.f i = i'
⊢ Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 i')

Tactic:
simp [extendMap_f _ e hi]

Premises used: HomologicalComplex.extendMap_f
-- 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
e : c.Embedding c'
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ Eq.{v_1 + 1} (α := (K.extend e).X i' ⟶ (L.extend e).X i') (Hom.f (extendMap 0 e) i') (Hom.f 0 i')

Tactic:
apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.eq_of_src, Exists.intro
-- 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' : ι'
⊢ Hom.f (Iso.inv (K.extendOpIso e)) i' ≫ (K.op.extend e.op).d i' j' =
    (K.extend e).op.d i' j' ≫ Hom.f (Iso.inv (K.extendOpIso e)) j'

Tactic:
have := (K.extendOpIso e).inv.comm i' 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 : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
i' j' : ι'
this :
  Eq (α := Opposite.op ((K.extend e).X i') ⟶ (K.op.extend e.op).X j')
    (Hom.f (Iso.inv (K.extendOpIso e)) i' ≫ (K.op.extend e.op).d i' j')
    (((K.extend e).d j' i').op ≫ Hom.f (Iso.inv (K.extendOpIso e)) j')
rw :
  (K.op.extend e.op).d i' j' =
    CategoryStruct.comp (Y := (K.extend e).op.X i') (Hom.f (Iso.hom (K.extendOpIso e)) i')
      (Hom.f (Iso.inv (K.extendOpIso e)) i' ≫ (K.op.extend e.op).d i' j')
rw₁ :
  (K.op.extend e.op).d i' j' =
    Hom.f (CategoryStruct.comp (Y := (K.extend e).op) (Iso.hom (K.extendOpIso e)) (Iso.inv (K.extendOpIso e))) i' ≫
      (K.op.extend e.op).d i' j'
rw₂ : (K.op.extend e.op).d i' j' = Hom.f (𝟙 (K.op.extend e.op)) i' ≫ (K.op.extend e.op).d i' j'
rw₃ : (K.op.extend e.op).d i' j' = 𝟙 ((K.op.extend e.op).X i') ≫ (K.op.extend e.op).d i' j'
rw₄ rw₅ : (K.op.extend e.op).d i' j' = (K.op.extend e.op).d i' j'
⊢ (K.op.extend e.op).d i' j' =
    CategoryStruct.comp (Y := (K.extend e).op.X i') (Hom.f (Iso.hom (K.extendOpIso e)) i')
      (((K.extend e).d j' i').op ≫ Hom.f (Iso.inv (K.extendOpIso e)) j')

Tactic:
rw [← this, ← comp_f_assoc, Iso.hom_inv_id, id_f, id_comp]

Premises used: HomologicalComplex.id_f, CategoryTheory.Iso.hom_inv_id, HomologicalComplex.comp_f_assoc, CategoryTheory.Category.id_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 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ φ' : K ⟶ L
e : c.Embedding c'
h :
  ∀ (i' : ι'),
    Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f i'
⊢ extendMap (φ + φ') e = HAdd.hAdd (α := K.extend e ⟶ L.extend 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 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
pos :
  ∀ (hi' : ∃ (i : ι), e.f i = i'),
    Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f i'
neg :
  ∀ (hi' : ¬∃ (i : ι), e.f i = i'),
    Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f i'
⊢ Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f 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 : Preadditive.{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'
pos :
  ∀ (i : ι) (hi : e.f i = i'),
    Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f i'
⊢ Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f 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 : Preadditive.{v_1, u_3} C
K L : HomologicalComplex.{v_1, u_3, u_1} C c
φ φ' : K ⟶ L
e : c.Embedding c'
i' : ι'
i : ι
hi : e.f i = i'
⊢ Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f i'

Tactic:
simp [extendMap_f _ e hi]

Premises used: HomologicalComplex.extendMap_f
-- 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 : Preadditive.{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'
⊢ Hom.f (extendMap (φ + φ') e) i' = (HAdd.hAdd (α := K.extend e ⟶ L.extend e) (extendMap φ e) (extendMap φ' e)).f i'

Tactic:
apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.eq_of_src, Exists.intro
-- 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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
j' k' : ι'
pos :
  ∀ (hj : ∃ (j : ι), e.f j = j'),
    Eq.{v_1 + 1} (α :=
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
        HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
      (d (extend (Functor.obj (single C c i) X) e) j' k') 0
neg :
  ∀ (hj : ¬∃ (j : ι), e.f j = j'),
    Eq.{v_1 + 1} (α :=
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
        HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
      (d (extend (Functor.obj (single C c i) X) e) j' k') 0
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) j' k') 0

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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
j' k' : ι'
hj : ∃ (j : ι), e.f j = j'
pos :
  ∀ (j : ι),
    Eq.{v_1 + 1} (α :=
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
        HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
      (d (extend (Functor.obj (single C c i) X) e) (e.f j) k') 0
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) j' k') 0

Tactic:
obtain ⟨j, rfl⟩ := hj

Premises used: 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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
k' : ι'
j : ι
pos :
  ∀ (hk : ∃ (k : ι), e.f k = k'),
    Eq.{v_1 + 1} (α :=
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
        HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
      (d (extend (Functor.obj (single C c i) X) e) (e.f j) k') 0
neg :
  ∀ (hk : ¬∃ (k : ι), e.f k = k'),
    Eq.{v_1 + 1} (α :=
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
        HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
      (d (extend (Functor.obj (single C c i) X) e) (e.f j) k') 0
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) (e.f j) k') 0

Tactic:
by_cases hk : ∃ k, e.f k = k'
-- 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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
k' : ι'
j : ι
hk : ∃ (k : ι), e.f k = k'
pos :
  ∀ (k : ι),
    Eq.{v_1 + 1} (α :=
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
        HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f k))
      (d (extend (Functor.obj (single C c i) X) e) (e.f j) (e.f k)) 0
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) (e.f j) k') 0

Tactic:
obtain ⟨k, rfl⟩ := hk

Premises used: 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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i j k : ι
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f k))
    (d (extend (Functor.obj (single C c i) X) e) (e.f j) (e.f k)) 0

Tactic:
simp [extend_d_eq _ _ rfl rfl]

Premises used: HomologicalComplex.extend_d_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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
k' : ι'
j : ι
hk : ¬∃ (k : ι), e.f k = k'
tauto tauto₁ : ∀ (i : ι), e.f i ≠ k'
tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : ∀ (i : ι), e.f i = k' → False
⊢ ∀ (i : ι), e.f i ≠ k'

Tactic:
tauto
-- 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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
k' : ι'
j : ι
hk : ¬∃ (k : ι), e.f k = k'
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) (e.f j) ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) (e.f j) k') 0

Tactic:
exact IsZero.eq_of_tgt (isZero_extend_X _ _ _ (by tauto)) _ _

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.eq_of_tgt
-- 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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
j' k' : ι'
hj : ¬∃ (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.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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
i : ι
j' k' : ι'
hj : ¬∃ (j : ι), e.f j = j'
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k')
    (d (extend (Functor.obj (single C c i) X) e) j' k') 0

Tactic:
exact IsZero.eq_of_src (isZero_extend_X _ _ _ (by tauto)) _ _

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.eq_of_src
-- 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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
⊢ ∀ (i_1 : ι'),
    c'.Rel i_1 i' →
      Eq.{v_1 + 1} (α := HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) i_1 ⟶ X)
        (d (extend (Functor.obj (single C c i) X) e) i_1 i' ≫
          Iso.hom (extendXIso (Functor.obj (single C c i) X) e h) ≫ Iso.hom (singleObjXSelf c i X))
        0

Tactic:
simp
-- 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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
⊢ ∀ (k : ι'),
    c'.Rel i' k →
      Eq.{v_1 + 1} (α := X ⟶ HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) k)
        ((Iso.inv (singleObjXSelf c i X) ≫ Iso.inv (extendXIso (Functor.obj (single C c i) X) e h)) ≫
          d (extend (Functor.obj (single C c i) X) e) i' k)
        0

Tactic:
simp
-- 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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
h₁ :
  ∀ (j' : ι'),
    Eq.{v_1 + 1} (α :=
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j' ⟶
        HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) j')
      (Hom.f
        (CategoryStruct.comp (Y := Functor.obj (single C c' i') X)
          (mkHomToSingle (Iso.hom (extendXIso (Functor.obj (single C c i) X) e h) ≫ Iso.hom (singleObjXSelf c i X)) ⋯)
          (mkHomFromSingle (Iso.inv (singleObjXSelf c i X) ≫ Iso.inv (extendXIso (Functor.obj (single C c i) X) e h))
            ⋯))
        j')
      (Hom.f (𝟙 (extend (Functor.obj (single C c i) X) e)) j')
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_1, u_3, u_2} C c') (extend (Functor.obj (single C c i) X) e)
      (extend (Functor.obj (single C c i) X) e))
    (CategoryStruct.comp (Y := Functor.obj (single C c' i') X)
      (mkHomToSingle (Iso.hom (extendXIso (Functor.obj (single C c i) X) e h) ≫ Iso.hom (singleObjXSelf c i X)) ⋯)
      (mkHomFromSingle (Iso.inv (singleObjXSelf c i X) ≫ Iso.inv (extendXIso (Functor.obj (single C c i) X) e h)) ⋯))
    (𝟙 (extend (Functor.obj (single C c i) X) e))

Tactic:
ext j'