awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℤ), 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₁ : Triangle.mor₁ (obj L.mapTriangle T₁') ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ Triangle.mor₁ (obj L.mapTriangle T₂')
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ Triangle.mor₂ (obj L.mapTriangle T₁')
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ Triangle.mor₂ (obj L.mapTriangle T₂')
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have comm₃ : Triangle.mor₃ (obj L.mapTriangle T₁') ≫ map (shiftFunctor D (A := ℤ) 1) e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃
Tactic: have comm₃ := e₁.inv.comm₃
-- 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 : ℤ), 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₁ : Triangle.mor₁ (obj L.mapTriangle T₁') ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ Triangle.mor₁ (obj L.mapTriangle T₂')
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ Triangle.mor₂ (obj L.mapTriangle T₁')
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ Triangle.mor₂ (obj L.mapTriangle T₂')
comm₃ : Triangle.mor₃ (obj L.mapTriangle T₁') ≫ map (shiftFunctor D (A := ℤ) 1) e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have comm₃' : T₂.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) e₂.hom.hom₁ = e₂.hom.hom₃ ≫ Triangle.mor₃ (obj L.mapTriangle T₂')
Tactic: have comm₃' := e₂.hom.comm₃
-- 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 : ℤ), 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₃ :
  (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₃
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₁
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have 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₃
Tactic: simp only [assoc] at comm₃
Cleared hypotheses: comm₃
-- 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₃
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have obtain : ∀ (φ : 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₂),
  ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
Tactic: obtain ⟨φ, hφ₁, hφ₂⟩ := H T₁' T₂' hT₁' hT₂' (e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁)
    (e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂)
    (by simp only [assoc, ← comm₁', ← reassoc_of% fac, ← reassoc_of% comm₁])
-- 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 : ℤ), 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₂
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have h₂ : Triangle.mor₂ (obj L.mapTriangle T₁') ≫ φ.hom₃ = φ.hom₂ ≫ Triangle.mor₂ (obj L.mapTriangle T₂')
Tactic: have h₂ := φ.comm₂
-- 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 : ℤ), 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₂ : Triangle.mor₂ (obj L.mapTriangle T₁') ≫ φ.hom₃ = φ.hom₂ ≫ Triangle.mor₂ (obj L.mapTriangle T₂')
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have h₃ : Triangle.mor₃ (obj L.mapTriangle T₁') ≫ map (shiftFunctor D (A := ℤ) 1) φ.hom₁ =
  φ.hom₃ ≫ Triangle.mor₃ (obj L.mapTriangle T₂')
Tactic: have h₃ := φ.comm₃
-- 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 : ℤ), 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₁)
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have 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₁)
Tactic: simp only [assoc] at h₃
Cleared hypotheses: 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 : ℤ), 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₁)
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have refine_1 : T₁.mor₂ ≫ e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
Tactic: refine ⟨e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.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 : ℤ), 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 : T₁.mor₂ ≫ e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃ = b ≫ T₂.mor₂
⊢ ∃ (c : T₁.obj₃ ⟶ T₂.obj₃), T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = c ≫ T₂.mor₃
have refine_2 : T₁.mor₃ ≫ map (shiftFunctor D (A := ℤ) 1) a = (e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃) ≫ T₂.mor₃
Tactic: refine ⟨e₁.hom.hom₃ ≫ φ.hom₃ ≫ e₂.inv.hom₃, ?_, ?_⟩