mathlib-initiative/mathlib-tactics huggingface dataset:
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''
α : Cochain K ((singleFunctor C q).obj X) (n - 1)
g : K.X p'' ⟶ X
hα : n.negOnePow • Cochain.toSingleMk (K.d p p'' ≫ g) h = Cochain.toSingleMk f h
hg : Cochain.toSingleMk g ⋯ = α
⊢ (Cochain.toSingleEquiv h).symm (K.d p p'' ≫ (n.negOnePow • g)) = (Cochain.toSingleEquiv h).symm f

Tactic:
by

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
⊢ ((((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).obj P).p ≫
      (G.map P.decompId_p).f ≫ (((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).obj P).p =
    (G.map P.decompId_p).f

Tactic:
by

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 Q : Karoubi C
f : P ⟶ Q
⊢ (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).map f ≫
      { f := (G.map Q.decompId_p).f, comm := ⋯ } =
    { f := (G.map P.decompId_p).f, comm := ⋯ } ≫ ((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).map f

Tactic:
by

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) ≫
      { X₁ := Q.complex.X (0 + 2), X₂ := Q.complex.X (0 + 1), X₃ := Q.complex.X 0, f := Q.complex.d (0 + 2) (0 + 1),
          g := Q.complex.d (0 + 1) 0, zero := ⋯ }.g =
    0

Tactic:
by

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
⊢ (((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).obj P).p ≫
      (G.map P.decompId_i).f ≫
        ((((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).obj P).p =
    (G.map P.decompId_i).f

Tactic:
by

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
p'' : ℤ
hp'' : p + 1 = p''
g : K.X p'' ⟶ X
hf : K.d p' p ≫ K.d p p'' ≫ g = 0
⊢ p'' + (n - 1) = q

Tactic:
by

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 Q : Karoubi C
f : P ⟶ Q
⊢ ((𝟭 (Karoubi C ⥤ Karoubi D)).obj G).map f ≫ { f := (G.map Q.decompId_i).f, comm := ⋯ } =
    { f := (G.map P.decompId_i).f, comm := ⋯ } ≫
      (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G).map f

Tactic:
by

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
n : ℕ
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') ≫
      { X₁ := Q.complex.X (n + 1 + 2), X₂ := Q.complex.X (n + 1 + 1), X₃ := Q.complex.X (n + 1),
          f := Q.complex.d (n + 1 + 2) (n + 1 + 1), g := Q.complex.d (n + 1 + 1) (n + 1), zero := ⋯ }.g =
    0

Tactic:
by

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
p'' : ℤ
hp'' : p + 1 = p''
g : K.X p'' ⟶ X
hf : K.d p' p ≫ K.d p p'' ≫ g = 0
⊢ δ (n - 1) n (n.negOnePow • Cochain.toSingleMk g ⋯) = ↑(toSingleMk (K.d p p'' ≫ g) h p' hp' hf)

Tactic:
by

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:
by

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:
by

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
⊢ { app := fun P ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ } ≫
      { app := fun P ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ } =
    𝟙 (((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).obj G)

Tactic:
by

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''
⊢ toSingleMk f h p' hp' hf ∈ coboundaries K ((singleFunctor C q).obj X) n ↔ ∃ g, K.d p p'' ≫ g = f

Tactic:
by

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
⊢ { app := fun P ↦ { f := (G.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ } ≫
      { app := fun P ↦ { f := (G.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ } =
    𝟙 ((𝟭 (Karoubi C ⥤ Karoubi D)).obj G)

Tactic:
by

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:
by

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
X Y : Karoubi C ⥤ Karoubi D
φ : X ⟶ Y
⊢ ((whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C) ⋙ functorExtension₁ C D).map φ ≫
      { hom := { app := fun P ↦ { f := (Y.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ },
          inv := { app := fun P ↦ { f := (Y.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom =
    { hom := { app := fun P ↦ { f := (X.map P.decompId_p).f, comm := ⋯ }, naturality := ⋯ },
          inv := { app := fun P ↦ { f := (X.map P.decompId_i).f, comm := ⋯ }, naturality := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      (𝟭 (Karoubi C ⥤ Karoubi D)).map φ

Tactic:
by

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
g h : P.complex ⟶ Q.complex
g_comm : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
h_comm : h ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (g - h) ≫ Q.π = 0

Tactic:
by

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
⊢ (functorExtension₁ C D).map ((functorExtension₁CompWhiskeringLeftToKaroubiIso C D).symm.hom.app F) ≫
      (KaroubiUniversal₁.counitIso C D).hom.app ((functorExtension₁ C D).obj F) =
    𝟙 ((functorExtension₁ C D).obj F)

Tactic:
by

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:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P : ProjectiveResolution X
⊢ Homotopy (lift (𝟙 X) P P) (𝟙 P.complex)

Tactic:
by

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
⊢ ∀ {X Y : C ⥤ D} (f : X ⟶ Y),
    (functorExtension₂ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).map f ≫
        (NatIso.ofComponents
            (fun X ↦
              {
                hom :=
                  {
                    f :=
                      𝟙
                        (((functorExtension₂ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj
                                Y).obj
                            X).X,
                    comm := ⋯ },
                inv := { f := 𝟙 ((((whiskeringRight C D (Karoubi D)).obj (toKaroubi D)).obj Y).obj X).X, comm := ⋯ },
                hom_inv_id := ⋯, inv_hom_id := ⋯ })
            ⋯).hom =
      (NatIso.ofComponents
            (fun X_1 ↦
              {
                hom :=
                  {
                    f :=
                      𝟙
                        (((functorExtension₂ C D ⋙ (whiskeringLeft C (Karoubi C) (Karoubi D)).obj (toKaroubi C)).obj
                                X).obj
                            X_1).X,
                    comm := ⋯ },
                inv := { f := 𝟙 ((((whiskeringRight C D (Karoubi D)).obj (toKaroubi D)).obj X).obj X_1).X, comm := ⋯ },
                hom_inv_id := ⋯, inv_hom_id := ⋯ })
            ⋯).hom ≫
        ((whiskeringRight C D (Karoubi D)).obj (toKaroubi D)).map f

Tactic:
by

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
inst✝ : IsIdempotentComplete D
⊢ (functorExtension₂ C D).IsEquivalence

Tactic:
by

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
inst✝ : IsIdempotentComplete D
⊢ (functorExtension C D).IsEquivalence

Tactic:
by

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
inst✝ : IsIdempotentComplete D
⊢ ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C) ⋙
      (whiskeringRight C D (Karoubi D)).obj (toKaroubi D) ⋙
        (whiskeringRight C (Karoubi D) D).obj (toKaroubi D).inv).IsEquivalence

Tactic:
by

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
inst✝ : IsIdempotentComplete D
⊢ ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).IsEquivalence

Tactic:
by

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

Goal state before:
pp: 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
⊢ Homotopy (lift (f ≫ g) P R) (lift f P Q ≫ lift g Q R)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P Q : ProjectiveResolution X
⊢ Homotopy (lift (𝟙 X ≫ 𝟙 X) P P) (𝟙 P.complex)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P Q : ProjectiveResolution X
⊢ Homotopy (lift (𝟙 X ≫ 𝟙 X) Q Q) (𝟙 Q.complex)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : IsIdempotentComplete D
F G : Karoubi C ⥤ D
τ : toKaroubi C ⋙ F ⟶ toKaroubi C ⋙ G
P : Karoubi C
⊢ (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app P =
    F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P Q : ProjectiveResolution X
⊢ (P.homotopyEquiv Q).hom ≫ Q.π = P.π

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P Q : ProjectiveResolution X
⊢ (P.homotopyEquiv Q).inv ≫ P.π = Q.π

Tactic:
by

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:
by

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✝ : HasProjectiveResolutions C
X : C
⊢ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map
      (ProjectiveResolution.lift (𝟙 X) (projectiveResolution X) (projectiveResolution X)) =
    𝟙 ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj (projectiveResolution X).complex)

Tactic:
by

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:
by

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✝ : HasProjectiveResolutions C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map
      (ProjectiveResolution.lift (f ≫ g) (projectiveResolution X✝) (projectiveResolution Z✝)) =
    (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map
        (ProjectiveResolution.lift f (projectiveResolution X✝) (projectiveResolution Y✝)) ≫
      (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map
        (ProjectiveResolution.lift g (projectiveResolution Y✝) (projectiveResolution Z✝))

Tactic:
by

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✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ P.iso.inv ≫ (projectiveResolutions C).map f = (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ ≫ Q.iso.inv

Tactic:
by

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 Y : Karoubi C
f : X ⟶ Y
⊢ F.map f ≫ F.map Y.decompId_i ≫ τ.app Y.X ≫ G.map Y.decompId_p =
    (F.map X.decompId_i ≫ τ.app X.X ≫ G.map X.decompId_p) ≫ G.map f

Tactic:
by

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✝ : HasProjectiveResolutions C
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
⊢ (projectiveResolutions C).map f ≫ Q.iso.hom = P.iso.hom ≫ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ

Tactic:
by

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:
by

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:
by

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
⊢ { X₁ := syzygies f, X₂ := X, X₃ := Y, f := d f, g := f, zero := ⋯ }.Exact

Tactic:
by

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:
by

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
⊢ (ofComplex Z).d 1 0 = d (Projective.π Z)

Tactic:
by

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:
by

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:
by

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
⊢ ((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map
      { app := fun P ↦ F.map P.decompId_i ≫ τ.app P.X ≫ G.map P.decompId_p, naturality := ⋯ } =
    τ

Tactic:
by

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
τ : F ⟶ G
⊢ {
      app := fun P ↦
        F.map P.decompId_i ≫ (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map τ).app P.X ≫ G.map P.decompId_p,
      naturality := ⋯ } =
    τ

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Ext

Goal state before:
pp: R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
x : Opposite.unop (Opposite.op ((ProjectiveResolution.self X).complex.X (n + 1))) ⟶ Y
⊢ n + 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Ext

Goal state before:
pp: R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ IsZero (((Ext R C (n + 1)).obj (Opposite.op X)).obj Y)

Tactic:
by

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 : ℕ
⊢ HomologicalComplex.ExactAt (ofComplex Z) (n + 1)

Tactic:
by

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 : ℕ
⊢ Projective ((ofComplex Z).X n)

Tactic:
by

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
⊢ (ofComplex Z).d 1 0 ≫ Projective.π Z = 0

Tactic:
by

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
⊢ Epi
    { X₁ := syzygies (Projective.π Z), X₂ := over Z, X₃ := Z, f := d (Projective.π Z), g := Projective.π Z,
        zero := ⋯ }.g

Tactic:
by

Goal state after: