awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n : ℤ
φ : (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
h₃ :
  IsIso (X :=
    Precomp.obj
      (mk₄ (X₀ := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₂))
        (X₁ :=
        Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
        (X₂ := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1)) (Functor.obj (quotient C (up ℤ)) S.X₁))
        (X₄ :=
        Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
          (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
        (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) n)
          (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f)))
        (Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0)
          (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁) (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))
          n (n + 1) ⋯)
        (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
          (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f))
        (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
          (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))))
      (Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₁)) 3)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) S.X₁)
⊢ IsIso (app' φ 3 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6)

Tactic:
dsimp [φ]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n : ℤ
φ : (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ IsIso (X :=
    Precomp.obj
      (mk₄ (X₀ := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₂))
        (X₁ :=
        Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
        (X₂ := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1)) (Functor.obj (quotient C (up ℤ)) S.X₁))
        (X₄ :=
        Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
          (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
        (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) n)
          (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f)))
        (Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0)
          (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁) (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))
          n (n + 1) ⋯)
        (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
          (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f))
        (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
          (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))))
      (Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₁)) 3)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) S.X₁)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n : ℤ
φ : (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
h₄ :
  Mono (X :=
    Precomp.obj
      (mk₄ (X₀ := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₂))
        (X₁ :=
        Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
        (X₂ := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1)) (Functor.obj (quotient C (up ℤ)) S.X₁))
        (X₄ :=
        Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
          (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
        (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) n)
          (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f)))
        (Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0)
          (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁) (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))
          n (n + 1) ⋯)
        (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
          (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f))
        (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
          (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))))
      (Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₁)) 4)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) S.X₂)
⊢ Mono (app' φ 4 Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7)

Tactic:
dsimp [φ]
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n : ℤ
φ : (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ Mono (X :=
    Precomp.obj
      (mk₄ (X₀ := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₂))
        (X₁ :=
        Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
        (X₂ := Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1)) (Functor.obj (quotient C (up ℤ)) S.X₁))
        (X₄ :=
        Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
          (Functor.obj (quotient C (up ℤ)) (mappingCone S.f)))
        (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) n)
          (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f)))
        (Functor.homologySequenceδ (homologyFunctor C (up ℤ) 0)
          (Triangle.mk (X := Functor.obj (quotient C (up ℤ)) S.X₁) (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f)
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))
            (CategoryTheory.Functor.map (quotient C (up ℤ)) (triangle S.f).mor₃ ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso (quotient C (up ℤ)) 1)) S.X₁))
          n (n + 1) ⋯)
        (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
          (CategoryTheory.Functor.map (quotient C (up ℤ)) S.f))
        (CategoryTheory.Functor.map (Functor.shift (homologyFunctor C (up ℤ) 0) (n + 1))
          (CategoryTheory.Functor.map (quotient C (up ℤ)) (inr S.f))))
      (Functor.obj (Functor.shift (homologyFunctor C (up ℤ) 0) n) (Functor.obj (quotient C (up ℤ)) S.X₁)) 4)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) S.X₂)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n : ℤ
φ : (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ IsIso (X := Functor.obj (quotient C (up ℤ) ⋙ homologyFunctor C (up ℤ) n) (mappingCone S.f)) (Y :=
    HomologicalComplex.homology S.X₃ n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (mappingCone S.f) ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)

Tactic:
have : IsIso ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
        HomologicalComplex.homologyMap (descShortComplex S) n) := by
      apply Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono
        ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅_exact _
          (mappingCone_triangleh_distinguished S.f) n _ rfl).δlast
        (composableArrows₅_exact hS n _ rfl).δlast φ
      all_goals dsimp [φ]; infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
hS : S.ShortExact
n : ℤ
φ : (Functor.homologySequenceComposableArrows₅ (homologyFunctor C (up ℤ) 0) (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₂)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₁)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) (n + 1))) (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
this :
  IsIso (X := Functor.obj (quotient C (up ℤ) ⋙ homologyFunctor C (up ℤ) n) (mappingCone S.f)) (Y :=
    HomologicalComplex.homology S.X₃ n)
    (NatTrans.app (Iso.hom (homologyFunctorFactors C (up ℤ) n)) (mappingCone S.f) ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
⊢ IsIso (X := HomologicalComplex.homology (mappingCone S.f) n) (Y := HomologicalComplex.homology S.X₃ n)
    (HomologicalComplex.homologyMap (descShortComplex S) n)

Tactic:
apply IsIso.of_isIso_comp_left ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f))

Premises used: CategoryTheory.IsIso.of_isIso_comp_left, HomotopyCategory.homologyFunctorFactors, CochainComplex.mappingCone, Int, CategoryTheory.ShortComplex.f, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
f : S₁ ⟶ S₂
h :
  ∀ (n : ℤ),
    HomologicalComplex.Hom.f (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂) n = (descShortComplex S₁ ≫ f.τ₃).f n
⊢ map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂ = descShortComplex S₁ ≫ f.τ₃

Tactic:
ext n
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
f : S₁ ⟶ S₂
n : ℤ
h :
  CategoryStruct.comp (Y := (mappingCone S₁.f).X n)
      (HomComplex.Cochain.v (inl S₁.f) (n + 1) n ⋯ : S₁.X₁.X (n + 1) ⟶ (mappingCone S₁.f).X n)
      (HomologicalComplex.Hom.f (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂) n :
        (mappingCone S₁.f).X n ⟶ S₂.X₃.X n) =
    HomComplex.Cochain.v (inl S₁.f) (n + 1) n ⋯ ≫ (descShortComplex S₁ ≫ f.τ₃).f n
h₁ :
  CategoryStruct.comp (Y := (mappingCone S₁.f).X n)
      (HomologicalComplex.Hom.f (inr S₁.f) n : S₁.X₂.X n ⟶ (mappingCone S₁.f).X n)
      (HomologicalComplex.Hom.f (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂) n :
        (mappingCone S₁.f).X n ⟶ S₂.X₃.X n) =
    HomologicalComplex.Hom.f (inr S₁.f) n ≫ (descShortComplex S₁ ≫ f.τ₃).f n
⊢ HomologicalComplex.Hom.f (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂) n = (descShortComplex S₁ ≫ f.τ₃).f n

Tactic:
apply ext_from _ (n + 1) n rfl

Premises used: CochainComplex.mappingCone.ext_from, HAdd.hAdd, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
f : S₁ ⟶ S₂
n : ℤ
⊢ CategoryStruct.comp (Y := (mappingCone S₁.f).X n)
      (HomComplex.Cochain.v (inl S₁.f) (n + 1) n ⋯ : S₁.X₁.X (n + 1) ⟶ (mappingCone S₁.f).X n)
      (HomologicalComplex.Hom.f (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂) n :
        (mappingCone S₁.f).X n ⟶ S₂.X₃.X n) =
    HomComplex.Cochain.v (inl S₁.f) (n + 1) n ⋯ ≫ (descShortComplex S₁ ≫ f.τ₃).f n

Tactic:
simp [map]

Premises used: CochainComplex.mappingCone.map
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
S₁ S₂ : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
f : S₁ ⟶ S₂
n : ℤ
⊢ CategoryStruct.comp (Y := (mappingCone S₁.f).X n)
      (HomologicalComplex.Hom.f (inr S₁.f) n : S₁.X₂.X n ⟶ (mappingCone S₁.f).X n)
      (HomologicalComplex.Hom.f (map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂) n :
        (mappingCone S₁.f).X n ⟶ S₂.X₃.X n) =
    HomologicalComplex.Hom.f (inr S₁.f) n ≫ (descShortComplex S₁ ≫ f.τ₃).f n

Tactic:
simp [map, ← HomologicalComplex.comp_f, f.comm₂₃]

Premises used: CochainComplex.mappingCone.map, HomologicalComplex.comp_f, CategoryTheory.ShortComplex.Hom.comm₂₃
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
D : Type u_2
inst_2 : Category.{v_2, u_2} D
inst_3 : Abelian.{v_2, u_2} D
F : CategoryTheory.Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Additive
S : ShortComplex (CochainComplex.{v_1, u_1, 0} C ℤ)
n : ℤ
⊢ Eq (α :=
    HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (up ℤ)) (mappingCone S.f)) n ⟶
      HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (up ℤ)) S.X₃) n)
    (HomologicalComplex.Hom.f (CategoryTheory.Functor.map (F.mapHomologicalComplex (up ℤ)) (descShortComplex S)) n :
      HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (up ℤ)) (mappingCone S.f)) n ⟶
        HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (up ℤ)) S.X₃) n)
    (HomologicalComplex.Hom.f
        (CategoryStruct.comp (Y :=
          mappingCone (F := Functor.obj (F.mapHomologicalComplex (up ℤ)) S.X₁)
            (CategoryTheory.Functor.map (F.mapHomologicalComplex (up ℤ)) S.f))
          (Iso.hom (mapHomologicalComplexIso S.f F) :
            Quiver.Hom (V := HomologicalComplex.{v_2, u_2, 0} D (up ℤ))
              (Functor.obj (F.mapHomologicalComplex (up ℤ)) (mappingCone S.f))
              (mappingCone (F := Functor.obj (F.mapHomologicalComplex (up ℤ)) S.X₁)
                (CategoryTheory.Functor.map (F.mapHomologicalComplex (up ℤ)) S.f)))
          (descShortComplex (S.map (F.mapHomologicalComplex (up ℤ))) :
            Quiver.Hom (V := CochainComplex.{v_2, u_2, 0} D ℤ)
              (mappingCone (F := ShortComplex.X₁ (S.map (F.mapHomologicalComplex (up ℤ))))
                (ShortComplex.f (S.map (F.mapHomologicalComplex (up ℤ)))))
              (ShortComplex.X₃ (S.map (F.mapHomologicalComplex (up ℤ))))))
        n :
      HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (up ℤ)) (mappingCone S.f)) n ⟶
        HomologicalComplex.X (Functor.obj (F.mapHomologicalComplex (up ℤ)) S.X₃) n)

Tactic:
simp [mapHomologicalComplexIso, descShortComplex, mapHomologicalComplexXIso,
    mapHomologicalComplexXIso'_hom, Functor.mapHomologicalComplex_map_f,
    desc_f _ _ _ _ n (n + 1) rfl]

Premises used: CochainComplex.mappingCone.descShortComplex, CategoryTheory.Functor.mapHomologicalComplex_map_f, CochainComplex.mappingCone.mapHomologicalComplexXIso, HAdd.hAdd, CochainComplex.mappingCone.desc_f, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, OfNat.ofNat, rfl, CochainComplex.mappingCone.mapHomologicalComplexIso
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a a' : ℤ
ha' : n + a = a'
X : C
i : ℤ
⊢ a' = a + n

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a a' : ℤ
ha' : n + a = a'
X : C
i : ℤ
obtain :
  ∀ (ha' : n + a = a + n),
    HomologicalComplex.X.{v, u, 0}
        (Functor.obj
          (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
        i =
      HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i
⊢ HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) a' ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
      i =
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i

Tactic:
obtain rfl : a' = a + n := by lia

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
pos :
  ∀ (h : i = a),
    HomologicalComplex.X.{v, u, 0}
        (Functor.obj
          (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
        i =
      HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i
neg :
  ∀ (h : ¬i = a),
    HomologicalComplex.X.{v, u, 0}
        (Functor.obj
          (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
        i =
      HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i
⊢ HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      i =
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i

Tactic:
by_cases h : i = a
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : i = a
pos :
  ∀ (ha' : n + i = i + n),
    HomologicalComplex.X.{v, u, 0}
        (Functor.obj
          (single C (ComplexShape.up ℤ) (i + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n) X)
        i =
      HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) X) i
⊢ HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      i =
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i

Tactic:
subst h
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n : ℤ
X : C
i : ℤ
ha' : n + i = i + n
⊢ HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) (i + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      i =
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) i) X) i

Tactic:
simp only [Functor.comp_obj, shiftFunctor_obj_X', single_obj_X_self]

Premises used: CategoryTheory.Functor.comp_obj, HomologicalComplex.single_obj_X_self, CochainComplex.shiftFunctor_obj_X'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : ¬i = a
neg : (if i + n = a + n then X else 0) = if i = a then X else 0
⊢ HomologicalComplex.X.{v, u, 0}
      (Functor.obj (single C (ComplexShape.up ℤ) (a + n) ⋙ CategoryTheory.shiftFunctor (CochainComplex.{v, u, 0} C ℤ) n)
        X)
      i =
    HomologicalComplex.X.{v, u, 0} (Functor.obj (single C (ComplexShape.up ℤ) a) X) i

Tactic:
dsimp [single]

Premises used: HomologicalComplex.single
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : ¬i = a
h' : i + n = a + n
⊢ i = a

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a : ℤ
X : C
i : ℤ
ha' : n + a = a + n
h : ¬i = a
neg : (if i + n = a + n then X else 0) = 0
neg₁ neg₂ : Eq.{u + 1} (α := C) 0 0
⊢ (if i + n = a + n then X else 0) = if i = a then X else 0

Tactic:
rw [if_neg h, if_neg (fun h' => h (by lia))]

Premises used: if_neg
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasZeroObject.{v, u} C
n a a' : ℤ
ha' : n + a = a'
X Y : C
f : X ⟶ Y
⊢ a' = a + n

Tactic:
lia