mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ ((pullFunctor F w).map
            (((pullFunctorIdIso F S).symm ≪≫ pullFunctorIso F ⋯ ⋯ ≪≫ (pullFunctorCompIso F w w' (𝟙 S) ⋯ ⋯).symm).hom.app
              D) ≫
          (pullFunctorCompIso F w' w (𝟙 S') ⋯ ⋯ ≪≫ pullFunctorIso F ⋯ ⋯ ≪≫ pullFunctorIdIso F S').hom.app
            ((pullFunctor F w).obj D)).hom
      j =
    (𝟙 ((pullFunctor F w).obj D)).hom j

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
S' : C
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ (F.map (p' j).op.toLoc).toFunctor.map
        ((F.mapId { as := op (X (α j)) }).inv.toNatTrans.app (D.obj (α j)) ≫
          D.hom (𝟙 (X (α j)) ≫ f (α j)) (𝟙 (X (α j))) (q' (α j) ≫ p' (β (α j))) ⋯ ⋯ ≫
            (F.mapComp' (p' (β (α j))).op.toLoc (q' (α j)).op.toLoc ((p' (β (α j))).op.toLoc ≫ (q' (α j)).op.toLoc)
                      ⋯).hom.toNatTrans.app
              (D.obj (α (β (α j))))) ≫
      (F.mapComp' (q' (α j)).op.toLoc (p' j).op.toLoc ((q' (α j)).op.toLoc ≫ (p' j).op.toLoc) ⋯).inv.toNatTrans.app
          ((F.map (p' (β (α j))).op.toLoc).toFunctor.obj (D.obj (α (β (α j))))) ≫
        pullFunctorObjHom w D ((p' j ≫ q' (α j)) ≫ f' (β (α j))) (p' j ≫ q' (α j)) (𝟙 (X' j)) ⋯ ⋯ ≫
          (F.mapId { as := op (X' j) }).hom.toNatTrans.app ((F.map (p' j).op.toLoc).toFunctor.obj (D.obj (α j))) =
    𝟙 ((F.map (p' j).op.toLoc).toFunctor.obj (D.obj (α j)))
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α β : Type uᵒᵖ
f : α ⟶ β
⊢ S.map f ≫ (evalEquiv S hs (unop β)).toIso.hom =
    (evalEquiv S hs (unop α)).toIso.hom ≫ (yoneda.obj (S.obj (op PUnit.{u + 1}))).map f

Tactic:
dsimp

Goal state after:
S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α β : Type uᵒᵖ
f : α ⟶ β
⊢ S.map f ≫ (evalEquiv S hs (unop β)).toIso.hom = (evalEquiv S hs (unop α)).toIso.hom ≫ ↾fun g ↦ f.unop ≫ g
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α
x : α
hsx : ¬S.arrows (↾fun x_1 ↦ x)
β : Type u
f : β ⟶ PUnit.{u + 1}
hf : (Sieve.pullback (↾fun x_1 ↦ x) S).arrows f
⊢ (ConcreteCategory.hom ((yoneda.obj (ULift.{u, 0} Bool)).map f.op)) (↾fun x ↦ { down := true }) =
    (ConcreteCategory.hom ((yoneda.obj (ULift.{u, 0} Bool)).map f.op)) (↾fun x ↦ { down := false })

Tactic:
dsimp

Goal state after:
α : Type u
S : Sieve α
hs : S ∈ (Sheaf.finestTopologySingle (yoneda.obj (ULift.{u, 0} Bool))) α
x : α
hsx : ¬S.arrows (↾fun x_1 ↦ x)
β : Type u
f : β ⟶ PUnit.{u + 1}
hf : (Sieve.pullback (↾fun x_1 ↦ x) S).arrows f
⊢ (f ≫ ↾fun x ↦ { down := true }) = f ≫ ↾fun x ↦ { down := false }
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
c : Classifier C
Y : C
f : Y ⟶ c.Ω₀
⊢ c.χ (𝟙 Y) = c.χ₀ Y ≫ c.truth

Tactic:
simp [← (c.isPullback (𝟙 Y)).w]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
c : Classifier C
Y : C
f : Y ⟶ c.Ω₀
⊢ c.χ (𝟙 Y) = c.χ₀ Y ≫ c.truth

Tactic:
by simp [← (c.isPullback (𝟙 Y)).w]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ pullback.snd 𝒞.truth (𝒞.χ i) ≫ (Iso.refl X).hom =
    (underlyingIso (pullback.snd ((MonoOver.forget 𝒞.Ω).obj (MonoOver.mk 𝒞.truth)).hom (𝒞.χ i))).symm.hom ≫
      ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ pullback.snd 𝒞.truth (𝒞.χ i) ≫ 𝟙 X =
    (underlyingIso (pullback.snd 𝒞.truth (𝒞.χ i))).inv ≫ ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
X : Cᵒᵖ
x : G.obj X
Y Z : C
f : Y ⟶ Opposite.unop X
a : (fun X ↦ X) (F.obj (Opposite.op Y))
ha : (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a
g : Z ⟶ Y
⊢ ∃ a, (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) a

Tactic:
use F.map g.op a

Goal state after:
case h
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
X : Cᵒᵖ
x : G.obj X
Y Z : C
f : Y ⟶ Opposite.unop X
a : (fun X ↦ X) (F.obj (Opposite.op Y))
ha : (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a
g : Z ⟶ Y
⊢ (ConcreteCategory.hom (G.map (g ≫ f).op)) x =
    (ConcreteCategory.hom (m.app (Opposite.op Z))) ((ConcreteCategory.hom (F.map g.op)) a)
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
⊢ Sieve.pullback f.op.unop ((ConcreteCategory.hom (χ'.app X)).toFun x) = ⊤ ↔
    ((ConcreteCategory.hom
              (↾fun x ↦
                {
                  arrows := fun Y f ↦
                    ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
                  downward_closed := ⋯ })).toFun
          x).arrows
      f.op.unop

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
X : Cᵒᵖ
x : G.obj X
h₁ : ∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun x_1 ↦ ⊤
h₂ : ∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x), (ConcreteCategory.hom (m.app x)) x₁ = (ConcreteCategory.hom (m.app x)) y₁ → x₁ = y₁
h₃ :
  ∀ (x : Cᵒᵖ) (x₂ : G.obj x), (ConcreteCategory.hom (χ'.app x)) x₂ = ⊤ → ∃ x₁, (ConcreteCategory.hom (m.app x)) x₁ = x₂
Y : C
f : Y ⟶ Opposite.unop X
⊢ Sieve.pullback f ((ConcreteCategory.hom (χ'.app X)) x) = ⊤ ↔
    ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: case fst
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
y : ↑(F.H' n S.X₄)
⊢ ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
        ((ConcreteCategory.hom
            (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op)))
          y)).1 =
    ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
        ((ConcreteCategory.hom
            (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
          ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
            (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))).1

Tactic:
← AddCommGrpCat.biprodIsoProd_inv_comp_fst_apply,

Goal state after:
case fst
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
y : ↑(F.H' n S.X₄)
⊢ (ConcreteCategory.hom biprod.fst)
      ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).inv)
        ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
          ((ConcreteCategory.hom
              (biprod.lift ((F.cohomologyPresheaf n).map S.f₂₄.op) ((F.cohomologyPresheaf n).map S.f₃₄.op)))
            y))) =
    ((AddCommGrpCat.Hom.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
        ((ConcreteCategory.hom
            (((F.cohomologyPresheaf n).obj (op S.X₂)).biprodIsoProd ((F.cohomologyPresheaf n).obj (op S.X₃))).inv)
          ((ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₂₄.op)) y,
            (ConcreteCategory.hom ((F.cohomologyPresheaf n).map S.f₃₄.op)) y))).1
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
x₂ : ↑(F.H' n S.X₂)
x₃ : ↑(F.H' n S.X₃)
⊢ (Ext.mk₀ S.shortComplex.f).comp
      (Ext.biprodAddEquiv.symm
        ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
          (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv.symm (x₂, x₃))))
      ⋯ =
    (ConcreteCategory.hom (S.fromBiprod F n))
      (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv.symm (x₂, x₃))

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n : ℕ
x₂ : ↑(F.H' n S.X₂)
x₃ : ↑(F.H' n S.X₃)
⊢ (Ext.mk₀ S.shortComplex.f).comp
      (Ext.biprodAddEquiv.symm
        ((ConcreteCategory.hom ((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).hom)
          (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv.symm (x₂, x₃))))
      ⋯ =
    (ConcreteCategory.hom (S.fromBiprod F n))
      (((F.H' n S.X₂).biprodIsoProd (F.H' n S.X₃)).addCommGroupIsoToAddEquiv.symm (x₂, x₃))
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ (S.sequence F n₀ n₁ h).map' 2 3 _proof_299✝ _proof_452✝ ≫ (Iso.refl ((S.sequence F n₀ n₁ h).obj' 3 _proof_452✝)).hom =
    (Iso.refl ((S.sequence F n₀ n₁ h).obj' 2 _proof_451✝)).hom ≫
      (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 2 3 _proof_299✝ _proof_452✝

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Precomp.map (mk₄ (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁) (S.fromBiprod F n₁)) (S.toBiprod F n₀) 2 3 ⋯ ≫
      𝟙 (Precomp.obj (mk₄ (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁) (S.fromBiprod F n₁)) (F.H' n₀ S.X₄) 3) =
    𝟙 (Precomp.obj (mk₄ (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁) (S.fromBiprod F n₁)) (F.H' n₀ S.X₄) 2) ≫
      (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map (homOfLE ⋯)
Module: Mathlib.CategoryTheory.Triangulated.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
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
P✝ : C
φ : P✝ ⟶ Z
hφ : φ ≫ (adj.homEquiv Z T.obj₃) h = 0
⊢ φ ≫ (Triangle.mk (G.map T.mor₁) f g).mor₃ = 0

Tactic:
dsimp

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
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
P✝ : C
φ : P✝ ⟶ Z
hφ : φ ≫ (adj.homEquiv Z T.obj₃) h = 0
⊢ φ ≫ g = 0
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: case e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map (𝟙 ((shiftFunctor D (-n)).op.obj (op (F.obj (unop X))))).unop ≫
      (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Tactic:
dsimp

Goal state after:
case e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctor D n).map (𝟙 ((shiftFunctor D (-n)).obj (F.obj (unop X)))) ≫
      (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

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
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 ((𝟭 Cᵒᵖ).obj X)).unop =
    (((opShiftFunctorEquivalence D n).counitIso.hom.app (op (F.obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).inv.app (unop X)).op).unop ≫
          ((commShiftIso F.op n).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop) ≫
      ((commShiftIso F.op n).inv.app (op ((shiftFunctor C n).obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).hom.app (unop X)).op).unop ≫
          ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X)))).unop

Tactic:
dsimp

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
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map (𝟙 (unop X)) =
    (((opShiftFunctorEquivalence D n).counitIso.hom.app (op (F.obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).inv.app (unop X)).op).unop ≫
          ((commShiftIso F.op n).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop) ≫
      ((commShiftIso F.op n).inv.app (op ((shiftFunctor C n).obj (unop X)))).unop ≫
        ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).hom.app (unop X)).op).unop ≫
          ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X)))).unop
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: case h₁
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ ((F.mapTriangle.op ⋙ (triangleOpEquivalence D).functor).map f✝ ≫
        (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop Y✝)).hom).hom₁ =
    ((F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop X✝)).hom ≫
        ((triangleOpEquivalence C).functor ⋙ F.op.mapTriangle).map f✝).hom₁

Tactic:
dsimp

Goal state after:
case h₁
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (F.map f✝.unop.hom₃).op ≫ 𝟙 (op (F.obj (unop Y✝).obj₃)) = 𝟙 (op (F.obj (unop X✝).obj₃)) ≫ (F.map f✝.unop.hom₃).op
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: case h₂
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ ((F.mapTriangle.op ⋙ (triangleOpEquivalence D).functor).map f✝ ≫
        (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop Y✝)).hom).hom₂ =
    ((F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop X✝)).hom ≫
        ((triangleOpEquivalence C).functor ⋙ F.op.mapTriangle).map f✝).hom₂

Tactic:
dsimp

Goal state after:
case h₂
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (F.map f✝.unop.hom₂).op ≫ 𝟙 (op (F.obj (unop Y✝).obj₂)) = 𝟙 (op (F.obj (unop X✝).obj₂)) ≫ (F.map f✝.unop.hom₂).op
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: case h₃
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ ((F.mapTriangle.op ⋙ (triangleOpEquivalence D).functor).map f✝ ≫
        (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop Y✝)).hom).hom₃ =
    ((F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp (unop X✝)).hom ≫
        ((triangleOpEquivalence C).functor ⋙ F.op.mapTriangle).map f✝).hom₃

Tactic:
dsimp

Goal state after:
case h₃
C : Type u_1
D : Type u_2
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Category.{v_2, u_2} D
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
F : C ⥤ D
inst✝⁸ : F.CommShift ℤ
inst✝⁷ : HasZeroObject C
inst✝⁶ : Preadditive C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasZeroObject D
inst✝² : Preadditive D
inst✝¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝ : Pretriangulated D
X✝ Y✝ : (Triangle C)ᵒᵖ
f✝ : X✝ ⟶ Y✝
⊢ (F.map f✝.unop.hom₁).op ≫ 𝟙 (op (F.obj (unop Y✝).obj₁)) = 𝟙 (op (F.obj (unop X✝).obj₁)) ≫ (F.map f✝.unop.hom₁).op
Module: Mathlib.CategoryTheory.Triangulated.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
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
φ : Y ⟶ G.obj T.obj₃
⊢ (φ ≫ G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁) ≫
      (shiftFunctor C 1).map (Triangle.mk (G.map T.mor₁) f g).mor₁ =
    0

Tactic:
dsimp

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
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
φ : Y ⟶ G.obj T.obj₃
⊢ (φ ≫ G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁) ≫ (shiftFunctor C 1).map (G.map T.mor₁) = 0