awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
⊢ T₁.mor₂ ≫
      Iso.hom
        (Functor.mapIso Triangle.π₃
          (h.choose (p := fun (e' : T₁ ≅ T₂) ↦
            e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
              e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))))) =
    e₂.hom ≫ T₂.mor₂
have eq : h.choose (p := fun (e' : T₁ ≅ T₂) ↦
        e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ sorry)) ∧
          e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ sorry))).hom.hom₂ =
  Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ sorry))
Tactic: have eq := h.choose_spec.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
eq :
  h.choose (p := fun (e' : T₁ ≅ T₂) ↦
          e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
            e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))).hom.hom₂ =
    Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
⊢ T₁.mor₂ ≫
      Iso.hom
        (Functor.mapIso Triangle.π₃
          (h.choose (p := fun (e' : T₁ ≅ T₂) ↦
            e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
              e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))))) =
    e₂.hom ≫ T₂.mor₂
have dsimp : T₁.mor₂ ≫ h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ = e₂.hom ≫ T₂.mor₂
Tactic: dsimp at eq ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
eq : h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₂ = e₂.hom
| e₂.hom ≫ T₂.mor₂
have rw : T₁.mor₂ ≫ h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃
Tactic: rw [← eq, ← TriangleMorphism.comm₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
eq : h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₂ = e₂.hom
⊢ T₁.mor₂ ≫ h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ = e₂.hom ≫ T₂.mor₂
have conv_rhs : T₁.mor₂ ≫ h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ = e₂.hom ≫ T₂.mor₂
Tactic: conv_rhs => rw [← eq, ← TriangleMorphism.comm₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
eq : h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₂ = e₂.hom
conv_rhs :
  T₁.mor₂ ≫ h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ = e₂.hom ≫ T₂.mor₂
⊢ T₁.mor₂ ≫ h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ = e₂.hom ≫ T₂.mor₂
have conv_rhs₁ : T₁.mor₂ ≫ h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ =
  T₁.mor₂ ≫ h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃
Tactic: conv_rhs => rw [← eq, ← TriangleMorphism.comm₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
⊢ T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom =
    Iso.hom
        (Functor.mapIso Triangle.π₃
          (h.choose (p := fun (e' : T₁ ≅ T₂) ↦
            e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
              e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))))) ≫
      T₂.mor₃
have eq : h.choose (p := fun (e' : T₁ ≅ T₂) ↦
        e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ sorry)) ∧
          e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ sorry))).hom.hom₁ =
  Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ sorry))
Tactic: have eq := h.choose_spec.1
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
eq :
  h.choose (p := fun (e' : T₁ ≅ T₂) ↦
          e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
            e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))).hom.hom₁ =
    Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
⊢ T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom =
    Iso.hom
        (Functor.mapIso Triangle.π₃
          (h.choose (p := fun (e' : T₁ ≅ T₂) ↦
            e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
              e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))))) ≫
      T₂.mor₃
have dsimp : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom =
  h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ ≫ T₂.mor₃
Tactic: dsimp at eq ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
eq : h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₁ = e₁.hom
| T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom
have rw : h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ ≫ T₂.mor₃
Tactic: rw [← eq, TriangleMorphism.comm₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
eq : h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₁ = e₁.hom
⊢ T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom =
    h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ ≫ T₂.mor₃
have conv_lhs : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom =
  h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ ≫ T₂.mor₃
Tactic: conv_lhs => rw [← eq, TriangleMorphism.comm₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ (e' : T₁ ≅ T₂),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk e₁ e₂ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk e₁ e₂ ⋯))
eq : h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₁ = e₁.hom
conv_lhs :
  T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom =
    h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ ≫ T₂.mor₃
⊢ T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom =
    h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ ≫ T₂.mor₃
have conv_lhs₁ : h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ ≫ T₂.mor₃ =
  h.choose (p := fun (e' : T₁ ≅ T₂) ↦ e'.hom.hom₁ = e₁.hom ∧ e'.hom.hom₂ = e₂.hom).hom.hom₃ ≫ T₂.mor₃
Tactic: conv_lhs => rw [← eq, TriangleMorphism.comm₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
⊢ Iso.hom (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) ≫ (Arrow.mk T₂.invRotate.mor₁).hom =
    (Arrow.mk T₁.invRotate.mor₁).hom ≫ e₁.hom
have this : Eq (α :=
  Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1 ⋙ shiftFunctor C (A := ℤ) (-1)) T₁.obj₁ ⟶
    Functor.obj.{v, v, u, u} (𝟭 C) T₂.obj₁)
  (Functor.map (shiftFunctor C (A := ℤ) 1 ⋙ shiftFunctor C (A := ℤ) (-1)) e₁.hom ≫
    NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) T₂.obj₁)
  (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) T₁.obj₁ ≫ Functor.map (𝟭 C) e₁.hom)
Tactic: have := (shiftFunctorCompIsoId C (1 : ℤ) (-1) (by simp)).hom.naturality e₁.hom
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
this :
  Eq (α :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1 ⋙ shiftFunctor C (A := ℤ) (-1)) T₁.obj₁ ⟶
      Functor.obj.{v, v, u, u} (𝟭 C) T₂.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) 1 ⋙ shiftFunctor C (A := ℤ) (-1)) e₁.hom ≫
      NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₂.obj₁)
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₁.obj₁ ≫ Functor.map (𝟭 C) e₁.hom)
⊢ Iso.hom (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) ≫ (Arrow.mk T₂.invRotate.mor₁).hom =
    (Arrow.mk T₁.invRotate.mor₁).hom ≫ e₁.hom
have dsimp : Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
  (Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom ≫
      (-Functor.map (shiftFunctor C (A := ℤ) (-1)) T₂.mor₃ ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) T₂.obj₁) :
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
  ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) T₁.mor₃ ≫
          NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) T₁.obj₁) ≫
      e₁.hom :
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
Tactic: dsimp at this ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
this :
  Eq (α :=
    Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1))
        (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₁.obj₁) ⟶
      T₂.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) (Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom) ≫
        NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₂.obj₁ :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1))
          (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₁.obj₁) ⟶
        T₂.obj₁)
    (NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₁.obj₁ ≫ e₁.hom :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1))
          (Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) 1) T₁.obj₁) ⟶
        T₂.obj₁)
⊢ Eq (α := Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
    (Functor.map (shiftFunctor C (A := ℤ) (-1)) e₃.hom ≫
        (-Functor.map (shiftFunctor C (A := ℤ) (-1)) T₂.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₂.obj₁) :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
    ((-Functor.map (shiftFunctor C (A := ℤ) (-1)) T₁.mor₃ ≫
            NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) ⋯)) T₁.obj₁) ≫
        e₁.hom :
      Functor.obj.{v, v, u, u} (shiftFunctor C (A := ℤ) (-1)) T₁.obj₃ ⟶ T₂.obj₁)
have simp : Functor.map (shiftFunctor C (A := ℤ) (-1)) (T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom) ≫
    NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) T₂.obj₁ =
  Functor.map (shiftFunctor C (A := ℤ) (-1)) T₁.mor₃ ≫
    NatTrans.app (Iso.hom (shiftFunctorCompIsoId C 1 (-1) sorry)) T₁.obj₁ ≫ e₁.hom
Tactic: simp only [comp_neg, neg_comp, assoc, neg_inj, ← Functor.map_comp_assoc, ← comm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
⊢ T₁ ≅ T₂
have h : ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
  e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ sorry)) ∧
    e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ sorry))
Tactic: have h := exists_iso_of_arrow_iso _ _ (inv_rot_of_distTriang _ hT₁)
    (inv_rot_of_distTriang _ hT₂)
    (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ (by
      have := (shiftFunctorCompIsoId C (1 : ℤ) (-1) (by simp)).hom.naturality e₁.hom
      dsimp at this ⊢
      simp only [comp_neg, neg_comp, assoc, neg_inj, ← Functor.map_comp_assoc, ← comm]
      simp [this]))
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
⊢ T₁ ≅ T₂
have h₁ : e.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ sorry))
Tactic: have h₁ : e.hom.hom₁ = _ := h.choose_spec.1
-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.Pretriangulated (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroObject.{v, u} C
inst_2 : HasShift.{v, u, 0} C ℤ
inst_3 : Preadditive.{v, u} C
inst_4 : ∀ (n : ℤ), Functor.Additive.{v, u, v, u} (shiftFunctor C n)
hC : Pretriangulated.{v, u} C
T₁ T₂ : Triangle.{v, u} C
hT₁ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₁
hT₂ : Membership.mem (γ := Set (Triangle.{v, u} C)) (@distinguishedTriangles _ _ inst_1 _ inst_3 inst_4 _) T₂
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ Functor.map (shiftFunctor C (A := ℤ) 1) e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ (e' : T₁.invRotate ≅ T₂.invRotate),
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
e : T₁.invRotate ≅ T₂.invRotate :=
  h.choose (p := fun (e' : T₁.invRotate ≅ T₂.invRotate) ↦
    e'.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)) ∧
      e'.hom.hom₂ = Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯)))
h₁ : e.hom.hom₁ = Arrow.Hom.left (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ ⋯))
⊢ T₁ ≅ T₂
have h₂ : Arrow.Hom.right (Iso.hom (Arrow.isoMk (Functor.mapIso (shiftFunctor C (A := ℤ) (-1)) e₃) e₁ sorry)) = e.hom.hom₂
Tactic: have h₂ : _ = e.hom.hom₂ := h.choose_spec.2.symm