mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ Z✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ autoParam
    ({ f := (CategoryTheory.shiftFunctor C n).map (f ≫ g).f, comm := ⋯ }.f =
      ({ f := (CategoryTheory.shiftFunctor C n).map f.f, comm := ⋯ } ≫
          { f := (CategoryTheory.shiftFunctor C n).map g.f, comm := ⋯ }).f)
    ext._auto_1

Tactic:
dsimp

Goal state after:
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X✝ Y✝ Z✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ autoParam
    ((CategoryTheory.shiftFunctor C n).map (f.f ≫ g.f) =
      (CategoryTheory.shiftFunctor C n).map f.f ≫ (CategoryTheory.shiftFunctor C n).map g.f)
    ext._auto_1
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ : ι
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
hi₀₁ : c.Rel i₀ k₀
h : i₀ ≠ k₀
φ₁ : X₁ ⟶ K.X k₀
comm : φ₀ ≫ K.d i₀ k₀ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel k₀ k → φ₁ ≫ K.d k₀ k = 0
⊢ (if hk₁ : k₀ = k₀ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0) ≫ K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0

Tactic:
dsimp

Goal state after:
case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ : ι
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
hi₀₁ : c.Rel i₀ k₀
h : i₀ ≠ k₀
φ₁ : X₁ ⟶ K.X k₀
comm : φ₀ ≫ K.d i₀ k₀ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel k₀ k → φ₁ ≫ K.d k₀ k = 0
⊢ (if k₀ = k₀ then 𝟙 ((double f hi₀₁).X k₀) ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ 𝟙 (K.X k₀) else 0) ≫ K.d k₀ k₁ =
    (double f hi₀₁).d k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ ≫ eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case refine_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X : DifferentialObject S C
⊢ ((shiftFunctor C (m + n)).obj X).d ≫ (CategoryTheory.shiftFunctor C 1).map (shiftAdd X.obj m n).hom =
    (shiftAdd X.obj m n).hom ≫ ((shiftFunctor C m ⋙ shiftFunctor C n).obj X).d

Tactic:
dsimp

Goal state after:
case refine_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X : DifferentialObject S C
⊢ ((CategoryTheory.shiftFunctor C (m + n)).map X.d ≫ (shiftFunctorComm C 1 (m + n)).hom.app X.obj) ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj) =
    (CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj ≫
      (CategoryTheory.shiftFunctor C n).map
          ((CategoryTheory.shiftFunctor C m).map X.d ≫ (shiftFunctorComm C 1 m).hom.app X.obj) ≫
        (shiftFunctorComm C 1 n).hom.app ((CategoryTheory.shiftFunctor C m).obj X.obj)
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case refine_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X : DifferentialObject S C
⊢ (CategoryTheory.shiftFunctor C m ⋙ CategoryTheory.shiftFunctor C n).map X.d ≫
      (CategoryTheory.shiftFunctorAdd C m n).inv.app ((CategoryTheory.shiftFunctor C 1).obj X.obj) ≫
        (shiftFunctorComm C 1 (m + n)).hom.app X.obj ≫
          (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj) =
    (CategoryTheory.shiftFunctor C n).map
        ((CategoryTheory.shiftFunctor C m).map X.d ≫ (shiftFunctorComm C 1 m).hom.app X.obj) ≫
      (shiftFunctorComm C 1 n).hom.app ((CategoryTheory.shiftFunctor C m).obj X.obj)

Tactic:
dsimp

Goal state after:
case refine_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X : DifferentialObject S C
⊢ (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C m).map X.d) ≫
      (CategoryTheory.shiftFunctorAdd C m n).inv.app ((CategoryTheory.shiftFunctor C 1).obj X.obj) ≫
        (shiftFunctorComm C 1 (m + n)).hom.app X.obj ≫
          (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj) =
    (CategoryTheory.shiftFunctor C n).map
        ((CategoryTheory.shiftFunctor C m).map X.d ≫ (shiftFunctorComm C 1 m).hom.app X.obj) ≫
      (shiftFunctorComm C 1 n).hom.app ((CategoryTheory.shiftFunctor C m).obj X.obj)
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case refine_2
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ autoParam
    (((shiftFunctor C (m + n)).map f ≫ (mkIso (shiftAdd Y✝.obj m n) ⋯).hom).f =
      ((mkIso (shiftAdd X✝.obj m n) ⋯).hom ≫ (shiftFunctor C m ⋙ shiftFunctor C n).map f).f)
    ext._auto_1

Tactic:
dsimp

Goal state after:
case refine_2
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
m n : S
X✝ Y✝ : DifferentialObject S C
f : X✝ ⟶ Y✝
⊢ autoParam
    ((CategoryTheory.shiftFunctor C (m + n)).map f.f ≫ (mkIso (shiftAdd Y✝.obj m n) ⋯).hom.f =
      (mkIso (shiftAdd X✝.obj m n) ⋯).hom.f ≫
        (CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctor C m).map f.f))
    ext._auto_1
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
⊢ (ComplexShape.embeddingUpIntLE (-1)).f n = Int.negSucc n

Tactic:
dsimp

Goal state after:
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''
n : ℕ
⊢ -1 - ↑n = Int.negSucc n
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n + 1) = Int.negSucc (n + 1)

Tactic:
dsimp

Goal state after:
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''
n : ℕ
⊢ -1 - (↑n + 1) = Int.negSucc (n + 1)
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case refine_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ ((shiftFunctor C 0).obj X).d ≫ (CategoryTheory.shiftFunctor C 1).map ((shiftFunctorZero C S).app X.obj).hom =
    (CategoryTheory.shiftFunctor C 0).map ((𝟭 (DifferentialObject S C)).obj X).2 ≫
      (shiftFunctorZero C S).hom.app ((CategoryTheory.shiftFunctor C 1).obj ((𝟭 (DifferentialObject S C)).obj X).1)

Tactic:
dsimp

Goal state after:
case refine_1
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
X : DifferentialObject S C
⊢ ((CategoryTheory.shiftFunctor C 0).map X.d ≫ (shiftFunctorComm C 1 0).hom.app X.obj) ≫
      (CategoryTheory.shiftFunctor C 1).map ((shiftFunctorZero C S).hom.app X.obj) =
    (CategoryTheory.shiftFunctor C 0).map X.2 ≫
      (shiftFunctorZero C S).hom.app ((CategoryTheory.shiftFunctor C 1).obj X.1)
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = ↑n
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology L n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0)).HasHomology n
⊢ (ComplexShape.embeddingUpIntGE 0).f (n - 1) = m - 1

Tactic:
by have := NeZero.ne n; cases n <;> simp <;> lia

Goal state after:
Module: Mathlib.Algebra.Homology.Functor

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i : ι
⊢ { f := fun i ↦ (C.X i).map (𝟙 t), comm' := ⋯ }.f i =
    (𝟙 { X := fun i ↦ (C.X i).obj t, d := fun i j ↦ (C.d i j).app t, shape := ⋯, d_comp_d' := ⋯ }).f i

Tactic:
dsimp

Goal state after:
T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
t : T
i : ι
⊢ (C.X i).map (𝟙 t) = 𝟙 ((C.X i).obj t)
Module: Mathlib.Algebra.Homology.Functor

Goal state before:
pp: T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
X✝ Y✝ Z✝ : T
h₁ : X✝ ⟶ Y✝
h₂ : Y✝ ⟶ Z✝
i : ι
⊢ { f := fun i ↦ (C.X i).map (h₁ ≫ h₂), comm' := ⋯ }.f i =
    ({ f := fun i ↦ (C.X i).map h₁, comm' := ⋯ } ≫ { f := fun i ↦ (C.X i).map h₂, comm' := ⋯ }).f i

Tactic:
dsimp

Goal state after:
T : Type u_1
inst✝² : Category.{v_1, u_1} T
V : Type u_2
inst✝¹ : Category.{v_2, u_2} V
inst✝ : HasZeroMorphisms V
ι : Type u_3
c : ComplexShape ι
C : HomologicalComplex (T ⥤ V) c
X✝ Y✝ Z✝ : T
h₁ : X✝ ⟶ Y✝
h₂ : Y✝ ⟶ Z✝
i : ι
⊢ (C.X i).map (h₁ ≫ h₂) = (C.X i).map h₁ ≫ (C.X i).map h₂
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: 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''
n : ℕ
inst✝² : NeZero n
m : ℤ
hm : m = -↑(n + 1)
inst✝¹ : HasHomology h.cochainComplex m
inst✝ : HasHomology K n
this : (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).HasHomology n
⊢ (ComplexShape.embeddingUpIntLE (-1)).f (n - 1) = m + 1

Tactic:
by have := NeZero.ne n; cases n <;> simp <;> lia

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso ((twoδ₂Toδ₁ f g fg h).app 0)

Tactic:
dsimp

Goal state after:
case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso (𝟙 i)
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso ((twoδ₂Toδ₁ f g fg h).app 1)

Tactic:
dsimp

Goal state after:
case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso g
⊢ IsIso g
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso ((twoδ₁Toδ₀ f g fg h).app 0)

Tactic:
dsimp

Goal state after:
case left
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso f
Module: Mathlib.CategoryTheory.ComposableArrows.Two

Goal state before:
pp: case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso ((twoδ₁Toδ₀ f g fg h).app 1)

Tactic:
dsimp

Goal state after:
case right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
i j k : C
f : i ⟶ j
g : j ⟶ k
fg : i ⟶ k
h : f ≫ g = fg
inst✝ : IsIso f
⊢ IsIso (𝟙 k)
Module: Mathlib.Algebra.Homology.LeftResolution.Transport

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
A' : Type u_3
C' : Type u_4
inst✝¹ : Category.{v_3, u_4} C'
inst✝ : Category.{v_4, u_3} A'
ι : C ⥤ A
Λ : LeftResolution ι
ι' : C' ⥤ A
G : C ⥤ C'
e : G ⋙ ι' ≅ ι
x✝ : A
⊢ Epi (((Λ.F.associator G ι').hom ≫ Λ.F.whiskerLeft e.hom ≫ Λ.π).app x✝)

Tactic:
dsimp

Goal state after:
A : Type u_1
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Category.{v_2, u_1} A
A' : Type u_3
C' : Type u_4
inst✝¹ : Category.{v_3, u_4} C'
inst✝ : Category.{v_4, u_3} A'
ι : C ⥤ A
Λ : LeftResolution ι
ι' : C' ⥤ A
G : C ⥤ C'
e : G ⋙ ι' ≅ ι
x✝ : A
⊢ Epi (𝟙 (ι'.obj (G.obj (Λ.F.obj x✝))) ≫ e.hom.app (Λ.F.obj x✝) ≫ Λ.π.app x✝)
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
⊢ ((Cofork.π (CokernelCofork.ofπ (pOpcycles P.complex 0) ⋯) ≫
          (P.complex.isoHomologyι₀.symm ≪≫
              isoOfQuasiIsoAt P.π 0 ≪≫ singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z).hom) ≫
        (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 P.cokernelCofork.pt).inv) ≫
      (isoHomologyι₀ ((single C (ComplexShape.down ℕ) 0).obj P.cokernelCofork.pt)).hom =
    (Cofork.π P.cokernelCofork ≫ (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 P.cokernelCofork.pt).inv) ≫
      (isoHomologyι₀ ((single C (ComplexShape.down ℕ) 0).obj P.cokernelCofork.pt)).hom

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
⊢ ((pOpcycles P.complex 0 ≫
          P.complex.isoHomologyι₀.inv ≫ homologyMap P.π 0 ≫ (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z).hom) ≫
        (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z).inv) ≫
      ((single C (ComplexShape.down ℕ) 0).obj Z).homologyι 0 =
    (P.π.f 0 ≫ (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z).inv) ≫
      ((single C (ComplexShape.down ℕ) 0).obj Z).homologyι 0
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
P : Karoubi C
⊢ ((((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).app
        P).f =
    (({ 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 φ).app
        P).f

Tactic:
dsimp

Goal state after:
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
P : Karoubi C
⊢ ((X.map ((toKaroubi C).map P.p)).f ≫ (φ.app ((toKaroubi C).obj P.X)).f) ≫ (Y.map P.decompId_p).f =
    (X.map P.decompId_p).f ≫ (φ.app P).f
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
P : Karoubi C
⊢ (((functorExtension₁ C D).map ((functorExtension₁CompWhiskeringLeftToKaroubiIso C D).symm.hom.app F) ≫
            (KaroubiUniversal₁.counitIso C D).hom.app ((functorExtension₁ C D).obj F)).app
        P).f =
    ((𝟙 ((functorExtension₁ C D).obj F)).app P).f

Tactic:
dsimp

Goal state after:
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
P : Karoubi C
⊢ ((F.map P.p).f ≫ (F.obj P.X).p) ≫ (F.map P.p).f = (F.map P.p).f
Module: Mathlib.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: case e_a.e_a
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 { X := P.X, p := 𝟙 P.X, idem := ⋯ } =
    (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).map
          (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ)).app
      P.X

Tactic:
dsimp

Goal state after:
case e_a.e_a
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 { X := P.X, p := 𝟙 P.X, idem := ⋯ } =
    (((whiskeringLeft C (Karoubi C) D).obj (toKaroubi C)).preimage τ).app ((toKaroubi C).obj P.X)
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
⊢ (((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 := ⋯ }).app
      X =
    τ.app X

Tactic:
dsimp

Goal state after:
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
⊢ F.map ((toKaroubi C).obj X).decompId_i ≫ τ.app X ≫ G.map ((toKaroubi C).obj X).decompId_p = τ.app X
Module: Mathlib.CategoryTheory.Abelian.Projective.Resolution

Goal state before:
pp: case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ { X₁ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj (ofComplex Z)).X₁,
        X₂ := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj (ofComplex Z)).X₂,
        X₃ :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj
              ((ChainComplex.single₀ C).obj Z)).X₂,
        f := ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).obj (ofComplex Z)).f,
        g :=
          ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).map
              (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩)).τ₂,
        zero := ⋯ }.Exact ∧
    Epi
      ((HomologicalComplex.shortComplexFunctor' C (ComplexShape.down ℕ) 1 0 0).map
          (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩)).τ₂

Tactic:
dsimp

Goal state after:
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ { X₁ := (ofComplex Z).X 1, X₂ := (ofComplex Z).X 0, X₃ := Z, f := (ofComplex Z).d 1 0,
        g := (((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩).f 0, zero := ⋯ }.Exact ∧
    Epi ((((ofComplex Z).toSingle₀Equiv Z).symm ⟨Projective.π Z, ⋯⟩).f 0)
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:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Epi (Projective.π Z)
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
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
F : C ⥤ D
inst✝ : F.Additive
⊢ F.leftDerivedToHomotopyCategory.map f ≫ (Q.isoLeftDerivedToHomotopyCategoryObj F).hom =
    (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map φ

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
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
F : C ⥤ D
inst✝ : F.Additive
⊢ F.leftDerivedToHomotopyCategory.map f ≫ (Q.isoLeftDerivedToHomotopyCategoryObj F).hom =
    (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)