-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
@[reassoc]
lemma comp_add (f : X' ⟶ Y') (g₁ g₂ : Y' ⟶ Z') :
    f ≫ add W eY eZ g₁ g₂ = add W eX eZ (f ≫ g₁) (f ≫ 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 : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
⊢ (homEquiv eX eY).symm f ≫ add W eY eZ ((homEquiv eY eZ).symm g₁) ((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:
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'
g₁ g₂ : Y' ⟶ Z'
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv eX eY).symm f ≫ add W eY eZ g₁ 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
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 : L.obj X ⟶ L.obj Y
g₁ : L.obj Y ⟶ L.obj Z
⊢ (homEquiv eX eY).symm f ≫ add W eY eZ ((homEquiv eY eZ).symm g₁) g₂ =
    add W eX eZ ((homEquiv eX eY).symm f ≫ (homEquiv eY eZ).symm g₁) ((homEquiv eX eY).symm f ≫ g₂)

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 : X' ⟶ Y'
g₁ g₂ : Y' ⟶ Z'
⊢ f ≫ add W eY eZ g₁ 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'
g₁ g₂ : Y' ⟶ Z'
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv eX eY).symm f ≫ add W eY eZ g₁ 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 : L.obj X ⟶ L.obj Y
g₁ : L.obj Y ⟶ L.obj Z
⊢ (homEquiv eX eY).symm f ≫ add W eY eZ ((homEquiv eY eZ).symm g₁) g₂ =
    add W eX eZ ((homEquiv eX eY).symm f ≫ (homEquiv eY eZ).symm 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 : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
⊢ (homEquiv eX eY).symm f ≫ add W eY eZ ((homEquiv eY eZ).symm g₁) ((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₂)