-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/Preadditive.lean
@[reassoc (attr := simp)]
lemma add'_comp (f₁ f₂ : L.obj X ⟶ L.obj Y) (g : L.obj Y ⟶ L.obj Z) :
    add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)

Proof state:
case 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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.f ≫ γ.s = α.s ≫ γ.f
⊢ (LeftFraction.mk ((α.f + α.f') ≫ γ.f) (β.s ≫ γ.s) ⋯).map L ⋯ =
    (LeftFraction.mk (α.f ≫ γ.f + α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).map L ⋯

Tactic:
rw [add_comp]

Result:
no goals

Proof state:
case 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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.f ≫ γ.s = α.s ≫ γ.f
⊢ add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)

Tactic:
rw [add'_eq W f₁ f₂ α h₁ h₂, add'_eq W (f₁ ≫ g) (f₂ ≫ g)
  (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s)
  (W.comp_mem _ _ β.hs γ.hs))]

Result:
case 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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.f ≫ γ.s = α.s ≫ γ.f
⊢ α.add.map L ⋯ ≫ g = (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).add.map L ⋯

case intro.intro.intro.intro.hφ₁
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
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.f ≫ γ.s = α.s ≫ γ.f
⊢ f₁ ≫ g = (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).fst.map L ⋯

case intro.intro.intro.intro.hφ₂
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
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.f ≫ γ.s = α.s ≫ γ.f
⊢ f₂ ≫ g = (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).snd.map L ⋯

Proof state:
case 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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.f ≫ γ.s = α.s ≫ γ.f
⊢ α.add.map L ⋯ ≫ g = (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).add.map L ⋯

Tactic:
rw [hβ, LeftFraction.map_comp_map_eq_map _ _ γ hγ]

Result:
case 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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.f ≫ γ.s = α.s ≫ γ.f
⊢ (α.add.comp₀ β γ).map L ⋯ = (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).add.map L ⋯

Proof state:
case 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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.f ≫ γ.s = α.s ≫ γ.f
⊢ (α.add.comp₀ β γ).map L ⋯ = (LeftFraction₂.mk (α.f ≫ γ.f) (α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).add.map L ⋯

Tactic:
dsimp [LeftFraction₂.add]

Result:
case 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
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.f ≫ γ.s = α.s ≫ γ.f
⊢ (LeftFraction.mk ((α.f + α.f') ≫ γ.f) (β.s ≫ γ.s) ⋯).map L ⋯ =
    (LeftFraction.mk (α.f ≫ γ.f + α.f' ≫ γ.f) (β.s ≫ γ.s) ⋯).map L ⋯

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

Tactic:
obtain ⟨α, h₁, h₂⟩ := exists_leftFraction₂ L W f₁ 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
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
⊢ add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)