mathlib-initiative/mathlib-tactics huggingface dataset:
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₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
⊢ e₂.symm = e₂'.symm

Tactic:
ext

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₂ e₂' : shiftFunctor D a ⋙ G ≅ G ⋙ shiftFunctor C a
h : CompatibilityUnit adj e₁ e₂
h' : CompatibilityUnit adj e₁ e₂'
x✝ : D
⊢ e₂.symm.hom.app x✝ = e₂'.symm.hom.app 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₃ : 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
⊢ isoWhiskerRight (pullbackShiftIso C φ 0 (φ 0) ⋯) F ≪≫
      commShiftIso F (φ 0) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ 0 (φ 0) ⋯).symm =
    CommShift.isoZero (PullbackShift.functor φ F) A

Tactic:
ext

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
x✝ : PullbackShift C φ
⊢ (isoWhiskerRight (pullbackShiftIso C φ 0 (φ 0) ⋯) F ≪≫
            commShiftIso F (φ 0) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ 0 (φ 0) ⋯).symm).hom.app
      x✝ =
    (CommShift.isoZero (PullbackShift.functor φ F) A).hom.app 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₂
⊢ e₁ = e₁'

Tactic:
ext

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₁ 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✝
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
⊢ isoWhiskerRight (pullbackShiftIso C φ (x✝¹ + x✝) (φ (x✝¹ + x✝)) ⋯) F ≪≫
      commShiftIso F (φ (x✝¹ + x✝)) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ (x✝¹ + x✝) (φ (x✝¹ + x✝)) ⋯).symm =
    CommShift.isoAdd
      (isoWhiskerRight (pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯) F ≪≫
        commShiftIso F (φ x✝¹) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).symm)
      (isoWhiskerRight (pullbackShiftIso C φ x✝ (φ x✝) ⋯) F ≪≫
        commShiftIso F (φ x✝) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ x✝ (φ x✝) ⋯).symm)

Tactic:
ext

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
x✝² x✝¹ : A
x✝ : PullbackShift C φ
⊢ (isoWhiskerRight (pullbackShiftIso C φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯) F ≪≫
            commShiftIso F (φ (x✝² + x✝¹)) ≪≫
              F.isoWhiskerLeft (pullbackShiftIso D φ (x✝² + x✝¹) (φ (x✝² + x✝¹)) ⋯).symm).hom.app
      x✝ =
    (CommShift.isoAdd
            (isoWhiskerRight (pullbackShiftIso C φ x✝² (φ x✝²) ⋯) F ≪≫
              commShiftIso F (φ x✝²) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ x✝² (φ x✝²) ⋯).symm)
            (isoWhiskerRight (pullbackShiftIso C φ x✝¹ (φ x✝¹) ⋯) F ≪≫
              commShiftIso F (φ x✝¹) ≪≫ F.isoWhiskerLeft (pullbackShiftIso D φ x✝¹ (φ x✝¹) ⋯).symm)).hom.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ᵒᵖ
⊢ ((shiftFunctor Cᵒᵖ n).map
          ((NatIso.op (shiftFunctorCompIsoId C (-n) n ⋯) ≪≫
                  Functor.isoWhiskerRight (shiftFunctorOpIso C n (-n) ⋯).symm (shiftFunctor C n).op).hom.app
            X) ≫
        ((shiftFunctor C n).op.isoWhiskerLeft (shiftFunctorOpIso C n (-n) ⋯) ≪≫
                NatIso.op (shiftFunctorCompIsoId C n (-n) ⋯).symm).hom.app
          ((shiftFunctor Cᵒᵖ n).obj X)).unop =
    (𝟙 ((shiftFunctor Cᵒᵖ n).obj X)).unop

Tactic:
by
    dsimp [shiftFunctorOpIso]
    erw [comp_id, Functor.map_id, comp_id]
    change (shiftFunctorCompIsoId C n (-n) (add_neg_cancel n)).inv.app (X.unop⟦-n⟧) ≫
      ((shiftFunctorCompIsoId C (-n) n (neg_add_cancel n)).hom.app X.unop)⟦-n⟧' = 𝟙 _
    rw [shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app n X.unop, Iso.inv_hom_id_app]

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
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
x✝ : NatTrans.CommShift adj.unit A
a : A
⊢ (Functor.commShiftIso (G ⋙ F) a).hom ≫ Functor.whiskerRight adj.counit (shiftFunctor D a) =
    (shiftFunctor D a).whiskerLeft adj.counit ≫ (Functor.commShiftIso (𝟭 D) a).hom

Tactic:
ext

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
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
x✝¹ : NatTrans.CommShift adj.unit A
a : A
x✝ : D
⊢ ((Functor.commShiftIso (G ⋙ F) a).hom ≫ Functor.whiskerRight adj.counit (shiftFunctor D a)).app x✝ =
    ((shiftFunctor D a).whiskerLeft adj.counit ≫ (Functor.commShiftIso (𝟭 D) a).hom).app 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₃ : 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
τ : F ⟶ G
inst✝ : CommShift τ B
x✝ : A
⊢ (commShiftIso (PullbackShift.functor φ F) x✝).hom ≫
      whiskerRight (PullbackShift.natTrans φ τ) (shiftFunctor (PullbackShift D φ) x✝) =
    (shiftFunctor (PullbackShift C φ) x✝).whiskerLeft (PullbackShift.natTrans φ τ) ≫
      (commShiftIso (PullbackShift.functor φ G) x✝).hom

Tactic:
ext

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
τ : F ⟶ G
inst✝ : CommShift τ B
x✝¹ : A
x✝ : PullbackShift C φ
⊢ ((commShiftIso (PullbackShift.functor φ F) x✝¹).hom ≫
          whiskerRight (PullbackShift.natTrans φ τ) (shiftFunctor (PullbackShift D φ) x✝¹)).app
      x✝ =
    ((shiftFunctor (PullbackShift C φ) x✝¹).whiskerLeft (PullbackShift.natTrans φ τ) ≫
          (commShiftIso (PullbackShift.functor φ G) x✝¹).hom).app
      x✝
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ᵒᵖ
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles ↔
    ∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

Tactic:
constructor

Goal state after:
case mp
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ᵒᵖ
⊢ Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles →
    ∃ T',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))

case mpr
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',
      ∃ (_ : T' ∈ Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (triangleOpEquivalence C).functor.obj (Opposite.op T'))) →
    Opposite.unop ((triangleOpEquivalence C).inverse.obj T) ∈ Pretriangulated.distinguishedTriangles
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
x✝ : A
⊢ (Functor.commShiftIso (𝟭 (PullbackShift C φ)) x✝).hom ≫
      Functor.whiskerRight (PullbackShift.natIsoId C φ).hom (shiftFunctor (PullbackShift C φ) x✝) =
    (shiftFunctor (PullbackShift C φ) x✝).whiskerLeft (PullbackShift.natIsoId C φ).hom ≫
      (Functor.commShiftIso (PullbackShift.functor φ (𝟭 C)) x✝).hom

Tactic:
ext

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
x✝¹ : A
x✝ : PullbackShift C φ
⊢ ((Functor.commShiftIso (𝟭 (PullbackShift C φ)) x✝¹).hom ≫
          Functor.whiskerRight (PullbackShift.natIsoId C φ).hom (shiftFunctor (PullbackShift C φ) x✝¹)).app
      x✝ =
    ((shiftFunctor (PullbackShift C φ) x✝¹).whiskerLeft (PullbackShift.natIsoId C φ).hom ≫
          (Functor.commShiftIso (PullbackShift.functor φ (𝟭 C)) x✝¹).hom).app
      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✝³ : AddGroup A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : G.CommShift A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.commShiftIso G 0)

Tactic:
G.commShiftIso_zero

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✝ : G.CommShift A
⊢ CommShift.CompatibilityUnit adj (Functor.CommShift.isoZero F A) (Functor.CommShift.isoZero G A)
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
X : Cᵒᵖ
⊢ ((shiftFunctor C (-1)).map 0).op = 0

Tactic:
Functor.map_zero,

Goal state after:
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
X : Cᵒᵖ
⊢ Quiver.Hom.op 0 = 0
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
⊢ (commShiftIso (PullbackShift.functor φ (F ⋙ G)) x✝).hom ≫
      whiskerRight (PullbackShift.natIsoComp φ F G).hom (shiftFunctor (PullbackShift E φ) x✝) =
    (shiftFunctor (PullbackShift C φ) x✝).whiskerLeft (PullbackShift.natIsoComp φ F G).hom ≫
      (commShiftIso (PullbackShift.functor φ F ⋙ PullbackShift.functor φ G) x✝).hom

Tactic:
ext

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 φ
⊢ ((commShiftIso (PullbackShift.functor φ (F ⋙ G)) x✝¹).hom ≫
          whiskerRight (PullbackShift.natIsoComp φ F G).hom (shiftFunctor (PullbackShift E φ) x✝¹)).app
      x✝ =
    ((shiftFunctor (PullbackShift C φ) x✝¹).whiskerLeft (PullbackShift.natIsoComp φ F G).hom ≫
          (commShiftIso (PullbackShift.functor φ F ⋙ PullbackShift.functor φ G) x✝¹).hom).app
      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:
ext

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

Tactic:
ext

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.Localization.Linear

Goal state before:
pp: R : Type w
inst✝⁷ : Ring R
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : L.Additive
inst✝ : Linear R C
this : Linear R D := linear R L W
⊢ Functor.Linear R L

Tactic:
constructor

Goal state after:
R : Type w
inst✝⁷ : Ring R
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : L.Additive
inst✝ : Linear R C
this : Linear R D := ⋯
⊢ autoParam (∀ {X Y : C} (f : X ⟶ Y) (r : R), L.map (r • f) = r • L.map f) Functor.Linear.map_smul._autoParam
Module: Mathlib.CategoryTheory.Localization.Linear

Goal state before:
pp: 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

Tactic:
constructor

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
⊢ Functor.Linear R F → Functor.Linear R G

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.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).obj (L.objPreimage X)) ≫ G.map e.hom) = r • 𝟙 (G.obj X)

Tactic:
Linear.comp_smul

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
⊢ r • G.map e.inv ≫ 𝟙 ((L ⋙ G).obj (L.objPreimage X)) ≫ G.map e.hom = r • 𝟙 (G.obj X)
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 • x = x.comp (mk₀ (r • 𝟙 Y)) ⋯

Tactic:
ext

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 := ⋯
⊢ (r • x).hom = (x.comp (mk₀ (r • 𝟙 Y)) ⋯).hom
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
X : C
S : ShortComplex C
hS : S.ShortExact
n₁ : ℕ
x₁ : Ext X S.X₁ n₁
hx₁ : x₁.comp (mk₀ S.f) ⋯ = 0
n₀ : ℕ
hn₀ : n₀ + 1 = n₁
this :
  ∀
    (x₂ :
      ↑{ X₁ := AddCommGrpCat.of (Ext X S.X₃ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₁ n₁),
            X₃ := AddCommGrpCat.of (Ext X S.X₂ n₁), f := AddCommGrpCat.ofHom (hS.extClass.postcomp X hn₀),
            g := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), zero := ⋯ }.X₂),
    (ConcreteCategory.hom
            { X₁ := AddCommGrpCat.of (Ext X S.X₃ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₁ n₁),
                X₃ := AddCommGrpCat.of (Ext X S.X₂ n₁), f := AddCommGrpCat.ofHom (hS.extClass.postcomp X hn₀),
                g := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), zero := ⋯ }.g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              { X₁ := AddCommGrpCat.of (Ext X S.X₃ n₀), X₂ := AddCommGrpCat.of (Ext X S.X₁ n₁),
                  X₃ := AddCommGrpCat.of (Ext X S.X₂ n₁), f := AddCommGrpCat.ofHom (hS.extClass.postcomp X hn₀),
                  g := AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X ⋯), zero := ⋯ }.f)
            x₁ =
          x₂
⊢ ∃ x₃, x₃.comp hS.extClass hn₀ = x₁

Tactic:
exact this x₁ hx₁

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Ext.Basic

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M N : ModuleCat R
r : R
i : ℕ
x✝ : Ext N M i
⊢ ⇑(ConcreteCategory.hom (AddCommGrpCat.ofHom ((mk₀ (r • 𝟙 M)).postcomp N ⋯))) = HSMul.hSMul r

Tactic:
ext

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Small.{v, u} R
M N : ModuleCat R
r : R
i : ℕ
x✝¹ x✝ : Ext N M i
⊢ (ConcreteCategory.hom (AddCommGrpCat.ofHom ((mk₀ (r • 𝟙 M)).postcomp N ⋯))) x✝ = r • x✝