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
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.LeftFraction₂ X Y
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : W.IsInvertedBy F
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : F.Additive
this : IsIso (F.map (φ.s (W := W)))
rw :
  φ.add (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) =
    (φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF) ≫ F.map (φ.s (W := W))
rw₁ :
  φ.add (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) =
    φ.fst (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
rw₂ :
  F.map (φ.add (W := W).f (W := W)) =
    φ.fst (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
rw₃ :
  F.map (φ.add (W := W).f (W := W)) =
    F.map (φ.fst (W := W).f (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
rw₄ : F.map (φ.add (W := W).f (W := W)) = F.map (φ.fst (W := W).f (W := W)) + F.map (φ.snd (W := W).f (W := W))
rw₅ rw₆ :
  F.map (φ.f (W := W)) + F.map (φ.f' (W := W)) = F.map (φ.fst (W := W).f (W := W)) + F.map (φ.snd (W := W).f (W := W))
⊢ φ.add (W := W).map (W := W) F hF = φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF

Tactic:
rw [← cancel_mono (F.map φ.s), add_comp, LeftFraction.map_comp_map_s,
    LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, F.map_add]

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂.s, CategoryTheory.Functor.map_add, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Preadditive.add_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s
-- 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 ⋯
⊢ ∃ (φ₀ : W.LeftFraction X Y) (_ : f = φ₀.map (W := W) L ⋯), neg' W f = φ₀.neg (W := W).map (W := W) L ⋯

Tactic:
⟨_, (exists_leftFraction L W f).choose_spec, rfl⟩

Premises used: Exists.choose_spec, CategoryTheory.Localization.exists_leftFraction, Exists.intro, 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 : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map (W := W) L ⋯
obtain :
  ∀ (φ₀ : W.LeftFraction X Y) (hφ : φ₀.map (W := W) L ⋯ = φ.map (W := W) L ⋯)
    (hφ₀ : neg' W (φ₀.map (W := W) L ⋯) = φ₀.neg (W := W).map (W := W) L ⋯),
    neg' W (φ₀.map (W := W) L ⋯) = φ.neg (W := W).map (W := W) L ⋯
⊢ neg' W f = φ.neg (W := W).map (W := W) L ⋯

Tactic:
obtain ⟨φ₀, rfl, hφ₀⟩ : ∃ (φ₀ : W.LeftFraction X Y)
    (_ : f = φ₀.map L (inverts L W)),
      neg' W f = φ₀.neg.map L (inverts L W) :=
    ⟨_, (exists_leftFraction L W f).choose_spec, rfl⟩

Premises used: CategoryTheory.MorphismProperty.LeftFraction, CategoryTheory.Localization.Preadditive.neg', 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
φ φ₀ : W.LeftFraction X Y
hφ : φ₀.map (W := W) L ⋯ = φ.map (W := W) L ⋯
hφ₀ : neg' W (φ₀.map (W := W) L ⋯) = φ₀.neg (W := W).map (W := W) L ⋯
⊢ LeftFractionRel (W := W) φ₀ φ

Tactic:
rw [MorphismProperty.LeftFraction.map_eq_iff] at hφ

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map_eq_iff
-- 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
φ φ₀ : W.LeftFraction X Y
hφ : φ₀.map (W := W) L ⋯ = φ.map (W := W) L ⋯
hφ₀ : neg' W (φ₀.map (W := W) L ⋯) = φ₀.neg (W := W).map (W := W) L ⋯
hφ₁ : LeftFractionRel (W := W) φ₀ φ
⊢ neg' W (φ₀.map (W := W) L ⋯) = φ₀.neg (W := W).map (W := W) L ⋯

Tactic:
rw [MorphismProperty.LeftFraction.map_eq_iff] at hφ

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map_eq_iff
-- 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
φ φ₀ : W.LeftFraction X Y
hφ : LeftFractionRel (W := W) φ₀ φ
hφ₀ : neg' W (φ₀.map (W := W) L ⋯) = φ₀.neg (W := W).map (W := W) L ⋯
obtain :
  ∀ (Y' : C) (t₁ : φ₀.Y' (W := W) ⟶ Y') (t₂ : φ.Y' (W := W) ⟶ Y') (hst : φ₀.s (W := W) ≫ t₁ = φ.s (W := W) ≫ t₂)
    (hft : φ₀.f (W := W) ≫ t₁ = φ.f (W := W) ≫ t₂) (ht : W (φ₀.s (W := W) ≫ t₁)),
    neg' W (φ₀.map (W := W) L ⋯) = φ.neg (W := W).map (W := W) L ⋯
⊢ neg' W (φ₀.map (W := W) L ⋯) = φ.neg (W := W).map (W := W) L ⋯

Tactic:
obtain ⟨Y', t₁, t₂, hst, hft, ht⟩ := 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 : C
φ φ₀ : W.LeftFraction X Y
hφ₀ : neg' W (φ₀.map (W := W) L ⋯) = φ₀.neg (W := W).map (W := W) L ⋯
Y' : C
t₁ : φ₀.Y' (W := W) ⟶ Y'
t₂ : φ.Y' (W := W) ⟶ Y'
hst : φ₀.s (W := W) ≫ t₁ = φ.s (W := W) ≫ t₂
hft : φ₀.f (W := W) ≫ t₁ = φ.f (W := W) ≫ t₂
ht : W (φ₀.s (W := W) ≫ t₁)
⊢ IsIso (L.map (φ₀.s (W := W) ≫ t₁))

Tactic:
have := inverts L W _ ht
-- 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
φ φ₀ : W.LeftFraction X Y
hφ₀ : neg' W (φ₀.map (W := W) L ⋯) = φ₀.neg (W := W).map (W := W) L ⋯
Y' : C
t₁ : φ₀.Y' (W := W) ⟶ Y'
t₂ : φ.Y' (W := W) ⟶ Y'
hst : φ₀.s (W := W) ≫ t₁ = φ.s (W := W) ≫ t₂
hft : φ₀.f (W := W) ≫ t₁ = φ.f (W := W) ≫ t₂
ht : W (φ₀.s (W := W) ≫ t₁)
this : IsIso (L.map (φ₀.s (W := W) ≫ t₁))
rw :
  neg' W (φ₀.map (W := W) L ⋯) ≫ L.map (φ₀.s (W := W) ≫ t₁) =
    φ.neg (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W) ≫ t₁)
⊢ neg' W (φ₀.map (W := W) L ⋯) = φ.neg (W := W).map (W := W) L ⋯

Tactic:
rw [← cancel_mono (L.map (φ₀.s ≫ t₁))]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.LeftFraction.s
-- 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
φ φ₀ : W.LeftFraction X Y
hφ₀ : neg' W (φ₀.map (W := W) L ⋯) = φ₀.neg (W := W).map (W := W) L ⋯
Y' : C
t₁ : φ₀.Y' (W := W) ⟶ Y'
t₂ : φ.Y' (W := W) ⟶ Y'
hst : φ₀.s (W := W) ≫ t₁ = φ.s (W := W) ≫ t₂
hft : φ₀.f (W := W) ≫ t₁ = φ.f (W := W) ≫ t₂
ht : W (φ₀.s (W := W) ≫ t₁)
this : IsIso (L.map (φ₀.s (W := W) ≫ t₁))
nth_rw :
  neg' W (φ₀.map (W := W) L ⋯) ≫ L.map (φ₀.s (W := W)) ≫ L.map t₁ =
    φ.neg (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W) ≫ t₁)
⊢ neg' W (φ₀.map (W := W) L ⋯) ≫ L.map (φ₀.s (W := W) ≫ t₁) =
    φ.neg (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W) ≫ t₁)

Tactic:
nth_rw 1 [L.map_comp]

Premises used: CategoryTheory.Functor.map_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
φ φ₀ : W.LeftFraction X Y
hφ₀ : neg' W (φ₀.map (W := W) L ⋯) = φ₀.neg (W := W).map (W := W) L ⋯
Y' : C
t₁ : φ₀.Y' (W := W) ⟶ Y'
t₂ : φ.Y' (W := W) ⟶ Y'
hst : φ₀.s (W := W) ≫ t₁ = φ.s (W := W) ≫ t₂
hft : φ₀.f (W := W) ≫ t₁ = φ.f (W := W) ≫ t₂
ht : W (φ₀.s (W := W) ≫ t₁)
this : IsIso (L.map (φ₀.s (W := W) ≫ t₁))
rw :
  φ₀.neg (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W)) ≫ L.map t₁ =
    φ.neg (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W) ≫ t₁)
rw₁ :
  φ₀.neg (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W)) ≫ L.map t₁ =
    φ.neg (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W) ≫ t₂)
rw₂ : L.map (φ₀.neg (W := W).f (W := W)) ≫ L.map t₁ = φ.neg (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W) ≫ t₂)
rw₃ : L.map (φ₀.neg (W := W).f (W := W)) ≫ L.map t₁ = φ.neg (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)) ≫ L.map t₂
rw₄ : L.map (φ₀.neg (W := W).f (W := W)) ≫ L.map t₁ = L.map (φ.neg (W := W).f (W := W)) ≫ L.map t₂
rw₅ : L.map (φ₀.neg (W := W).f (W := W) ≫ t₁) = L.map (φ.neg (W := W).f (W := W)) ≫ L.map t₂
rw₆ : L.map (φ₀.neg (W := W).f (W := W) ≫ t₁) = L.map (φ.neg (W := W).f (W := W) ≫ t₂)
rw₇ : L.map (-φ₀.f (W := W) ≫ t₁) = L.map (φ.neg (W := W).f (W := W) ≫ t₂)
rw₈ : L.map (-φ₀.f (W := W) ≫ t₁) = L.map (-φ.f (W := W) ≫ t₂)
rw₉ rw₁₀ : L.map (-φ.f (W := W) ≫ t₂) = L.map (-φ.f (W := W) ≫ t₂)
⊢ neg' W (φ₀.map (W := W) L ⋯) ≫ L.map (φ₀.s (W := W)) ≫ L.map t₁ =
    φ.neg (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W) ≫ t₁)

Tactic:
rw [hφ₀, hst, LeftFraction.map_comp_map_s_assoc, L.map_comp,
    LeftFraction.map_comp_map_s_assoc, ← L.map_comp, ← L.map_comp,
    neg_comp, neg_comp, hft]

Premises used: CategoryTheory.Preadditive.neg_comp, CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_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 : C
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 ⋯
⊢ ∃ (φ₀ : W.LeftFraction₂ X Y) (_ : f₁ = φ₀.fst (W := W).map (W := W) L ⋯) (_ : f₂ = φ₀.snd (W := W).map (W := W) L ⋯),
    add' W f₁ f₂ = φ₀.add (W := W).map (W := W) L ⋯

Tactic:
⟨(exists_leftFraction₂ L W f₁ f₂).choose,
      (exists_leftFraction₂ L W f₁ f₂).choose_spec.1,
      (exists_leftFraction₂ L W f₁ f₂).choose_spec.2, rfl⟩

Premises used: Exists.choose_spec, CategoryTheory.Localization.exists_leftFraction₂, And.right, And.left, Exists.intro, Exists.choose, 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₂ : 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 ⋯
obtain :
  ∀ (φ₀ : W.LeftFraction₂ X Y) (hφ₁ : φ₀.fst (W := W).map (W := W) L ⋯ = φ.fst (W := W).map (W := W) L ⋯)
    (hφ₂ : φ₀.snd (W := W).map (W := W) L ⋯ = φ.snd (W := W).map (W := W) L ⋯)
    (hφ₀ :
      add' W (φ₀.fst (W := W).map (W := W) L ⋯) (φ₀.snd (W := W).map (W := W) L ⋯) = φ₀.add (W := W).map (W := W) L ⋯),
    add' W (φ₀.fst (W := W).map (W := W) L ⋯) (φ₀.snd (W := W).map (W := W) L ⋯) = φ.add (W := W).map (W := W) L ⋯
⊢ add' W f₁ f₂ = φ.add (W := W).map (W := W) L ⋯

Tactic:
obtain ⟨φ₀, rfl, rfl, hφ₀⟩ : ∃ (φ₀ : W.LeftFraction₂ X Y)
    (_ : f₁ = φ₀.fst.map L (inverts L W))
    (_ : f₂ = φ₀.snd.map L (inverts L W)),
    add' W f₁ f₂ = φ₀.add.map L (inverts L W) :=
    ⟨(exists_leftFraction₂ L W f₁ f₂).choose,
      (exists_leftFraction₂ L W f₁ f₂).choose_spec.1,
      (exists_leftFraction₂ L W f₁ f₂).choose_spec.2, rfl⟩

Premises used: CategoryTheory.Localization.Preadditive.add', CategoryTheory.MorphismProperty.LeftFraction₂, 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
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst (W := W).map (W := W) L ⋯ = φ.fst (W := W).map (W := W) L ⋯
hφ₂ : φ₀.snd (W := W).map (W := W) L ⋯ = φ.snd (W := W).map (W := W) L ⋯
hφ₀ : add' W (φ₀.fst (W := W).map (W := W) L ⋯) (φ₀.snd (W := W).map (W := W) L ⋯) = φ₀.add (W := W).map (W := W) L ⋯
obtain :
  ∀ (Z : C) (t₁ : φ₀.Y' (W := W) ⟶ Z) (t₂ : φ.Y' (W := W) ⟶ Z) (hst : φ₀.s (W := W) ≫ t₁ = φ.s (W := W) ≫ t₂)
    (hft : φ₀.f (W := W) ≫ t₁ = φ.f (W := W) ≫ t₂) (hft' : φ₀.f' (W := W) ≫ t₁ = φ.f' (W := W) ≫ t₂)
    (ht : W (φ₀.s (W := W) ≫ t₁)),
    add' W (φ₀.fst (W := W).map (W := W) L ⋯) (φ₀.snd (W := W).map (W := W) L ⋯) = φ.add (W := W).map (W := W) L ⋯
⊢ add' W (φ₀.fst (W := W).map (W := W) L ⋯) (φ₀.snd (W := W).map (W := W) L ⋯) = φ.add (W := W).map (W := W) L ⋯

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, hft', ht⟩ := (LeftFraction₂.map_eq_iff L W φ₀ φ).1 ⟨hφ₁, hφ₂⟩

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂.map_eq_iff, And.intro, Iff.mp
-- 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
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst (W := W).map (W := W) L ⋯ = φ.fst (W := W).map (W := W) L ⋯
hφ₂ : φ₀.snd (W := W).map (W := W) L ⋯ = φ.snd (W := W).map (W := W) L ⋯
hφ₀ : add' W (φ₀.fst (W := W).map (W := W) L ⋯) (φ₀.snd (W := W).map (W := W) L ⋯) = φ₀.add (W := W).map (W := W) L ⋯
Z : C
t₁ : φ₀.Y' (W := W) ⟶ Z
t₂ : φ.Y' (W := W) ⟶ Z
hst : φ₀.s (W := W) ≫ t₁ = φ.s (W := W) ≫ t₂
hft : φ₀.f (W := W) ≫ t₁ = φ.f (W := W) ≫ t₂
hft' : φ₀.f' (W := W) ≫ t₁ = φ.f' (W := W) ≫ t₂
ht : W (φ₀.s (W := W) ≫ t₁)
⊢ IsIso (L.map (φ₀.s (W := W) ≫ t₁))

Tactic:
have := inverts L W _ ht
-- 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
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst (W := W).map (W := W) L ⋯ = φ.fst (W := W).map (W := W) L ⋯
hφ₂ : φ₀.snd (W := W).map (W := W) L ⋯ = φ.snd (W := W).map (W := W) L ⋯
hφ₀ : add' W (φ₀.fst (W := W).map (W := W) L ⋯) (φ₀.snd (W := W).map (W := W) L ⋯) = φ₀.add (W := W).map (W := W) L ⋯
Z : C
t₁ : φ₀.Y' (W := W) ⟶ Z
t₂ : φ.Y' (W := W) ⟶ Z
hst : φ₀.s (W := W) ≫ t₁ = φ.s (W := W) ≫ t₂
hft : φ₀.f (W := W) ≫ t₁ = φ.f (W := W) ≫ t₂
hft' : φ₀.f' (W := W) ≫ t₁ = φ.f' (W := W) ≫ t₂
ht : W (φ₀.s (W := W) ≫ t₁)
this : IsIso (L.map (φ₀.s (W := W) ≫ t₁))
rw :
  φ₀.add (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W) ≫ t₁) =
    φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W) ≫ t₁)
⊢ add' W (φ₀.fst (W := W).map (W := W) L ⋯) (φ₀.snd (W := W).map (W := W) L ⋯) = φ.add (W := W).map (W := W) L ⋯

Tactic:
rw [hφ₀, ← cancel_mono (L.map (φ₀.s ≫ t₁))]

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂.s, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.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
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst (W := W).map (W := W) L ⋯ = φ.fst (W := W).map (W := W) L ⋯
hφ₂ : φ₀.snd (W := W).map (W := W) L ⋯ = φ.snd (W := W).map (W := W) L ⋯
hφ₀ : add' W (φ₀.fst (W := W).map (W := W) L ⋯) (φ₀.snd (W := W).map (W := W) L ⋯) = φ₀.add (W := W).map (W := W) L ⋯
Z : C
t₁ : φ₀.Y' (W := W) ⟶ Z
t₂ : φ.Y' (W := W) ⟶ Z
hst : φ₀.s (W := W) ≫ t₁ = φ.s (W := W) ≫ t₂
hft : φ₀.f (W := W) ≫ t₁ = φ.f (W := W) ≫ t₂
hft' : φ₀.f' (W := W) ≫ t₁ = φ.f' (W := W) ≫ t₂
ht : W (φ₀.s (W := W) ≫ t₁)
this : IsIso (L.map (φ₀.s (W := W) ≫ t₁))
nth_rw :
  φ₀.add (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W) ≫ t₁) =
    φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W) ≫ t₂)
⊢ φ₀.add (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W) ≫ t₁) =
    φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W) ≫ t₁)

Tactic:
nth_rw 2 [hst]
-- 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
φ φ₀ : W.LeftFraction₂ X Y
hφ₁ : φ₀.fst (W := W).map (W := W) L ⋯ = φ.fst (W := W).map (W := W) L ⋯
hφ₂ : φ₀.snd (W := W).map (W := W) L ⋯ = φ.snd (W := W).map (W := W) L ⋯
hφ₀ : add' W (φ₀.fst (W := W).map (W := W) L ⋯) (φ₀.snd (W := W).map (W := W) L ⋯) = φ₀.add (W := W).map (W := W) L ⋯
Z : C
t₁ : φ₀.Y' (W := W) ⟶ Z
t₂ : φ.Y' (W := W) ⟶ Z
hst : φ₀.s (W := W) ≫ t₁ = φ.s (W := W) ≫ t₂
hft : φ₀.f (W := W) ≫ t₁ = φ.f (W := W) ≫ t₂
hft' : φ₀.f' (W := W) ≫ t₁ = φ.f' (W := W) ≫ t₂
ht : W (φ₀.s (W := W) ≫ t₁)
this : IsIso (L.map (φ₀.s (W := W) ≫ t₁))
rw :
  φ₀.add (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W)) ≫ L.map t₁ =
    φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W) ≫ t₂)
rw₁ :
  φ₀.add (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W)) ≫ L.map t₁ =
    φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)) ≫ L.map t₂
rw₂ : L.map (φ₀.add (W := W).f (W := W)) ≫ L.map t₁ = φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)) ≫ L.map t₂
rw₃ : L.map (φ₀.add (W := W).f (W := W)) ≫ L.map t₁ = L.map (φ.add (W := W).f (W := W)) ≫ L.map t₂
rw₄ : L.map (φ₀.add (W := W).f (W := W) ≫ t₁) = L.map (φ.add (W := W).f (W := W)) ≫ L.map t₂
rw₅ : L.map (φ₀.add (W := W).f (W := W) ≫ t₁) = L.map (φ.add (W := W).f (W := W) ≫ t₂)
rw₆ : L.map (φ₀.f (W := W) ≫ t₁ + φ₀.f' (W := W) ≫ t₁) = L.map (φ.add (W := W).f (W := W) ≫ t₂)
rw₇ : L.map (φ₀.f (W := W) ≫ t₁ + φ₀.f' (W := W) ≫ t₁) = L.map (φ.f (W := W) ≫ t₂ + φ.f' (W := W) ≫ t₂)
rw₈ : L.map (φ.f (W := W) ≫ t₂ + φ₀.f' (W := W) ≫ t₁) = L.map (φ.f (W := W) ≫ t₂ + φ.f' (W := W) ≫ t₂)
rw₉ rw₁₀ : L.map (φ.f (W := W) ≫ t₂ + φ.f' (W := W) ≫ t₂) = L.map (φ.f (W := W) ≫ t₂ + φ.f' (W := W) ≫ t₂)
⊢ φ₀.add (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W) ≫ t₁) =
    φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W) ≫ t₂)

Tactic:
rw [L.map_comp, L.map_comp, LeftFraction.map_comp_map_s_assoc,
    LeftFraction.map_comp_map_s_assoc, ← L.map_comp, ← L.map_comp,
    add_comp, add_comp, hft, hft']

Premises used: CategoryTheory.Preadditive.add_comp, CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_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 : C
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 ⋯),
    add' W f₁ f₂ = add' W f₂ f₁
⊢ add' W f₁ f₂ = add' W f₂ f₁

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 : C
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 ⋯
rw : α.add (W := W).map (W := W) L ⋯ = add' W f₂ f₁
rw₁ : α.add (W := W).map (W := W) L ⋯ = α.symm (W := W).add (W := W).map (W := W) L ⋯
rw₂ rw₃ : α.add (W := W).map (W := W) L ⋯ = α.add (W := W).map (W := W) L ⋯
⊢ add' W f₁ f₂ = add' W f₂ f₁

Tactic:
rw [add'_eq W f₁ f₂ α h₁ h₂, add'_eq W f₂ f₁ α.symm h₂ h₁, α.symm_add]

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂.symm_add, CategoryTheory.Localization.Preadditive.add'_eq, CategoryTheory.MorphismProperty.LeftFraction₂.symm
-- 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
obtain : ∀ (α : W.LeftFraction X Y) (hα : f = α.map (W := W) L ⋯), add' W f (L.map 0) = f
⊢ add' W f (L.map 0) = f

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

Tactic:
rw [add'_eq W f (L.map 0) (LeftFraction₂.mk α.f 0 α.s α.hs) hα, hα]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.Localization.Preadditive.add'_eq, CategoryTheory.Functor.map, CategoryTheory.MorphismProperty.LeftFraction.f, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.LeftFraction₂.mk, OfNat.ofNat