awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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
φ : Functor.obj (e.extendFunctor C) K ⟶ Functor.obj (e.extendFunctor C) L
i j : ι
h : c.Rel i j
this :
  φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯) ≫ L.d i j ≫ Iso.inv (L.extendXIso e ⋯) =
    (Iso.hom (K.extendXIso e ⋯) ≫ K.d i j ≫ Iso.inv (K.extendXIso e ⋯)) ≫ φ.f (e.f j)
⊢ (Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯)) ≫ L.d i j =
    K.d i j ≫ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f j) ≫ Iso.hom (L.extendXIso e ⋯)

Tactic:
simp [← cancel_mono (L.extendXIso e rfl).inv, Category.assoc, this]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, HomologicalComplex.extendXIso, CategoryTheory.Iso.inv, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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
φ : Functor.obj (e.extendFunctor C) K ⟶ Functor.obj (e.extendFunctor C) L
h :
  ∀ (i' : ι'),
    HomologicalComplex.Hom.f
        (CategoryTheory.Functor.map (e.extendFunctor C)
          { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯), comm' := ⋯ })
        i' =
      φ.f i'
⊢ CategoryTheory.Functor.map (e.extendFunctor C)
      { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯), comm' := ⋯ } =
    φ

Tactic:
ext i'
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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
φ : Functor.obj (e.extendFunctor C) K ⟶ Functor.obj (e.extendFunctor C) L
i' : ι'
pos :
  ∀ (hi' : ∃ (i : ι), e.f i = i'),
    HomologicalComplex.Hom.f
        (CategoryTheory.Functor.map (e.extendFunctor C)
          { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯), comm' := ⋯ })
        i' =
      φ.f i'
neg :
  ∀ (hi' : ¬∃ (i : ι), e.f i = i'),
    HomologicalComplex.Hom.f
        (CategoryTheory.Functor.map (e.extendFunctor C)
          { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯), comm' := ⋯ })
        i' =
      φ.f i'
⊢ HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (e.extendFunctor C)
        { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯), comm' := ⋯ })
      i' =
    φ.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 ι'
e : c.Embedding c'
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
φ : Functor.obj (e.extendFunctor C) K ⟶ Functor.obj (e.extendFunctor C) L
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
pos :
  ∀ (i : ι),
    Eq (α := (Functor.obj (e.extendFunctor C) K).X (e.f i) ⟶ (Functor.obj (e.extendFunctor C) L).X (e.f i))
      (HomologicalComplex.Hom.f
        (CategoryTheory.Functor.map (e.extendFunctor C)
          { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯), comm' := ⋯ })
        (e.f i))
      (φ.f (e.f i))
⊢ HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (e.extendFunctor C)
        { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯), comm' := ⋯ })
      i' =
    φ.f i'

Tactic:
obtain ⟨i, rfl⟩ := hi'

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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
φ : Functor.obj (e.extendFunctor C) K ⟶ Functor.obj (e.extendFunctor C) L
i : ι
⊢ Eq (α := (Functor.obj (e.extendFunctor C) K).X (e.f i) ⟶ (Functor.obj (e.extendFunctor C) L).X (e.f i))
    (HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (e.extendFunctor C)
        { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯), comm' := ⋯ })
      (e.f i))
    (φ.f (e.f i))

Tactic:
simp [HomologicalComplex.extendMap_f _ _ rfl]

Premises used: HomologicalComplex.extendMap_f, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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
φ : Functor.obj (e.extendFunctor C) K ⟶ Functor.obj (e.extendFunctor C) L
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
tauto tauto₁ : ∀ (i : ι), e.f i ≠ i'
tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : ∀ (i : ι), e.f i = i' → False
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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
φ : Functor.obj (e.extendFunctor C) K ⟶ Functor.obj (e.extendFunctor C) L
i' : ι'
hi' : ¬∃ (i : ι), e.f i = i'
⊢ HomologicalComplex.Hom.f
      (CategoryTheory.Functor.map (e.extendFunctor C)
        { f := fun (i : ι) ↦ Iso.inv (K.extendXIso e ⋯) ≫ φ.f (e.f i) ≫ Iso.hom (L.extendXIso e ⋯), comm' := ⋯ })
      i' =
    φ.f i'

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

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 ι'
e : c.Embedding c'
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
f : K ⟶ L
h :
  ∀ (i : ι),
    HomologicalComplex.Hom.f
        {
          f := fun (i : ι) ↦
            CategoryStruct.comp (Y := (K.extend e).X (e.f i)) (Iso.inv (K.extendXIso e ⋯))
              (CategoryStruct.comp (Y := (Functor.obj (e.extendFunctor C) L).X (e.f i))
                (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (e.extendFunctor C) f) (e.f i))
                (Iso.hom (L.extendXIso e ⋯))),
          comm' := ⋯ }
        i =
      f.f i
⊢ {
      f := fun (i : ι) ↦
        CategoryStruct.comp (Y := (K.extend e).X (e.f i)) (Iso.inv (K.extendXIso e ⋯))
          (CategoryStruct.comp (Y := (Functor.obj (e.extendFunctor C) L).X (e.f i))
            (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (e.extendFunctor C) f) (e.f i))
            (Iso.hom (L.extendXIso e ⋯))),
      comm' := ⋯ } =
    f

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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
f : K ⟶ L
i : ι
⊢ HomologicalComplex.Hom.f
      {
        f := fun (i : ι) ↦
          CategoryStruct.comp (Y := (K.extend e).X (e.f i)) (Iso.inv (K.extendXIso e ⋯))
            (CategoryStruct.comp (Y := (Functor.obj (e.extendFunctor C) L).X (e.f i))
              (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (e.extendFunctor C) f) (e.f i))
              (Iso.hom (L.extendXIso e ⋯))),
        comm' := ⋯ }
      i =
    f.f i

Tactic:
simp [HomologicalComplex.extendMap_f _ _ rfl]

Premises used: HomologicalComplex.extendMap_f, rfl
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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
⊢ Functor.Faithful (C := HomologicalComplex.{v_1, u_3, u_1} C c) (e.extendFunctor C)

Tactic:
(e.fullyFaithfulExtendFunctor C).faithful

Premises used: CategoryTheory.Functor.FullyFaithful.faithful, ComplexShape.Embedding.fullyFaithfulExtendFunctor
-- Module: Mathlib.Algebra.Homology.Embedding.Extend
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
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
⊢ Functor.Full (C := HomologicalComplex.{v_1, u_3, u_1} C c) (e.extendFunctor C)

Tactic:
(e.fullyFaithfulExtendFunctor C).full

Premises used: CategoryTheory.Functor.FullyFaithful.full, ComplexShape.Embedding.fullyFaithfulExtendFunctor
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
pos : ∀ (hjk : c.Rel j k), φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
neg : ∀ (hjk : ¬c.Rel j k), φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0

Tactic:
by_cases hjk : c.Rel j k

Premises used: ComplexShape.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'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
rw : e.f k = c'.next j'
rw₁ : e.f k = c'.next (e.f j)
rw₂ rw₃ : e.f k = e.f k
⊢ e.f k = k'

Tactic:
rw [← hk', ← hj', c'.next_eq' (e.rel hjk)]

Premises used: ComplexShape.Embedding.rel, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
⊢ e.f k = k'

Tactic:
have hk' : e.f k = k' := by rw [← hk', ← hj', c'.next_eq' (e.rel hjk)]
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk'_1 : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
hk' : e.f k = k'
pos :
  φ ≫ K.d j k = 0 ↔
    Eq (α := W ⟶ (K.extend e).X k')
      (φ ≫
        CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj'))
          (Iso.hom (K.extendXIso e hj') ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk')))
      0
pos₁ : φ ≫ K.d j k = 0 ↔ Eq (α := W ⟶ (K.extend e).X k') (φ ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk')) 0
pos₂ :
  Eq (α := W ⟶ (K.extend e).X k') ((φ ≫ K.d j k) ≫ Iso.inv (K.extendXIso e hk')) (0 ≫ Iso.inv (K.extendXIso e hk')) ↔
    Eq (α := W ⟶ (K.extend e).X k') (φ ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk')) 0
pos₃ :
  Eq (α := W ⟶ (K.extend e).X k') ((φ ≫ K.d j k) ≫ Iso.inv (K.extendXIso e hk')) 0 ↔
    Eq (α := W ⟶ (K.extend e).X k') (φ ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk')) 0
pos₄ pos₅ :
  Eq (α := W ⟶ (K.extend e).X k') (φ ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk')) 0 ↔
    Eq (α := W ⟶ (K.extend e).X k') (φ ≫ K.d j k ≫ Iso.inv (K.extendXIso e hk')) 0
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0

Tactic:
rw [K.extend_d_eq e hj' hk', Iso.inv_hom_id_assoc,
      ← cancel_mono (K.extendXIso e hk').inv, zero_comp, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Limits.zero_comp, 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'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : ¬c.Rel j k
neg : φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0

Tactic:
simp only [K.shape _ _ hjk, comp_zero, true_iff]

Premises used: CategoryTheory.Limits.comp_zero, true_iff, 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'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : ¬c.Rel j k
neg : ¬c.Rel j (c.next j)
⊢ φ ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0

Tactic:
rw [K.extend_d_from_eq_zero e j' k' j hj', comp_zero, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.extend_d_from_eq_zero
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk neg : ¬c.Rel j k
⊢ ¬c.Rel j (c.next j)

Tactic:
rw [hk]
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : ¬c.Rel j k
⊢ ¬c.Rel j k

Tactic:
hjk
-- Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology
Goal:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst : Category.{v_1, u_3} C
inst_1 : HasZeroMorphisms.{v_1, u_3} C
inst_2 : HasZeroObject.{v_1, u_3} C
K : HomologicalComplex.{v_1, u_3, u_1} C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : ¬c.Rel j k
⊢ ¬c.Rel j k

Tactic:
exact hjk
-- 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 : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
pos : ∀ (hij : c.Rel i j), K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
neg : ∀ (hij : ¬c.Rel i j), K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
⊢ K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0

Tactic:
by_cases hij : c.Rel i j

Premises used: ComplexShape.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 : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ 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 : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ 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 : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi'_1 : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
hi' : e.f i = i'
pos :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (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 (K.extendXIso e hj') ≫ φ))
      0
pos₁ :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (Iso.hom (K.extendXIso e hi') ≫
        CategoryStruct.comp (Y := (K.extend e).X j') (K.d i j ≫ Iso.inv (K.extendXIso e hj'))
          (Iso.hom (K.extendXIso e hj') ≫ φ))
      0
pos₂ :
  K.d i j ≫ φ = 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W)
      (Iso.hom (K.extendXIso e hi') ≫
        K.d i j ≫
          CategoryStruct.comp (Y := (K.extend e).X j') (Iso.inv (K.extendXIso e hj'))
            (Iso.hom (K.extendXIso e hj') ≫ φ))
      0
pos₃ : K.d i j ≫ φ = 0 ↔ Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ φ) 0
pos₄ :
  Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ φ) (Iso.hom (K.extendXIso e hi') ≫ 0) ↔
    Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ φ) 0
pos₅ pos₆ :
  Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ φ) 0 ↔
    Eq (α := (K.extend e).X i' ⟶ W) (Iso.hom (K.extendXIso e hi') ≫ K.d i j ≫ φ) 0
⊢ K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0

Tactic:
rw [K.extend_d_eq e hi' hj', assoc, assoc, Iso.inv_hom_id_assoc,
      ← cancel_epi (K.extendXIso e hi').hom, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Iso.inv_hom_id_assoc, HomologicalComplex.extend_d_eq, 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 : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : ¬c.Rel i j
neg : (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0
⊢ K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0

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

Premises used: true_iff, 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 : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : ¬c.Rel i j
neg : ¬c.Rel (c.prev j) j
⊢ (K.extend e).d i' j' ≫ Iso.hom (K.extendXIso e hj') ≫ φ = 0

Tactic:
rw [K.extend_d_to_eq_zero e i' j' j hj', zero_comp]

Premises used: HomologicalComplex.extend_d_to_eq_zero, CategoryTheory.Limits.zero_comp
-- 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 : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij neg : ¬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 : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : ¬c.Rel i j
⊢ ¬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 : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : ¬c.Rel i j
⊢ ¬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 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
rw : Fork.ι cone ≫ Iso.inv (K.extendXIso e hj') ≫ (K.extend e).d j' k' = 0
rw₁ : Fork.ι cone ≫ K.d j k = 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := cone.pt ⟶ K.X k) 0 0
⊢ (Fork.ι cone ≫ 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' cone.ι, cone.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.KernelFork.condition, CategoryTheory.Limits.Fork.ι, 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 : 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
pos : ∀ (hij : c.Rel i j), f' ≫ φ = 0 ↔ f'' ≫ φ = 0
neg : ∀ (hij : ¬c.Rel i j), f' ≫ φ = 0 ↔ f'' ≫ φ = 0
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0

Tactic:
by_cases hij : c.Rel i j

Premises used: ComplexShape.Rel