mathlib-initiative/mathlib-tactics huggingface dataset:
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.descOpcycles ((K.restrictionXIso e hj').inv ≫ (K.restriction e).pOpcycles j) i' hi'' ⋯ ≫
      (K.restriction e).descOpcycles ((K.restrictionXIso e hj').hom ≫ K.pOpcycles j') i hi ⋯ =
    𝟙 (K.opcycles j')

Tactic:
by simp [← cancel_epi (K.pOpcycles j')]

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

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✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c' j').map (K.πTruncGE e))

Tactic:
let φ := (shortComplexFunctor C c' j').map (K.πTruncGE e)

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✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
j : ι
j' : ι'
hj' : e.f j = j'
hj : ¬e.BoundaryGE j
φ : (shortComplexFunctor C c' j').obj K ⟶ (shortComplexFunctor C c' j').obj (K.truncGE e) :=
  (shortComplexFunctor C c' j').map (K.πTruncGE e)
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c' j').map (K.πTruncGE e))
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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncLE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hj : e.BoundaryLE j
⊢ ((K.truncLE' e).d i j).op = ((K.truncLE'XIso e hi' ⋯).hom ≫ K.toCycles i' j' ≫ (K.truncLE'XIsoCycles e hj' hj).inv).op

Tactic:
by
    simpa [truncLE', truncLE'XIso, truncLE'XIsoCycles]
      using! K.op.truncGE'_d_eq_fromOpcycles e.op hij hj' hi' (by simpa)

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 ι₂
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
h : K.IsSupportedOutside e₁
i : ι
hi : ∀ (i_1 : ι₂), e₂.f i_1 ≠ i
⊢ K.ExactAt i

Tactic:
obtain ⟨i₁, rfl⟩ := ac.exists_i₁ i hi
      exact h.exactAt i₁

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 ι₂
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
h : K.IsSupportedOutside e₁
i : ι
hi : ∀ (i_1 : ι₂), e₂.f i_1 ≠ i
⊢ K.ExactAt i

Tactic:
by
      obtain ⟨i₁, rfl⟩ := ac.exists_i₁ i hi
      exact h.exactAt i₁

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

Goal state before:
pp: case pos.hg
ι : 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'
⊢ { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
        X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
        g := ⋯.δ (e.f i) j' hj', zero := ⋯ }.g =
    0

Tactic:
· simp

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

Goal state before:
pp: case inr.inl
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝² : HasZeroObject C
i : ℤ
inst✝¹ : K.IsStrictlyGE i
inst✝ : K.IsStrictlyLE i
⊢ (mkHomToSingle (𝟙 (K.X i)) ⋯ ≫ mkHomFromSingle (𝟙 (K.X i)) ⋯).f i = (𝟙 K).f i

pp: case inr.inr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝² : HasZeroObject C
n : ℤ
inst✝¹ : K.IsStrictlyGE n
inst✝ : K.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ (mkHomToSingle (𝟙 (K.X n)) ⋯ ≫ mkHomFromSingle (𝟙 (K.X n)) ⋯).f i = (𝟙 K).f i

Tactic:
· simp

Goal state after:
case inr.inr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝² : HasZeroObject C
n : ℤ
inst✝¹ : K.IsStrictlyGE n
inst✝ : K.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ (mkHomToSingle (𝟙 (K.X n)) ⋯ ≫ mkHomFromSingle (𝟙 (K.X n)) ⋯).f i = (𝟙 K).f i
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mp
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i') → ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i

Tactic:
intro h i hi
    obtain ⟨k, rfl⟩ := Int.le.dest hi
    exact h k _ rfl

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

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : X.IsStrictlyLE n
X' : CochainComplex C ℤ
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
this : IsIso (Q.map (CochainComplex.truncLEMap s n))
⊢ inv (Q.map s) ≫ Q.map g =
    inv (Q.map (CochainComplex.truncLEMap s n ≫ X.ιTruncLE n)) ≫ Q.map (CochainComplex.truncLEMap g n ≫ Y.ιTruncLE n)

Tactic:
· simp

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
this : IsIso (((single C c j).obj A).iCycles j)
⊢ ((single C c j).obj A).homologyπ j ≫ (singleObjHomologySelfIso c j A).hom =
    ((single C c j).obj A).iCycles j ≫ (singleObjXSelf c j A).hom

Tactic:
homologyπ_singleObjHomologySelfIso_hom,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
this : IsIso (((single C c j).obj A).iCycles j)
⊢ (singleObjCyclesSelfIso c j A).hom = ((single C c j).obj A).iCycles j ≫ (singleObjXSelf c j A).hom
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 B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j ≫ ((single C c j).obj B).homologyπ j ≫ (singleObjHomologySelfIso c j B).hom =
    ((single C c j).obj A).homologyπ j ≫ (singleObjHomologySelfIso c j A).hom ≫ f

Tactic:
homologyπ_singleObjHomologySelfIso_hom,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ cyclesMap ((single C c j).map f) j ≫ (singleObjCyclesSelfIso c j B).hom =
    ((single C c j).obj A).homologyπ j ≫ (singleObjHomologySelfIso c j A).hom ≫ f
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ HasSmallLocalizedHom W X Y → Small.{w, v₂} (L.obj X ⟶ L.obj Y)

pp: case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y) → HasSmallLocalizedHom W X Y

Tactic:
· intro h
    exact small_map (homEquiv W W.Q L).symm

Goal state after:
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ Small.{w, v₂} (L.obj X ⟶ L.obj Y) → HasSmallLocalizedHom W X Y
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
hi : ¬∃ j, c.Rel i j
⊢ Epi (homologyMap φ.τ₃ i)

Tactic:
have := hS₂.epi_g
    have eq := (homologyFunctor C _ i).congr_map φ.comm₂₃
    dsimp at eq
    simp only [homologyMap_comp] at eq
    have := epi_homologyMap_of_epi_of_not_rel S₂.g i (by simpa using hi)
    exact epi_of_epi_fac eq.symm

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 : C
J : Type u_1
inst✝ : Fintype J
Y : J → C
c : Bicone Y
hc : c.IsBilimit
n : ℕ
x✝ : (i : J) → Ext X (Y i) n
⊢ (fun e i ↦ e.comp (mk₀ (c.π i)) ⋯) ((fun e ↦ ∑ i, (e i).comp (mk₀ (c.ι i)) ⋯) x✝) = x✝

Tactic:
ext i
    simp only [Ext.sum_comp, comp_assoc_of_second_deg_zero, mk₀_comp_mk₀]
    rw [Finset.sum_eq_single i _ (by simp), bicone_ι_π_self, comp_mk₀_id]
    intro _ _ hij
    rw [c.ι_π, dif_neg hij, mk₀_zero, comp_zero]

Goal state after:
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✝ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact (SmallHom.mkInv qis hqis).comp (SmallHom.mk W δ)

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₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityCounit adj e₁ e₂
X : C
this :
  adj.counit.app ((shiftFunctor D a).obj (F.obj X)) =
    F.map (e₂.hom.app (F.obj X)) ≫ e₁.hom.app (G.obj (F.obj X)) ≫ (shiftFunctor D a).map (adj.counit.app (F.obj X))
⊢ e₁.hom.app X =
    F.map ((shiftFunctor C a).map (adj.unit.app X)) ≫
      F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app ((shiftFunctor D a).obj (F.obj X))

Tactic:
rw [← cancel_epi (F.map (e₂.inv.app _)), ← assoc, ← F.map_comp, Iso.inv_hom_id_app, F.map_id,
    id_comp] at this

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₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityCounit adj e₁ e₂
X : C
this :
  F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app ((shiftFunctor D a).obj (F.obj X)) =
    e₁.hom.app (G.obj (F.obj X)) ≫ (shiftFunctor D a).map (adj.counit.app (F.obj X))
⊢ e₁.hom.app X =
    F.map ((shiftFunctor C a).map (adj.unit.app X)) ≫
      F.map (e₂.inv.app (F.obj X)) ≫ adj.counit.app ((shiftFunctor D a).obj (F.obj X))
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₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ {
      X₁ :=
        (mk₂ ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨0, ⋯⟩,
      X₂ :=
        (mk₂ ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨1, ⋯⟩,
      X₃ :=
        (mk₂ ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨2, ⋯⟩,
      f :=
        (mk₂ ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
          0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
      g :=
        (mk₂ ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
          1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
      zero := ⋯ }.Exact

Tactic:
rwa [ShortComplex.exact_iff_mono _ (by simp)]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
              (shiftFunctor C a).map ((shiftFunctor Cᵒᵖ a).map g).unop) ≫
            (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z =
    ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          (Quiver.Hom.unop g ≫
            ((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
              (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z

Tactic:
rw [← unop_comp_assoc]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y Z : C
a b : ℤ
f : ShiftedHom (Opposite.op Z) (Opposite.op Y) a
g : ShiftedHom (Opposite.op Y) (Opposite.op X) b
c : ℤ
h : b + a = c
⊢ ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          ((((opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
              (shiftFunctor C a).map ((shiftFunctor Cᵒᵖ a).map g).unop) ≫
            (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z =
    ((opShiftFunctorEquivalence C b).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C b).map
          (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y) ≫ g).unop ≫
            (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: case refine_2.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₁' : Mono (R₁.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
hR₂' : Mono (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_6)
h₁ : IsIso (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)
h₂ : Mono (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
ψ : mk₄ 0 0 (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) ⟶ mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) :=
  homMk₄ 0 0 (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) ⋯ ⋯ ⋯ ⋯
⊢ {
      X₁ :=
        (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨0, ⋯⟩,
      X₂ :=
        (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨1, ⋯⟩,
      X₃ :=
        (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).obj
          ⟨2, ⋯⟩,
      f :=
        (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
          0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
      g :=
        (mk₂ ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 0 1 isComplex₂_iff._proof_2 ⋯)
              ((mk₄ 0 0 (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯)).δ₀.map' 1 2 isComplex₂_iff._proof_4 ⋯)).map'
          1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
      zero := ⋯ }.Exact

Tactic:
rwa [ShortComplex.exact_iff_mono _ (by simp)]

Goal state after:
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₃
D : Type u_4
inst✝⁶ : Category.{v_2, u_4} D
inst✝⁵ : HasShift D B
F : C ⥤ D
inst✝⁴ : F.CommShift B
G✝ : C ⥤ D
inst✝³ : G✝.CommShift B
E : Type u_5
inst✝² : Category.{v_3, u_5} E
inst✝¹ : HasShift E B
G : D ⥤ E
inst✝ : G.CommShift B
x✝¹ : A
x✝ : PullbackShift C φ
⊢ (commShiftIso (PullbackShift.functor φ (F ⋙ G)) x✝¹).hom.app x✝ ≫
      (shiftFunctor (PullbackShift E φ) x✝¹).map (𝟙 ((PullbackShift.functor φ (F ⋙ G)).obj x✝)) =
    𝟙 ((PullbackShift.functor φ (F ⋙ G)).obj ((shiftFunctor (PullbackShift C φ) x✝¹).obj x✝)) ≫
      (commShiftIso (PullbackShift.functor φ F ⋙ PullbackShift.functor φ G) x✝¹).hom.app x✝

Tactic:
simp only [commShiftPullback_iso_eq φ _ _ _ rfl, Iso.trans_hom, isoWhiskerRight_hom,
      isoWhiskerLeft_hom, Iso.symm_hom, comp_app, comp_obj, whiskerRight_app, Functor.comp_map,
      commShiftIso_comp_hom_app, whiskerLeft_app, assoc, map_id, comp_id, map_comp, id_comp]

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₃
D : Type u_4
inst✝⁶ : Category.{v_2, u_4} D
inst✝⁵ : HasShift D B
F : C ⥤ D
inst✝⁴ : F.CommShift B
G✝ : C ⥤ D
inst✝³ : G✝.CommShift B
E : Type u_5
inst✝² : Category.{v_3, u_5} E
inst✝¹ : HasShift E B
G : D ⥤ E
inst✝ : G.CommShift B
x✝¹ : A
x✝ : PullbackShift C φ
⊢ G.map (F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝)) ≫
      G.map ((commShiftIso F (φ x✝¹)).hom.app x✝) ≫
        (commShiftIso G (φ x✝¹)).hom.app (F.obj x✝) ≫ (pullbackShiftIso E φ x✝¹ (φ x✝¹) ⋯).inv.app (G.obj (F.obj x✝)) =
    (PullbackShift.functor φ G).map (F.map ((pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯).hom.app x✝)) ≫
      (PullbackShift.functor φ G).map ((commShiftIso F (φ x✝¹)).hom.app x✝) ≫
        (PullbackShift.functor φ G).map ((pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).inv.app (F.obj x✝)) ≫
          G.map ((pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).hom.app ((PullbackShift.functor φ F).obj x✝)) ≫
            (commShiftIso G (φ x✝¹)).hom.app ((PullbackShift.functor φ F).obj x✝) ≫
              (pullbackShiftIso E φ x✝¹ (φ x✝¹) ⋯).inv.app (G.obj ((PullbackShift.functor φ F).obj x✝))
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((inverse C ⋙ functor C).obj T).mor₁ ≫ (Iso.refl ((inverse C ⋙ functor C).obj T).obj₂).hom =
    (Iso.refl ((inverse C ⋙ functor C).obj T).obj₁).hom ≫ ((𝟭 (Triangle Cᵒᵖ)).obj T).mor₁

pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((inverse C ⋙ functor C).obj T).mor₂ ≫ (Iso.refl ((inverse C ⋙ functor C).obj T).obj₃).hom =
    (Iso.refl ((inverse C ⋙ functor C).obj T).obj₂).hom ≫ ((𝟭 (Triangle Cᵒᵖ)).obj T).mor₂

pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((inverse C ⋙ functor C).obj T).mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map (Iso.refl ((inverse C ⋙ functor C).obj T).obj₁).hom =
    (Iso.refl ((inverse C ⋙ functor C).obj T).obj₃).hom ≫ ((𝟭 (Triangle Cᵒᵖ)).obj T).mor₃

Tactic:
· simp

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((inverse C ⋙ functor C).obj T).mor₂ ≫ (Iso.refl ((inverse C ⋙ functor C).obj T).obj₃).hom =
    (Iso.refl ((inverse C ⋙ functor C).obj T).obj₂).hom ≫ ((𝟭 (Triangle Cᵒᵖ)).obj T).mor₂

case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((inverse C ⋙ functor C).obj T).mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map (Iso.refl ((inverse C ⋙ functor C).obj T).obj₁).hom =
    (Iso.refl ((inverse C ⋙ functor C).obj T).obj₃).hom ≫ ((𝟭 (Triangle Cᵒᵖ)).obj T).mor₃
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((inverse C ⋙ functor C).obj T).mor₂ ≫ (Iso.refl ((inverse C ⋙ functor C).obj T).obj₃).hom =
    (Iso.refl ((inverse C ⋙ functor C).obj T).obj₂).hom ≫ ((𝟭 (Triangle Cᵒᵖ)).obj T).mor₂

pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((inverse C ⋙ functor C).obj T).mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map (Iso.refl ((inverse C ⋙ functor C).obj T).obj₁).hom =
    (Iso.refl ((inverse C ⋙ functor C).obj T).obj₃).hom ≫ ((𝟭 (Triangle Cᵒᵖ)).obj T).mor₃

Tactic:
· simp

Goal state after:
case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((inverse C ⋙ functor C).obj T).mor₃ ≫ (shiftFunctor Cᵒᵖ 1).map (Iso.refl ((inverse C ⋙ functor C).obj T).obj₁).hom =
    (Iso.refl ((inverse C ⋙ functor C).obj T).obj₃).hom ≫ ((𝟭 (Triangle Cᵒᵖ)).obj T).mor₃
Module: Mathlib.CategoryTheory.Triangulated.Yoneda

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
B : C
n a a' : ℤ
h : n + a = a'
⊢ ∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
    (shiftFunctor Cᵒᵖ n ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).map f ≫
        (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' n a a' h).symm;
            { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso.hom =
      (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' n a a' h).symm;
            { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso.hom ≫
        (preadditiveYoneda.obj ((shiftFunctor C a').obj B)).map f

Tactic:
intros; ext; apply ShiftedHom.opEquiv'_symm_comp _ _ _ h

Goal state after: