mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : n.negOnePow • f ≫ K.d (i + n) (j + n) = 0
⊢ n.negOnePow • 0 = 0

Tactic:
smul_zero

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K : CochainComplex C ℤ
A : C
n i : ℤ
f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i
j : ℤ
hj : i + 1 = j
hi' : n + i = i + n
hj' : i + n + 1 = j + n
hf : n.negOnePow • f ≫ K.d (i + n) (j + n) = 0
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
Y Z✝ Z' : C
f₁ f₂ : Y ⟶ Z✝
s : Z✝ ⟶ Z'
hf₁ : f₁ ≫ s = f₂ ≫ s
Z : C
g : Z ⟶ Z✝
h : Z' ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g s h ∈ distinguishedTriangles
mem : P Z
hf₂ : (f₁ - f₂) ≫ s = 0
q : Y ⟶ (Triangle.mk g s h).obj₁
hq : f₁ - f₂ = q ≫ (Triangle.mk g s h).mor₁
Y' : C
r : Y' ⟶ Y
t : (Triangle.mk g s h).obj₁ ⟶ (shiftFunctor C 1).obj Y'
mem' : Triangle.mk r q t ∈ distinguishedTriangles
eq : r ≫ q = 0
⊢ r ≫ f₁ - r ≫ f₂ = 0

Tactic:
← comp_sub,

Goal state after:
case refine_2
C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
Y Z✝ Z' : C
f₁ f₂ : Y ⟶ Z✝
s : Z✝ ⟶ Z'
hf₁ : f₁ ≫ s = f₂ ≫ s
Z : C
g : Z ⟶ Z✝
h : Z' ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g s h ∈ distinguishedTriangles
mem : P Z
hf₂ : (f₁ - f₂) ≫ s = 0
q : Y ⟶ (Triangle.mk g s h).obj₁
hq : f₁ - f₂ = q ≫ (Triangle.mk g s h).mor₁
Y' : C
r : Y' ⟶ Y
t : (Triangle.mk g s h).obj₁ ⟶ (shiftFunctor C 1).obj Y'
mem' : Triangle.mk r q t ∈ distinguishedTriangles
eq : r ≫ q = 0
⊢ r ≫ (f₁ - f₂) = 0
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
hi : ∀ (i : ι), e.f i ≠ i'
⊢ ¬∃ i, e.f i = i'

Tactic:
rintro ⟨i, hi'⟩

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
i' : ι'
hi : ∀ (i : ι), e.f i ≠ i'
i : ι
hi' : e.f i = i'
⊢ False
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel i j
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = 0

Tactic:
K.fromOpcycles_eq_zero hij,

Goal state after:
case neg
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : ¬c.Rel i j
⊢ Quiver.Hom.op 0 ≫ (K.cyclesOpIso i).inv = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ¬∃ j, e.f j = j'
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')

Tactic:
have hj' := e.r_eq_none j' (fun j'' hj'' => hj ⟨j'', hj''⟩)

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' : ι'
x✝ : c'.Rel i' j'
i : ι
hi : e.f i = i'
hj : ¬∃ j, e.f j = j'
hj' : e.r j' = none
⊢ extend.mapX φ (e.r i') ≫ (L.extend e).d i' j' = (K.extend e).d i' j' ≫ extend.mapX φ (e.r j')
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
i : ι
i' : ι'
h : e.f i = i'
⊢ (extendMap φ e).f i' = (K.extendXIso e h).hom ≫ φ.f i ≫ (L.extendXIso e h).inv

Tactic:
by
  dsimp [extendMap]
  rw [extend.mapX_some φ (e.r_eq_some h)]
  rfl

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ (K.extendXIso e hj').inv ≫ (K.extend e).d j' k' = 0

Tactic:
have hk' : e.f k = k' := by rw [← hk', ← hj', c'.next_eq' (e.rel hjk)]
    rw [K.extend_d_eq e hj' hk', Iso.inv_hom_id_assoc,
      ← cancel_mono (K.extendXIso e hk').inv, zero_comp, assoc]

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
j : ι
hj : e.f j = j'
⊢ ((K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv) ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j'

Tactic:
rw [f_eq φ hj, L.extend_d_eq e hi hj]

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : K.restriction e ⟶ L
hφ : e.HasLift φ
i' j' : ι'
hij' : c'.Rel i' j'
i : ι
hi : e.f i = i'
j : ι
hj : e.f j = j'
⊢ ((K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv) ≫
      (L.extendXIso e hi).hom ≫ L.d i j ≫ (L.extendXIso e hj).inv =
    K.d i' j' ≫ (K.restrictionXIso e hj).inv ≫ φ.f j ≫ (L.extendXIso e hj).inv
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
⊢ Fork.ι cone ≫ (K.extendXIso e hj').inv ≫ (K.extend e).d j' k' = 0

Tactic:
← comp_d_eq_zero_iff K e hj' hk hk' cone.ι,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
⊢ Fork.ι cone ≫ K.d j k = 0
Module: Mathlib.Algebra.Homology.Embedding.RestrictionHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
⊢ K.liftCycles ((K.restriction e).iCycles j ≫ (K.restrictionXIso e hj').hom) k' hk'' ⋯ ≫
      (K.restriction e).liftCycles (K.iCycles j' ≫ (K.restrictionXIso e hj').inv) k hk ⋯ =
    𝟙 ((K.restriction e).cycles j)

Tactic:
by simp [← cancel_mono ((K.restriction e).iCycles j)]

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

Goal state before:
pp: case mp
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
a✝ : QuasiIso (K.πTruncGE e)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ K.ExactAt i'

Tactic:
exactAt_iff_of_quasiIsoAt (K.πTruncGE e) i'

Goal state after:
case mp
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
a✝ : QuasiIso (K.πTruncGE e)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ (K.truncGE e).ExactAt i'
Module: Mathlib.Algebra.Homology.Embedding.TruncLE

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i : ι
hi : ¬e.BoundaryLE i
i' : ι'
h : e.f i = i'
⊢ ((truncLE'Map φ e).f i).op = ((K.truncLE'XIso e h hi).hom ≫ φ.f i' ≫ (L.truncLE'XIso e h hi).inv).op

Tactic:
simpa using! truncGE'Map_f_eq ((opFunctor C c').map φ.op) e.op (by simpa) h

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

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
⊢ (desc.aux X (ac.equiv (ac.equiv.symm (e₁.f i₁))) (e₁.f i₁) ⋯) (ac.desc' x₁ x₂ (ac.equiv.symm (e₁.f i₁))) = x₁ i₁

Tactic:
rw [ac.desc'_inl _ _ _ i₁ (ac.equiv.injective (by simp)), desc.aux_trans]

Goal state after:
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
⊢ (desc.aux X (e₁.f i₁) (e₁.f i₁) ⋯) (x₁ i₁) = x₁ i₁
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

Goal state before:
pp: case pos.hf
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ homologyMap (K.ιTruncLE e ≫ cokernel.π (K.ιTruncLE e)) (e.f i) = 0

Tactic:
cokernel.condition,

Goal state after:
case pos.hf
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ homologyMap 0 (e.f i) = 0
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K : HomologicalComplex C c
⊢ K.IsSupportedOutside e₁ ↔ K.IsSupported e₂

Tactic:
constructor
  · intro h
    exact ⟨fun i hi => by
      obtain ⟨i₁, rfl⟩ := ac.exists_i₁ i hi
      exact h.exactAt i₁⟩
  · intro _
    exact ⟨fun i₁ => K.exactAt_of_isSupported e₂ _
      (fun i₂ => (ac.disjoint i₁ i₂).symm)⟩

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
A B : C
X : CochainComplex C ℤ
w✝² : X.IsStrictlyGE n
w✝¹ : X.IsStrictlyLE n
s : X ⟶ (CochainComplex.singleFunctor C n).obj A
w✝ : IsIso (Q.map s)
g : X ⟶ (CochainComplex.singleFunctor C n).obj B
⊢ ∃ f', inv (Q.map s) ≫ Q.map g = Q.map f'

Tactic:
obtain ⟨A₀, ⟨e⟩⟩ := X.exists_iso_single n

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
A B : C
X : CochainComplex C ℤ
w✝² : X.IsStrictlyGE n
w✝¹ : X.IsStrictlyLE n
s : X ⟶ (CochainComplex.singleFunctor C n).obj A
w✝ : IsIso (Q.map s)
g : X ⟶ (CochainComplex.singleFunctor C n).obj B
A₀ : C
e : X ≅ (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A₀
⊢ ∃ f', inv (Q.map s) ≫ Q.map g = Q.map f'
Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₁ ≫
      (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₂).hom =
    (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom ≫ (triangleOfSES hS).mor₁

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₂ ≫
      (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom =
    (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₂).hom ≫ (triangleOfSES hS).mor₂

pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map
        (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom =
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom ≫ (triangleOfSES hS).mor₃

Tactic:
· dsimp [triangleOfSES]
    simp only [comp_id, id_comp]

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₂ ≫
      (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom =
    (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₂).hom ≫ (triangleOfSES hS).mor₂

case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map
        (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom =
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom ≫ (triangleOfSES hS).mor₃
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℕ
R₁ R₂ : ComposableArrows C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 3 ≤ n
h₁ : Mono (app' φ (k₀ + 1) ⋯)
h₃ : Mono (app' φ (k₀ + 3) ⋯)
h₀ : Epi (app' φ (k₀ + 0) ⋯)
⊢ Mono (app' φ (k₀ + 2) ⋯)

Tactic:
rw [← natAddLEFunctor_app' h] at h₀ h₁ h₃ ⊢

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
n : ℕ
R₁ R₂ : ComposableArrows C n
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
k₀ : ℕ
h : k₀ + 3 ≤ n
h₁ : Mono (app' ((natAddLEFunctor h).map φ) 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' ((natAddLEFunctor h).map φ) 3 mono_of_epi_of_mono_of_mono'._proof_7)
h₀ : Epi (app' ((natAddLEFunctor h).map φ) 0 mono_of_epi_of_mono_of_mono'._proof_13)
⊢ Mono (app' ((natAddLEFunctor h).map φ) 2 mono_of_epi_of_mono_of_mono'._proof_4)
Module: Mathlib.CategoryTheory.Shift.Opposite

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
⊢ (shiftFunctorZero (OppositeShift C A) A).hom.app X ≫ (shiftFunctorZero (OppositeShift C A) A).inv.app X =
    ((shiftFunctorZero C A).inv.app (Opposite.unop X)).op ≫ (shiftFunctorZero (OppositeShift C A) A).inv.app X

Tactic:
Iso.hom_inv_id_app,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
⊢ 𝟙 ((shiftFunctor (OppositeShift C A) 0).obj X) =
    ((shiftFunctorZero C A).inv.app (Opposite.unop X)).op ≫ (shiftFunctorZero (OppositeShift C A) A).inv.app X
Module: Mathlib.CategoryTheory.Shift.Opposite

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
⊢ 𝟙 ((shiftFunctor (OppositeShift C A) 0).obj X) =
    ((shiftFunctorZero C A).hom.app (Opposite.unop X) ≫ (shiftFunctorZero C A).inv.app (Opposite.unop X)).op

Tactic:
Iso.hom_inv_id_app,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
⊢ 𝟙 ((shiftFunctor (OppositeShift C A) 0).obj X) = (𝟙 ((shiftFunctor C 0).obj (Opposite.unop X))).op
Module: Mathlib.CategoryTheory.Shift.Opposite

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
a b : A
⊢ (shiftFunctorAdd (OppositeShift C A) a b).hom.app X ≫ (shiftFunctorAdd (OppositeShift C A) a b).inv.app X =
    ((shiftFunctorAdd C a b).inv.app (Opposite.unop X)).op ≫ (shiftFunctorAdd (OppositeShift C A) a b).inv.app X

Tactic:
Iso.hom_inv_id_app,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
a b : A
⊢ 𝟙 ((shiftFunctor (OppositeShift C A) (a + b)).obj X) =
    ((shiftFunctorAdd C a b).inv.app (Opposite.unop X)).op ≫ (shiftFunctorAdd (OppositeShift C A) a b).inv.app X
Module: Mathlib.CategoryTheory.Shift.Opposite

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
a b : A
⊢ 𝟙 ((shiftFunctor (OppositeShift C A) (a + b)).obj X) =
    ((shiftFunctorAdd C a b).hom.app (Opposite.unop X) ≫ (shiftFunctorAdd C a b).inv.app (Opposite.unop X)).op

Tactic:
Iso.hom_inv_id_app,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X : OppositeShift C A
a b : A
⊢ 𝟙 ((shiftFunctor (OppositeShift C A) (a + b)).obj X) = (𝟙 ((shiftFunctor C (a + b)).obj (Opposite.unop X))).op
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctorZero Cᵒᵖ ℤ).hom.app X ≫ (shiftFunctorZero Cᵒᵖ ℤ).inv.app X =
    (shiftFunctorZero Cᵒᵖ ℤ).hom.app X ≫
      ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C 0 0 ⋯).inv.app X

Tactic:
Iso.hom_inv_id_app,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ 𝟙 ((shiftFunctor Cᵒᵖ 0).obj X) =
    (shiftFunctorZero Cᵒᵖ ℤ).hom.app X ≫
      ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C 0 0 ⋯).inv.app X
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ 𝟙 ((shiftFunctor Cᵒᵖ 0).obj X) =
    (shiftFunctorOpIso C 0 0 ⋯).hom.app X ≫
      ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X) ≫ (shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op ≫
        (shiftFunctorOpIso C 0 0 ⋯).inv.app X

Tactic:
Iso.hom_inv_id_app,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ 𝟙 ((shiftFunctor Cᵒᵖ 0).obj X) =
    (shiftFunctorOpIso C 0 0 ⋯).hom.app X ≫
      (𝟙 ((shiftFunctor C 0).obj (Opposite.unop X))).op ≫ (shiftFunctorOpIso C 0 0 ⋯).inv.app X
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X ≫ (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).inv.app X =
    (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X ≫
      (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).hom.app X) ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).op.obj X) ≫
          ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X

Tactic:
Iso.hom_inv_id_app,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ a₃).obj X) =
    (shiftFunctorAdd' Cᵒᵖ a₁ a₂ a₃ h).hom.app X ≫
      (shiftFunctor Cᵒᵖ a₂).map ((shiftFunctorOpIso C a₁ b₁ h₁).hom.app X) ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).op.obj X) ≫
          ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).inv.app X
Module: Mathlib.CategoryTheory.Shift.Pullback

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ 𝟙 ((shiftFunctor (PullbackShift C φ) a₁ ⋙ shiftFunctor (PullbackShift C φ) a₂).obj X) =
    (shiftFunctor (PullbackShift C φ) a₂).map
      ((pullbackShiftIso C φ a₁ b₁ h₁).hom.app X ≫ (pullbackShiftIso C φ a₁ b₁ h₁).inv.app X)

Tactic:
Iso.hom_inv_id_app,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : HasShift C B
φ : A →+ B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ 𝟙 ((shiftFunctor (PullbackShift C φ) a₁ ⋙ shiftFunctor (PullbackShift C φ) a₂).obj X) =
    (shiftFunctor (PullbackShift C φ) a₂).map (𝟙 ((shiftFunctor (PullbackShift C φ) a₁).obj X))