-- Mathlib/CategoryTheory/Localization/Triangulated.lean
lemma complete_distinguished_triangle_morphism (T₁ T₂ : Triangle D)
    (hT₁ : T₁ ∈ L.essImageDistTriang) (hT₂ : T₂ ∈ L.essImageDistTriang)
    (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂) (fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁) :
    ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ a⟦1⟧' = c ≫ T₂.mor₃

Proof state:
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{u_4, u_1} C
inst✝¹⁰ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
this✝ : IsIso (L.map β.s)
this : IsIso (L.map γ.s)
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
hT₃ : T₃ ∈ distinguishedTriangles
hβγσ : W (β.s ≫ γ.s ≫ σ)
⊢ T₂.mor₁ ≫ β.s ≫ γ.s ≫ σ = α.s ≫ β.f ≫ γ.s ≫ σ

Tactic:
rw [reassoc_of% hβ]

Result:
no goals

Proof state:
case intro.intro
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{u_4, u_1} C
inst✝¹⁰ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ :
  (MorphismProperty.RightFraction.mk α.s ⋯ T₂.mor₁).f ≫ β.s = (MorphismProperty.RightFraction.mk α.s ⋯ T₂.mor₁).s ≫ β.f
⊢ ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b

Tactic:
obtain ⟨γ, hγ⟩ := exists_leftFraction L W (b ≫ L.map β.s)

Result:
case intro.intro.intro
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{u_4, u_1} C
inst✝¹⁰ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ :
  (MorphismProperty.RightFraction.mk α.s ⋯ T₂.mor₁).f ≫ β.s = (MorphismProperty.RightFraction.mk α.s ⋯ T₂.mor₁).s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
⊢ ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{u_4, u_1} C
inst✝¹⁰ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
this✝¹ : IsIso (L.map β.s)
this✝ : IsIso (L.map γ.s)
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
hT₃ : T₃ ∈ distinguishedTriangles
hβγσ : W (β.s ≫ γ.s ≫ σ)
ψ₃ : T₂.obj₃ ⟶ T₃.obj₃
hψ₃ : W ψ₃
hψ₁ : T₂.mor₂ ≫ ψ₃ = (β.s ≫ γ.s ≫ σ) ≫ T₃.mor₂
hψ₂ : T₂.mor₃ ≫ (shiftFunctor C 1).map α.s = ψ₃ ≫ T₃.mor₃
ψ : T₂ ⟶ T₃ := T₂.homMk T₃ α.s (β.s ≫ γ.s ≫ σ) ψ₃ ⋯ hψ₁ hψ₂
this : IsIso (L.mapTriangle.map ψ)
⊢ L.map (γ.f ≫ σ) = b ≫ L.map (β.s ≫ γ.s ≫ σ)

Tactic:
simp only [Functor.map_comp, reassoc_of% hγ,
  MorphismProperty.LeftFraction.map_comp_map_s_assoc]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{u_4, u_1} C
inst✝¹⁰ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
this✝ : IsIso (L.map β.s)
this : IsIso (L.map γ.s)
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
hT₃ : T₃ ∈ distinguishedTriangles
⊢ ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b

Tactic:
have hβγσ : W (β.s ≫ γ.s ≫ σ) := W.comp_mem _ _ β.hs (W.comp_mem _ _ γ.hs hσ)

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{u_4, u_1} C
inst✝¹⁰ : Category.{u_3, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
fac✝ : L.map T₁.mor₁ ≫ b = a ≫ L.map T₂.mor₁
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
hγ : b ≫ L.map β.s = γ.map L ⋯
this✝ : IsIso (L.map β.s)
this : IsIso (L.map γ.s)
Z₂ : C
σ : γ.Y' ⟶ Z₂
hσ : W σ
fac : α.f ≫ β.f ≫ γ.s ≫ σ = T₁.mor₁ ≫ γ.f ≫ σ
Y₃ : C
g : Z₂ ⟶ Y₃
h : Y₃ ⟶ (shiftFunctor C 1).obj α.Y'
T₃ : Triangle C := Triangle.mk (β.f ≫ γ.s ≫ σ) g h
hT₃ : T₃ ∈ distinguishedTriangles
hβγσ : W (β.s ≫ γ.s ≫ σ)
⊢ ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b