mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    inv
        (Q.map
          (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
      Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁) ≫
          (shiftFunctor (DerivedCategory C) 1).map
            (𝟙
              (Q.obj
                (({ functor := fun n ↦ HomologicalComplex.single C (ComplexShape.up ℤ) n,
                          shiftIso := fun n a a' ha' ↦
                            NatIso.ofComponents (fun X ↦ HomologicalComplex.Hom.isoOfComponents (fun i ↦ eqToIso ⋯) ⋯)
                              ⋯,
                          shiftIso_zero := ⋯, shiftIso_add := ⋯ }.functor
                      0).obj
                  S.X₁)))

Tactic:
Functor.map_id,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
S : ShortComplex C
hS : S.ShortExact
inst✝ : HasDerivedCategory C
⊢ (isoOfHom Q W (CochainComplex.mappingCone.descShortComplex (S.map (CochainComplex.singleFunctor C 0))) ⋯).inv ≫
      Q.map (CochainComplex.mappingCone.triangle ((CochainComplex.singleFunctor C 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((CochainComplex.singleFunctor C 0).obj S.X₁) =
    inv
        (Q.map
          (CochainComplex.mappingCone.descShortComplex (S.map (HomologicalComplex.single C (ComplexShape.up ℤ) 0)))) ≫
      Q.map (CochainComplex.mappingCone.triangle ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).map S.f)).mor₃ ≫
        (Functor.commShiftIso Q 1).hom.app ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.X₁) ≫
          𝟙
            ((shiftFunctor (DerivedCategory C) 1).obj
              (Q.obj ((HomologicalComplex.single C (ComplexShape.up ℤ) 0).obj S.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
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ (a₁ + a₂) ⋯).inv.app X =
    (pullbackShiftIso C φ a₂ (φ a₂) ⋯).hom.app ((shiftFunctor (PullbackShift C φ) a₁).obj X) ≫
      (shiftFunctor C (φ a₂)).map ((pullbackShiftIso C φ a₁ (φ a₁) ⋯).hom.app X) ≫
        (shiftFunctorAdd' C (φ a₁) (φ a₂) (φ a₁ + φ a₂) ⋯).inv.app X ≫
          (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.app X

Tactic:
Functor.map_id,

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
h₃ : φ a₁ + φ a₂ = φ (a₁ + a₂)
⊢ (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ (a₁ + a₂) ⋯).inv.app X =
    (pullbackShiftIso C φ a₂ (φ a₂) ⋯).hom.app ((shiftFunctor (PullbackShift C φ) a₁).obj X) ≫
      𝟙 ((shiftFunctor C (φ a₂)).obj ((shiftFunctor (PullbackShift C φ) a₁).obj X)) ≫
        (shiftFunctorAdd' C (φ a₁) (φ a₂) (φ a₁ + φ a₂) ⋯).inv.app X ≫
          (pullbackShiftIso C φ (a₁ + a₂) (φ a₁ + φ a₂) h₃).inv.app X
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: 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₁' : 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₁ : Epi (app' φ 2 mono_of_epi_of_epi_mono'._proof_1)
⊢ Epi (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_6)

Tactic:
let ψ : mk₃ (R₁.map' 0 1) (R₁.map' 1 2) (0 : _ ⟶ R₁.obj' 0) ⟶
    mk₃ (R₂.map' 0 1) (R₂.map' 1 2) (0 : _ ⟶ R₁.obj' 0) := homMk₃ (app' φ 0) (app' φ 1)
      (app' φ 2) (𝟙 _) (naturality' φ 0 1) (naturality' φ 1 2) (by simp)
  refine epi_of_epi_of_epi_of_mono' ψ (exact₂_mk _ (by simp) ?_)
    (hR₂.exact 0).exact_toComposableArrows (by simp)
    h₀ h₁ (by dsimp [ψ]; infer_instance)
  rw [ShortComplex.exact_iff_epi _ (by simp)]
  exact hR₁'

Goal state after:
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))) ≫
          (shiftFunctor Cᵒᵖ a₂).map (𝟙 ((shiftFunctor C b₁).op.obj 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:
Functor.map_id,

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 ≫
        (shiftFunctorOpIso C a₂ b₂ h₂).inv.app (Opposite.op ((shiftFunctor C b₁).1 (Opposite.unop X))) ≫
          𝟙 ((shiftFunctor Cᵒᵖ a₂).obj (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
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

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

Tactic:
Functor.map_id,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
n : ℤ
X : Cᵒᵖ
⊢ (shiftFunctorCompIsoId C n (-n) ⋯).inv.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)) ≫
      ((shiftFunctor Cᵒᵖ n).map
          (((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
            (𝟙 ((shiftFunctor C n).obj (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op)).unop =
    𝟙 (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X))
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₁ e₁' : shiftFunctor C a ⋙ F ≅ F ⋙ shiftFunctor D a
e₂ : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁' e₂
x✝ : C
⊢ e₁.hom.app x✝ = e₁'.hom.app x✝

Tactic:
rw [compatibilityCounit_left adj e₁ e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h),
    compatibilityCounit_left adj e₁' e₂ (compatibilityCounit_of_compatibilityUnit adj _ _ h')]

Goal state after:
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ᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C p).map ((shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map ((shiftFunctorOpIso C n (-n) ⋯).inv.app X).unop).op ≫
        ((shiftFunctor C n).map
              ((shiftFunctor C m).map ((shiftFunctorOpIso C m (-m) ⋯).inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop ≫
                (shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctorAdd' C m n p h).hom.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
            ((shiftFunctor C p).map
                ((shiftFunctorOpIso C m (-m) ⋯).hom.app ((shiftFunctor Cᵒᵖ n).obj X) ≫
                    ((shiftFunctor C (-m)).map ((shiftFunctorOpIso C n (-n) ⋯).hom.app X).unop).op ≫
                      ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op ≫
                        (shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).op

Tactic:
Functor.map_id,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C p).obj (Opposite.unop ((shiftFunctor Cᵒᵖ p).obj X)))).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map ((shiftFunctorOpIso C n (-n) ⋯).inv.app X).unop).op ≫
        ((shiftFunctor C n).map
              ((shiftFunctor C m).map ((shiftFunctorOpIso C m (-m) ⋯).inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop ≫
                (shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctorAdd' C m n p h).hom.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
            ((shiftFunctor C p).map
                ((shiftFunctorOpIso C m (-m) ⋯).hom.app ((shiftFunctor Cᵒᵖ n).obj X) ≫
                    ((shiftFunctor C (-m)).map ((shiftFunctorOpIso C n (-n) ⋯).hom.app X).unop).op ≫
                      ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op ≫
                        (shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).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ᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C p).obj (Opposite.unop ((shiftFunctor Cᵒᵖ p).obj X)))).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map ((shiftFunctorOpIso C n (-n) ⋯).inv.app X).unop).op ≫
        ((shiftFunctor C n).map
              ((shiftFunctor C m).map ((shiftFunctorOpIso C m (-m) ⋯).inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop ≫
                (shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctorAdd' C m n p h).hom.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
            ((shiftFunctor C p).map
                ((shiftFunctorOpIso C m (-m) ⋯).hom.app ((shiftFunctor Cᵒᵖ n).obj X) ≫
                    ((shiftFunctor C (-m)).map ((shiftFunctorOpIso C n (-n) ⋯).hom.app X).unop).op ≫
                      ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op ≫
                        (shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).op

Tactic:
Functor.map_id,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C p).obj (Opposite.unop ((shiftFunctor Cᵒᵖ p).obj X)))).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C n).obj (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctor C n).map
              ((shiftFunctor C m).map ((shiftFunctorOpIso C m (-m) ⋯).inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop ≫
                (shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctorAdd' C m n p h).hom.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
            ((shiftFunctor C p).map
                ((shiftFunctorOpIso C m (-m) ⋯).hom.app ((shiftFunctor Cᵒᵖ n).obj X) ≫
                    ((shiftFunctor C (-m)).map ((shiftFunctorOpIso C n (-n) ⋯).hom.app X).unop).op ≫
                      ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op ≫
                        (shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).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ᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C p).obj (Opposite.unop ((shiftFunctor Cᵒᵖ p).obj X)))).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C n).obj (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctor C n).map
              ((shiftFunctor C m).map ((shiftFunctorOpIso C m (-m) ⋯).inv.app ((shiftFunctor Cᵒᵖ n).obj X)).unop ≫
                (shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctorAdd' C m n p h).hom.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
            ((shiftFunctor C p).map
                ((shiftFunctorOpIso C m (-m) ⋯).hom.app ((shiftFunctor Cᵒᵖ n).obj X) ≫
                    ((shiftFunctor C (-m)).map ((shiftFunctorOpIso C n (-n) ⋯).hom.app X).unop).op ≫
                      ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op ≫
                        (shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).op

Tactic:
Functor.map_id,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C p).obj (Opposite.unop ((shiftFunctor Cᵒᵖ p).obj X)))).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C n).obj (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctor C n).map
              (𝟙 ((shiftFunctor C m).obj (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))) ≫
                (shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctorAdd' C m n p h).hom.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
            ((shiftFunctor C p).map
                ((shiftFunctorOpIso C m (-m) ⋯).hom.app ((shiftFunctor Cᵒᵖ n).obj X) ≫
                    ((shiftFunctor C (-m)).map ((shiftFunctorOpIso C n (-n) ⋯).hom.app X).unop).op ≫
                      ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op ≫
                        (shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).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ᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C p).obj (Opposite.unop ((shiftFunctor Cᵒᵖ p).obj X)))).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C n).obj (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctor C n).map
              (𝟙 ((shiftFunctor C m).obj (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))) ≫
                (shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctorAdd' C m n p h).hom.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
            ((shiftFunctor C p).map
                ((shiftFunctorOpIso C m (-m) ⋯).hom.app ((shiftFunctor Cᵒᵖ n).obj X) ≫
                    ((shiftFunctor C (-m)).map ((shiftFunctorOpIso C n (-n) ⋯).hom.app X).unop).op ≫
                      ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op ≫
                        (shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).op

Tactic:
Functor.map_id,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
m n p : ℤ
h : m + n = p
⊢ ((shiftFunctorCompIsoId C (-p) p ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C p).obj (Opposite.unop ((shiftFunctor Cᵒᵖ p).obj X)))).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      (𝟙 ((shiftFunctor C n).obj (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
        ((shiftFunctor C n).map
              (𝟙 ((shiftFunctor C m).obj (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))) ≫
                (shiftFunctorCompIsoId C (-m) m ⋯).hom.app (Opposite.unop ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
          ((shiftFunctorAdd' C m n p h).hom.app
                (Opposite.unop ((shiftFunctor Cᵒᵖ m).obj ((shiftFunctor Cᵒᵖ n).obj X)))).op ≫
            ((shiftFunctor C p).map
                ((shiftFunctorOpIso C m (-m) ⋯).hom.app ((shiftFunctor Cᵒᵖ n).obj X) ≫
                    (𝟙 ((shiftFunctor C (-m)).obj (Opposite.unop ((shiftFunctor C (-n)).op.obj X)))).op ≫
                      ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X)).op ≫
                        (shiftFunctorOpIso C p (-p) ⋯).inv.app X).unop).op
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✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ (Functor.commShiftIso F a).hom.app X✝ ≫ (shiftFunctor D a).map (𝟙 (F.obj X✝)) = (Functor.commShiftIso F a).hom.app X✝

Tactic:
Functor.map_id,

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✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a : A
X✝ : C
⊢ (Functor.commShiftIso F a).hom.app X✝ ≫ 𝟙 ((shiftFunctor D a).obj (F.obj X✝)) = (Functor.commShiftIso F a).hom.app X✝
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

Goal state before:
pp: case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((opShiftFunctorEquivalence C 1).counitIso.inv.app T.obj₃ ≫
        (shiftFunctor Cᵒᵖ 1).map
          (((shiftFunctor C 1).map T.mor₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app T.obj₁)) ≫
      (shiftFunctor Cᵒᵖ 1).map (𝟙 T.obj₁) =
    𝟙 T.obj₃ ≫ T.mor₃

Tactic:
Functor.map_id,

Goal state after:
case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
T : Triangle Cᵒᵖ
⊢ ((opShiftFunctorEquivalence C 1).counitIso.inv.app T.obj₃ ≫
        (shiftFunctor Cᵒᵖ 1).map
          (((shiftFunctor C 1).map T.mor₃.unop).op ≫ (opShiftFunctorEquivalence C 1).unitIso.inv.app T.obj₁)) ≫
      𝟙 ((shiftFunctor Cᵒᵖ 1).obj T.obj₁) =
    𝟙 T.obj₃ ≫ T.mor₃
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝¹ : Functor.Linear R (L ⋙ G)
this✝ : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this : r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
⊢ G.map e.inv ≫ (r • (L ⋙ G).map (𝟙 (L.objPreimage X))) ≫ G.map e.hom = r • 𝟙 (G.obj X)

Tactic:
Functor.map_id,

Goal state after:
case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
a✝ : Functor.Linear R F
this✝¹ : Functor.Linear R (L ⋙ G)
this✝ : L.EssSurj
X : D
r : R
e : L.obj (L.objPreimage X) ≅ X
this : r • 𝟙 X = e.inv ≫ (r • 𝟙 (L.obj (L.objPreimage X))) ≫ e.hom
⊢ G.map e.inv ≫ (r • 𝟙 ((L ⋙ G).obj (L.objPreimage X))) ≫ G.map e.hom = r • 𝟙 (G.obj X)
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: case mp
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
⊢ Functor.Linear R F → Functor.Linear R G

pp: case mpr
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
⊢ Functor.Linear R G → Functor.Linear R F

Tactic:
· intro
    have : (L ⋙ G).Linear R := Functor.linear_of_iso _ (Lifting.iso L W F G).symm
    have := Localization.essSurj L W
    rw [Functor.linear_iff]
    intro X r
    have e := L.objObjPreimageIso X
    have : r • 𝟙 X = e.inv ≫ (r • 𝟙 _) ≫ e.hom := by simp
    rw [this, G.map_comp, G.map_comp, ← L.map_id, ← L.map_smul, ← Functor.comp_map,
      (L ⋙ G).map_smul, Functor.map_id, Linear.smul_comp, Linear.comp_smul]
    dsimp
    rw [Category.id_comp, ← G.map_comp, e.inv_hom_id, G.map_id]

Goal state after:
case mpr
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹¹ : Category.{v₂, u₂} D
inst✝¹⁰ : Preadditive C
inst✝⁹ : Preadditive D
E : Type u_1
inst✝⁸ : Category.{v_1, u_1} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
inst✝⁶ : Preadditive E
R : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Linear R C
inst✝³ : Linear R D
inst✝² : Linear R E
inst✝¹ : Functor.Linear R L
F : C ⥤ E
G : D ⥤ E
inst✝ : Lifting L W F G
⊢ Functor.Linear R G → Functor.Linear R F
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Linear

Goal state before:
pp: R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y : C
n : ℕ
x : Ext X Y n
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ r • homEquiv x = x.hom.comp (ShiftedHom.mk₀ (↑0) mk₀._proof_1 (r • (DerivedCategory.singleFunctor C 0).map (𝟙 Y))) ⋯

Tactic:
Functor.map_id,

Goal state after:
R : Type t
inst✝⁴ : Ring R
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : Linear R C
inst✝ : HasExt C
X Y : C
n : ℕ
x : Ext X Y n
r : R
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ r • homEquiv x = x.hom.comp (ShiftedHom.mk₀ (↑0) mk₀._proof_1 (r • 𝟙 ((DerivedCategory.singleFunctor C 0).obj Y))) ⋯