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
    ((CategoryTheory.shiftFunctor C n).map f.f ≫ (CategoryTheory.shiftFunctor C n).map g.f =
      (CategoryTheory.shiftFunctor C n).map f.f ≫ (CategoryTheory.shiftFunctor C n).map g.f)
    ext._auto_1

Tactic:
]

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

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : ¬n + 1 = m
⊢ 0 = 0

Tactic:
]

Goal state after:
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
⊢ 0 = 0

Tactic:
]

Goal state after:
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.shiftFunctorAdd C m n).inv.app X.obj ≫
      ((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).inv.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)

Tactic:
]

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.shiftFunctorAdd C m n).inv.app X.obj ≫
      ((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).inv.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.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : n + 1 = m
hmp : ¬m + 1 = p
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: 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₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (doubleXIso₀ f hi₀₁).hom ≫ φ₀ = (doubleXIso₀ f hi₀₁).hom ≫ φ₀

Tactic:
]

Goal state after:
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:
]

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 ⋙ 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)
Module: Mathlib.Algebra.Homology.Double

Goal state before:
pp: 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₀ i₁ : ι
hi₀₁ : c.Rel i₀ i₁
h : i₀ ≠ i₁
K : HomologicalComplex C c
φ₀ : X₀ ⟶ K.X i₀
φ₁ : X₁ ⟶ K.X i₁
comm : φ₀ ≫ K.d i₀ i₁ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel i₁ k → φ₁ ≫ K.d i₁ k = 0
⊢ (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁ = (doubleXIso₁ f hi₀₁ h).hom ≫ φ₁

Tactic:
]

Goal state after:
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 : ℕ
⊢ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom ≫ L.d n (n + 1) =
    ((restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom ≫
        L.d n (n + 1) ≫ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).inv) ≫
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom

Tactic:
]

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 : ℕ
⊢ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom ≫ L.d n (n + 1) =
    ((restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom ≫
        L.d n (n + 1) ≫ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).inv) ≫
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ⋯).hom
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:
]

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
⊢ ((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)
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 : ℕ
⊢ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom ≫ K.d (n + 1) n =
    ((restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom ≫
        K.d (n + 1) n ≫ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).inv) ≫
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom

Tactic:
]

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 : ℕ
⊢ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom ≫ K.d (n + 1) n =
    ((restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom ≫
        K.d (n + 1) n ≫ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).inv) ≫
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom
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 j : ι
h : ¬c.Rel i j
this : ∀ (x : T), (C.d i j).app x = NatTrans.app 0 x
⊢ (C.d i j).app t = 0

Tactic:
]

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 j : ι
h : ¬c.Rel i j
this : ∀ (x : T), (C.d i j).app x = NatTrans.app 0 x
⊢ (C.d i j).app t = 0
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 j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
this : ∀ (x : T), (C.d i j ≫ C.d j k).app x = NatTrans.app 0 x
⊢ (C.d i j).app t ≫ (C.d j k).app t = 0

Tactic:
]

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 j k : ι
x✝¹ : c.Rel i j
x✝ : c.Rel j k
this : ∀ (x : T), (C.d i j ≫ C.d j k).app x = NatTrans.app 0 x
⊢ (C.d i j).app t ≫ (C.d j k).app t = 0
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 : ι
⊢ 𝟙 ((C.X i).obj t) = 𝟙 ((C.X i).obj t)

Tactic:
]

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
X✝ Y✝ Z✝ : T
h₁ : X✝ ⟶ Y✝
h₂ : Y✝ ⟶ Z✝
i : ι
⊢ (C.X i).map h₁ ≫ (C.X i).map h₂ = (C.X i).map h₁ ≫ (C.X i).map h₂

Tactic:
]

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✝ : Abelian V
S₁ S₂ : ShortComplex (T ⥤ V)
f : S₁ ⟶ S₂
hf : ∀ (j : T), QuasiIso (((evaluation T V).obj j).mapShortComplex.map f)
⊢ ∀ (X : T), IsIso ((homologyMap f).app X)

Tactic:
]

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✝ : Abelian V
S₁ S₂ : ShortComplex (T ⥤ V)
f : S₁ ⟶ S₂
hf : ∀ (j : T), QuasiIso (((evaluation T V).obj j).mapShortComplex.map f)
⊢ ∀ (X : T), IsIso ((homologyMap f).app X)
Module: Mathlib.Algebra.Homology.ExactSequenceFour

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this✝¹ : HasZeroObject C
this✝ : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
⊢ S.map' (k + 1) (k + 2) ⋯ ⋯ = (S.sc hS (k + 1) ⋯).f

Tactic:
]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS k ⋯).Exact
this✝¹ : HasZeroObject C
this✝ : (S.sc hS k ⋯).HasHomology
h : (S.sc hS k ⋯).RightHomologyData := hS'.rightHomologyDataOfIsColimitCokernelCofork cc hcc
this : Mono h.g'
⊢ S.map' (k + 1) (k + 2) ⋯ ⋯ = (S.sc hS k ⋯).g

Tactic:
]

Goal state after:
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
inst✝³ : HasHomology h.cochainComplex m
inst✝² : HasHomology L n
inst✝¹ : HasHomology h'.cochainComplex m
inst✝ : HasHomology L' n
⊢ homologyMap (h.map h' fK fL f_comm) m ≫ homologyι h'.cochainComplex m =
    ((h.homologyIsoPos n m hmn).hom ≫ homologyMap fL n ≫ (h'.homologyIsoPos n m hmn).inv) ≫
      homologyι h'.cochainComplex m

Tactic:
]

Goal state after:
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
inst✝³ : HasHomology h.cochainComplex m
inst✝² : HasHomology L n
inst✝¹ : HasHomology h'.cochainComplex m
inst✝ : HasHomology L' n
⊢ homologyMap (h.map h' fK fL f_comm) m ≫ homologyι h'.cochainComplex m =
    ((h.homologyIsoPos n m hmn).hom ≫ homologyMap fL n ≫ (h'.homologyIsoPos n m hmn).inv) ≫
      homologyι h'.cochainComplex m
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
m : ℤ
hmn : m = ↑n
inst✝³ : HasHomology h.cochainComplex m
inst✝² : HasHomology L n
inst✝¹ : HasHomology h'.cochainComplex m
inst✝ : HasHomology L' n
⊢ pOpcycles h.cochainComplex m ≫ opcyclesMap (h.map h' fK fL f_comm) m =
    pOpcycles h.cochainComplex m ≫
      (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:
]

Goal state after:
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
m : ℤ
hmn : m = ↑n
inst✝³ : HasHomology h.cochainComplex m
inst✝² : HasHomology L n
inst✝¹ : HasHomology h'.cochainComplex m
inst✝ : HasHomology L' n
⊢ pOpcycles h.cochainComplex m ≫ opcyclesMap (h.map h' fK fL f_comm) m =
    pOpcycles h.cochainComplex m ≫
      (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
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 ≫ homologyι h'.cochainComplex m =
    ((h.homologyIsoNeg n m hmn).hom ≫ homologyMap fK n ≫ (h'.homologyIsoNeg n m hmn).inv) ≫
      homologyι h'.cochainComplex m

Tactic:
]

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

Goal state after:
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
m : ℤ
hmn : m = -↑(n + 1)
inst✝³ : HasHomology h.cochainComplex m
inst✝² : HasHomology K n
inst✝¹ : HasHomology h'.cochainComplex m
inst✝ : HasHomology K' n
⊢ pOpcycles h.cochainComplex m ≫ opcyclesMap (h.map h' fK fL f_comm) m =
    pOpcycles h.cochainComplex m ≫
      (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
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).app 0) ∧ IsIso ((twoδ₂Toδ₁ f g fg h).app 1)

Tactic:
]

Goal state after:
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) ∧ IsIso ((twoδ₂Toδ₁ f g fg h).app 1)
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).app 0) ∧ IsIso ((twoδ₁Toδ₀ f g fg h).app 1)

Tactic:
]

Goal state after:
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) ∧ IsIso ((twoδ₁Toδ₀ f g fg h).app 1)
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:
]

Goal state after:
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'
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:
]

Goal state after:
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'
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 ≫ P.decompId_p) ≫ φ.app P

Tactic:
]

Goal state after:
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 ≫ P.decompId_p) ≫ φ.app 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 : ℤ
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:
]

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