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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
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) 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')
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) 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.{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')

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
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
hj : ∃ (j : ι), e.f j = j'
pos :
  ∀ (j : ι) (hj : 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) 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.{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')

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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
j : ι
hj : e.f j = j'
pos :
  ∀ (hij : j = i),
    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')
neg :
  ∀ (hij : ¬j = i),
    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.{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')

Tactic:
by_cases hij : j = 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
inst_3 : DecidableEq ι
e : c.Embedding c'
X : C
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
j : ι
hj : e.f j = j'
hij : j = i
rw : i' = e.f j
rw₁ : i' = e.f i
rw₂ rw₃ : i' = i'
⊢ i' = j'

Tactic:
rw [← hj, hij, h]
-- 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'
j' : ι'
j : ι
hj : e.f j = j'
hij : j = i
pos :
  ∀ (hj : e.f j = i'),
    Eq.{v_1 + 1} (α :=
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) i' ⟶
        HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) i')
      (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))
            ⋯))
        i')
      (Hom.f (𝟙 (extend (Functor.obj (single C c i) X) e)) i')
⊢ 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')

Tactic:
obtain rfl : i' = j' := by rw [← hj, hij, h]

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
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j : ι
hij : j = i
hj : e.f j = i'
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) i' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) i')
    (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)) ⋯))
      i')
    (Hom.f (𝟙 (extend (Functor.obj (single C c i) X) e)) i')

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'
j' : ι'
j : ι
hj : e.f j = j'
hij : ¬j = i
⊢ 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')

Tactic:
((isZero_single_obj_X _ _ _ _ hij).of_iso
          (((single C c i).obj X).extendXIso e hj)).eq_of_src _ _

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Limits.IsZero.eq_of_src, HomologicalComplex.extendXIso, CategoryTheory.Functor.obj, HomologicalComplex.single
-- 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'
j' : ι'
j : ι
hj : e.f j = j'
hij : ¬j = i
⊢ 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')

Tactic:
exact ((isZero_single_obj_X _ _ _ _ hij).of_iso
          (((single C c i).obj X).extendXIso e hj)).eq_of_src _ _

Premises used: HomologicalComplex.isZero_single_obj_X, CategoryTheory.Limits.IsZero.of_iso, CategoryTheory.Limits.IsZero.eq_of_src, HomologicalComplex.extendXIso, CategoryTheory.Functor.obj, HomologicalComplex.single
-- 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'
j' : ι'
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
inst_4 : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
j' : ι'
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) 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')

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'
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) i' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (Functor.obj (single C c' i') X) i')
    (Hom.f (Iso.hom (extendSingleIso e X i i' h)) i')
    (Iso.hom (extendXIso (Functor.obj (single C c i) X) e h) ≫
      Iso.hom (singleObjXSelf c i X) ≫ Iso.inv (singleObjXSelf c' i' X))

Tactic:
simp [extendSingleIso]

Premises used: HomologicalComplex.extendSingleIso
-- 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'
⊢ Eq.{v_1 + 1} (α :=
    HomologicalComplex.X.{v_1, u_3, u_2} (Functor.obj (single C c' i') X) i' ⟶
      HomologicalComplex.X.{v_1, u_3, u_2} (extend (Functor.obj (single C c i) X) e) i')
    (Hom.f (Iso.inv (extendSingleIso e X i i' h)) i')
    (Iso.hom (singleObjXSelf c' i' X) ≫
      Iso.inv (singleObjXSelf c i X) ≫ Iso.inv (extendXIso (Functor.obj (single C c i) X) e h))

Tactic:
simp [extendSingleIso]

Premises used: HomologicalComplex.extendSingleIso
-- 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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Projective.{v_1, u_3} (K.X i)
i' : ι'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Projective.{v_1, u_3} ((K.extend e).X i')
neg : ∀ (hi' : ∀ (i : ι), e.f i ≠ i'), Projective.{v_1, u_3} ((K.extend e).X i')
⊢ Projective.{v_1, u_3} ((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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Projective.{v_1, u_3} (K.X i)
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
pos : ∀ (i : ι) (hi : e.f i = i'), Projective.{v_1, u_3} ((K.extend e).X i')
⊢ Projective.{v_1, u_3} ((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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Projective.{v_1, u_3} (K.X i)
i' : ι'
i : ι
hi : e.f i = i'
⊢ Projective.{v_1, u_3} ((K.extend e).X i')

Tactic:
Projective.of_iso (K.extendXIso e hi).symm inferInstance

Premises used: inferInstance, CategoryTheory.Projective.of_iso, CategoryTheory.Iso.symm, 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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Projective.{v_1, u_3} (K.X i)
i' : ι'
i : ι
hi : e.f i = i'
⊢ Projective.{v_1, u_3} ((K.extend e).X i')

Tactic:
exact Projective.of_iso (K.extendXIso e hi).symm inferInstance

Premises used: inferInstance, CategoryTheory.Projective.of_iso, CategoryTheory.Iso.symm, 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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Projective.{v_1, u_3} (K.X i)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Projective.{v_1, u_3} ((K.extend e).X i')

Tactic:
(isZero_extend_X K e i' hi').projective

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.projective
-- 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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Projective.{v_1, u_3} (K.X i)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Projective.{v_1, u_3} ((K.extend e).X i')

Tactic:
exact (isZero_extend_X K e i' hi').projective

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.projective
-- 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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Injective.{v_1, u_3} (K.X i)
i' : ι'
pos : ∀ (hi' : ∃ (i : ι), e.f i = i'), Injective.{v_1, u_3} ((K.extend e).X i')
neg : ∀ (hi' : ∀ (i : ι), e.f i ≠ i'), Injective.{v_1, u_3} ((K.extend e).X i')
⊢ Injective.{v_1, u_3} ((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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Injective.{v_1, u_3} (K.X i)
i' : ι'
hi' : ∃ (i : ι), e.f i = i'
pos : ∀ (i : ι) (hi : e.f i = i'), Injective.{v_1, u_3} ((K.extend e).X i')
⊢ Injective.{v_1, u_3} ((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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Injective.{v_1, u_3} (K.X i)
i' : ι'
i : ι
hi : e.f i = i'
⊢ Injective.{v_1, u_3} ((K.extend e).X i')

Tactic:
Injective.of_iso (K.extendXIso e hi).symm inferInstance

Premises used: CategoryTheory.Injective.of_iso, inferInstance, CategoryTheory.Iso.symm, 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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Injective.{v_1, u_3} (K.X i)
i' : ι'
i : ι
hi : e.f i = i'
⊢ Injective.{v_1, u_3} ((K.extend e).X i')

Tactic:
exact Injective.of_iso (K.extendXIso e hi).symm inferInstance

Premises used: CategoryTheory.Injective.of_iso, inferInstance, CategoryTheory.Iso.symm, 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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Injective.{v_1, u_3} (K.X i)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Injective.{v_1, u_3} ((K.extend e).X i')

Tactic:
(isZero_extend_X K e i' hi').injective

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.injective
-- 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
e : c.Embedding c'
K : HomologicalComplex.{v_1, u_3, u_1} C c
inst_3 : ∀ (i : ι), Injective.{v_1, u_3} (K.X i)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Injective.{v_1, u_3} ((K.extend e).X i')

Tactic:
exact (isZero_extend_X K e i' hi').injective

Premises used: HomologicalComplex.isZero_extend_X, CategoryTheory.Limits.IsZero.injective
-- 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
⊢ Eq (α := (Functor.obj (e.extendFunctor C) K).X (e.f i) ⟶ (Functor.obj (e.extendFunctor C) L).X (e.f j))
    (φ.f (e.f i) ≫ (Functor.obj (e.extendFunctor C) L).d (e.f i) (e.f j))
    ((Functor.obj (e.extendFunctor C) K).d (e.f i) (e.f j) ≫ φ.f (e.f j))

Tactic:
have := φ.comm (e.f i) (e.f j)
-- 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 :
  Eq (α := (Functor.obj (e.extendFunctor C) K).X (e.f i) ⟶ (Functor.obj (e.extendFunctor C) L).X (e.f j))
    (φ.f (e.f i) ≫ (Functor.obj (e.extendFunctor C) L).d (e.f i) (e.f j))
    ((Functor.obj (e.extendFunctor C) K).d (e.f i) (e.f j) ≫ φ.f (e.f j))
⊢ φ.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)

Tactic:
simp only [extendFunctor_obj, K.extend_d_eq e rfl rfl, L.extend_d_eq e rfl rfl] at this

Premises used: HomologicalComplex.extend_d_eq, ComplexShape.Embedding.extendFunctor_obj, rfl