-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
@[reassoc]
lemma add_comp (f₁ f₂ : X' ⟶ Y') (g : Y' ⟶ Z') :
    add W eX eY f₁ f₂ ≫ g = add W eX eZ (f₁ ≫ g) (f₂ ≫ g)

Proof state:
case intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
f₂ : X' ⟶ Y'
g : Y' ⟶ Z'
f₁ : L.obj X ⟶ L.obj Y
⊢ add W eX eY ((homEquiv eX eY).symm f₁) f₂ ≫ g = add W eX eZ ((homEquiv eX eY).symm f₁ ≫ g) (f₂ ≫ g)

Tactic:
obtain ⟨f₂, rfl⟩ := (homEquiv eX eY).symm.surjective f₂

Result:
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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
g : Y' ⟶ Z'
f₁ f₂ : L.obj X ⟶ L.obj Y
⊢ add W eX eY ((homEquiv eX eY).symm f₁) ((homEquiv eX eY).symm f₂) ≫ g =
    add W eX eZ ((homEquiv eX eY).symm f₁ ≫ g) ((homEquiv eX eY).symm f₂ ≫ g)

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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
g : Y' ⟶ Z'
f₁ f₂ : L.obj X ⟶ L.obj Y
⊢ add W eX eY ((homEquiv eX eY).symm f₁) ((homEquiv eX eY).symm f₂) ≫ g =
    add W eX eZ ((homEquiv eX eY).symm f₁ ≫ g) ((homEquiv eX eY).symm f₂ ≫ g)

Tactic:
obtain ⟨g, rfl⟩ := (homEquiv eY eZ).symm.surjective g

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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
⊢ add W eX eY ((homEquiv eX eY).symm f₁) ((homEquiv eX eY).symm f₂) ≫ (homEquiv eY eZ).symm g =
    add W eX eZ ((homEquiv eX eY).symm f₁ ≫ (homEquiv eY eZ).symm g)
      ((homEquiv eX eY).symm f₂ ≫ (homEquiv eY eZ).symm g)

Proof state:
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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
⊢ add W eX eY ((homEquiv eX eY).symm f₁) ((homEquiv eX eY).symm f₂) ≫ (homEquiv eY eZ).symm g =
    add W eX eZ ((homEquiv eX eY).symm f₁ ≫ (homEquiv eY eZ).symm g)
      ((homEquiv eX eY).symm f₂ ≫ (homEquiv eY eZ).symm g)

Tactic:
simp [add]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
f₁ f₂ : X' ⟶ Y'
g : Y' ⟶ Z'
⊢ add W eX eY f₁ f₂ ≫ g = add W eX eZ (f₁ ≫ g) (f₂ ≫ g)

Tactic:
obtain ⟨f₁, rfl⟩ := (homEquiv eX eY).symm.surjective f₁

Result:
case intro
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_3, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
f₂ : X' ⟶ Y'
g : Y' ⟶ Z'
f₁ : L.obj X ⟶ L.obj Y
⊢ add W eX eY ((homEquiv eX eY).symm f₁) f₂ ≫ g = add W eX eZ ((homEquiv eX eY).symm f₁ ≫ g) (f₂ ≫ g)