awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
rw :
  L.map 0 ≫ L.map (α.s (W := W)) =
    (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).map (W := W) L ⋯ ≫ L.map (α.s (W := W))
rw₁ :
  L.map (0 ≫ α.s (W := W)) =
    (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).map (W := W) L ⋯ ≫ L.map (α.s (W := W))
rw₂ :
  L.map 0 =
    (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).map (W := W) L ⋯ ≫ L.map (α.s (W := W))
rw₃ rw₄ : L.map 0 = L.map ((LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).f (W := W))
⊢ L.map 0 = (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).map (W := W) L ⋯

Tactic:
rw [← cancel_mono (L.map α.s), ← L.map_comp, Limits.zero_comp,
      LeftFraction.map_comp_map_s]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
dsimp : (LeftFraction.mk (W := W) (α.f (W := W) + 0) (α.s (W := W)) ⋯).map (W := W) L ⋯ = α.map (W := W) L ⋯
⊢ (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).add (W := W).map (W := W) L ⋯ = α.map (W := W) L ⋯

Tactic:
dsimp [LeftFraction₂.add]

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂.add
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
rw rw₁ : (LeftFraction.mk (W := W) (α.f (W := W)) (α.s (W := W)) ⋯).map (W := W) L ⋯ = α.map (W := W) L ⋯
⊢ (LeftFraction.mk (W := W) (α.f (W := W) + 0) (α.s (W := W)) ⋯).map (W := W) L ⋯ = α.map (W := W) L ⋯

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
rw : add' W f (L.map 0) = f
rw₁ rw₂ : f = f
⊢ add' W (L.map 0) f = f

Tactic:
rw [add'_comm, add'_zero]

Premises used: CategoryTheory.Localization.Preadditive.add'_comm, CategoryTheory.Localization.Preadditive.add'_zero
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ f₃ : L.obj X ⟶ L.obj Y
obtain :
  ∀ (α : W.LeftFraction₃ X Y) (h₁ : f₁ = α.fst (W := W).map (W := W) L ⋯) (h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯)
    (h₃ : f₃ = α.thd (W := W).map (W := W) L ⋯), add' W (add' W f₁ f₂) f₃ = add' W f₁ (add' W f₂ f₃)
⊢ add' W (add' W f₁ f₂) f₃ = add' W f₁ (add' W f₂ f₃)

Tactic:
obtain ⟨α, h₁, h₂, h₃⟩ := exists_leftFraction₃ L W f₁ f₂ f₃

Premises used: CategoryTheory.Localization.exists_leftFraction₃
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ f₃ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₃ X Y
h₁ : f₁ = α.fst (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
h₃ : f₃ = α.thd (W := W).map (W := W) L ⋯
rw :
  (LeftFraction₂.mk (W := W) (α.f (W := W) + α.f' (W := W)) (α.f'' (W := W)) (α.s (W := W)) ⋯).add (W := W).map (W := W)
      L ⋯ =
    (LeftFraction₂.mk (W := W) (α.f (W := W)) (α.f' (W := W) + α.f'' (W := W)) (α.s (W := W)) ⋯).add (W := W).map (W :=
      W) L ⋯
⊢ add' W (add' W f₁ f₂) f₃ = add' W f₁ (add' W f₂ f₃)

Tactic:
rw [add'_eq W f₁ f₂ α.forgetThd h₁ h₂, add'_eq W f₂ f₃ α.forgetFst h₂ h₃,
    add'_eq W _ _ (LeftFraction₂.mk (α.f + α.f') α.f'' α.s α.hs) rfl h₃,
    add'_eq W _ _ (LeftFraction₂.mk α.f (α.f' + α.f'') α.s α.hs) h₁ rfl]

Premises used: CategoryTheory.MorphismProperty.LeftFraction₃.s, CategoryTheory.Localization.Preadditive.add'_eq, CategoryTheory.MorphismProperty.LeftFraction₃.hs, HAdd.hAdd, CategoryTheory.MorphismProperty.LeftFraction₃.forgetFst, CategoryTheory.MorphismProperty.LeftFraction₃.forgetThd, CategoryTheory.MorphismProperty.LeftFraction₃.f, CategoryTheory.MorphismProperty.LeftFraction₂.mk, CategoryTheory.MorphismProperty.LeftFraction₃.f'', CategoryTheory.MorphismProperty.LeftFraction₃.f', rfl
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ f₃ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₃ X Y
h₁ : f₁ = α.fst (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
h₃ : f₃ = α.thd (W := W).map (W := W) L ⋯
dsimp :
  (LeftFraction.mk (W := W) (α.f (W := W) + α.f' (W := W) + α.f'' (W := W)) (α.s (W := W)) ⋯).map (W := W) L ⋯ =
    (LeftFraction.mk (W := W) (α.f (W := W) + (α.f' (W := W) + α.f'' (W := W))) (α.s (W := W)) ⋯).map (W := W) L ⋯
⊢ (LeftFraction₂.mk (W := W) (α.f (W := W) + α.f' (W := W)) (α.f'' (W := W)) (α.s (W := W)) ⋯).add (W := W).map (W := W)
      L ⋯ =
    (LeftFraction₂.mk (W := W) (α.f (W := W)) (α.f' (W := W) + α.f'' (W := W)) (α.s (W := W)) ⋯).add (W := W).map (W :=
      W) L ⋯

Tactic:
dsimp [LeftFraction₂.add]

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂.add
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ f₃ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₃ X Y
h₁ : f₁ = α.fst (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
h₃ : f₃ = α.thd (W := W).map (W := W) L ⋯
rw rw₁ :
  (LeftFraction.mk (W := W) (α.f (W := W) + (α.f' (W := W) + α.f'' (W := W))) (α.s (W := W)) ⋯).map (W := W) L ⋯ =
    (LeftFraction.mk (W := W) (α.f (W := W) + (α.f' (W := W) + α.f'' (W := W))) (α.s (W := W)) ⋯).map (W := W) L ⋯
⊢ (LeftFraction.mk (W := W) (α.f (W := W) + α.f' (W := W) + α.f'' (W := W)) (α.s (W := W)) ⋯).map (W := W) L ⋯ =
    (LeftFraction.mk (W := W) (α.f (W := W) + (α.f' (W := W) + α.f'' (W := W))) (α.s (W := W)) ⋯).map (W := W) L ⋯

Tactic:
rw [add_assoc]

Premises used: add_assoc
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
obtain :
  ∀ (α : W.LeftFraction₂ X Y) (h₁ : f₁ = α.fst (W := W).map (W := W) L ⋯) (h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯),
    add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
⊢ add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)

Tactic:
obtain ⟨α, h₁, h₂⟩ := exists_leftFraction₂ L W f₁ f₂

Premises used: CategoryTheory.Localization.exists_leftFraction₂
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : 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 (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
obtain : ∀ (β : W.LeftFraction Y Z) (hβ : g = β.map (W := W) L ⋯), add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
⊢ add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)

Tactic:
obtain ⟨β, hβ⟩ := exists_leftFraction L W g

Premises used: CategoryTheory.Localization.exists_leftFraction
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : 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 (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map (W := W) L ⋯
obtain :
  ∀ (γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W)))
    (hγ :
      (RightFraction.mk (W := W) (α.s (W := W)) ⋯ (β.f (W := W))).f (W := W) ≫ γ.s (W := W) =
        (RightFraction.mk (W := W) (α.s (W := W)) ⋯ (β.f (W := W))).s (W := W) ≫ γ.f (W := W)),
    add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
⊢ add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)

Tactic:
obtain ⟨γ, hγ⟩ := (RightFraction.mk _ α.hs β.f).exists_leftFraction

Premises used: CategoryTheory.MorphismProperty.RightFraction.mk, CategoryTheory.MorphismProperty.LeftFraction₂.hs, CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction, CategoryTheory.MorphismProperty.LeftFraction.f
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : 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 (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.f (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
rw :
  α.add (W := W).map (W := W) L ⋯ ≫ g =
    (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W))
              (β.s (W := W) ≫ γ.s (W := W)) ⋯).add
          (W := W).map
      (W := W) L ⋯
hφ₁ :
  f₁ ≫ g =
    (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W))
              (β.s (W := W) ≫ γ.s (W := W)) ⋯).fst
          (W := W).map
      (W := W) L ⋯
hφ₂ :
  f₂ ≫ g =
    (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W))
              (β.s (W := W) ≫ γ.s (W := W)) ⋯).snd
          (W := W).map
      (W := W) L ⋯
⊢ 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))]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.Localization.Preadditive.add'_eq, CategoryTheory.MorphismProperty.LeftFraction₂.f', CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.LeftFraction.f, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.LeftFraction₂.f, CategoryTheory.MorphismProperty.LeftFraction₂.mk
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : 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 (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.f (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
hφ₁ :
  α.fst (W := W).map (W := W) L ⋯ ≫ β.map (W := W) L ⋯ =
    (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W))
              (β.s (W := W) ≫ γ.s (W := W)) ⋯).fst
          (W := W).map
      (W := W) L ⋯
⊢ f₁ ≫ g =
    (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W))
              (β.s (W := W) ≫ γ.s (W := W)) ⋯).fst
          (W := W).map
      (W := W) L ⋯

Tactic:
rw [h₁, hβ]
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : 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 (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.f (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
⊢ α.fst (W := W).map (W := W) L ⋯ ≫ β.map (W := W) L ⋯ =
    (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W))
              (β.s (W := W) ≫ γ.s (W := W)) ⋯).fst
          (W := W).map
      (W := W) L ⋯

Tactic:
LeftFraction.map_comp_map_eq_map _ _ _ hγ _

Premises used: CategoryTheory.MorphismProperty.LeftFraction.comp₀, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_eq_map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : 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 (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.f (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
⊢ α.fst (W := W).map (W := W) L ⋯ ≫ β.map (W := W) L ⋯ =
    (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W))
              (β.s (W := W) ≫ γ.s (W := W)) ⋯).fst
          (W := W).map
      (W := W) L ⋯

Tactic:
exact LeftFraction.map_comp_map_eq_map _ _ _ hγ _

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_eq_map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : 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 (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.f (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
hφ₂ :
  α.snd (W := W).map (W := W) L ⋯ ≫ β.map (W := W) L ⋯ =
    (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W))
              (β.s (W := W) ≫ γ.s (W := W)) ⋯).snd
          (W := W).map
      (W := W) L ⋯
⊢ f₂ ≫ g =
    (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W))
              (β.s (W := W) ≫ γ.s (W := W)) ⋯).snd
          (W := W).map
      (W := W) L ⋯

Tactic:
rw [h₂, hβ]
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : 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 (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.f (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
⊢ α.snd (W := W).map (W := W) L ⋯ ≫ β.map (W := W) L ⋯ =
    (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W))
              (β.s (W := W) ≫ γ.s (W := W)) ⋯).snd
          (W := W).map
      (W := W) L ⋯

Tactic:
LeftFraction.map_comp_map_eq_map _ _ _ hγ _

Premises used: CategoryTheory.MorphismProperty.LeftFraction.comp₀, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_eq_map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : 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 (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.f (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
⊢ α.snd (W := W).map (W := W) L ⋯ ≫ β.map (W := W) L ⋯ =
    (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W))
              (β.s (W := W) ≫ γ.s (W := W)) ⋯).snd
          (W := W).map
      (W := W) L ⋯

Tactic:
exact LeftFraction.map_comp_map_eq_map _ _ _ hγ _

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_eq_map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : 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 (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.f (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
rw :
  (α.add (W := W).comp₀ (W := W) β γ).map (W := W) L ⋯ =
    (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W))
              (β.s (W := W) ≫ γ.s (W := W)) ⋯).add
          (W := W).map
      (W := W) L ⋯
⊢ α.add (W := W).map (W := W) L ⋯ ≫ g =
    (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W))
              (β.s (W := W) ≫ γ.s (W := W)) ⋯).add
          (W := W).map
      (W := W) L ⋯

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

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_eq_map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : 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 (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.f (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
dsimp :
  (LeftFraction.mk (W := W) ((α.f (W := W) + α.f' (W := W)) ≫ γ.f (W := W)) (β.s (W := W) ≫ γ.s (W := W)) ⋯).map (W :=
      W) L ⋯ =
    (LeftFraction.mk (W := W) (α.f (W := W) ≫ γ.f (W := W) + α.f' (W := W) ≫ γ.f (W := W)) (β.s (W := W) ≫ γ.s (W := W))
          ⋯).map
      (W := W) L ⋯
⊢ (α.add (W := W).comp₀ (W := W) β γ).map (W := W) L ⋯ =
    (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W))
              (β.s (W := W) ≫ γ.s (W := W)) ⋯).add
          (W := W).map
      (W := W) L ⋯

Tactic:
dsimp [LeftFraction₂.add]

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂.add
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : 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 (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map (W := W) L ⋯
γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W))
hγ : β.f (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f (W := W)
rw rw₁ :
  (LeftFraction.mk (W := W) (α.f (W := W) ≫ γ.f (W := W) + α.f' (W := W) ≫ γ.f (W := W)) (β.s (W := W) ≫ γ.s (W := W))
          ⋯).map
      (W := W) L ⋯ =
    (LeftFraction.mk (W := W) (α.f (W := W) ≫ γ.f (W := W) + α.f' (W := W) ≫ γ.f (W := W)) (β.s (W := W) ≫ γ.s (W := W))
          ⋯).map
      (W := W) L ⋯
⊢ (LeftFraction.mk (W := W) ((α.f (W := W) + α.f' (W := W)) ≫ γ.f (W := W)) (β.s (W := W) ≫ γ.s (W := W)) ⋯).map (W :=
      W) L ⋯ =
    (LeftFraction.mk (W := W) (α.f (W := W) ≫ γ.f (W := W) + α.f' (W := W) ≫ γ.f (W := W)) (β.s (W := W) ≫ γ.s (W := W))
          ⋯).map
      (W := W) L ⋯

Tactic:
rw [add_comp]

Premises used: CategoryTheory.Preadditive.add_comp
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : W.HasLeftCalculusOfFractions
X Y Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
obtain : ∀ (α : W.LeftFraction X Y) (hα : f = α.map (W := W) L ⋯), f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)

Tactic:
obtain ⟨α, hα⟩ := exists_leftFraction L W f

Premises used: CategoryTheory.Localization.exists_leftFraction