awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle.{v_1, u_1} C
hT₁ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₂
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac_1 : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map (W := W) L ⋯
β : W.LeftFraction (α.Y' (W := W)) T₂.obj₂
hβ : T₂.mor₁ ≫ β.s (W := W) = α.s (W := W) ≫ β.f (W := W)
γ : W.LeftFraction T₁.obj₂ (β.Y' (W := W))
hγ : b ≫ L.map (β.s (W := W)) = γ.map (W := W) L ⋯
Z₂ : C
σ : γ.Y' (W := W) ⟶ Z₂
hσ : W σ
fac : α.f (W := W) ≫ β.f (W := W) ≫ γ.s (W := W) ≫ σ = T₁.mor₁ ≫ γ.f (W := W) ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) (α.Y' (W := W))
T₃ : Triangle.{v_1, u_1} C := Triangle.mk (β.f (W := W) ≫ γ.s (W := W) ≫ σ) g h
hT₃ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₃
hβγσ : W (β.s (W := W) ≫ γ.s (W := W) ≫ σ)
ψ₃ : T₂.obj₃ ⟶ T₃.obj₃
hψ₃ : W ψ₃
hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ≫ T₃.mor₂
hψ₂ : T₂.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) (α.s (W := W)) = ψ₃ ≫ T₃.mor₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ (α.s (W := W)) (β.s (W := W) ≫ γ.s (W := W) ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (C := Triangle.{v_2, u_2} D) (X := Functor.obj L.mapTriangle T₂) (Functor.map L.mapTriangle ψ)
⊢ L.map (γ.f (W := W) ≫ σ) = b ≫ L.map (β.s (W := W) ≫ γ.s (W := W) ≫ σ)

Tactic:
simp only [Functor.map_comp, reassoc_of% hγ,
      MorphismProperty.LeftFraction.map_comp_map_s_assoc]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : W.IsCompatibleWithTriangulation
inst_12 : HasZeroObject.{v_2, u_2} D
inst_13 : Preadditive.{v_2, u_2} D
inst_14 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_15 : L.Additive
⊢ L.IsTriangulated

Tactic:
letI : Pretriangulated D := pretriangulated L W
  ⟨fun T hT => ⟨T, Iso.refl _, hT⟩⟩

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Functor.mapTriangle, Exists.intro, CategoryTheory.Functor.IsTriangulated.mk, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : HasZeroObject.{v_2, u_2} D
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : Pretriangulated.{v_2, u_2} D
inst_15 : L.IsTriangulated
inst_16 : IsTriangulated.{v_1, u_1} C
⊢ Functor.EssSurj (C := ComposableArrows.{v_1, u_1} C 2) (L.mapComposableArrows 2)

Tactic:
have := essSurj_mapComposableArrows L W 2
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : HasZeroObject.{v_2, u_2} D
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : Pretriangulated.{v_2, u_2} D
inst_15 : L.IsTriangulated
inst_16 : IsTriangulated.{v_1, u_1} C
this : Functor.EssSurj (C := ComposableArrows.{v_1, u_1} C 2) (L.mapComposableArrows 2)
⊢ IsTriangulated.{v_2, u_2} D

Tactic:
isTriangulated_of_essSurj_mapComposableArrows_two L

Premises used: CategoryTheory.isTriangulated_of_essSurj_mapComposableArrows_two
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : HasZeroObject.{v_2, u_2} D
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : Pretriangulated.{v_2, u_2} D
inst_15 : L.IsTriangulated
inst_16 : IsTriangulated.{v_1, u_1} C
this : Functor.EssSurj (C := ComposableArrows.{v_1, u_1} C 2) (L.mapComposableArrows 2)
⊢ IsTriangulated.{v_2, u_2} D

Tactic:
exact isTriangulated_of_essSurj_mapComposableArrows_two L

Premises used: CategoryTheory.isTriangulated_of_essSurj_mapComposableArrows_two
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : HasZeroObject.{v_2, u_2} D
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : W.IsCompatibleWithTriangulation
n : ℤ
rw : (W.Q ⋙ shiftFunctor W.Localization n).Additive
⊢ Functor.Additive (C := W.Localization) (shiftFunctor W.Localization n)

Tactic:
rw [Localization.functor_additive_iff W.Q W]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.functor_additive_iff
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : HasZeroObject.{v_2, u_2} D
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : W.IsCompatibleWithTriangulation
n : ℤ
⊢ (W.Q ⋙ shiftFunctor W.Localization n).Additive

Tactic:
Functor.additive_of_iso (W.Q.commShiftIso n)

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.additive_of_iso, CategoryTheory.Functor.CommShift.commShiftIso
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : HasZeroObject.{v_2, u_2} D
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : W.IsCompatibleWithTriangulation
n : ℤ
⊢ (W.Q ⋙ shiftFunctor W.Localization n).Additive

Tactic:
exact Functor.additive_of_iso (W.Q.commShiftIso n)

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.additive_of_iso, CategoryTheory.Functor.CommShift.commShiftIso
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : HasZeroObject.{v_2, u_2} D
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : W.IsCompatibleWithTriangulation
inst_15 : IsTriangulated.{v_1, u_1} C
⊢ IsTriangulated W.Localization

Tactic:
isTriangulated W.Q W

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Triangulated.Localization.isTriangulated
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : HasZeroObject.{v_2, u_2} D
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : W.IsCompatibleWithTriangulation
inst_15 : MorphismProperty.HasLocalization.{u_3, v_1, u_1} W
n : ℤ
rw :
  Functor.Additive.{v_1, u_1, u_3, u_1} (D := MorphismProperty.Localization'.{u_3, v_1, u_1} W)
    (W.Q' ⋙ shiftFunctor (MorphismProperty.Localization'.{u_3, v_1, u_1} W) n)
⊢ Functor.Additive.{u_3, u_1, u_3, u_1} (C := MorphismProperty.Localization'.{u_3, v_1, u_1} W)
    (shiftFunctor (MorphismProperty.Localization'.{u_3, v_1, u_1} W) n)

Tactic:
rw [Localization.functor_additive_iff W.Q' W]

Premises used: CategoryTheory.Localization.functor_additive_iff, CategoryTheory.MorphismProperty.Q'
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : HasZeroObject.{v_2, u_2} D
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : W.IsCompatibleWithTriangulation
inst_15 : MorphismProperty.HasLocalization.{u_3, v_1, u_1} W
n : ℤ
⊢ Functor.Additive.{v_1, u_1, u_3, u_1} (D := MorphismProperty.Localization'.{u_3, v_1, u_1} W)
    (W.Q' ⋙ shiftFunctor (MorphismProperty.Localization'.{u_3, v_1, u_1} W) n)

Tactic:
Functor.additive_of_iso (W.Q'.commShiftIso n)

Premises used: CategoryTheory.Functor.additive_of_iso, CategoryTheory.MorphismProperty.Q', CategoryTheory.Functor.CommShift.commShiftIso
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : HasZeroObject.{v_2, u_2} D
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : W.IsCompatibleWithTriangulation
inst_15 : MorphismProperty.HasLocalization.{u_3, v_1, u_1} W
n : ℤ
⊢ Functor.Additive.{v_1, u_1, u_3, u_1} (D := MorphismProperty.Localization'.{u_3, v_1, u_1} W)
    (W.Q' ⋙ shiftFunctor (MorphismProperty.Localization'.{u_3, v_1, u_1} W) n)

Tactic:
exact Functor.additive_of_iso (W.Q'.commShiftIso n)

Premises used: CategoryTheory.Functor.additive_of_iso, CategoryTheory.MorphismProperty.Q', CategoryTheory.Functor.CommShift.commShiftIso
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Functor.Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
W : MorphismProperty.{v_1, u_1} C
inst_9 : L.IsLocalization W
inst_10 : W.HasLeftCalculusOfFractions
inst_11 : HasZeroObject.{v_2, u_2} D
inst_12 : Preadditive.{v_2, u_2} D
inst_13 : ∀ (n : ℤ), Functor.Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_14 : W.IsCompatibleWithTriangulation
inst_15 : MorphismProperty.HasLocalization.{u_3, v_1, u_1} W
inst_16 : IsTriangulated.{v_1, u_1} C
⊢ IsTriangulated.{u_3, u_1} (MorphismProperty.Localization'.{u_3, v_1, u_1} W)

Tactic:
isTriangulated W.Q' W

Premises used: CategoryTheory.Triangulated.Localization.isTriangulated, CategoryTheory.MorphismProperty.Q'
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : L.mapArrow.EssSurj
inst_14 : L.IsTriangulated
T : Triangle.{v_2, u_2} D
mp :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T →
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T
mpr :
  Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T →
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T ↔
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : L.mapArrow.EssSurj
inst_14 : L.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T
f : Arrow.{v_1, u_1} C := L.mapArrow.objPreimage (Arrow.mk T.mor₁)
mp :
  ∀ (Z : C) (g : f.right ⟶ Z) (h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) f.left)
    (mem :
      Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
        (Triangle.mk f.hom g h)),
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T

Tactic:
obtain ⟨Z, g : f.right ⟶ Z, h : Z ⟶ f.left⟦(1 : ℤ)⟧, mem⟩ :=
      Pretriangulated.distinguished_cocone_triangle f.hom

Premises used: CategoryTheory.Arrow.left, CategoryTheory.Arrow.hom, CategoryTheory.Pretriangulated.distinguished_cocone_triangle, OfNat.ofNat, CategoryTheory.Arrow.right
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : L.mapArrow.EssSurj
inst_14 : L.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T
f : Arrow.{v_1, u_1} C := L.mapArrow.objPreimage (Arrow.mk T.mor₁)
Z : C
g : f.right ⟶ Z
h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) f.left
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
    (Triangle.mk f.hom g h)
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T

Tactic:
⟨_, (exists_iso_of_arrow_iso T _ hT (L.map_distinguished _ mem)
      (L.mapArrow.objObjPreimageIso T.mor₁).symm).choose, mem⟩

Premises used: Set.Mem, setOf, CategoryTheory.Functor.objObjPreimageIso, Exists.intro, CategoryTheory.Iso.symm, Exists.choose, CategoryTheory.Functor.essImageDistTriang, CategoryTheory.Functor.mapArrow, CategoryTheory.Pretriangulated.exists_iso_of_arrow_iso, CategoryTheory.Arrow.mk, CategoryTheory.Pretriangulated.Triangle.mor₁, CategoryTheory.Functor.map_distinguished
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : L.mapArrow.EssSurj
inst_14 : L.IsTriangulated
T : Triangle.{v_2, u_2} D
hT : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T
f : Arrow.{v_1, u_1} C := L.mapArrow.objPreimage (Arrow.mk T.mor₁)
Z : C
g : f.right ⟶ Z
h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) f.left
mem :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
    (Triangle.mk f.hom g h)
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T

Tactic:
exact ⟨_, (exists_iso_of_arrow_iso T _ hT (L.map_distinguished _ mem)
      (L.mapArrow.objObjPreimageIso T.mor₁).symm).choose, mem⟩
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : L.mapArrow.EssSurj
inst_14 : L.IsTriangulated
T : Triangle.{v_2, u_2} D
T₀ : Triangle.{v_1, u_1} C
e : T ≅ obj L.mapTriangle T₀
hT₀ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₀
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T

Tactic:
isomorphic_distinguished _ (L.map_distinguished _ hT₀) _ e

Premises used: CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Functor.map_distinguished
-- Module: Mathlib.CategoryTheory.Localization.Triangulated
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : HasShift.{v_1, u_1, 0} C ℤ
inst_3 : Preadditive.{v_1, u_1} C
inst_4 : HasZeroObject.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : HasShift.{v_2, u_2, 0} D ℤ
inst_8 : L.CommShift ℤ
inst_9 : HasZeroObject.{v_2, u_2} D
inst_10 : Preadditive.{v_2, u_2} D
inst_11 : ∀ (n : ℤ), Additive.{v_2, u_2, v_2, u_2} (shiftFunctor D n)
inst_12 : Pretriangulated.{v_2, u_2} D
inst_13 : L.mapArrow.EssSurj
inst_14 : L.IsTriangulated
T : Triangle.{v_2, u_2} D
T₀ : Triangle.{v_1, u_1} C
e : T ≅ obj L.mapTriangle T₀
hT₀ : Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₀
⊢ Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) (@distinguishedTriangles _ _ inst_9 _ inst_10 inst_11 _) T

Tactic:
exact isomorphic_distinguished _ (L.map_distinguished _ hT₀) _ e

Premises used: CategoryTheory.Pretriangulated.isomorphic_distinguished, CategoryTheory.Functor.map_distinguished