mathlib-initiative/mathlib-tactics huggingface dataset:
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✝ : F.CommShift A
a b : A
x✝ : Cᵒᵖ
⊢ (F.map ((shiftFunctorAdd C a b).inv.app (Opposite.unop x✝))).op ≫
      ((commShiftIso F b).inv.app ((shiftFunctor C a).obj (Opposite.unop x✝))).op ≫
        ((shiftFunctor D b).map ((commShiftIso F a).inv.app (Opposite.unop x✝))).op ≫
          ((shiftFunctorAdd D a b).hom.app (F.obj (Opposite.unop x✝))).op =
    (OppositeShift.functor A F).map ((shiftFunctorAdd C a b).inv.app (Opposite.unop x✝)).op ≫
      ((commShiftIso F b).inv.app (Opposite.unop ((shiftFunctor (OppositeShift C A) a).obj x✝))).op ≫
        (shiftFunctor (OppositeShift D A) b).map ((commShiftIso F a).inv.app (Opposite.unop x✝)).op ≫
          ((shiftFunctorAdd D a b).hom.app (Opposite.unop ((OppositeShift.functor A F).obj x✝))).op

Tactic:
rfl

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
x✝ : C
⊢ ((OppositeShift.functor A F).map ((shiftFunctorZero C A).hom.app (Opposite.unop (Opposite.op x✝))).op).unop ≫
      ((shiftFunctorZero D A).inv.app (Opposite.unop ((OppositeShift.functor A F).obj (Opposite.op x✝)))).op.unop =
    F.map ((shiftFunctorZero C A).hom.app x✝) ≫ (shiftFunctorZero D A).inv.app (F.obj x✝)

Tactic:
rfl

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).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✝)

Tactic:
rfl

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
x✝¹ : A
x✝ : OppositeShift C A
⊢ 𝟙 ((shiftFunctor (OppositeShift C A) x✝¹).obj x✝) = 𝟙 (Opposite.op ((shiftFunctor C x✝¹).obj (Opposite.unop x✝)))

Tactic:
rfl

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
E : Type u_4
inst✝³ : Category.{v_3, u_4} E
inst✝² : HasShift E A
G : D ⥤ E
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
x✝¹ : A
x✝ : OppositeShift C A
⊢ ((Functor.commShiftIso (F ⋙ G) x✝¹).inv.app (Opposite.unop x✝)).op =
    (Functor.commShiftIso (OppositeShift.functor A F ⋙ OppositeShift.functor A G) x✝¹).hom.app x✝

Tactic:
rfl

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✝ F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : OppositeShift D A
⊢ (𝟙 (G.obj (Opposite.unop x✝))).op = 𝟙 (Opposite.op (G.obj (Opposite.unop x✝)))

Tactic:
rfl

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✝ F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
x✝ : OppositeShift C A
⊢ (𝟙 (F.obj (Opposite.unop x✝))).op = 𝟙 (Opposite.op (F.obj (Opposite.unop x✝)))

Tactic:
rfl

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
a : A
⊢ shiftFunctor (PullbackShift C φ) a = shiftFunctor C (φ a)

Tactic:
rfl

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 φ
⊢ 𝟙 ((𝟭 (PullbackShift C φ)).obj X) = 𝟙 ((𝟭 C).obj X)

Tactic:
rfl

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 ℤ
n : ℤ
hnm : n + -n = 0
⊢ shiftFunctor Cᵒᵖ n = (shiftFunctor C (-n)).op

Tactic:
rfl

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
⊢ (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₃ b₃ ⋯).hom.app X ≫
      ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app (Opposite.unop X)).op ≫
        (pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₂ b₂ ⋯).inv.app
            ((shiftFunctor (OppositeShift C ℤ) b₁).obj X) ≫
          (shiftFunctor (PullbackShift (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯)) a₂).map
            ((pullbackShiftIso (OppositeShift C ℤ) (AddMonoidHom.mk' (fun n ↦ -n) ⋯) a₁ b₁ ⋯).inv.app 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 ((shiftFunctorOpIso C a₁ b₁ h₁).inv.app X)

Tactic:
rfl

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₃
⊢ 𝟙 ((shiftFunctor (PullbackShift C φ) a₁ ⋙ shiftFunctor (PullbackShift C φ) a₂).obj X) =
    𝟙 ((shiftFunctor (PullbackShift C φ) a₂).obj ((shiftFunctor (PullbackShift C φ) a₁).obj X))

Tactic:
rfl

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
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ 0 (φ 0) ⋯).hom.app x✝) ≫
      F.map ((shiftFunctorZero' (PullbackShift C φ) (φ 0) ⋯).hom.app x✝) ≫
        (shiftFunctorZero' (PullbackShift D φ) (φ 0) ⋯).inv.app (F.obj x✝) ≫
          (pullbackShiftIso D φ 0 (φ 0) ⋯).inv.app (F.obj x✝) =
    (PullbackShift.functor φ F).map ((pullbackShiftIso C φ 0 (φ 0) ⋯).hom.app x✝) ≫
      (PullbackShift.functor φ F).map ((shiftFunctorZero' C (φ 0) ⋯).hom.app x✝) ≫
        (shiftFunctorZero' D (φ 0) ⋯).inv.app ((PullbackShift.functor φ F).obj x✝) ≫
          (pullbackShiftIso D φ 0 (φ 0) ⋯).inv.app ((PullbackShift.functor φ F).obj x✝)

Tactic:
rfl

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 : ℤ
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

Tactic:
rfl

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 : ℤ
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

Tactic:
rfl

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 : ℤ
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

Tactic:
rfl

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 : ℤ
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)))

Tactic:
rfl

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 (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((shiftFunctorCompIsoId C (-m) m ⋯).hom.app ((shiftFunctor C (-n)).obj (Opposite.unop X)))).op ≫
        ((shiftFunctorAdd' C m n p h).hom.app
              ((shiftFunctor C (-m)).obj ((shiftFunctor C (-n)).obj (Opposite.unop X)))).op ≫
          ((shiftFunctor C p).map ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X))).op =
    ((shiftFunctorCompIsoId C (-n) n ⋯).hom.app (Opposite.unop X)).op ≫
      ((shiftFunctor C n).map
            ((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 ((shiftFunctorAdd' C (-n) (-m) (-p) ⋯).hom.app (Opposite.unop X))).op

Tactic:
rfl

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
          (((shiftFunctor Cᵒᵖ a ⋙ (shiftFunctor C a).op).map g ≫
                (opShiftFunctorEquivalence C a).unitIso.inv.app ((shiftFunctor Cᵒᵖ b).obj (Opposite.op X))).unop ≫
            (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
        (shiftFunctorAdd' C a b c ⋯).inv.app Z

Tactic:
rfl

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 : C
a' : ℤ
f : ShiftedHom X Y a'
n a : ℤ
h : n + a = a'
⊢ (opEquiv' n a a' h) f = (opEquiv n) (f ≫ (shiftFunctorAdd' C a n a' ⋯).hom.app Y)

Tactic:
rfl

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 : C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
x : Opposite.op ((shiftFunctor C a).obj Y) ⟶ (shiftFunctor Cᵒᵖ (m + n)).obj (Opposite.op X)
⊢ ((opShiftFunctorEquivalence C m).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C m).map
          ((opShiftFunctorEquivalence C n).unitIso.inv.app ((shiftFunctor Cᵒᵖ m).obj (Opposite.op X))).unop ≫
        (shiftFunctor C n ⋙ shiftFunctor C m).map ((shiftFunctorAdd' Cᵒᵖ m n (m + n) ⋯).hom.app (Opposite.op X)).unop ≫
          (shiftFunctor C n ⋙ shiftFunctor C m).map x.unop ≫
            (shiftFunctorAdd' C n m (m + n) ⋯).inv.app ((shiftFunctor C a).obj Y) ≫
              (shiftFunctorAdd' C a (m + n) a'' ⋯).inv.app Y =
    ((opShiftFunctorEquivalence C m).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C m).map
          ((opShiftFunctorEquivalence C n).unitIso.inv.app
              (Opposite.op ((shiftFunctor C ((AddMonoidHom.mk' (fun n ↦ -n) ⋯) m)).obj X))).unop ≫
        (shiftFunctor C m).map
            ((shiftFunctor C n).map ((shiftFunctorAdd' Cᵒᵖ m n (m + n) ⋯).hom.app (Opposite.op X)).unop) ≫
          (shiftFunctor C m).map ((shiftFunctor C n).map x.unop) ≫
            (shiftFunctorAdd' C n m (m + n) ⋯).inv.app ((shiftFunctor C a).obj Y) ≫
              (shiftFunctorAdd' C a (m + n) a'' ⋯).inv.app Y

Tactic:
rfl

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 : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n : ℤ
x y : ShiftedHom (Opposite.op Y) (Opposite.op X) n
⊢ ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C n).map (Quiver.Hom.unop x + Quiver.Hom.unop y) =
    ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
      ((shiftFunctor C n).map (Quiver.Hom.unop x) + (shiftFunctor C n).map (Quiver.Hom.unop y))

Tactic:
← Functor.map_add

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasShift C ℤ
X Y : C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n : ℤ
x y : ShiftedHom (Opposite.op Y) (Opposite.op X) n
⊢ ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C n).map (Quiver.Hom.unop x + Quiver.Hom.unop y) =
    ((opShiftFunctorEquivalence C n).unitIso.inv.app (Opposite.op X)).unop ≫
      (shiftFunctor C n).map (Quiver.Hom.unop x + Quiver.Hom.unop y)
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
x✝² x✝¹ : A
x✝ : PullbackShift C φ
⊢ F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      F.map ((shiftFunctorAdd' (PullbackShift C φ) (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
        (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor (PullbackShift C φ) (φ x✝²)).obj x✝) ≫
          (shiftFunctor (PullbackShift D φ) (φ x✝¹)).map ((commShiftIso F (φ x✝²)).hom.app x✝) ≫
            (shiftFunctorAdd' (PullbackShift D φ) (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) ≫
              (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) =
    F.map ((pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
      F.map ((shiftFunctorAdd' C (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).hom.app x✝) ≫
        (commShiftIso F (φ x✝¹)).hom.app ((shiftFunctor C (φ x✝²)).obj x✝) ≫
          (shiftFunctor D (φ x✝¹)).map ((commShiftIso F (φ x✝²)).hom.app x✝) ≫
            (shiftFunctorAdd' D (φ x✝²) (φ x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝) ≫
              (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).inv.app (F.obj x✝)

Tactic:
rfl

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
D : Type u_4
inst✝² : Category.{v_2, u_4} D
inst✝¹ : HasShift D B
F : C ⥤ D
inst✝ : F.CommShift B
a : A
⊢ commShiftIso (PullbackShift.functor φ F) a =
    isoWhiskerRight (pullbackShiftIso C φ a (φ a) ⋯) F ≪≫
      commShiftIso F (φ a) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ a (φ a) ⋯).symm

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Triangle

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

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ T ∈ distinguishedTriangles C ↔
    Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles

Tactic:
rfl

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
E : C ≌ D
A : Type u_3
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift C A
inst✝⁸ : HasShift D A
inst✝⁷ : E.functor.CommShift A
inst✝⁶ : E.inverse.CommShift A
F : Type u_4
inst✝⁵ : Category.{v_3, u_4} F
inst✝⁴ : HasShift F A
E' : D ≌ F
inst✝³ : E.CommShift A
inst✝² : E'.functor.CommShift A
inst✝¹ : E'.inverse.CommShift A
inst✝ : E'.CommShift A
⊢ (E.trans E').functor.CommShift A

Tactic:
by
  dsimp
  infer_instance

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
E : C ≌ D
A : Type u_3
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift C A
inst✝⁸ : HasShift D A
inst✝⁷ : E.functor.CommShift A
inst✝⁶ : E.inverse.CommShift A
F : Type u_4
inst✝⁵ : Category.{v_3, u_4} F
inst✝⁴ : HasShift F A
E' : D ≌ F
inst✝³ : E.CommShift A
inst✝² : E'.functor.CommShift A
inst✝¹ : E'.inverse.CommShift A
inst✝ : E'.CommShift A
⊢ (E.trans E').inverse.CommShift A

Tactic:
by
  dsimp
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Yoneda

Goal state before:
pp: case e_a.e_a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
T : Triangle C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
B : C
x : T.obj₁ ⟶ (shiftFunctor C n₀).obj B
⊢ ((triangleOpEquivalence C).functor.obj (op T)).mor₃ = (ShiftedHom.opEquiv 1) T.mor₃

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : HasZeroObject C
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle Cᵒᵖ
⊢ T ∈ distinguishedTriangles ↔ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ distinguishedTriangles

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughProjectives

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
P : C
inst✝² : Projective P
K : CochainComplex C ℤ
i : ℤ
π : K ⟶ (singleFunctor C i).obj P
inst✝¹ : K.IsStrictlyLE i
inst✝ : QuasiIsoAt π i
e : cycles K i ≅ K.X i := iCyclesIso K i (i + 1) ⋯ ⋯
α : K.X i ⟶ P := e.inv ≫ homologyπ K i ≫ homologyMap π i ≫ (singleObjHomologySelfIso (ComplexShape.up ℤ) i P).hom
this : π.f i = α ≫ (singleObjXSelf (ComplexShape.up ℤ) i P).inv
⊢ 𝟙 (((single C (ComplexShape.up ℤ) i).obj P).X i) = 𝟙 (((singleFunctor C i).obj P).X i)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

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
X : C
n₀ : ℕ
x : Ext X S.X₃ n₀
n₁ : ℕ
h : n₀ + 1 = n₁
⊢ x.hom ≫
      (shiftFunctor (DerivedCategory C) ↑n₀).map hS.singleTriangle.mor₃ ≫
        (shiftFunctorAdd' (DerivedCategory C) 1 ↑n₀ ↑n₁ ⋯).inv.app hS.singleTriangle.obj₁ =
    x.hom ≫
      (shiftFunctor (DerivedCategory C) ↑n₀).map hS.singleδ ≫
        (shiftFunctorAdd' (DerivedCategory C) ↑1 ↑n₀ ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj S.X₁)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences

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
Y : C
n₀ : ℕ
x : Ext S.X₁ Y n₀
n₁ : ℕ
h : 1 + n₀ = n₁
⊢ hS.singleTriangle.mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map x.hom ≫
        (shiftFunctorAdd' (DerivedCategory C) (↑n₀) 1 ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj Y) =
    hS.singleδ ≫
      (shiftFunctor (DerivedCategory C) ↑1).map x.hom ≫
        (shiftFunctorAdd' (DerivedCategory C) ↑n₀ ↑1 ↑n₁ ⋯).inv.app ((singleFunctor C 0).obj Y)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.Basic

Goal state before:
pp: A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
⊢ Submodule.span A (Set.range relations.relation) ≤ solution.π.ker

Tactic:
by
  rw [Submodule.span_le]
  rintro _ ⟨r, rfl⟩
  simp only [SetLike.mem_coe, LinearMap.mem_ker, π_relation]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Finite ι
M : ι → ι → R
i j : ι
⊢ (Pi.basisFun R ι).toMatrix M i j = Mᵀ i j

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
R₁ : Type u_9
S : Type u_10
inst✝⁴ : CommSemiring R₁
inst✝³ : Semiring S
inst✝² : Algebra R₁ S
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : S
b : Basis ι R₁ S
w : ι → S
i✝ j✝ : ι
⊢ ((Algebra.leftMulMatrix b) x *ᵥ ⇑(b.repr (w j✝))) i✝ = ((Algebra.leftMulMatrix b) x * b.toMatrix w) i✝ j✝

Tactic:
rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Basis

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
κ : Type u_3
κ' : Type u_4
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type u_7
M₂ : Type u_8
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e✝ : Basis ι R M
v✝ : ι' → M
i✝ : ι
j✝ : ι'
inst✝ : Fintype ι
e : Basis ι R M
v w : ι → M
i j : ι
⊢ (e.repr (v j) + e.repr (w j)) i = e.toMatrix v i j + e.toMatrix w i j

Tactic:
rfl

Goal state after: