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

Goal state before:
pp: 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
m : ℤ
hmn : m = -↑(n + 1)
inst✝³ : HasHomology h.cochainComplex m
inst✝² : HasHomology K n
inst✝¹ : HasHomology h'.cochainComplex m
inst✝ : HasHomology K' n
⊢ homologyMap (h.map h' fK fL f_comm) m =
    (h.homologyIsoNeg n m hmn).hom ≫ homologyMap fK n ≫ (h'.homologyIsoNeg n m hmn).inv

Tactic:
by

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

Goal state before:
pp: 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)

Tactic:
by

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

Goal state before:
pp: 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)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
i j i' j' n : ℕ
x✝⁴ : i ≤ j
x✝³ : i' ≤ j'
x✝² : i ≤ i'
x✝¹ : j ≤ j'
x✝ : j' ≤ n
S : ComposableArrows C n
⊢ ((functorArrows C i j n ⋯ ⋯).obj S).map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ S.map' j j' x✝¹ x✝ =
    S.map' i i' x✝² ⋯ ≫ ((functorArrows C i' j' n ⋯ ⋯).obj S).map' 0 1 homMk₁._proof_4 homMk₁._proof_5

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
⊢ fromSingleMk 0 h = 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 : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
⊢ (fromSingleMk f h).v p q h = (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).hom ≫ f

Tactic:
by

Goal state after:
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'
eA : A' ≌ A
eC : C' ≌ C
e : ι' ⋙ eA.functor ≅ eC.functor ⋙ ι
x✝ : A'
⊢ Epi
    ((((eA.functor ⋙ Λ.F ⋙ eC.inverse) ⋙ ι').rightUnitor.inv ≫
          ((eA.functor ⋙ Λ.F ⋙ eC.inverse) ⋙ ι').whiskerLeft eA.unitIso.hom ≫
            ((eA.functor ⋙ Λ.F ⋙ eC.inverse).associator ι' (eA.functor ⋙ eA.inverse)).hom ≫
              (eA.functor ⋙ Λ.F ⋙ eC.inverse).whiskerLeft (ι'.associator eA.functor eA.inverse).inv ≫
                (eA.functor ⋙ Λ.F ⋙ eC.inverse).whiskerLeft (whiskerRight e.hom eA.inverse) ≫
                  ((eA.functor ⋙ Λ.F ⋙ eC.inverse).associator (eC.functor ⋙ ι) eA.inverse).inv ≫
                    whiskerRight ((eA.functor ⋙ Λ.F ⋙ eC.inverse).associator eC.functor ι).inv eA.inverse ≫
                      whiskerRight (whiskerRight (eA.functor.associator (Λ.F ⋙ eC.inverse) eC.functor).hom ι)
                          eA.inverse ≫
                        whiskerRight
                            (whiskerRight
                              (eA.functor.whiskerLeft
                                ((Λ.F.associator eC.inverse eC.functor).hom ≫
                                  Λ.F.whiskerLeft eC.counitIso.hom ≫ Λ.F.rightUnitor.hom))
                              ι)
                            eA.inverse ≫
                          whiskerRight
                              ((eA.functor.associator Λ.F ι).hom ≫
                                eA.functor.whiskerLeft Λ.π ≫ eA.functor.rightUnitor.hom)
                              eA.inverse ≫
                            eA.unitIso.inv).app
      x✝)

Tactic:
by

Goal state after:
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:
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 : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : q + 1 = q'
⊢ n + 1 = n'

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 : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : q + 1 = q'
⊢ p - 1 + 1 = p

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 : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
hq : ¬q + 1 = q'
⊢ ¬n + 1 = n'

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 : 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:
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 : X ⟶ K.X q
n : ℤ
h : p + n = q
n' q' : ℤ
h' : p + n' = q'
⊢ δ n n' (fromSingleMk f h) = fromSingleMk (f ≫ K.d q q') h'

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
α : Cochain ((singleFunctor C p).obj X) K n
⊢ (fun f ↦ fromSingleMk f h) ((fun α ↦ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).inv ≫ α.v p q h) α) =
    α

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
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:
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
⊢ ∀ (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:
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 : X ⟶ K.X q
n : ℤ
h : p + n = q
⊢ (fromSingleEquiv h) (fromSingleMk f h) = 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 ℤ
X' : C
g : X' ⟶ X
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
⊢ fromSingleMk (g ≫ f) h = (ofHom ((singleFunctor C p).map g)).comp (fromSingleMk f h) ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
D₁ D₂ : ComposableArrows (CochainComplex C ℤ) 2
φ : D₁ ⟶ D₂
⊢ (ComposableArrows.functorArrows (CochainComplex C ℤ) 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙
            composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)).map
        φ ≫
      ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj
          (CochainComplex.mappingConeCompTriangle
            (D₂.map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
            (D₂.map' 1 2 spectralObjectMappingCone._proof_2 spectralObjectMappingCone._proof_3))).mor₃ =
    ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj
          (CochainComplex.mappingConeCompTriangle
            (D₁.map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
            (D₁.map' 1 2 spectralObjectMappingCone._proof_2 spectralObjectMappingCone._proof_3))).mor₃ ≫
      (ComposableArrows.functorArrows (CochainComplex C ℤ) 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)) ⋙
              shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        φ

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 : X ⟶ K.X q
n : ℤ
h : p + n = q
L : CochainComplex C ℤ
g : K ⟶ L
⊢ (fromSingleEquiv h) (fromSingleMk (f ≫ g.f q) h) = (fromSingleEquiv h) ((fromSingleMk f h).comp (ofHom 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 n : ℤ
h : p + n = q
⊢ toSingleMk 0 h = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
D : ComposableArrows (CochainComplex C ℤ) 2
⊢ Pretriangulated.Triangle.mk
      ((composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)).map
        ((ComposableArrows.mapFunctorArrows (CochainComplex C ℤ) 0 1 0 2 2 SpectralObject._proof_6
              SpectralObject._proof_8 SpectralObject._proof_10 SpectralObject._proof_2 SpectralObject._proof_4).app
          D))
      ((composableArrowsFunctor C ⋙ quotient C (ComplexShape.up ℤ)).map
        ((ComposableArrows.mapFunctorArrows (CochainComplex C ℤ) 0 2 1 2 2 SpectralObject._proof_8
              SpectralObject._proof_2 SpectralObject._proof_6 SpectralObject._proof_4 SpectralObject._proof_4).app
          D))
      ({
            app := fun D ↦
              ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj
                  (CochainComplex.mappingConeCompTriangle
                    (D.map' 0 1 composableArrowsFunctor._proof_1 spectralObjectMappingCone._proof_2)
                    (D.map' 1 2 spectralObjectMappingCone._proof_2 spectralObjectMappingCone._proof_3))).mor₃,
            naturality := ⋯ }.app
        D) ∈
    CategoryTheory.Pretriangulated.distinguishedTriangles

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
⊢ (toSingleMk f h).v p q h = f ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).inv

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
n' p' : ℤ
h' : p' + n' = q
hp : p' + 1 = p
⊢ n + 1 = n'

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
n' p' : ℤ
h' : p' + n' = q
hp : p' + 1 = p
⊢ p' + 1 = p

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
n' p' : ℤ
h' : p' + n' = q
hp : ¬p' + 1 = p
⊢ ¬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
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
F G : Karoubi C ⥤ D
φ : F ⟶ G
P : Karoubi C
⊢ φ.app P = F.map P.decompId_i ≫ φ.app { X := P.X, p := 𝟙 P.X, idem := ⋯ } ≫ G.map P.decompId_p

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
P : Karoubi C
⊢ (F.map P.p).f ≫ (F.map P.p).f = (F.map P.p).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 : ℤ
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:
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
X✝ Y✝ : Karoubi C
f : X✝ ⟶ Y✝
⊢ { X := (F.obj X✝.X).X, p := (F.map X✝.p).f, idem := ⋯ }.p ≫
      (F.map f.f).f ≫ { X := (F.obj Y✝.X).X, p := (F.map Y✝.p).f, idem := ⋯ }.p =
    (F.map f.f).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 : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
n' p' : ℤ
h' : p' + n' = q
⊢ δ n n' (toSingleMk f h) = n'.negOnePow • toSingleMk (K.d p' p ≫ f) h'

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
α : Cochain K ((singleFunctor C q).obj X) n
⊢ (fun f ↦ toSingleMk f h) ((fun α ↦ α.v p q h ≫ (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).hom) α) = α

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
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:
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
⊢ ∀ (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:
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
⊢ (toSingleEquiv h) (toSingleMk f h) = 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 : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
X' : C
g : X ⟶ X'
⊢ toSingleMk (f ≫ g) h = (toSingleMk f h).comp (ofHom ((singleFunctor C q).map 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
L : CochainComplex C ℤ
g : L ⟶ K
⊢ (toSingleEquiv h) (toSingleMk (g.f p ≫ f) h) = (toSingleEquiv h) ((ofHom g).comp (toSingleMk f h) ⋯)

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 : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 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
F G : C ⥤ Karoubi D
φ : F ⟶ G
P : Karoubi C
⊢ ((obj F).obj P).p ≫ ((F.map P.p).f ≫ (φ.app P.X).f) ≫ ((obj G).obj P).p = (F.map P.p).f ≫ (φ.app P.X).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 : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
⊢ δ n (n + 1) (Cochain.fromSingleMk f h) = 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 ℤ
X' : C
g : X' ⟶ X
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
⊢ (g ≫ f) ≫ K.d q q' = 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 ℤ
X' : C
g : X' ⟶ X
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.fromSingleEquiv h) ↑(fromSingleMk (g ≫ f) h q' hq' ⋯) =
    (Cochain.fromSingleEquiv h) ↑((fromSingleMk f h q' hq' hf).precomp ((singleFunctor C p).map 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 ℤ
X' : C
g : X' ⟶ X
p q : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
⊢ fromSingleMk (g ≫ f) h q' hq' ⋯ = (fromSingleMk f h q' hq' hf).precomp ((singleFunctor C p).map 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 : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
L : CochainComplex C ℤ
g : K ⟶ L
⊢ (f ≫ g.f q) ≫ L.d q q' = 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 : ℤ
f : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
L : CochainComplex C ℤ
g : K ⟶ L
⊢ (Cochain.fromSingleEquiv h) ↑(fromSingleMk (f ≫ g.f q) h q' hq' ⋯) =
    (Cochain.fromSingleEquiv h) ↑((fromSingleMk f h q' hq' hf).postcomp 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 : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
L : CochainComplex C ℤ
g : K ⟶ L
⊢ fromSingleMk (f ≫ g.f q) h q' hq' ⋯ = (fromSingleMk f h q' hq' hf).postcomp 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 n : ℤ
α : Cocycle ((singleFunctor C p).obj X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = ↑α
hα : δ n (n + 1) (Cochain.fromSingleMk f h) = 0
⊢ p + (n + 1) = q'

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 n : ℤ
α : Cocycle ((singleFunctor C p).obj X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = ↑α
hα : Cochain.fromSingleMk (f ≫ K.d q q') ⋯ = 0
⊢ p + (n + 1) = q'

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 n : ℤ
α : Cocycle ((singleFunctor C p).obj X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = ↑α
hα : (Cochain.fromSingleMk (f ≫ K.d q q') ⋯).v p q' ⋯ = Cochain.v 0 p q' ⋯
⊢ f ≫ K.d q q' = 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 n : ℤ
α : Cocycle ((singleFunctor C p).obj X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
f : X ⟶ K.X q
hf : Cochain.fromSingleMk f h = ↑α
hα : (Cochain.fromSingleMk (f ≫ K.d q q') ⋯).v p q' ⋯ = Cochain.v 0 p q' ⋯
⊢ fromSingleMk f h q' hq' ⋯ = α

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 n : ℤ
α : Cocycle ((singleFunctor C p).obj X) K n
q : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
⊢ ∃ f, ∃ (hf : f ≫ K.d q q' = 0), fromSingleMk f h q' hq' hf = α

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

Tactic:
by

Goal state after: