mathlib-initiative/mathlib-tactics huggingface dataset:
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'
h : (K.sc' i j k).RightHomologyData
⊢ ((K.extend e).sc' i' j' k').f ≫ (K.extendXIso e hj').hom ≫ h.p = 0

Tactic:
dsimp
    rw [← d_comp_eq_zero_iff K e hj' hi hi']
    exact h.wp

Goal state after:
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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.restriction e).homologyπ j ≫
      ShortComplex.homologyMap ((natIsoSc' C c i j k hi hk).hom.app (K.restriction e)) ≫
        ShortComplex.homologyMap (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom ≫
          ShortComplex.homologyMap ((natIsoSc' C c' i' j' k' hi'' hk'').inv.app K) =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j'

Tactic:
← ShortComplex.homologyMap_comp,

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
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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.restriction e).homologyπ j ≫
      ShortComplex.homologyMap ((natIsoSc' C c i j k hi hk).hom.app (K.restriction e)) ≫
        ShortComplex.homologyMap
          ((restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom ≫ (natIsoSc' C c' i' j' k' hi'' hk'').inv.app K) =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j'
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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.restriction e).homologyπ j ≫
      ShortComplex.homologyMap ((natIsoSc' C c i j k hi hk).hom.app (K.restriction e)) ≫
        ShortComplex.homologyMap
          ((restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom ≫ (natIsoSc' C c' i' j' k' hi'' hk'').inv.app K) =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j'

Tactic:
← ShortComplex.homologyMap_comp,

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
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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.restriction e).homologyπ j ≫
      ShortComplex.homologyMap
        ((natIsoSc' C c i j k hi hk).hom.app (K.restriction e) ≫
          (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom ≫ (natIsoSc' C c' i' j' k' hi'' hk'').inv.app K) =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j'
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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (K.restriction e).homologyπ j ≫
      ShortComplex.homologyMap
        ((natIsoSc' C c i j k hi hk).hom.app (K.restriction e) ≫
          (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom ≫ (natIsoSc' C c' i' j' k' hi'' hk'').inv.app K) =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j'

Tactic:
← cancel_mono (K.sc j').homologyι,

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
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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ ((K.restriction e).homologyπ j ≫
        ShortComplex.homologyMap
          ((natIsoSc' C c i j k hi hk).hom.app (K.restriction e) ≫
            (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').hom ≫ (natIsoSc' C c' i' j' k' hi'' hk'').inv.app K)) ≫
      (K.sc j').homologyι =
    ((K.restrictionCyclesIso e j k hk hj' hk' hk'').hom ≫ K.homologyπ j') ≫ (K.sc j').homologyι
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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ ((ShortComplex.homologyMap ((natIsoSc' C c' i' j' k' hi'' hk'').hom.app K) ≫
          ShortComplex.homologyMap (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv) ≫
        ShortComplex.homologyMap ((natIsoSc' C c i j k hi hk).inv.app (K.restriction e))) ≫
      (K.restriction e).homologyι j =
    K.homologyι j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv

Tactic:
← ShortComplex.homologyMap_comp,

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
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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (ShortComplex.homologyMap
          ((natIsoSc' C c' i' j' k' hi'' hk'').hom.app K ≫ (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv) ≫
        ShortComplex.homologyMap ((natIsoSc' C c i j k hi hk).inv.app (K.restriction e))) ≫
      (K.restriction e).homologyι j =
    K.homologyι j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv
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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ (ShortComplex.homologyMap
          ((natIsoSc' C c' i' j' k' hi'' hk'').hom.app K ≫ (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv) ≫
        ShortComplex.homologyMap ((natIsoSc' C c i j k hi hk).inv.app (K.restriction e))) ≫
      (K.restriction e).homologyι j =
    K.homologyι j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv

Tactic:
← ShortComplex.homologyMap_comp,

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
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
this✝ : ((K.restriction e).sc' i j k).HasHomology
this : (K.sc' i' j' k').HasHomology
⊢ ShortComplex.homologyMap
        (((natIsoSc' C c' i' j' k' hi'' hk'').hom.app K ≫ (restriction.sc'Iso K e i j k hi' hj' hk' hi'' hk'').inv) ≫
          (natIsoSc' C c i j k hi hk).inv.app (K.restriction e)) ≫
      (K.restriction e).homologyι j =
    K.homologyι j' ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

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.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
⊢ (K.restrictionToTruncGE' e).f i =
    (K.restrictionXIso e hi').hom ≫ K.pOpcycles i' ≫ (K.truncGE'XIsoOpcycles e hi' hi).inv

Tactic:
apply restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv

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

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i' j' : ι'
hij' : c'.Rel i' j'
hj : ∃ j, e.f j = j'
⊢ ⋯.δ i' j' hij' = 0

Tactic:
obtain ⟨j, rfl⟩ := hj

Goal state after:
case pos
ι : 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 : ι
hij' : c'.Rel i' (e.f j)
⊢ ⋯.δ i' (e.f j) hij' = 0
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝¹ : HasZeroObject C
inst✝ : ∀ (i : ℤ), HasHomology K i
n : ℤ
k : ℕ
hq : n ≤ n + ↑k
⊢ QuasiIsoAt (K.πTruncGE n) (n + ↑k)

Tactic:
exact HomologicalComplex.quasiIsoAt_πTruncGE (j := k) _ _ (by simp)

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

Goal state before:
pp: case pos
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
i : ℤ
hi : i ≤ n₀
⊢ (∃ i₁, (embeddingUpIntLE n₀).f i₁ = i) ∨ ∃ i₂, (embeddingUpIntGE n₁).f i₂ = i

Tactic:
obtain ⟨k, rfl⟩ := Int.exists_add_of_le hi
      exact Or.inl ⟨k, by dsimp; lia⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ (singleObjHomologySelfIso c j A).inv ≫ ((single C c j).obj A).homologyι j = (singleObjOpcyclesSelfIso c j A).hom

Tactic:
by
  rw [← cancel_epi (singleObjCyclesSelfIso c j A).hom,
    singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, homology_π_ι,
    singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom]

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
⊢ mk₀ (-f) = -mk₀ f

Tactic:
let := HasDerivedCategory.standard C; ext; simp [neg_hom']

Goal state after:
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₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
      (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₁ h ≫
        (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁ =
    (homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
      (homologyFunctorFactors C (up ℤ) n₀).hom.app (mappingCone S.f) ≫
        HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
          hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁)

Tactic:
Iso.inv_hom_id_app_assoc

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₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (homologyFunctorFactors C (up ℤ) n₀).inv.app (mappingCone S.f) ≫
      (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₁ h ≫
        (homologyFunctorFactors C (up ℤ) n₁).hom.app S.X₁ =
    HomologicalComplex.homologyMap (descShortComplex S) n₀ ≫
      hS.δ n₀ n₁ h ≫ 𝟙 ((HomologicalComplex.homologyFunctor C (up ℤ) n₁).obj S.X₁)
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 : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝¹ x✝ : Ext X c.pt n
⊢ (fun i ↦ (x✝¹ + x✝).comp (mk₀ (c.π i)) ⋯) = (fun i ↦ x✝¹.comp (mk₀ (c.π i)) ⋯) + fun i ↦ x✝.comp (mk₀ (c.π i)) ⋯

Tactic:
by
    simp only [add_comp, Pi.add_def]

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₁ X₂ Y : C
n : ℕ
x✝ : Ext (X₁ ⊞ X₂) Y n
⊢ (fun e ↦ (mk₀ biprod.fst).comp e.1 ⋯ + (mk₀ biprod.snd).comp e.2 ⋯)
      ((fun e ↦ ((mk₀ biprod.inl).comp e ⋯, (mk₀ biprod.inr).comp e ⋯)) x✝) =
    x✝

Tactic:
simp only [mk₀_comp_mk₀_assoc, ← add_comp, ← mk₀_add, biprod.total, mk₀_id_comp]

Goal state after:
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
x✝ : C
⊢ ((OppositeShift.functor A F).map ((shiftFunctorAdd Cᵒᵖ a b).inv.app (Opposite.op x✝))).unop ≫
      ((commShiftIso (OppositeShift.functor A F) b).inv.app ((shiftFunctor Cᵒᵖ a).obj (Opposite.op x✝))).unop ≫
        ((shiftFunctor Dᵒᵖ b).map ((commShiftIso (OppositeShift.functor A F) a).inv.app (Opposite.op x✝))).unop ≫
          ((shiftFunctorAdd Dᵒᵖ a b).hom.app ((OppositeShift.functor A F).obj (Opposite.op x✝))).unop =
    F.map ((shiftFunctorAdd C a b).hom.app x✝) ≫
      ((commShiftIso (OppositeShift.functor A F) b).inv.app (Opposite.op ((shiftFunctor C a).obj x✝))).unop ≫
        (shiftFunctor D b).map ((commShiftIso (OppositeShift.functor A F) a).inv.app (Opposite.op x✝)).unop ≫
          (shiftFunctorAdd D a b).inv.app (F.obj x✝)

Tactic:
erw [oppositeShiftFunctorAdd_hom_app, oppositeShiftFunctorAdd_inv_app]

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
⊢ ((OppositeShift.functor A F).map ((shiftFunctorAdd C a b).hom.app (Opposite.unop (Opposite.op x✝))).op).unop ≫
      ((commShiftIso (OppositeShift.functor A F) b).inv.app ((shiftFunctor Cᵒᵖ a).obj (Opposite.op x✝))).unop ≫
        ((shiftFunctor Dᵒᵖ b).map ((commShiftIso (OppositeShift.functor A F) a).inv.app (Opposite.op x✝))).unop ≫
          ((shiftFunctorAdd D a b).inv.app (Opposite.unop ((OppositeShift.functor A F).obj (Opposite.op x✝)))).op.unop =
    F.map ((shiftFunctorAdd C a b).hom.app x✝) ≫
      ((commShiftIso (OppositeShift.functor A F) b).inv.app (Opposite.op ((shiftFunctor C a).obj x✝))).unop ≫
        (shiftFunctor D b).map ((commShiftIso (OppositeShift.functor A F) a).inv.app (Opposite.op x✝)).unop ≫
          (shiftFunctorAdd D a b).inv.app (F.obj 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) =
    (shiftFunctorZero Cᵒᵖ ℤ).hom.app X ≫
      ((shiftFunctorZero C ℤ).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C 0 0 ⋯).inv.app X

Tactic:
shiftFunctorZero_op_hom_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 ≫ ((shiftFunctorZero C ℤ).inv.app (Opposite.unop X)).op) ≫
      ((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ᵒᵖ
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) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).1 (Opposite.unop 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.inv_hom_id_app_assoc

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) =
    (shiftFunctorOpIso C a₃ b₃ h₃).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app (Opposite.unop X)).op ≫ (shiftFunctorOpIso C a₃ b₃ h₃).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ᵒᵖ
⊢ (shiftFunctorCompIsoId C 0 0 ⋯).inv.app (Opposite.unop X) ≫
      (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).hom.app X).unop =
    (shiftFunctorZero C ℤ).inv.app (Opposite.unop X) ≫ (shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop

Tactic:
shiftFunctorZero_op_hom_app,

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

Goal state before:
pp: case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ { X₁ := (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.obj ⟨0, ⋯⟩,
      X₂ := (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.obj ⟨1, ⋯⟩,
      X₃ := (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.obj ⟨2, ⋯⟩,
      f := (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
      g := (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
      zero := ⋯ }.Exact

Tactic:
rw [ShortComplex.exact_iff_epi _ (by simp)]

Goal state after:
case refine_1.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 2
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
hR₁' : Epi (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
hR₂' : Epi (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_epi_mono'._proof_1)
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_2)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
ψ : mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0 ⟶ mk₄ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 0 :=
  homMk₄ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) 0 0 ⋯ ⋯ ⋯ ⋯
⊢ Epi
    { X₁ := (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.obj ⟨0, ⋯⟩,
        X₂ := (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.obj ⟨1, ⋯⟩,
        X₃ := (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.obj ⟨2, ⋯⟩,
        f :=
          (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
        g :=
          (mk₄ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 0).δ₀.δ₀.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
        zero := ⋯ }.f