awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : GrothendieckTopology.{v, u} C
F G : Sheaf J_1 (Type (max u v))
J : GrothendieckTopology.{v, u} C
⊢ Presieve.IsSheaf J (closedSieves J).toFunctor

Tactic:
CategoryTheory.classifier_isSheaf J

Premises used: CategoryTheory.classifier_isSheaf
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : GrothendieckTopology.{v, u} C
F G : Sheaf J_1 (Type (max u v))
J : GrothendieckTopology.{v, u} C
⊢ Presieve.IsSheaf J (closedSieves J).toFunctor

Tactic:
exact CategoryTheory.classifier_isSheaf J

Premises used: CategoryTheory.classifier_isSheaf
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
X : Cᵒᵖ
simp :
  ∀ (y : G.obj (P := Presheaf.IsSheaf J).obj X),
    J.IsClosed (X := Opposite.unop X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Presheaf.χ m.hom).app X) :
          (a : G.obj.obj X) → Sieve (Opposite.unop X))
        y)
⊢ (Subfunctor.range (Presheaf.χ m.hom)).obj X ≤ (closedSieves J).obj X

Tactic:
simp only [sieves_obj, Subfunctor.range_obj, closedSieves_obj, Set.le_iff_subset,
      Set.range_subset_iff, Set.mem_setOf_eq]

Premises used: CategoryTheory.Functor.closedSieves_obj, Set.mem_setOf_eq, CategoryTheory.Subfunctor.range_obj, CategoryTheory.Functor.sieves_obj, Set.le_iff_subset, Set.range_subset_iff
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
X : Cᵒᵖ
⊢ ∀ (y : G.obj (P := Presheaf.IsSheaf J).obj X),
    J.IsClosed (X := Opposite.unop X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Presheaf.χ m.hom).app X) :
          (a : G.obj.obj X) → Sieve (Opposite.unop X))
        y)

Tactic:
J.isClosed_χ_app_apply_of_isSheaf_of_isSeparated m.hom
      ((isSheaf_iff_isSheaf_of_type _ _).mp F.property)
      ((isSheaf_iff_isSheaf_of_type _ _).mp G.property).isSeparated _

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.isSheaf_iff_isSheaf_of_type, Iff.mp, CategoryTheory.Presieve.IsSheaf.isSeparated, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.GrothendieckTopology.isClosed_χ_app_apply_of_isSheaf_of_isSeparated
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
X : Cᵒᵖ
⊢ ∀ (y : G.obj (P := Presheaf.IsSheaf J).obj X),
    J.IsClosed (X := Opposite.unop X)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((Presheaf.χ m.hom).app X) :
          (a : G.obj.obj X) → Sieve (Opposite.unop X))
        y)

Tactic:
exact J.isClosed_χ_app_apply_of_isSheaf_of_isSeparated m.hom
      ((isSheaf_iff_isSheaf_of_type _ _).mp F.property)
      ((isSheaf_iff_isSheaf_of_type _ _).mp G.property).isSeparated _

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.isSheaf_iff_isSheaf_of_type, Iff.mp, CategoryTheory.Presieve.IsSheaf.isSeparated, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.GrothendieckTopology.isClosed_χ_app_apply_of_isSheaf_of_isSeparated
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
e : m ≫ χ m = (isTerminalTerminal J Types.isTerminalPUnit).from F ≫ truth J
H :
  IsPullback (P := obj (sheafToPresheaf J (Type (max u v))) F) (map (sheafToPresheaf J (Type (max u v))) m)
    (map (sheafToPresheaf J (Type (max u v))) ((isTerminalTerminal J Types.isTerminalPUnit).from F))
    (map (sheafToPresheaf J (Type (max u v))) (χ m)) (map (sheafToPresheaf J (Type (max u v))) (truth J))
⊢ IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) (χ m) (truth J)

Tactic:
apply IsPullback.of_map (sheafToPresheaf J _)

Premises used: CategoryTheory.IsPullback.of_map, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
e : (m ≫ χ m).hom = ((isTerminalTerminal J Types.isTerminalPUnit).from F ≫ truth J).hom
⊢ m ≫ χ m = (isTerminalTerminal J Types.isTerminalPUnit).from F ≫ truth J

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
e : m.hom ≫ Presheaf.χ m.hom = ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom ≫ Presheaf.truth C
⊢ (m ≫ χ m).hom = ((isTerminalTerminal J Types.isTerminalPUnit).from F ≫ truth J).hom

Tactic:
simp only [Ω_obj, ObjectProperty.FullSubcategory.comp_hom, χ_hom, terminal_obj, truth_hom,
      ← cancel_mono (closedSieves J).ι, Category.assoc, Subfunctor.lift_ι]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.closedSieves, CategoryTheory.Sheaf.terminal_obj, CategoryTheory.Sheaf.χ_hom, CategoryTheory.Subfunctor.lift_ι, CategoryTheory.cancel_mono, CategoryTheory.Sheaf.truth_hom, CategoryTheory.Subfunctor.ι, CategoryTheory.Sheaf.Ω_obj, CategoryTheory.ObjectProperty.FullSubcategory.comp_hom
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
⊢ m.hom ≫ Presheaf.χ m.hom = ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom ≫ Presheaf.truth C

Tactic:
Presheaf.comp_χ_eq m.hom

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.Presheaf.comp_χ_eq, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
⊢ m.hom ≫ Presheaf.χ m.hom = ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom ≫ Presheaf.truth C

Tactic:
exact Presheaf.comp_χ_eq m.hom

Premises used: CategoryTheory.Presheaf.comp_χ_eq, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
H :
  IsPullback m.hom ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom (Subfunctor.lift (Presheaf.χ m.hom) ⋯)
    (Subfunctor.lift (Presheaf.truth C) ⋯)
⊢ IsPullback (P := obj (sheafToPresheaf J (Type (max u v))) F) (map (sheafToPresheaf J (Type (max u v))) m)
    (map (sheafToPresheaf J (Type (max u v))) ((isTerminalTerminal J Types.isTerminalPUnit).from F))
    (map (sheafToPresheaf J (Type (max u v))) (χ m)) (map (sheafToPresheaf J (Type (max u v))) (truth J))

Tactic:
simp only [ObjectProperty.ι_obj, terminal_obj, Ω_obj, ObjectProperty.ι_map, χ_hom, truth_hom]

Premises used: CategoryTheory.Sheaf.terminal_obj, CategoryTheory.ObjectProperty.ι_map, CategoryTheory.Sheaf.χ_hom, CategoryTheory.ObjectProperty.ι_obj, CategoryTheory.Sheaf.truth_hom, CategoryTheory.Sheaf.Ω_obj
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
⊢ (m.hom ≫ Subfunctor.lift (Presheaf.χ m.hom) ⋯) ≫ (closedSieves J).ι =
    (((isTerminalTerminal J Types.isTerminalPUnit).from F).hom ≫ Subfunctor.lift (Presheaf.truth C) ⋯) ≫
      (closedSieves J).ι

Tactic:
simpa using Presheaf.comp_χ_eq _

Premises used: CategoryTheory.Presheaf.comp_χ_eq
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
apply :
  IsPullback (m.hom ≫ 𝟙 (G.obj (P := Presheaf.IsSheaf J))) ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom
    (Presheaf.χ m.hom) (Subfunctor.lift (Presheaf.truth C) ⋯ ≫ (closedSieves J).ι)
apply₁ :
  𝟙 (G.obj (P := Presheaf.IsSheaf J)) ≫ Presheaf.χ m.hom = Subfunctor.lift (Presheaf.χ m.hom) ⋯ ≫ (closedSieves J).ι
⊢ IsPullback m.hom ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom (Subfunctor.lift (Presheaf.χ m.hom) ⋯)
    (Subfunctor.lift (Presheaf.truth C) ⋯)

Tactic:
apply IsPullback.of_right _
      ((cancel_mono ((closedSieves J).ι)).mp (by simpa using Presheaf.comp_χ_eq _))
      (.of_horiz_isIso_mono ⟨_⟩ : IsPullback (𝟙 _) _ (Presheaf.χ m.hom) (closedSieves J).ι)

Premises used: CategoryTheory.Functor.closedSieves, CategoryTheory.cancel_mono, CategoryTheory.CommSq.mk, CategoryTheory.Subfunctor.ι, Iff.mp, CategoryTheory.IsPullback.of_right, CategoryTheory.IsPullback.of_horiz_isIso_mono
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
simp :
  IsPullback m.hom ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom (Presheaf.χ m.hom)
    (Subfunctor.lift (Presheaf.truth C) ⋯ ≫ (closedSieves J).ι)
⊢ IsPullback (m.hom ≫ 𝟙 (G.obj (P := Presheaf.IsSheaf J))) ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom
    (Presheaf.χ m.hom) (Subfunctor.lift (Presheaf.truth C) ⋯ ≫ (closedSieves J).ι)

Tactic:
simp only [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
⊢ IsPullback m.hom ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom (Presheaf.χ m.hom)
    (Subfunctor.lift (Presheaf.truth C) ⋯ ≫ (closedSieves J).ι)

Tactic:
Presheaf.isPullback_χ_truth m.hom

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Limits.IsTerminal.from, TypeCat.Fun.comp, CategoryTheory.Presheaf.isPullback_χ_truth, CategoryTheory.InducedCategory.Hom.hom, CategoryTheory.Presheaf.truth
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
⊢ IsPullback m.hom ((isTerminalTerminal J Types.isTerminalPUnit).from F).hom (Presheaf.χ m.hom)
    (Subfunctor.lift (Presheaf.truth C) ⋯ ≫ (closedSieves J).ι)

Tactic:
exact Presheaf.isPullback_χ_truth m.hom

Premises used: CategoryTheory.Presheaf.isPullback_χ_truth, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
⊢ 𝟙 (G.obj (P := Presheaf.IsSheaf J)) ≫ Presheaf.χ m.hom = Subfunctor.lift (Presheaf.χ m.hom) ⋯ ≫ (closedSieves J).ι

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
h : χ'.hom = (χ m).hom
⊢ χ' = χ m

Tactic:
ext : 1
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
h : χ'.hom ≫ (closedSieves J).ι = Presheaf.χ m.hom
⊢ χ'.hom = (χ m).hom

Tactic:
rw [← cancel_mono (closedSieves J).ι, χ_hom, Subfunctor.lift_ι]

Premises used: CategoryTheory.Functor.closedSieves, CategoryTheory.Sheaf.χ_hom, CategoryTheory.Subfunctor.lift_ι, CategoryTheory.cancel_mono, CategoryTheory.Subfunctor.ι
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
h :
  IsPullback m.hom (IsTerminal.from (isTerminalConst Cᵒᵖ Types.isTerminalPUnit) (F.obj (P := Presheaf.IsSheaf J)))
    (χ'.hom ≫ (closedSieves J).ι) (Presheaf.truth C)
⊢ χ'.hom ≫ (closedSieves J).ι = Presheaf.χ m.hom

Tactic:
apply Presheaf.χ_unique _

Premises used: CategoryTheory.Presheaf.χ_unique
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
⊢ CommSq (𝟙 (G.obj (P := Presheaf.IsSheaf J))) χ'.hom (χ'.hom ≫ (closedSieves J).ι) (closedSieves J).ι

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
⊢ IsPullback (𝟙 (G.obj (P := Presheaf.IsSheaf J))) χ'.hom (χ'.hom ≫ (closedSieves J).ι) (closedSieves J).ι

Tactic:
have pb : IsPullback (𝟙 G.obj) χ'.hom (χ'.hom ≫ (closedSieves J).ι)
    (closedSieves J).ι := IsPullback.of_horiz_isIso_mono (by simp)
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
pb : IsPullback (𝟙 (G.obj (P := Presheaf.IsSheaf J))) χ'.hom (χ'.hom ≫ (closedSieves J).ι) (closedSieves J).ι
⊢ IsPullback m.hom (IsTerminal.from (isTerminalConst Cᵒᵖ Types.isTerminalPUnit) (F.obj (P := Presheaf.IsSheaf J)))
    χ'.hom (truth J).hom

Tactic:
simpa using hχ'.map (sheafToPresheaf J _)

Premises used: CategoryTheory.IsPullback.map, CategoryTheory.sheafToPresheaf
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
pb : IsPullback (𝟙 (G.obj (P := Presheaf.IsSheaf J))) χ'.hom (χ'.hom ≫ (closedSieves J).ι) (closedSieves J).ι
⊢ IsPullback m.hom (IsTerminal.from (isTerminalConst Cᵒᵖ Types.isTerminalPUnit) (F.obj (P := Presheaf.IsSheaf J)))
    χ'.hom (truth J).hom

Tactic:
have : IsPullback m.hom ?_ χ'.hom <| (truth J).hom := by
    simpa using hχ'.map (sheafToPresheaf J _)
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst_1 : Mono m
χ' : G ⟶ Ω J
hχ' : IsPullback m ((isTerminalTerminal J Types.isTerminalPUnit).from F) χ' (truth J)
pb : IsPullback (𝟙 (G.obj (P := Presheaf.IsSheaf J))) χ'.hom (χ'.hom ≫ (closedSieves J).ι) (closedSieves J).ι
this :
  IsPullback m.hom (IsTerminal.from (isTerminalConst Cᵒᵖ Types.isTerminalPUnit) (F.obj (P := Presheaf.IsSheaf J)))
    χ'.hom (truth J).hom
⊢ IsPullback m.hom (IsTerminal.from (isTerminalConst Cᵒᵖ Types.isTerminalPUnit) (F.obj (P := Presheaf.IsSheaf J)))
    (χ'.hom ≫ (closedSieves J).ι) (Presheaf.truth C)

Tactic:
simpa using this.paste_horiz pb

Premises used: CategoryTheory.IsPullback.paste_horiz
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
⊢ G.Additive

Tactic:
have : G.Additive := adj.right_adjoint_additive
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this : G.Additive
obtain :
  ∀ (Z : C) (f : G.obj T.obj₂ ⟶ Z) (g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁))
    (mem :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
        (Triangle.mk (G.map T.mor₁) f g)),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
      (Functor.obj G.mapTriangle T)
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Functor.obj G.mapTriangle T)

Tactic:
obtain ⟨Z, f, g, mem⟩ := distinguished_cocone_triangle (G.map T.mor₁)

Premises used: CategoryTheory.Functor.map, CategoryTheory.Pretriangulated.distinguished_cocone_triangle, CategoryTheory.Pretriangulated.Triangle.mor₁
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
⊢ Triangle.mor₁ (Functor.obj F.mapTriangle (Triangle.mk (G.map T.mor₁) f g)) ≫ adj.counit.app T.obj₂ =
    adj.counit.app T.obj₁ ≫ T.mor₁

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
obtain :
  ∀ (h : Triangle.obj₃ (Functor.obj F.mapTriangle (Triangle.mk (G.map T.mor₁) f g)) ⟶ T.obj₃)
    (h₁ :
      Triangle.mor₂ (Functor.obj F.mapTriangle (Triangle.mk (G.map T.mor₁) f g)) ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂)
    (h₂ :
      Triangle.mor₃ (Functor.obj F.mapTriangle (Triangle.mk (G.map T.mor₁) f g)) ≫
          Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
        h ≫ T.mor₃),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
      (Functor.obj G.mapTriangle T)
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Functor.obj G.mapTriangle T)

Tactic:
obtain ⟨h, ⟨h₁, h₂⟩⟩ := complete_distinguished_triangle_morphism _ _
      (F.map_distinguished _ mem) hT (adj.counit.app T.obj₁) (adj.counit.app T.obj₂) (by simp)

Premises used: CategoryTheory.Pretriangulated.Triangle.obj₁, CategoryTheory.Adjunction.counit, CategoryTheory.Pretriangulated.Triangle.obj₂, CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism, CategoryTheory.Functor.map_distinguished, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Triangulated.Adjunction
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : HasZeroObject.{v_1, u_1} C
inst_3 : HasZeroObject.{v_2, u_2} D
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : Preadditive.{v_2, u_2} D
inst_6 : HasShift.{v_1, u_1, 0} C ℤ
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_9 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_10 : Pretriangulated.{v_1, u_1} C
inst_11 : Pretriangulated.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
G : Functor.{v_2, v_1, u_2, u_1} D C
adj : F ⊣ G
inst_12 : F.CommShift ℤ
inst_13 : G.CommShift ℤ
inst_14 : adj.CommShift ℤ
inst_15 : F.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_3 _ inst_5 inst_9 _) T
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (G.obj T.obj₁)
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) f g)
h : Triangle.obj₃ (Functor.obj F.mapTriangle (Triangle.mk (G.map T.mor₁) f g)) ⟶ T.obj₃
h₁ : Triangle.mor₂ (Functor.obj F.mapTriangle (Triangle.mk (G.map T.mor₁) f g)) ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  Triangle.mor₃ (Functor.obj F.mapTriangle (Triangle.mk (G.map T.mor₁) f g)) ≫
      Functor.map (shiftFunctor D (A := ℤ) 1) (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
dsimp :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Triangle.mk (G.map T.mor₁) (G.map T.mor₂)
      (G.map T.mor₃ ≫ NatTrans.app (Iso.hom (Functor.commShiftIso G 1)) T.obj₁))
⊢ Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_2 _ inst_4 inst_8 _)
    (Functor.obj G.mapTriangle T)

Tactic:
dsimp at h h₁ h₂ ⊢