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 : ι'
⊢ (p' (β (α j))).op.toLoc ≫ (q' (α j)).op.toLoc ≫ (p' j).op.toLoc =
    ((p' (β (α j))).op.toLoc ≫ (q' (α j)).op.toLoc) ≫ (p' j).op.toLoc

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: ⊢ typesGrothendieckTopology = Sheaf.canonicalTopology (Type u)

Tactic:
refine le_antisymm typesGrothendieckTopology.le_canonical (sInf_le ?_)

Goal state after:
⊢ typesGrothendieckTopology ∈ Sheaf.finestTopologySingle '' Set.range yoneda.obj
Module: Mathlib.CategoryTheory.Subfunctor.Finite

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : C
U : Cᵒᵖ
u : (yoneda.obj X).obj U
⊢ (ConcreteCategory.hom ((yoneda.obj X).map (Quiver.Hom.op u))) (𝟙 X) = u

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S : SubmonoidFunctor M
S' : SubmonoidFunctor M'
x✝² x✝¹ : SubmonoidFunctor M
x✝ : C
⊢ x✝².obj x✝ ≤ { obj := fun x ↦ x✝².obj x ⊔ x✝¹.obj x, map := ⋯ }.obj x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S : SubmonoidFunctor M
S' : SubmonoidFunctor M'
x✝² x✝¹ : SubmonoidFunctor M
x✝ : C
⊢ x✝¹.obj x✝ ≤ { obj := fun x ↦ x✝².obj x ⊔ x✝¹.obj x, map := ⋯ }.obj x✝

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝¹ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S✝ : SubmonoidFunctor M
S'✝ : SubmonoidFunctor M'
p : M ⟶ M'
S : SubmonoidFunctor M
S' : SubmonoidFunctor M'
hp : image p ⊤ ≤ S'
U : C
x : ↑(M.obj U)
⊢ (MonCat.Hom.hom (p.app U)) x ∈ (image p ⊤).obj U

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Subobject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A : Subfunctor F
⊢ (𝟭 (Subfunctor F)).obj A =
    ({ obj := fun A ↦ MonoOver.mk A.ι, map := fun {A B} f ↦ MonoOver.homMk (homOfLe ⋯) ⋯, map_id := ⋯, map_comp := ⋯ } ⋙
          { obj := fun X ↦ range X.arrow, map := fun {X Y} f ↦ homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }).obj
      A

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Subobject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A : Subfunctor F
⊢ (fun X ↦ range X.arrow) ((fun A ↦ Subobject.mk A.ι) A) = A

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Subobject

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X : Subobject F
⊢ (fun A ↦ Subobject.mk A.ι) ((fun X ↦ range X.arrow) X) = X

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.RegularEpi

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{?u.8, u_2} D
J : GrothendieckTopology C
inst✝ : HasSheafify J (Type u)
F✝ G✝ : Sheaf J (Type u)
f : F✝ ⟶ G✝
hf : Epi f
⊢ factorThruImage f.hom ≫ image.ι f.hom = f.hom

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Presieve S
⊢ Sieve.generate (Sieve.generate R).arrows = Sieve.generate R

Tactic:
simp

Goal state after:
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
M N : ↑(F.obj { as := op S })
⊢ Function.Bijective (F.toDescentData f).map ↔
    Presieve.IsSheafFor (F.presheafHom M N) (Presieve.ofArrows (fun i ↦ Over.mk (f i)) fun i ↦ Over.homMk (f i) ⋯)

Tactic:
rw [Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible,
    ← (DescentData.subtypeCompatibleHomEquiv F f).bijective.of_comp_iff',
    ← Function.Bijective.of_comp_iff _ (presheafHomObjHomEquiv F).bijective]

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
M N : ↑(F.obj { as := op S })
⊢ Function.Bijective (F.toDescentData f).map ↔
    Function.Bijective
      ((⇑(DescentData.subtypeCompatibleHomEquiv F f) ∘
          Presieve.Arrows.toCompatible (F.presheafHom M N) fun i ↦ Over.homMk (f i) ⋯) ∘
        ⇑F.presheafHomObjHomEquiv)
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
Y : Over S₀
f : Y ⟶ Over.mk a
⊢ ((Sieve.overEquiv (Over.mk a)).symm R).arrows f →
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
          (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
      f

Tactic:
hf

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
S₀ : C
M N : ↑(F.obj { as := op S₀ })
a : S ⟶ S₀
h :
  Presieve.IsSheafFor (F.presheafHom M N)
    (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
Y : Over S₀
f : Y ⟶ Over.mk a
hf : ((Sieve.overEquiv (Over.mk a)).symm R).arrows f
⊢ (Sieve.pullback (Over.isoMk (Iso.refl ((Over.map a).obj (Over.mk (𝟙 S))).left) ⋯).inv
        (Sieve.functorPushforward (Over.map a) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R))).arrows
    f
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
⊢ 𝒞.χ i ≫ (Iso.refl 𝒞.Ω).hom = (Iso.refl X).hom ≫ 𝒞.χ i

Tactic:
simp

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
⊢ 𝒞.truth ≫ (Iso.refl 𝒞.Ω).hom = (Iso.refl 𝒞.Ω₀).hom ≫ 𝒞.truth

Tactic:
simp

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

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X✝ : C
φ : X✝ ⟶ 𝒞.Ω
⊢ (fun x ↦ 𝒞.χ (arrow x)) ((fun φ ↦ (pullback φ).obj 𝒞.truth_as_subobject) φ) = φ

Tactic:
simp

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

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
𝒞 : Classifier C
X✝ : C
x : (Subobject.presheaf C).obj (Opposite.op X✝)
⊢ (fun φ ↦ (pullback φ).obj 𝒞.truth_as_subobject) ((fun x ↦ 𝒞.χ (arrow x)) x) = x

Tactic:
simp

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

Goal state before:
pp: C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
X : C
π' : X ⟶ underlying.obj h.Ω₀
⊢ ∀ (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow), s.fst ≫ 𝟙 X = s.fst

Tactic:
simp

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U✝ X✝ : C
m : U✝ ⟶ X✝
x✝ : Mono m
⊢ m ≫ (Iso.refl X✝).hom = (Iso.refl U✝).hom ≫ m

Tactic:
simp

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U✝ X✝ : C
m : U✝ ⟶ X✝
x✝ : Mono m
⊢ h.χ m ≫ (Iso.refl Ω).hom = (Iso.refl X✝).hom ≫ h.χ m

Tactic:
simp

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U✝ X✝ : C
m : U✝ ⟶ X✝
x✝ : Mono m
⊢ h.Ω₀.arrow ≫ (Iso.refl Ω).hom = h.isoΩ₀.hom ≫ h.isoΩ₀.inv ≫ h.Ω₀.arrow

Tactic:
simp

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U X : C
m : U ⟶ X
x✝ : Mono m
χ₀ : U ⟶ ⊤_ C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (h.isoΩ₀.inv ≫ h.Ω₀.arrow)
⊢ m ≫ (Iso.refl X).hom = (Iso.refl U).hom ≫ m

Tactic:
simp

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U X : C
m : U ⟶ X
x✝ : Mono m
χ₀ : U ⟶ ⊤_ C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (h.isoΩ₀.inv ≫ h.Ω₀.arrow)
⊢ χ' ≫ (Iso.refl Ω).hom = (Iso.refl X).hom ≫ χ'

Tactic:
simp

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

Goal state before:
pp: C✝ : Type u
inst✝³ : Category.{v, u} C✝
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
inst✝ : HasTerminal C
U X : C
m : U ⟶ X
x✝ : Mono m
χ₀ : U ⟶ ⊤_ C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (h.isoΩ₀.inv ≫ h.Ω₀.arrow)
⊢ (h.isoΩ₀.inv ≫ h.Ω₀.arrow) ≫ (Iso.refl Ω).hom = h.isoΩ₀.symm.hom ≫ h.Ω₀.arrow

Tactic:
simp

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

Goal state before:
pp: case commfst
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ e.functor.map (e.inverse.map m) ≫ (e.counitIso.app G).hom = (e.counitIso.app F).hom ≫ m

Tactic:
simp

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

Goal state before:
pp: case commsnd
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F)) ≫ (Iso.refl (e.functor.obj 𝒞₁.Ω₀)).hom =
    (e.counitIso.app F).hom ≫ e.counitInv.app F ≫ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F))

Tactic:
simp

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

Goal state before:
pp: case commf
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ e.functor.map (𝒞₁.χ (e.inverse.map m)) ≫ (Iso.refl (e.functor.obj 𝒞₁.Ω)).hom =
    (e.counitIso.app G).hom ≫ e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))

Tactic:
simp

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

Goal state before:
pp: case commg
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ e.functor.map 𝒞₁.truth ≫ (Iso.refl (e.functor.obj 𝒞₁.Ω)).hom =
    (Iso.refl (e.functor.obj 𝒞₁.Ω₀)).hom ≫ e.functor.map 𝒞₁.truth

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
⊢ J.Covers ((ConcreteCategory.hom ((χ m).app X)) x) f → ((ConcreteCategory.hom ((χ m).app X)) x).arrows f

Tactic:
hf

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf : J.Covers ((ConcreteCategory.hom ((χ m).app X)) x) f
⊢ ((ConcreteCategory.hom ((χ m).app X)) x).arrows f
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((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 := ⋯ }))
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g → (fun X ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g),
    (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) (a Z g hg)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ :
  (Sieve.pullback f
        ((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 := ⋯ }))
          x)).arrows
    f₁
h₂ :
  (Sieve.pullback f
        ((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 := ⋯ }))
          x)).arrows
    f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (m.app (Opposite.op Z))) ((ConcreteCategory.hom (F.map g₁.op)) (a Y₁ f₁ h₁)) =
    (ConcreteCategory.hom (m.app (Opposite.op Z))) ((ConcreteCategory.hom (F.map g₂.op)) (a Y₂ f₂ h₂))

Tactic:
simp_rw [NatTrans.naturality_apply, ← ha, ← Functor.map_comp_apply, ← op_comp,
      reassoc_of% h]

Goal state after:
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
⊢ (F.mapTriangle.obj (Triangle.mk (G.map T.mor₁) f g)).mor₁ ≫ adj.counit.app T.obj₂ = adj.counit.app T.obj₁ ≫ T.mor₁

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
⊢ CommSq (𝟙 G.obj) χ'.hom (χ'.hom ≫ (closedSieves J).ι) (closedSieves J).ι

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
n : ℕ
⊢ ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.retractClosure.extensionProduct
        ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter
            n).retractClosure).retractClosure =
    ((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProduct (P.triangEnvelopeIter n)).retractClosure

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
n : ℕ
⊢ (((P.shiftClosure ℤ).binaryProductsClosure.retractClosure.extensionProductIter n).retractClosure.extensionProduct
        (P.shiftClosure ℤ).binaryProductsClosure.retractClosure.retractClosure).retractClosure =
    ((P.triangEnvelopeIter n).extensionProduct (P.shiftClosure ℤ).binaryProductsClosure.retractClosure).retractClosure

Tactic:
simp

Goal state after:
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).unitIso.inv.app (op (F.obj (unop X)))).unop ≫
      (shiftFunctor D n).map ((commShiftIso F.op n).inv.app X ≫ (commShiftIso F.op n).hom.app X).unop ≫
        ((opShiftFunctorEquivalence D n).unitIso.hom.app (op (F.obj (unop X)))).unop

Tactic:
simp

Goal state after:
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.obj (unop X)) =
    ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X))) ≫
        (shiftFunctor Dᵒᵖ n).map (𝟙 ((F ⋙ shiftFunctor D n).obj (unop X))).op ≫
          (opShiftFunctorEquivalence D n).counitIso.hom.app (op (F.obj (unop X)))).unop

Tactic:
simp

Goal state after:
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 ℤ
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
T : Triangle C
⊢ ((triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T))).mor₁ ≫
      (Iso.refl ((triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T))).obj₂).hom =
    (Iso.refl ((triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T))).obj₁).hom ≫
      (F.op.mapTriangle.obj ((triangleOpEquivalence C).functor.obj (op T))).mor₁

Tactic:
simp

Goal state after:
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 ℤ
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
T : Triangle C
⊢ ((triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T))).mor₂ ≫
      (Iso.refl ((triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T))).obj₃).hom =
    (Iso.refl ((triangleOpEquivalence D).functor.obj (op (F.mapTriangle.obj T))).obj₂).hom ≫
      (F.op.mapTriangle.obj ((triangleOpEquivalence C).functor.obj (op T))).mor₂

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ((opOp C).mapTriangle.obj T).mor₁ ≫ (Iso.refl ((opOp C).mapTriangle.obj T).obj₂).hom =
    (Iso.refl ((opOp C).mapTriangle.obj T).obj₁).hom ≫
      ((triangleOpEquivalence Cᵒᵖ).functor.obj (op ((triangleOpEquivalence C).functor.obj (op T)))).mor₁

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ((opOp C).mapTriangle.obj T).mor₂ ≫ (Iso.refl ((opOp C).mapTriangle.obj T).obj₃).hom =
    (Iso.refl ((opOp C).mapTriangle.obj T).obj₂).hom ≫
      ((triangleOpEquivalence Cᵒᵖ).functor.obj (op ((triangleOpEquivalence C).functor.obj (op T)))).mor₂

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : B ⟶ K
hk : ((shiftFunctor C 1).map (ι.map k) ≫ α) ≫ f₃ = 0
l : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂
hl : (shiftFunctor C 1).map (ι.map k) ≫ α = 0
hm : (shiftFunctor C 1).map ((shiftFunctor C 1).map (ι.map k)) = 0
⊢ (shiftFunctor C 1).map (ι.map k) = 0

Tactic:
exact (shiftFunctor C (1 : ℤ)).map_injective (by rw [hm, Functor.map_zero])

Goal state after: