Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
⊢ productTriangle T ∈ distinguishedTriangles

Tactic:
by
  /- The proof proceeds by constructing a morphism of triangles
    `φ' : T' ⟶ productTriangle T` with `T'` distinguished, and such that
    `φ'.hom₁` and `φ'.hom₂` are identities. Then, it suffices to show that
    `φ'.hom₃` is an isomorphism, which is achieved by using Yoneda's lemma
    and diagram chases. -/
  let f₁ := Limits.Pi.map (fun j => (T j).mor₁)
  obtain ⟨Z, f₂, f₃, hT'⟩ := distinguished_cocone_triangle f₁
  let T' := Triangle.mk f₁ f₂ f₃
  change T' ∈ distTriang C at hT'
  let φ : ∀ j, T' ⟶ T j := fun j => completeDistinguishedTriangleMorphism _ _
    hT' (hT j) (Pi.π _ j) (Pi.π _ j) (by simp [f₁, T'])
  let φ' := productTriangle.lift _ φ
  have h₁ : φ'.hom₁ = 𝟙 _ := by cat_disch
  have h₂ : φ'.hom₂ = 𝟙 _ := by cat_disch
  have : IsIso φ'.hom₁ := by rw [h₁]; infer_instance
  have : IsIso φ'.hom₂ := by rw [h₂]; infer_instance
  suffices IsIso φ'.hom₃ by
    have : IsIso φ' := by
      apply Triangle.isIso_of_isIsos
      all_goals infer_instance
    exact isomorphic_distinguished _ hT' _ (asIso φ').symm
  refine isIso_of_yoneda_map_bijective _ (fun A => ⟨?_, ?_⟩)
  /- the proofs by diagram chase start here -/
  · suffices Mono φ'.hom₃ by
      intro a₁ a₂ ha
      simpa only [← cancel_mono φ'.hom₃] using ha
    rw [mono_iff_cancel_zero]
    intro A f hf
    have hf' : f ≫ T'.mor₃ = 0 := by
      rw [← cancel_mono (φ'.hom₁⟦1⟧'), zero_comp, assoc, φ'.comm₃, reassoc_of% hf, zero_comp]
    obtain ⟨g, hg⟩ := T'.coyoneda_exact₃ hT' f hf'
    have hg' : ∀ j, (g ≫ Pi.π _ j) ≫ (T j).mor₂ = 0 := fun j => by
      have : g ≫ T'.mor₂ ≫ φ'.hom₃ ≫ Pi.π _ j = 0 := by
        rw [← reassoc_of% hg, reassoc_of% hf, zero_comp]
      rw [φ'.comm₂_assoc, h₂, id_comp] at this
      simpa using this
    have hg'' := fun j => (T j).coyoneda_exact₂ (hT j) _ (hg' j)
    let α := fun j => (hg'' j).choose
    have hα : ∀ j, _ = α j ≫ _ := fun j => (hg'' j).choose_spec
    have hg''' : g = Pi.lift α ≫ T'.mor₁ := by dsimp [f₁, T']; ext j; rw [hα]; simp
    rw [hg, hg''', assoc, comp_distTriang_mor_zero₁₂ _ hT', comp_zero]
  · intro a
    obtain ⟨a', ha'⟩ : ∃ (a' : A ⟶ Z), a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃ := by
      have zero : ((productTriangle T).mor₃) ≫ (shiftFunctor C 1).map T'.mor₁ = 0 := by
        rw [← cancel_mono (φ'.hom₂⟦1⟧'), zero_comp, assoc, ← Functor.map_comp, φ'.comm₁, h₁,
          id_comp, productTriangle.zero₃₁]
        intro j
        exact comp_distTriang_mor_zero₃₁ _ (hT j)
      have ⟨g, hg⟩ := T'.coyoneda_exact₁ hT' (a ≫ (productTriangle T).mor₃) (by
        rw [assoc, zero, comp_zero])
      exact ⟨g, hg.symm⟩
    have ha'' := fun (j : J) => (T j).coyoneda_exact₃ (hT j) ((a - a' ≫ φ'.hom₃) ≫ Pi.π _ j) (by
      simp only [sub_comp, assoc]
      erw [← (productTriangle.π T j).comm₃]
      rw [← φ'.comm₃_assoc]
      rw [reassoc_of% ha', sub_eq_zero, h₁, Functor.map_id, id_comp])
    let b := fun j => (ha'' j).choose
    have hb : ∀ j, _ = b j ≫ _ := fun j => (ha'' j).choose_spec
    have hb' : a - a' ≫ φ'.hom₃ = Pi.lift b ≫ (productTriangle T).mor₂ :=
      Limits.Pi.hom_ext _ _ (fun j => by rw [hb]; simp)
    have : (a' + (by exact Pi.lift b) ≫ T'.mor₂) ≫ φ'.hom₃ = a := by
      rw [add_comp, assoc, φ'.comm₂, h₂, id_comp, ← hb', add_sub_cancel]
    exact ⟨_, this⟩

Goal state after: