mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (mk₀ f).comp (mk₀ g) ⋯ = mk₀ (f ≫ g)

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
this : HasDerivedCategory C := ⋯
⊢ ((mk₀ f).comp (mk₀ g) ⋯).hom = (mk₀ (f ≫ g)).hom
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
⊢ IsZero (S.X₃.homology i)

Tactic:
by_cases! hi : ∃ j, c.Rel i j

Goal state after:
case pos
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
hi : ∃ j, c.Rel i j
⊢ IsZero (S.X₃.homology i)

case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
⊢ IsZero (S.X₃.homology i)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α₁ α₂ : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (α₁ + α₂).comp β h = α₁.comp β h + α₂.comp β h

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α₁ α₂ : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := ⋯
⊢ ((α₁ + α₂).comp β h).hom = (α₁.comp β h + α₂.comp β h).hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β₁ β₂ : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β₁ β₂ : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := ⋯
⊢ (α.comp (β₁ + β₂) h).hom = (α.comp β₁ h + α.comp β₂ h).hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (-α).comp β h = -α.comp β h

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := ⋯
⊢ ((-α).comp β h).hom = (-α.comp β h).hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp (-β) h = -α.comp β h

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := ⋯
⊢ (α.comp (-β) h).hom = (-α.comp β h).hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ comp 0 β h = 0

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := ⋯
⊢ (comp 0 β h).hom = hom 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
Z : C
m p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp 0 h = 0

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
Z : C
m p : ℕ
h : n + m = p
this : HasDerivedCategory C := ⋯
⊢ (α.comp 0 h).hom = hom 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (mk₀ (𝟙 X)).comp α ⋯ = α

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
this : HasDerivedCategory C := ⋯
⊢ ((mk₀ (𝟙 X)).comp α ⋯).hom = α.hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ α.comp (mk₀ (𝟙 Y)) ⋯ = α

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
this : HasDerivedCategory C := ⋯
⊢ (α.comp (mk₀ (𝟙 Y)) ⋯).hom = α.hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ mk₀ 0 = 0

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
this : HasDerivedCategory C := ⋯
⊢ (mk₀ 0).hom = hom 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
f g : X ⟶ Y
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ mk₀ (f + g) = mk₀ f + mk₀ g

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
f g : X ⟶ Y
this : HasDerivedCategory C := ⋯
⊢ (mk₀ (f + g)).hom = (mk₀ f + mk₀ g).hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
f g : X ⟶ Y
⊢ mk₀ (f + g) = mk₀ f + mk₀ g

Tactic:
by
  let := HasDerivedCategory.standard C; ext; simp [add_hom', ShiftedHom.mk₀]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
f : X ⟶ Y
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ mk₀ (-f) = -mk₀ f

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
f : X ⟶ Y
this : HasDerivedCategory C := ⋯
⊢ (mk₀ (-f)).hom = (-mk₀ f).hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := ⋯
β' : Ext (X ⊞ X) Y n := ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
⊢ (mk₀ biprod.inl).comp (α' + β') ⋯ = (mk₀ biprod.inl).comp (homEquiv.symm (α'.hom + β'.hom)) ⋯

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := ⋯
β' : Ext (X ⊞ X) Y n := ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
⊢ ((mk₀ biprod.inl).comp (α' + β') ⋯).hom = ((mk₀ biprod.inl).comp (homEquiv.symm (α'.hom + β'.hom)) ⋯).hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := ⋯
β' : Ext (X ⊞ X) Y n := ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
⊢ (mk₀ biprod.inr).comp (α' + β') ⋯ = (mk₀ biprod.inr).comp (homEquiv.symm (α'.hom + β'.hom)) ⋯

Tactic:
ext

Goal state after:
case h₂
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := ⋯
β' : Ext (X ⊞ X) Y n := ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
⊢ ((mk₀ biprod.inr).comp (α' + β') ⋯).hom = ((mk₀ biprod.inr).comp (homEquiv.symm (α'.hom + β'.hom)) ⋯).hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (ShiftedHom.mk₀ 0 mk₀._proof_1 ((singleFunctor C 0).map (biprod.lift (𝟙 X) (𝟙 X) ≫ biprod.fst))).comp α.hom ⋯ = α.hom

Tactic:
biprod.lift_fst,

Goal state after:
case e_a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (ShiftedHom.mk₀ 0 mk₀._proof_1 ((singleFunctor C 0).map (𝟙 X))).comp α.hom ⋯ = α.hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w', max u v}
          ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))) ↔
    ∀ (X Y : C) (n : ℕ), Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := ⋯
⊢ (∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w', max u v}
          ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))) →
    ∀ (X Y : C) (n : ℕ), Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)

case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := ⋯
⊢ (∀ (X Y : C) (n : ℕ), Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)) →
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w', max u v}
          ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (Ext.mk₀ S.g).comp hS.extClass ⋯ = 0

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := ⋯
⊢ ((Ext.mk₀ S.g).comp hS.extClass ⋯).hom = Ext.hom 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ hS.extClass.comp (Ext.mk₀ S.f) ⋯ = 0

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := ⋯
⊢ (hS.extClass.comp (Ext.mk₀ S.f) ⋯).hom = Ext.hom 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S₁ S₂ : ShortComplex C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ h₁.extClass.comp (Ext.mk₀ f.τ₁) ⋯ = (Ext.mk₀ f.τ₃).comp h₂.extClass ⋯

Tactic:
ext

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S₁ S₂ : ShortComplex C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
this : HasDerivedCategory C := ⋯
⊢ (h₁.extClass.comp (Ext.mk₀ f.τ₁) ⋯).hom = ((Ext.mk₀ f.τ₃).comp h₂.extClass ⋯).hom
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : F.CommShift A
⊢ (NatIso.op (CommShift.isoZero F A)).symm = CommShift.isoZero (OppositeShift.functor A F) A

Tactic:
ext

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : F.CommShift A
x✝ : Cᵒᵖ
⊢ (NatIso.op (CommShift.isoZero F A)).symm.hom.app x✝ = (CommShift.isoZero (OppositeShift.functor A F) A).hom.app x✝
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : F.CommShift A
a b : A
⊢ (NatIso.op (CommShift.isoAdd (commShiftIso F a) (commShiftIso F b))).symm =
    CommShift.isoAdd (NatIso.op (commShiftIso F a)).symm (NatIso.op (commShiftIso F b)).symm

Tactic:
ext

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : F.CommShift A
a b : A
x✝ : Cᵒᵖ
⊢ (NatIso.op (CommShift.isoAdd (commShiftIso F a) (commShiftIso F b))).symm.hom.app x✝ =
    (CommShift.isoAdd (NatIso.op (commShiftIso F a)).symm (NatIso.op (commShiftIso F b)).symm).hom.app x✝
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : (OppositeShift.functor A F).CommShift A
⊢ NatIso.removeOp (CommShift.isoZero (OppositeShift.functor A F) A).symm = CommShift.isoZero F A

Tactic:
ext

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : (OppositeShift.functor A F).CommShift A
x✝ : C
⊢ (NatIso.removeOp (CommShift.isoZero (OppositeShift.functor A F) A).symm).hom.app x✝ =
    (CommShift.isoZero F A).hom.app x✝
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : (OppositeShift.functor A F).CommShift A
a b : A
⊢ NatIso.removeOp
      (CommShift.isoAdd (commShiftIso (OppositeShift.functor A F) a)
          (commShiftIso (OppositeShift.functor A F) b)).symm =
    CommShift.isoAdd (NatIso.removeOp (commShiftIso (OppositeShift.functor A F) a).symm)
      (NatIso.removeOp (commShiftIso (OppositeShift.functor A F) b).symm)

Tactic:
ext

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
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
F : C ⥤ D
inst✝ : (OppositeShift.functor A F).CommShift A
a b : A
x✝ : C
⊢ (NatIso.removeOp
            (CommShift.isoAdd (commShiftIso (OppositeShift.functor A F) a)
                (commShiftIso (OppositeShift.functor A F) b)).symm).hom.app
      x✝ =
    (CommShift.isoAdd (NatIso.removeOp (commShiftIso (OppositeShift.functor A F) a).symm)
            (NatIso.removeOp (commShiftIso (OppositeShift.functor A F) b).symm)).hom.app
      x✝
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
F G : C ⥤ D
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
τ : F ⟶ G
inst✝ : CommShift τ A
x✝ : A
⊢ (Functor.commShiftIso (OppositeShift.functor A G) x✝).hom ≫
      Functor.whiskerRight (OppositeShift.natTrans A τ) (shiftFunctor (OppositeShift D A) x✝) =
    (shiftFunctor (OppositeShift C A) x✝).whiskerLeft (OppositeShift.natTrans A τ) ≫
      (Functor.commShiftIso (OppositeShift.functor A F) x✝).hom

Tactic:
ext

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
A : Type u_3
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
F G : C ⥤ D
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
τ : F ⟶ G
inst✝ : CommShift τ A
x✝¹ : A
x✝ : OppositeShift C A
⊢ ((Functor.commShiftIso (OppositeShift.functor A G) x✝¹).hom ≫
          Functor.whiskerRight (OppositeShift.natTrans A τ) (shiftFunctor (OppositeShift D A) x✝¹)).app
      x✝ =
    ((shiftFunctor (OppositeShift C A) x✝¹).whiskerLeft (OppositeShift.natTrans A τ) ≫
          (Functor.commShiftIso (OppositeShift.functor A F) x✝¹).hom).app
      x✝
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
F : C ⥤ D
x✝ : A
⊢ (Functor.commShiftIso (𝟭 (OppositeShift C A)) x✝).hom ≫
      Functor.whiskerRight (OppositeShift.natIsoId C A).hom (shiftFunctor (OppositeShift C A) x✝) =
    (shiftFunctor (OppositeShift C A) x✝).whiskerLeft (OppositeShift.natIsoId C A).hom ≫
      (Functor.commShiftIso (OppositeShift.functor A (𝟭 C)) x✝).hom

Tactic:
ext

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
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
F : C ⥤ D
x✝¹ : A
x✝ : OppositeShift C A
⊢ ((Functor.commShiftIso (𝟭 (OppositeShift C A)) x✝¹).hom ≫
          Functor.whiskerRight (OppositeShift.natIsoId C A).hom (shiftFunctor (OppositeShift C A) x✝¹)).app
      x✝ =
    ((shiftFunctor (OppositeShift C A) x✝¹).whiskerLeft (OppositeShift.natIsoId C A).hom ≫
          (Functor.commShiftIso (OppositeShift.functor A (𝟭 C)) x✝¹).hom).app
      x✝
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
inst✝⁴ : HasShift D A
F : C ⥤ D
E : Type u_4
inst✝³ : Category.{v_3, u_4} E
inst✝² : HasShift E A
G : D ⥤ E
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
x✝ : A
⊢ (Functor.commShiftIso (OppositeShift.functor A (F ⋙ G)) x✝).hom ≫
      Functor.whiskerRight (OppositeShift.natIsoComp A F G).hom (shiftFunctor (OppositeShift E A) x✝) =
    (shiftFunctor (OppositeShift C A) x✝).whiskerLeft (OppositeShift.natIsoComp A F G).hom ≫
      (Functor.commShiftIso (OppositeShift.functor A F ⋙ OppositeShift.functor A G) x✝).hom

Tactic:
ext

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
A : Type u_3
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
inst✝⁴ : HasShift D A
F : C ⥤ D
E : Type u_4
inst✝³ : Category.{v_3, u_4} E
inst✝² : HasShift E A
G : D ⥤ E
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
x✝¹ : A
x✝ : OppositeShift C A
⊢ ((Functor.commShiftIso (OppositeShift.functor A (F ⋙ G)) x✝¹).hom ≫
          Functor.whiskerRight (OppositeShift.natIsoComp A F G).hom (shiftFunctor (OppositeShift E A) x✝¹)).app
      x✝ =
    ((shiftFunctor (OppositeShift C A) x✝¹).whiskerLeft (OppositeShift.natIsoComp A F G).hom ≫
          (Functor.commShiftIso (OppositeShift.functor A F ⋙ OppositeShift.functor A G) x✝¹).hom).app
      x✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
⊢ (homologyFunctor C (up ℤ) 0).homologySequenceδ
        (Triangle.mk ((quotient C (up ℤ)).map S.f) ((quotient C (up ℤ)).map (inr S.f))
          ((quotient C (up ℤ)).map (triangle S.f).mor₃ ≫ (Functor.commShiftIso (quotient C (up ℤ)) 1).hom.app S.X₁))
        n (n + 1) ⋯ ≫
      (homologyFunctorFactors C (up ℤ) (n + 1)).hom.app S.X₁ =
    ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
        HomologicalComplex.homologyMap (descShortComplex S) n) ≫
      hS.δ n (n + 1) ⋯

Tactic:
erw [homologySequenceδ_triangleh hS]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
⊢ ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
        HomologicalComplex.homologyMap (descShortComplex S) n ≫
          hS.δ n (n + 1) ⋯ ≫ (homologyFunctorFactors C (up ℤ) (n + 1)).inv.app S.X₁) ≫
      (homologyFunctorFactors C (up ℤ) (n + 1)).hom.app S.X₁ =
    ((homologyFunctorFactors C (up ℤ) n).hom.app (mappingCone S.f) ≫
        HomologicalComplex.homologyMap (descShortComplex S) n) ≫
      hS.δ n (n + 1) ⋯
Module: Mathlib.CategoryTheory.Shift.Opposite

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
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
F✝ F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : OppositeShift D A
⊢ (functor A G).map
        (((NatTrans.OppositeShift.natIsoId D A).hom ≫
              natTrans A adj.counit ≫ (NatTrans.OppositeShift.natIsoComp A G F).hom).app
          x✝) ≫
      ((NatTrans.OppositeShift.natIsoComp A F G).inv ≫
            natTrans A adj.unit ≫ (NatTrans.OppositeShift.natIsoId C A).inv).app
        ((functor A G).obj x✝) =
    𝟙 ((functor A G).obj x✝)

Tactic:
by
    dsimp [OppositeShift.natTrans, NatTrans.OppositeShift.natIsoComp,
      NatTrans.OppositeShift.natIsoId, OppositeShift.functor]
    simp only [comp_id, id_comp, Quiver.Hom.unop_op]
    rw [← op_comp, adj.right_triangle_components]
    rfl

Goal state after:
Module: Mathlib.CategoryTheory.Shift.Adjunction

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 : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
⊢ e₂ = e₂'

Tactic:
rw [← Iso.symm_eq_iff]

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 : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : Type u_3
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
inst✝ : HasShift D A
a : A
e₁ : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
⊢ e₂.symm = e₂'.symm