-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
/-- A product of distinguished triangles is distinguished -/
lemma productTriangle_distinguished {J : Type*} (T : J → Triangle C)
    (hT : ∀ j, T j ∈ distTriang C)
    [HasProduct (fun j => (T j).obj₁)] [HasProduct (fun j => (T j).obj₂)]
    [HasProduct (fun j => (T j).obj₃)] [HasProduct (fun j => (T j).obj₁⟦(1 : ℤ)⟧)] :
    productTriangle T ∈ distTriang C

Proof state:
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₁
f₁ : (∏ᶜ fun j => (T j).obj₁) ⟶ ∏ᶜ fun j => (T j).obj₂ := Limits.Pi.map fun j => (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j => (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j => (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j =>
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j => (T j).obj₁) j) (Pi.π (fun j => (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
⊢ IsIso (𝟙 T'.obj₁)

Tactic:
infer_instance

Result:
no goals

Proof state:
case intro.intro.intro.refine_1.intro
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₁
f₁ : (∏ᶜ fun j => (T j).obj₁) ⟶ ∏ᶜ fun j => (T j).obj₂ := Limits.Pi.map fun j => (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j => (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j => (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j =>
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j => (T j).obj₁) j) (Pi.π (fun j => (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝ : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun j => (T j).obj₂) j) ≫ (T j).mor₂ = 0
hg'' : ∀ (j : J), ∃ g_1, g ≫ Pi.π (fun j => (T j).obj₂) j = g_1 ≫ (T j).mor₁
α : (j : J) → A ⟶ (T j).obj₁ := fun j => ⋯.choose
hα : ∀ (j : J), g ≫ Pi.π (fun j => (T j).obj₂) j = α j ≫ (T j).mor₁
hg''' : g = Pi.lift α ≫ T'.mor₁
⊢ f = 0

Tactic:
rw [hg, hg''', assoc, comp_distTriang_mor_zero₁₂ _ hT', comp_zero]

Result:
no goals

Proof state:
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₁
f₁ : (∏ᶜ fun j => (T j).obj₁) ⟶ ∏ᶜ fun j => (T j).obj₂ := Limits.Pi.map fun j => (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j => (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j => (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j =>
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j => (T j).obj₁) j) (Pi.π (fun j => (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝¹ : IsIso φ'.hom₁
this✝ : IsIso φ'.hom₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
j : J
this : g ≫ T'.mor₂ ≫ φ'.hom₃ ≫ Pi.π (fun j => (T j).obj₃) j = 0
⊢ (g ≫ Pi.π (fun j => (T j).obj₂) j) ≫ (T j).mor₂ = 0

Tactic:
rw [φ'.comm₂_assoc, h₂, id_comp] at this

Result:
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₁
f₁ : (∏ᶜ fun j => (T j).obj₁) ⟶ ∏ᶜ fun j => (T j).obj₂ := Limits.Pi.map fun j => (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j => (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j => (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j =>
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j => (T j).obj₁) j) (Pi.π (fun j => (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝¹ : IsIso φ'.hom₁
this✝ : IsIso φ'.hom₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
j : J
this : g ≫ (productTriangle T).mor₂ ≫ Pi.π (fun j => (T j).obj₃) j = 0
⊢ (g ≫ Pi.π (fun j => (T j).obj₂) j) ≫ (T j).mor₂ = 0

Proof state:
case intro.intro.intro
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₁
f₁ : (∏ᶜ fun j => (T j).obj₁) ⟶ ∏ᶜ fun j => (T j).obj₂ := Limits.Pi.map fun j => (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j => (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j => (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j =>
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j => (T j).obj₁) j) (Pi.π (fun j => (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
⊢ productTriangle T ∈ distinguishedTriangles

Tactic:
have h₂ : φ'.hom₂ = 𝟙 _ := by aesop_cat

Result:
case intro.intro.intro
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₁
f₁ : (∏ᶜ fun j => (T j).obj₁) ⟶ ∏ᶜ fun j => (T j).obj₂ := Limits.Pi.map fun j => (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j => (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j => (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j =>
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j => (T j).obj₁) j) (Pi.π (fun j => (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
⊢ productTriangle T ∈ distinguishedTriangles