awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
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 ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      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₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
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₁'
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₂'
comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂
comm₃' :
  T₂.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) e₂.hom.hom₁ =
    e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₂'.obj₁
comm₃ :
  L.map T₁'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₁'.obj₁ ≫ map (shiftFunctor D (A := ℤ) 1) e₁.inv.hom₁ =
    e₁.inv.hom₃ ≫ T₁.mor₃
φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')
hφ₁ : φ.hom₁ = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
hφ₂ : φ.hom₂ = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
h₂ : L.map T₁'.mor₂ ≫ φ.hom₃ = φ.hom₂ ≫ L.map T₂'.mor₂
h₃ :
  Eq (α := L.obj T₁'.obj₃ ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (L.obj T₂'.obj₁))
    (L.map T₁'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₁'.obj₁ ≫ map (shiftFunctor D (A := ℤ) 1) φ.hom₁)
    (φ.hom₃ ≫ L.map T₂'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₂'.obj₁)
⊢ T₁.mor₂ ≫ e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
have refine_1 : e₁.hom.hom₂ ≫ L.map T₁'.mor₂ ≫ φ.hom₃ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
Tactic: rw [reassoc_of% comm₂, reassoc_of% h₂, hφ₂, assoc, assoc,
      Iso.hom_inv_id_triangle_hom₂_assoc, ← reassoc_of% comm₂',
      Iso.hom_inv_id_triangle_hom₃, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
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 ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      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₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
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₁'
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₂'
comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂
comm₃' :
  T₂.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) e₂.hom.hom₁ =
    e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₂'.obj₁
comm₃ :
  L.map T₁'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₁'.obj₁ ≫ map (shiftFunctor D (A := ℤ) 1) e₁.inv.hom₁ =
    e₁.inv.hom₃ ≫ T₁.mor₃
φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')
hφ₁ : φ.hom₁ = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
hφ₂ : φ.hom₂ = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
h₂ : L.map T₁'.mor₂ ≫ φ.hom₃ = φ.hom₂ ≫ L.map T₂'.mor₂
h₃ :
  Eq (α := L.obj T₁'.obj₃ ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (L.obj T₂'.obj₁))
    (L.map T₁'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₁'.obj₁ ≫ map (shiftFunctor D (A := ℤ) 1) φ.hom₁)
    (φ.hom₃ ≫ L.map T₂'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₂'.obj₁)
refine_1 : e₁.hom.hom₂ ≫ L.map T₁'.mor₂ ≫ φ.hom₃ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
⊢ T₁.mor₂ ≫ e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
have refine_1₁ : e₁.hom.hom₂ ≫ φ.hom₂ ≫ L.map T₂'.mor₂ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
Tactic: rw [reassoc_of% comm₂, reassoc_of% h₂, hφ₂, assoc, assoc,
      Iso.hom_inv_id_triangle_hom₂_assoc, ← reassoc_of% comm₂',
      Iso.hom_inv_id_triangle_hom₃, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
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 ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      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₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
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₁'
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₂'
comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂
comm₃' :
  T₂.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) e₂.hom.hom₁ =
    e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₂'.obj₁
comm₃ :
  L.map T₁'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₁'.obj₁ ≫ map (shiftFunctor D (A := ℤ) 1) e₁.inv.hom₁ =
    e₁.inv.hom₃ ≫ T₁.mor₃
φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')
hφ₁ : φ.hom₁ = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
hφ₂ : φ.hom₂ = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
h₂ : L.map T₁'.mor₂ ≫ φ.hom₃ = φ.hom₂ ≫ L.map T₂'.mor₂
h₃ :
  Eq (α := L.obj T₁'.obj₃ ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (L.obj T₂'.obj₁))
    (L.map T₁'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₁'.obj₁ ≫ map (shiftFunctor D (A := ℤ) 1) φ.hom₁)
    (φ.hom₃ ≫ L.map T₂'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₂'.obj₁)
refine_1 : e₁.hom.hom₂ ≫ L.map T₁'.mor₂ ≫ φ.hom₃ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
refine_1₁ : e₁.hom.hom₂ ≫ φ.hom₂ ≫ L.map T₂'.mor₂ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
⊢ T₁.mor₂ ≫ e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
have refine_1₂ : e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ L.map T₂'.mor₂ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
Tactic: rw [reassoc_of% comm₂, reassoc_of% h₂, hφ₂, assoc, assoc,
      Iso.hom_inv_id_triangle_hom₂_assoc, ← reassoc_of% comm₂',
      Iso.hom_inv_id_triangle_hom₃, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
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 ℤ
H :
  ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
      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₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
            ∃ (φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')),
              φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle.{v_2, u_2} D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
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₁'
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₂'
comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂
comm₃' :
  T₂.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) e₂.hom.hom₁ =
    e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₂'.obj₁
comm₃ :
  L.map T₁'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₁'.obj₁ ≫ map (shiftFunctor D (A := ℤ) 1) e₁.inv.hom₁ =
    e₁.inv.hom₃ ≫ T₁.mor₃
φ : Quiver.Hom (V := Triangle.{v_2, u_2} D) (obj L.mapTriangle T₁') (obj L.mapTriangle T₂')
hφ₁ : φ.hom₁ = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
hφ₂ : φ.hom₂ = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
h₂ : L.map T₁'.mor₂ ≫ φ.hom₃ = φ.hom₂ ≫ L.map T₂'.mor₂
h₃ :
  Eq (α := L.obj T₁'.obj₃ ⟶ obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (L.obj T₂'.obj₁))
    (L.map T₁'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₁'.obj₁ ≫ map (shiftFunctor D (A := ℤ) 1) φ.hom₁)
    (φ.hom₃ ≫ L.map T₂'.mor₃ ≫ NatTrans.app (Iso.hom (commShiftIso L 1)) T₂'.obj₁)
refine_1 : e₁.hom.hom₂ ≫ L.map T₁'.mor₂ ≫ φ.hom₃ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
refine_1₁ : e₁.hom.hom₂ ≫ φ.hom₂ ≫ L.map T₂'.mor₂ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
refine_1₂ : e₁.hom.hom₂ ≫ (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂) ≫ L.map T₂'.mor₂ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
⊢ T₁.mor₂ ≫ e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
have refine_1₃ : e₁.hom.hom₂ ≫ e₁.inv.hom₂ ≫ (b ≫ e₂.hom.hom₂) ≫ L.map T₂'.mor₂ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
Tactic: rw [reassoc_of% comm₂, reassoc_of% h₂, hφ₂, assoc, assoc,
      Iso.hom_inv_id_triangle_hom₂_assoc, ← reassoc_of% comm₂',
      Iso.hom_inv_id_triangle_hom₃, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (hypothesis)
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
X Y : D
f : X ⟶ Y
⊢ ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (Triangle.mk f g h)
have this : L.mapArrow.EssSurj
Tactic: have := essSurj_mapArrow L W
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
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
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
⊢ ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (Triangle.mk f g h)
have obtain : ∀ (φ : Arrow.{v_1, u_1} C) (e : L.mapArrow.obj φ ≅ Arrow.mk f),
  ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (Triangle.mk f g h)
Tactic: obtain ⟨φ, ⟨e⟩⟩ : ∃ (φ : Arrow C), Nonempty (L.mapArrow.obj φ ≅ Arrow.mk f) :=
    ⟨_, ⟨Functor.objObjPreimageIso _ _⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
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
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow.{v_1, u_1} C
e : L.mapArrow.obj φ ≅ Arrow.mk f
⊢ ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (Triangle.mk f g h)
have obtain : ∀ (Z : C) (g : φ.right ⟶ Z) (h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) φ.left)
  (H :
    Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
      (Triangle.mk φ.hom g h)),
  ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (Triangle.mk f g h)
Tactic: obtain ⟨Z, g, h, H⟩ := Pretriangulated.distinguished_cocone_triangle φ.hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
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
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow.{v_1, u_1} C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : φ.right ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) φ.left
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
    (Triangle.mk φ.hom g h)
⊢ ∃ (Z : D) (g : Y ⟶ Z) (h : Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) X),
    Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang (Triangle.mk f g h)
have refine : Iso (C := Triangle.{v_2, u_2} D)
  (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
    (L.map h ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom)))
  (Functor.obj L.mapTriangle (Triangle.mk φ.hom g h))
Tactic: refine ⟨L.obj Z, e.inv.right ≫ L.map g,
    L.map h ≫ (L.commShiftIso (1 : ℤ)).hom.app _ ≫ e.hom.left⟦(1 : ℤ)⟧', _, ?_, H⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
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
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow.{v_1, u_1} C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : φ.right ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) φ.left
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
    (Triangle.mk φ.hom g h)
⊢ Iso (C := Triangle.{v_2, u_2} D)
    (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
      (L.map h ≫
        NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
          Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom)))
    (Functor.obj L.mapTriangle (Triangle.mk φ.hom g h))
have refine : Triangle.mor₃
      (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
        (L.map h ≫
          NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
            Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom))) ≫
    Functor.map (shiftFunctor D (A := ℤ) 1) (Iso.hom (Functor.mapIso Arrow.leftFunc e.symm)) =
  Iso.hom
      (Iso.refl
        (Triangle.obj₃
          (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
            (L.map h ≫
              NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
                Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom))))) ≫
    Triangle.mor₃ (Functor.obj L.mapTriangle (Triangle.mk φ.hom g h))
Tactic: refine Triangle.isoMk _ _ (Arrow.leftFunc.mapIso e.symm) (Arrow.rightFunc.mapIso e.symm)
    (Iso.refl _) e.inv.w.symm (by simp) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
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
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow.{v_1, u_1} C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : φ.right ⟶ Z
h : Z ⟶ Functor.obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) φ.left
H :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _)
    (Triangle.mk φ.hom g h)
⊢ Triangle.mor₃
        (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
          (L.map h ≫
            NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
              Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom))) ≫
      Functor.map (shiftFunctor D (A := ℤ) 1) (Iso.hom (Functor.mapIso Arrow.leftFunc e.symm)) =
    Iso.hom
        (Iso.refl
          (Triangle.obj₃
            (Triangle.mk f (Arrow.Hom.right e.inv ≫ L.map g)
              (L.map h ≫
                NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
                  Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom))))) ≫
      Triangle.mor₃ (Functor.obj L.mapTriangle (Triangle.mk φ.hom g h))
have dsimp : Eq (α := L.obj Z ⟶ Functor.obj.{v_2, v_2, u_2, u_2} (shiftFunctor D (A := ℤ) 1) (L.obj φ.left))
  ((L.map h ≫
      NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left ≫
        Functor.map (shiftFunctor D (A := ℤ) 1) (Arrow.Hom.left e.hom)) ≫
    Functor.map (shiftFunctor D (A := ℤ) 1) e.inv.left)
  (𝟙 (L.obj Z) ≫ L.map h ≫ NatTrans.app (Iso.hom (Functor.commShiftIso L 1)) φ.left)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Triangulated (goal)
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_2, u_2} D
hT₁ : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v_2, u_2} D)) L.essImageDistTriang T₂
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃),
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ Functor.map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have refine : ∀ (T₁' T₂' : Triangle.{v_1, u_1} C),
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_4 _ inst_3 inst_5 _) T₁' →
    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₂),
        L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ →
          ∃ (φ :
            Quiver.Hom (V := Triangle.{v_2, u_2} D) (Functor.obj L.mapTriangle T₁') (Functor.obj L.mapTriangle T₂')),
            φ.hom₁ = a ∧ φ.hom₂ = b
Tactic: refine L.complete_distinguished_essImageDistTriang_morphism ?_ T₁ T₂ hT₁ hT₂ a b fac