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

Goal state before:
pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ IsIso ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app S.X₁)

Tactic:
;

Goal state after:
case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ IsIso ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app S.X₁)
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShortExact

Goal state before:
pp: case h₄
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ Mono ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app S.X₂)

Tactic:
;

Goal state after:
case h₄
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n : ℤ
φ : ((homologyFunctor C (up ℤ) 0).homologySequenceComposableArrows₅ (triangleh S.f) n (n + 1) ⋯).δlast ⟶
  (composableArrows₅ hS n (n + 1) ⋯).δlast :=
  homMk₄ ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₂)
    ((homologyFunctorFactors C (up ℤ) n).hom.app (triangle S.f).obj₃ ≫
      HomologicalComplex.homologyMap (descShortComplex S) n)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₁)
    ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app (triangle S.f).obj₂) ⋯ ⋯ ⋯ ⋯
⊢ Mono ((homologyFunctorFactors C (up ℤ) (n + 1)).hom.app S.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)
ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 _proof_300✝)) ⋯ ⋯
    ⋯
⊢ Mono (𝟙 ((mk₃ (R₁.map (homOfLE ⋯)) (R₁.map (homOfLE ⋯)) 0).obj 3))

Tactic:
;

Goal state after:
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)
ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 _proof_300✝)) ⋯ ⋯
    ⋯
⊢ Mono (𝟙 ((mk₃ (R₁.map (homOfLE ⋯)) (R₁.map (homOfLE ⋯)) 0).obj 3))
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
a✝ b✝ : ℤ
⊢ -(a✝ + b✝) = -a✝ + -b✝

Tactic:
;

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
a✝ b✝ : ℤ
⊢ -(a✝ + b✝) = -a✝ + -b✝
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 m : ℤ
hnm : n + m = 0
⊢ shiftFunctor Cᵒᵖ n = (shiftFunctor C m).op

Tactic:
obtain rfl : m = -n := by lia

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
n : ℤ
hnm : n + -n = 0
⊢ shiftFunctor Cᵒᵖ n = (shiftFunctor C (-n)).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ᵒᵖ
a₁ a₂ a₃ : ℤ
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : ℤ
h₁ : a₁ + b₁ = 0
h₂ : a₂ + b₂ = 0
h₃ : a₃ + b₃ = 0
⊢ b₁ = -a₁

Tactic:
;

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
⊢ b₁ = -a₁
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
⊢ b₂ = -a₂

Tactic:
;

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
⊢ b₂ = -a₂
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
⊢ b₃ = -a₃

Tactic:
;

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
⊢ b₃ = -a₃
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)
ψ : mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0 ⟶ mk₃ (R₂.map' 0 1 ⋯ ⋯) (R₂.map' 1 2 ⋯ ⋯) 0 :=
  homMk₃ (app' φ 0 ⋯) (app' φ 1 ⋯) (app' φ 2 ⋯) (𝟙 ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).obj' 3 _proof_300✝)) ⋯ ⋯
    ⋯
⊢ Epi
    {
        X₁ :=
          (mk₂
                ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                  mono_of_epi_of_mono_of_mono'._proof_4)
                ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                  mono_of_epi_of_mono_of_mono'._proof_7)).obj
            ⟨0, ⋯⟩,
        X₂ :=
          (mk₂
                ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                  mono_of_epi_of_mono_of_mono'._proof_4)
                ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                  mono_of_epi_of_mono_of_mono'._proof_7)).obj
            ⟨1, ⋯⟩,
        X₃ :=
          (mk₂
                ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                  mono_of_epi_of_mono_of_mono'._proof_4)
                ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                  mono_of_epi_of_mono_of_mono'._proof_7)).obj
            ⟨2, ⋯⟩,
        f :=
          (mk₂
                ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                  mono_of_epi_of_mono_of_mono'._proof_4)
                ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                  mono_of_epi_of_mono_of_mono'._proof_7)).map'
            0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4,
        g :=
          (mk₂
                ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6
                  mono_of_epi_of_mono_of_mono'._proof_4)
                ((mk₃ (R₁.map' 0 1 ⋯ ⋯) (R₁.map' 1 2 ⋯ ⋯) 0).map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4
                  mono_of_epi_of_mono_of_mono'._proof_7)).map'
            1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5,
        zero := ⋯ }.f

Tactic:
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ᵒᵖ
n m : ℤ
hnm : n + m = 0
⊢ (opShiftFunctorEquivalence C n).unitIso.hom.app X =
    ((shiftFunctorCompIsoId C m n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map ((shiftFunctorOpIso C n m hnm).inv.app X).unop).op

Tactic:
obtain rfl : m = -n := by lia

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

Tactic:
obtain rfl : m = -n := by lia

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

Tactic:
obtain rfl : m = -n := by lia

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

Tactic:
obtain rfl : m = -n := by lia

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

Tactic:
obtain rfl : m = -n := by lia

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : C
n : ℤ
hmn : -n + n = 0
⊢ (shiftFunctor Cᵒᵖ (-n)).map ((opShiftFunctorEquivalence C n).counitIso.inv.app (Opposite.op X)) =
    (opShiftFunctorEquivalence C n).counitIso.inv.app ((shiftFunctor Cᵒᵖ (-n)).obj (Opposite.op X)) ≫
      (shiftFunctor Cᵒᵖ n).map
          ((shiftFunctor C n).map ((shiftFunctorOpIso C (-n) n hmn).hom.app (Opposite.op X)).unop).op ≫
        (shiftFunctor Cᵒᵖ n).map ((shiftFunctorOpIso C (-n) n hmn).inv.app (Opposite.op ((shiftFunctor C n).obj X))) ≫
          (shiftFunctorComm Cᵒᵖ n (-n)).inv.app (Opposite.op ((shiftFunctor C n).obj X))
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 : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ comp
      (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f))
      z h =
    (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.op z ≫ f).unop) ≫
      (shiftFunctorAdd' C b a c h).inv.app Z

Tactic:
ShiftedHom.comp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
      (shiftFunctor C a).map z ≫ (shiftFunctorAdd' C b a c h).inv.app Z =
    (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.op z ≫ f).unop) ≫
      (shiftFunctorAdd' C b a c h).inv.app Z
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
⊢ (shiftFunctor C a).map (adj.unit.app X✝) =
    adj.unit.app ((shiftFunctor C a).obj X✝) ≫
      G.map ((Functor.commShiftIso F a).hom.app X✝) ≫ (iso adj a).hom.app (F.obj X✝)

Tactic:
rw [← cancel_mono ((RightAdjointCommShift.iso adj a).inv.app _), assoc, assoc,
    Iso.hom_inv_id_app, RightAdjointCommShift.iso_inv_app adj _ _ (neg_add_cancel a)]

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
⊢ (shiftFunctor C a).map (adj.unit.app X✝) ≫
      adj.unit.app ((shiftFunctor C a).obj (G.obj (F.obj X✝))) ≫
        G.map ((shiftFunctorCompIsoId D (-a) a ⋯).inv.app (F.obj ((shiftFunctor C a).obj (G.obj (F.obj X✝))))) ≫
          G.map
              ((shiftFunctor D a).map
                ((shiftFunctor D (-a)).map ((Functor.commShiftIso F a).hom.app (G.obj (F.obj X✝))))) ≫
            G.map ((shiftFunctor D a).map ((shiftFunctorCompIsoId D a (-a) ⋯).hom.app (F.obj (G.obj (F.obj X✝))))) ≫
              G.map ((shiftFunctor D a).map (adj.counit.app (F.obj X✝))) =
    adj.unit.app ((shiftFunctor C a).obj X✝) ≫
      G.map ((Functor.commShiftIso F a).hom.app X✝) ≫ 𝟙 ((shiftFunctor D a ⋙ G).obj (F.obj X✝))
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:
;

Goal state after:
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✝
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✝
x✝ : ↑((shiftFunctor Cᵒᵖ n ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj X✝)
⊢ (AddCommGrpCat.Hom.hom
        ((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))
      x✝ =
    (AddCommGrpCat.Hom.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✝))
      x✝

Tactic:
;

Goal state after:
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✝
x✝ : ↑((shiftFunctor Cᵒᵖ n ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj X✝)
⊢ (AddCommGrpCat.Hom.hom
        ((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))
      x✝ =
    (AddCommGrpCat.Hom.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✝))
      x✝
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
a : ℤ
x✝¹ : Cᵒᵖ
x✝ : ↑((shiftFunctor Cᵒᵖ 0 ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj x✝¹)
⊢ (AddCommGrpCat.Hom.hom
        ((NatIso.ofComponents
                (fun A ↦
                  (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' 0 a a ⋯).symm;
                    { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
                ⋯).hom.app
          x✝¹))
      x✝ =
    (AddCommGrpCat.Hom.hom
        ((Functor.isoWhiskerRight (shiftFunctorZero Cᵒᵖ ℤ) (preadditiveYoneda.obj ((shiftFunctor C a).obj B)) ≪≫
                (preadditiveYoneda.obj ((shiftFunctor C a).obj B)).leftUnitor).hom.app
          x✝¹))
      x✝

Tactic:
;

Goal state after:
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
a : ℤ
x✝¹ : Cᵒᵖ
x✝ : ↑((shiftFunctor Cᵒᵖ 0 ⋙ preadditiveYoneda.obj ((shiftFunctor C a).obj B)).obj x✝¹)
⊢ (AddCommGrpCat.Hom.hom
        ((NatIso.ofComponents
                (fun A ↦
                  (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' 0 a a ⋯).symm;
                    { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
                ⋯).hom.app
          x✝¹))
      x✝ =
    (AddCommGrpCat.Hom.hom
        ((Functor.isoWhiskerRight (shiftFunctorZero Cᵒᵖ ℤ) (preadditiveYoneda.obj ((shiftFunctor C a).obj B)) ≪≫
                (preadditiveYoneda.obj ((shiftFunctor C a).obj B)).leftUnitor).hom.app
          x✝¹))
      x✝
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 m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
⊢ NatIso.ofComponents
      (fun A ↦
        (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' (m + n) a a'' ⋯).symm;
          { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
      ⋯ =
    Functor.isoWhiskerRight (shiftFunctorAdd Cᵒᵖ m n) (preadditiveYoneda.obj ((shiftFunctor C a).obj B)) ≪≫
      (shiftFunctor Cᵒᵖ m).associator (shiftFunctor Cᵒᵖ n) (preadditiveYoneda.obj ((shiftFunctor C a).obj B)) ≪≫
        (shiftFunctor Cᵒᵖ m).isoWhiskerLeft
            (NatIso.ofComponents
              (fun A ↦
                (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' n a a' ha').symm;
                  { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
              ⋯) ≪≫
          NatIso.ofComponents
            (fun A ↦
              (let __Equiv := Quiver.Hom.opEquiv.trans (ShiftedHom.opEquiv' m a' a'' ha'').symm;
                { toEquiv := __Equiv, map_add' := ⋯ }).toAddCommGrpIso)
            ⋯

Tactic:
ext _ x
    exact ShiftedHom.opEquiv'_add_symm n m a a' a'' ha' ha'' x.op

Goal state after:
Module: Mathlib.CategoryTheory.Center.Linear

Goal state before:
pp: R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
X : C
⊢ CatCenter.app { app := fun X ↦ (a + b) • 𝟙 X, naturality := ⋯ } X =
    ({ app := fun X ↦ a • 𝟙 X, naturality := ⋯ } + { app := fun X ↦ b • 𝟙 X, naturality := ⋯ }).app X

Tactic:
;

Goal state after:
R : Type w
inst✝³ : Ring R
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
a b : R
X : C
⊢ CatCenter.app { app := fun X ↦ (a + b) • 𝟙 X, naturality := ⋯ } X =
    ({ app := fun X ↦ a • 𝟙 X, naturality := ⋯ } + { app := fun X ↦ b • 𝟙 X, naturality := ⋯ }).app X