mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case negSucc.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
m : ℕ
⊢ (h.map h (𝟙 K) (𝟙 L) ⋯).f (Int.negSucc (m + 1)) = (𝟙 h.cochainComplex).f (Int.negSucc (m + 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case ofNat
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
m : ℕ
⊢ (h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.ofNat m) =
    (h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.ofNat m)

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ (h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.negSucc 0) =
    (h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.negSucc 0)

Tactic:
simp

Goal state after:
case negSucc.zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
⊢ ((match -1 with
      | Int.ofNat n => fL.f n
      | Int.negSucc n => fK.f n) ≫
      match -1 with
      | Int.ofNat n => fL'.f n
      | Int.negSucc n => fK'.f n) =
    match -1 with
    | Int.ofNat n => fL.f n ≫ fL'.f n
    | Int.negSucc n => fK.f n ≫ fK'.f n
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case negSucc.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
fK' : K' ⟶ K''
fL' : L' ⟶ L''
f_comm' : fK'.f 0 ≫ h''.d₀ = h'.d₀ ≫ fL'.f 0
m : ℕ
⊢ (h.map h' fK fL f_comm ≫ h'.map h'' fK' fL' f_comm').f (Int.negSucc (m + 1)) =
    (h.map h'' (fK ≫ fK') (fL ≫ fL') ⋯).f (Int.negSucc (m + 1))

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case e_a
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
K K' : ChainComplex C ℕ
L L' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst✝⁴ : NeZero n
inst✝³ : HasHomology L n
inst✝² : HasHomology L' n
inst✝¹ : HasHomology h.cochainComplex ↑n
inst✝ : HasHomology h'.cochainComplex ↑n
⊢ pOpcycles h.cochainComplex ↑n ≫ opcyclesMap (h.map h' fK fL f_comm) ↑n =
    pOpcycles h.cochainComplex ↑n ≫
      (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n ⋯ ⋯ ⋯ ⋯).inv ≫
        opcyclesMap h.restrictionGEIso.hom n ≫
          opcyclesMap fL n ≫
            opcyclesMap h'.restrictionGEIso.inv n ≫
              (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntGE 0) (n - 1) n ⋯ ⋯ ⋯ ⋯).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case e_a
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
K K' : ChainComplex C ℕ
L L' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
fK : K ⟶ K'
fL : L ⟶ L'
f_comm : fK.f 0 ≫ h'.d₀ = h.d₀ ≫ fL.f 0
n : ℕ
inst✝⁴ : NeZero n
inst✝³ : HasHomology K n
inst✝² : HasHomology K' n
inst✝¹ : HasHomology h.cochainComplex (Int.negSucc n)
inst✝ : HasHomology h'.cochainComplex (Int.negSucc n)
⊢ pOpcycles h.cochainComplex (Int.negSucc n) ≫ opcyclesMap (h.map h' fK fL f_comm) (Int.negSucc n) =
    pOpcycles h.cochainComplex (Int.negSucc n) ≫
      (restrictionOpcyclesIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯).inv ≫
        opcyclesMap h.restrictionLEIso.hom n ≫
          opcyclesMap fK n ≫
            opcyclesMap h'.restrictionLEIso.inv n ≫
              (restrictionOpcyclesIso h'.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) (n + 1) n ⋯ ⋯ ⋯ ⋯).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : q + 1 = q'
⊢ single (((HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).hom ≫ f) ≫ K.d q q') n' +
      n'.negOnePow •
        single
          (((singleFunctor C p).obj X).d (p - 1) p ≫
            (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).hom ≫ f)
          n' =
    single ((HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).hom ≫ f ≫ K.d q q') n'

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : ¬q + 1 = q'
⊢ ¬(ComplexShape.up ℤ).Rel q q'

Tactic:
simp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : ¬q + 1 = q'
⊢ ¬q + 1 = q'
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
f : X ⟶ K.X q
⊢ (fun α ↦ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).inv ≫ α.v p q h) ((fun f ↦ fromSingleMk f h) f) =
    f

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
⊢ ∀ (x y : Cochain ((singleFunctor C p).obj X) K n),
    (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).inv ≫ (x + y).v p q h =
      (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).inv ≫ x.v p q h +
        (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).inv ≫ y.v p q h

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
n' p' : ℤ
h' : p' + n' = q
hp : p' + 1 = p
⊢ single
        ((f ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).inv) ≫
          ((singleFunctor C q).obj X).d q (q + 1))
        n' +
      n'.negOnePow • single (K.d p' p ≫ f ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).inv) n' =
    n'.negOnePow • single ((K.d p' p ≫ f) ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).inv) n'

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
n' p' : ℤ
h' : p' + n' = q
hp : ¬p' + 1 = p
⊢ ¬(ComplexShape.up ℤ).Rel p' p

Tactic:
simp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
n' p' : ℤ
h' : p' + n' = q
hp : ¬p' + 1 = p
⊢ ¬p' + 1 = p
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
f : K.X p ⟶ X
⊢ (fun α ↦ α.v p q h ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom) ((fun f ↦ toSingleMk f h) f) = f

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
⊢ ∀ (x y : Cochain K ((singleFunctor C q).obj X) n),
    (x + y).v p q h ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom =
      x.v p q h ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom +
        y.v p q h ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
⊢ Cochain.fromSingleMk (f ≫ K.d q q') (CochainComplex.HomComplex.Cocycle.fromSingleMk._proof_1 p q n h q' hq') = 0

Tactic:
hf

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
⊢ Cochain.fromSingleMk 0 (CochainComplex.HomComplex.Cocycle.fromSingleMk._proof_1 p q n h q' hq') = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
⊢ Cochain.fromSingleMk 0 (CochainComplex.HomComplex.Cocycle.fromSingleMk._proof_1 p q n h q' hq') = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
⊢ 0 ≫ K.d q q' = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
q'' : ℤ
hq'' : q'' + 1 = q
⊢ n - 1 + 1 = n

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Reduced

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
inst✝² : Preadditive C
inst✝¹ : Preadditive A
inst✝ : ι.Additive
X : A
⊢ ((toKaroubi A ⋙ F Λ ⋙ (functorExtension₂ C A).obj ι).obj X).p ≫ Λ.π.app X ≫ ((toKaroubi A).obj X).p = Λ.π.app X

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
⊢ (n + 1).negOnePow •
      Cochain.toSingleMk (K.d p' p ≫ f) (CochainComplex.HomComplex.Cocycle.toSingleMk._proof_1 p q n h p' hp') =
    0

Tactic:
hf

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
⊢ (n + 1).negOnePow • Cochain.toSingleMk 0 (CochainComplex.HomComplex.Cocycle.toSingleMk._proof_1 p q n h p' hp') = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
⊢ (n + 1).negOnePow • Cochain.toSingleMk 0 (CochainComplex.HomComplex.Cocycle.toSingleMk._proof_1 p q n h p' hp') = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.LeftResolution.Reduced

Goal state before:
pp: case h₂
A : Type u_1
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
inst✝² : Preadditive C
inst✝¹ : Preadditive A
inst✝ : ι.Additive
X : A
⊢ (Arrow.Hom.right
        (Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ } (𝟙 (Arrow.mk ((π' Λ).app X)).right) ⋯ ≫
          Arrow.homMk { f := ι.map ((F' Λ).obj X).p, comm := ⋯ } (𝟙 (Arrow.mk ((toKaroubi A).map (Λ.π.app X))).right)
            ⋯)).f =
    (Arrow.Hom.right (𝟙 (Arrow.mk ((π' Λ).app X)))).f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ (ComplexShape.down ℕ).next (n + 1) = n

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ P.complex.d n (n + 1) ≫ P.complex.d (n + 1) (n + 2) = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
⊢ K.d p' p ≫ 0 = 0

Tactic:
simp

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
p' : ℤ
hp' : p' + 1 = p
hf : K.d p' p ≫ f = 0
p'' : ℤ
hp'' : p + 1 = p''
⊢ n - 1 + 1 = n

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
n : ℕ
⊢ Epi (P.π.f n)

Tactic:
cases n
  · exact epi_of_isColimit_cofork P.isColimitCokernelCofork
  · rw [π_f_succ]; infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: case succ
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
inst✝ : Projective Z
n✝ : ℕ
⊢ n✝ + 1 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ Karoubi D
X Y : C
f : X ⟶ Y
⊢ ((functorExtension₁ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).map f ≫
      { hom := { f := (F.obj Y).p, comm := ⋯ }, inv := { f := (F.obj Y).p, comm := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom =
    { hom := { f := (F.obj X).p, comm := ⋯ }, inv := { f := (F.obj X).p, comm := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      ((𝟭 (C ⥤ Karoubi D)).obj F).map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
f : Y ⟶ Z
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
⊢ (P.π ≫ (ChainComplex.single₀ C).map f).f 0 = P.π.f 0 ≫ f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ (toKaroubi C).map P.p ≫ P.decompId_p ≫ 𝟙 P = P.decompId_p

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
G : Karoubi C ⥤ Karoubi D
P : Karoubi C
⊢ 𝟙 P ≫ P.decompId_i ≫ (toKaroubi C).map P.p = P.decompId_i

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
⊢ f.f 0 = liftHomotopyZeroZero f comm ≫ Q.complex.d 1 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
⊢ f.f 1 = P.complex.d 1 0 ≫ liftHomotopyZeroZero f comm + liftHomotopyZeroOne f comm ≫ Q.complex.d 2 1

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
Y Z : C
P : ProjectiveResolution Y
Q : ProjectiveResolution Z
f : P.complex ⟶ Q.complex
comm : f ≫ Q.π = 0
n : ℕ
x✝ :
  (f_1 : P.complex.X n ⟶ Q.complex.X (n + 1)) ×'
    (f' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) ×'
      f.f (n + 1) = P.complex.d (n + 1) n ≫ f_1 + f' ≫ Q.complex.d (n + 2) (n + 1)
g : P.complex.X n ⟶ Q.complex.X (n + 1)
g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)
w : f.f (n + 1) = P.complex.d (n + 1) n ≫ g + g' ≫ Q.complex.d (n + 2) (n + 1)
⊢ f.f (n + 2) =
    P.complex.d (n + 2) (n + 1) ≫ ⟨g, ⟨g', w⟩⟩.snd.fst + liftHomotopyZeroSucc f n g g' w ≫ Q.complex.d (n + 3) (n + 2)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ D
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    ((functorExtension₂ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).map f ≫
        {
            hom :=
              {
                f :=
                  𝟙
                    (((functorExtension₂ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj
                        Y).X,
                comm := ⋯ },
            inv := { f := 𝟙 ((((whiskeringRight C D (Karoubi D)).obj (toKaroubi D)).obj F).obj Y).X, comm := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
      {
            hom :=
              {
                f :=
                  𝟙
                    (((functorExtension₂ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj F).obj
                        X).X,
                comm := ⋯ },
            inv := { f := 𝟙 ((((whiskeringRight C D (Karoubi D)).obj (toKaroubi D)).obj F).obj X).X, comm := ⋯ },
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        (((whiskeringRight C D (Karoubi D)).obj (toKaroubi D)).obj F).map f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: case g_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P : ProjectiveResolution X
⊢ lift (𝟙 X) P P ≫ P.π = P.π ≫ (ChainComplex.single₀ C).map (𝟙 X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: case h_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P : ProjectiveResolution X
⊢ 𝟙 P.complex ≫ P.π = P.π ≫ (ChainComplex.single₀ C).map (𝟙 X)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: case g_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : ProjectiveResolution X
Q : ProjectiveResolution Y
R : ProjectiveResolution Z
⊢ lift (f ≫ g) P R ≫ R.π = P.π ≫ (ChainComplex.single₀ C).map (f ≫ g)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: case h_comm
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
P : ProjectiveResolution X
Q : ProjectiveResolution Y
R : ProjectiveResolution Z
⊢ (lift f P Q ≫ lift g Q R) ≫ R.π = P.π ≫ (ChainComplex.single₀ C).map (f ≫ g)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi C
f : X ⟶ Y
⊢ f ≫ Y.decompId_i = X.decompId_i ≫ (toKaroubi C).map f.f

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
X Y : Karoubi C
f : X ⟶ Y
h₁ : f ≫ Y.decompId_i = X.decompId_i ≫ (toKaroubi C).map f.f
h₂ : (toKaroubi C ⋙ F).map f.f ≫ τ.app Y.X = τ.app X.X ≫ (toKaroubi C ⋙ G).map f.f
⊢ X.decompId_p ≫ f = (toKaroubi C).map f.f ≫ Y.decompId_p

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
⊢ d f ≫ f = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
⊢ kernel.ι f ≫ f = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z X₀✝ X₁✝ : C
f : X₁✝ ⟶ X₀✝
⊢ d f ≫ f = 0

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ (ComplexShape.down ℕ).prev (n + 1) = n + 1 + 1

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ (ComplexShape.down ℕ).next (n + 1) = n

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F G : Karoubi C ⥤ D
τ :
  ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj F ⟶
    ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).obj G
X : C
⊢ τ.app X ≫ G.map (𝟙 ((toKaroubi C).obj X)) = τ.app X

Tactic:
simp

Goal state after: