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 Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
obtain :
  ∀ (β : W.LeftFraction₂ Y Z) (hβ₁ : g₁ = β.fst (W := W).map (W := W) L ⋯) (hβ₂ : g₂ = β.snd (W := W).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β₁, hβ₂⟩ := exists_leftFraction₂ L W g₁ 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 : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst (W := W).map (W := W) L ⋯
hβ₂ : g₂ = β.snd (W := W).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))).f (W := W) ≫ γ.s (W := W) =
        (RightFraction₂.mk (W := W) (α.s (W := W)) ⋯ (β.f (W := W)) (β.f' (W := W))).s (W := W) ≫ γ.f (W := W))
    (hγ₂ :
      (RightFraction₂.mk (W := W) (α.s (W := W)) ⋯ (β.f (W := W)) (β.f' (W := W))).f' (W := W) ≫ γ.s (W := W) =
        (RightFraction₂.mk (W := W) (α.s (W := W)) ⋯ (β.f (W := W)) (β.f' (W := W))).s (W := W) ≫ γ.f' (W := W)),
    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γ₁, hγ₂⟩ := (RightFraction₂.mk _ α.hs β.f β.f').exists_leftFraction₂

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.LeftFraction₂.f', CategoryTheory.MorphismProperty.RightFraction₂.mk, 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 : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst (W := W).map (W := W) L ⋯
hβ₂ : g₂ = β.snd (W := W).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γ₂ : β.f' (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f' (W := W)
⊢ 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:
simpa only [hα, hβ₁] using LeftFraction.map_comp_map_eq_map α β.fst γ.fst hγ₁ L

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂.fst, 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 : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst (W := W).map (W := W) L ⋯
hβ₂ : g₂ = β.snd (W := W).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γ₂ : β.f' (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f' (W := W)
⊢ 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:
simpa only [hα, hβ₂] using LeftFraction.map_comp_map_eq_map α β.snd γ.snd hγ₂ L

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂.snd, 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 : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst (W := W).map (W := W) L ⋯
hβ₂ : g₂ = β.snd (W := W).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γ₂ : β.f' (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f' (W := W)
⊢ β.add (W := W).f (W := W) ≫ γ.add (W := W).s (W := W) = α.s (W := W) ≫ γ.add (W := W).f (W := W)

Tactic:
simp only [add_comp, hγ₁, hγ₂, comp_add]

Premises used: CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_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 : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst (W := W).map (W := W) L ⋯
hβ₂ : g₂ = β.snd (W := W).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γ₂ : β.f' (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f' (W := W)
rw :
  (α.comp₀ (W := W) (β.add (W := W)) (γ.add (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 ⋯
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)

Tactic:
rw [add'_eq W g₁ g₂ β hβ₁ hβ₂, add'_eq W (f ≫ g₁) (f ≫ g₂)
    (LeftFraction₂.mk (α.f ≫ γ.f) (α.f ≫ γ.f') (β.s ≫ γ.s) (W.comp_mem _ _ β.hs γ.hs))
    (by simpa only [hα, hβ₁] using LeftFraction.map_comp_map_eq_map α β.fst γ.fst hγ₁ L)
    (by simpa only [hα, hβ₂] using LeftFraction.map_comp_map_eq_map α β.snd γ.snd hγ₂ L),
    hα, LeftFraction.map_comp_map_eq_map α β.add γ.add
      (by simp only [add_comp, hγ₁, hγ₂, comp_add])]

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂.add, CategoryTheory.MorphismProperty.LeftFraction₂.s, CategoryTheory.Localization.Preadditive.add'_eq, CategoryTheory.MorphismProperty.LeftFraction₂.f', CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.LeftFraction₂.hs, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_eq_map, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.LeftFraction.f, 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 : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst (W := W).map (W := W) L ⋯
hβ₂ : g₂ = β.snd (W := W).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γ₂ : β.f' (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f' (W := W)
dsimp :
  LeftFraction.map (W := W)
      (LeftFraction.mk (W := W) (α.f (W := W) ≫ (γ.f (W := W) + γ.f' (W := W))) (β.s (W := W) ≫ γ.s (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 ⋯
⊢ (α.comp₀ (W := W) (β.add (W := W)) (γ.add (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 : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst (W := W).map (W := W) L ⋯
hβ₂ : g₂ = β.snd (W := W).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γ₂ : β.f' (W := W) ≫ γ.s (W := W) = α.s (W := W) ≫ γ.f' (W := W)
rw rw₁ :
  LeftFraction.map (W := W)
      (LeftFraction.mk (W := W) (α.f (W := W) ≫ γ.f (W := W) + α.f (W := W) ≫ γ.f' (W := W))
        (β.s (W := W) ≫ γ.s (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.map (W := W)
      (LeftFraction.mk (W := W) (α.f (W := W) ≫ (γ.f (W := W) + γ.f' (W := W))) (β.s (W := W) ≫ γ.s (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 [comp_add]

Premises used: CategoryTheory.Preadditive.comp_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₂ : X ⟶ Y
⊢ add' W (L.map f₁) (L.map f₂) = L.map (f₁ + f₂)

Tactic:
(add'_eq W (L.map f₁) (L.map f₂) (LeftFraction₂.mk f₁ f₂ (𝟙 _) (W.id_mem _))
    (LeftFraction.map_ofHom _ _ _ _).symm (LeftFraction.map_ofHom _ _ _ _).symm).trans
    (LeftFraction.map_ofHom _ _ _ _)

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map_ofHom, CategoryTheory.Localization.Preadditive.add'_eq, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, CategoryTheory.MorphismProperty.id_mem, CategoryTheory.MorphismProperty.LeftFraction₂.mk, Eq.symm, Eq.trans
-- 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
this_1 : Zero (L.obj X ⟶ L.obj Y) := { zero := L.map 0 }
this_2 : Add (L.obj X ⟶ L.obj Y) := { add := add' W }
this : Neg (L.obj X ⟶ L.obj Y) := { neg := neg' W }
⊢ AddCommGroup (L.obj X ⟶ L.obj Y)

Tactic:
exact
    { add_assoc := add'_assoc _
      add_zero := add'_zero _
      add_comm := add'_comm _
      zero_add := zero_add' _
      neg_add_cancel := neg'_add'_self _
      nsmul := nsmulRec
      zsmul := zsmulRec }
-- 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
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
x : X' ⟶ Y'
⊢ (fun (g : L.obj X ⟶ L.obj Y) ↦ eX.inv ≫ g ≫ eY.hom) ((fun (f : X' ⟶ Y') ↦ eX.hom ≫ f ≫ eY.inv) x) = x

Tactic:
simp
-- 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
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
x : L.obj X ⟶ L.obj Y
⊢ (fun (f : X' ⟶ Y') ↦ eX.hom ≫ f ≫ eY.inv) ((fun (g : L.obj X ⟶ L.obj Y) ↦ eX.inv ≫ g ≫ eY.hom) x) = x

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

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

Premises used: CategoryTheory.Localization.Preadditive.homEquiv, Equiv.surjective, Equiv.symm, 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 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 : L.obj Y ⟶ L.obj Z
⊢ add W eX eY f₁ f₂ ≫ ((homEquiv eY eZ).symm : (a : L.obj Y ⟶ L.obj Z) → Y' ⟶ Z') g =
    add W eX eZ (f₁ ≫ ((homEquiv eY eZ).symm : (a : L.obj Y ⟶ L.obj Z) → Y' ⟶ Z') g)
      (f₂ ≫ ((homEquiv eY eZ).symm : (a : L.obj Y ⟶ L.obj Z) → Y' ⟶ Z') g)

Tactic:
simp [add]

Premises used: CategoryTheory.Localization.Preadditive.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
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'
obtain :
  ∀ (f : L.obj X ⟶ L.obj Y),
    ((homEquiv eX eY).symm : (a : L.obj X ⟶ L.obj Y) → X' ⟶ Y') f ≫ add W eY eZ g₁ g₂ =
      add W eX eZ (((homEquiv eX eY).symm : (a : L.obj X ⟶ L.obj Y) → X' ⟶ Y') f ≫ g₁)
        (((homEquiv eX eY).symm : (a : L.obj X ⟶ L.obj Y) → X' ⟶ Y') f ≫ g₂)
⊢ 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

Premises used: CategoryTheory.Localization.Preadditive.homEquiv, Equiv.surjective, Equiv.symm, 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 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 : (a : L.obj X ⟶ L.obj Y) → X' ⟶ Y') f ≫ add W eY eZ g₁ g₂ =
    add W eX eZ (((homEquiv eX eY).symm : (a : L.obj X ⟶ L.obj Y) → X' ⟶ Y') f ≫ g₁)
      (((homEquiv eX eY).symm : (a : L.obj X ⟶ L.obj Y) → X' ⟶ Y') f ≫ g₂)

Tactic:
simp [add]

Premises used: CategoryTheory.Localization.Preadditive.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
X' Y' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
X'' Y'' : C
eX' : L.obj X'' ≅ X'
eY' : L.obj Y'' ≅ Y'
f₁ f₂ : X' ⟶ Y'
⊢ 𝟙 X' ≫ add W eX eY f₁ f₂ = add W eX' eY (𝟙 X' ≫ f₁) (𝟙 X' ≫ f₂)

Tactic:
have h₁ := comp_add W eX' eX eY (𝟙 _) f₁ 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 : C
X' Y' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
X'' Y'' : C
eX' : L.obj X'' ≅ X'
eY' : L.obj Y'' ≅ Y'
f₁ f₂ : X' ⟶ Y'
h₁ : 𝟙 X' ≫ add W eX eY f₁ f₂ = add W eX' eY (𝟙 X' ≫ f₁) (𝟙 X' ≫ f₂)
⊢ add W eX' eY f₁ f₂ ≫ 𝟙 Y' = add W eX' eY' (f₁ ≫ 𝟙 Y') (f₂ ≫ 𝟙 Y')

Tactic:
have h₂ := add_comp W eX' eY eY' f₁ 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 : C
X' Y' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
X'' Y'' : C
eX' : L.obj X'' ≅ X'
eY' : L.obj Y'' ≅ Y'
f₁ f₂ : X' ⟶ Y'
h₁ : 𝟙 X' ≫ add W eX eY f₁ f₂ = add W eX' eY (𝟙 X' ≫ f₁) (𝟙 X' ≫ f₂)
h₂ : add W eX' eY f₁ f₂ ≫ 𝟙 Y' = add W eX' eY' (f₁ ≫ 𝟙 Y') (f₂ ≫ 𝟙 Y')
⊢ add W eX eY f₁ f₂ = add W eX' eY f₁ f₂

Tactic:
simp only [id_comp] at h₁

Premises used: CategoryTheory.Category.id_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
X' Y' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
X'' Y'' : C
eX' : L.obj X'' ≅ X'
eY' : L.obj Y'' ≅ Y'
f₁ f₂ : X' ⟶ Y'
h₂ : add W eX' eY f₁ f₂ ≫ 𝟙 Y' = add W eX' eY' (f₁ ≫ 𝟙 Y') (f₂ ≫ 𝟙 Y')
h₁ : add W eX eY f₁ f₂ = add W eX' eY f₁ f₂
⊢ add W eX' eY f₁ f₂ = add W eX' eY' f₁ f₂

Tactic:
simp only [comp_id] at h₂

Premises used: CategoryTheory.Category.comp_id
-- 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
X' Y' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
X'' Y'' : C
eX' : L.obj X'' ≅ X'
eY' : L.obj Y'' ≅ Y'
f₁ f₂ : X' ⟶ Y'
h₁ : add W eX eY f₁ f₂ = add W eX' eY f₁ f₂
h₂ : add W eX' eY f₁ f₂ = add W eX' eY' f₁ f₂
rw : add W eX' eY f₁ f₂ = add W eX' eY' f₁ f₂
rw₁ rw₂ : add W eX' eY' f₁ f₂ = add W eX' eY' f₁ f₂
⊢ add W eX eY f₁ f₂ = add W eX' eY' f₁ f₂

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
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
⊢ L.EssSurj

Tactic:
have := Localization.essSurj L W
-- 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
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
this_1 : L.EssSurj
this : AddCommGroup (L.obj (L.objPreimage X') ⟶ L.obj (L.objPreimage Y')) :=
  addCommGroup' L W (L.objPreimage X') (L.objPreimage Y')
⊢ AddCommGroup (X' ⟶ Y')

Tactic:
exact Equiv.addCommGroup (homEquiv (L.objObjPreimageIso X') (L.objObjPreimageIso Y'))

Premises used: CategoryTheory.Localization.Preadditive.homEquiv, Equiv.addCommGroup, CategoryTheory.Functor.objObjPreimageIso
-- 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
X' Y' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
f₁ f₂ : X' ⟶ Y'
⊢ f₁ + f₂ = add W eX eY f₁ f₂

Tactic:
apply add_eq_add

Premises used: CategoryTheory.Localization.Preadditive.add_eq_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₂ : X ⟶ Y
rw : L.map (f₁ + f₂) = add W (Iso.refl (L.obj X)) (Iso.refl (L.obj Y)) (L.map f₁) (L.map f₂)
⊢ L.map (f₁ + f₂) = L.map f₁ + L.map f₂

Tactic:
rw [add_eq W (Iso.refl _) (Iso.refl _) (L.map f₁) (L.map f₂)]

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Functor.map, CategoryTheory.Localization.Preadditive.add_eq
-- 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₂ : X ⟶ Y
⊢ L.map (f₁ + f₂) = add W (Iso.refl (L.obj X)) (Iso.refl (L.obj Y)) (L.map f₁) (L.map f₂)

Tactic:
simp [add]

Premises used: CategoryTheory.Localization.Preadditive.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 x_1 x_2 : D
x_3 x_4 : x ⟶ x_1
x_5 : x_1 ⟶ x_2
⊢ (x_3 + x_4) ≫ x_5 = x_3 ≫ x_5 + x_4 ≫ x_5

Tactic:
apply Preadditive.add_comp

Premises used: CategoryTheory.Localization.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 x_1 x_2 : D
x_3 : x ⟶ x_1
x_4 x_5 : x_1 ⟶ x_2
⊢ x_3 ≫ (x_4 + x_5) = x_3 ≫ x_4 + x_3 ≫ x_5

Tactic:
apply Preadditive.comp_add

Premises used: CategoryTheory.Localization.Preadditive.comp_add