awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (goal)
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₂)
⊢ 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₁)
have rw₇ : L.map (-φ₀.f (W := W) ≫ t₁) = L.map (φ.neg (W := W).f (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (goal)
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₂)
⊢ 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₁)
have rw₈ : L.map (-φ₀.f (W := W) ≫ t₁) = L.map (-φ.f (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (goal)
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₂)
⊢ 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₁)
have rw₉ : L.map (-φ.f (W := W) ≫ t₂) = L.map (-φ.f (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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (goal)
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 ⋯
⊢ add' W f₁ f₂ = φ.add (W := W).map (W := W) L ⋯
have obtain : ∀ (φ₀ : W.LeftFraction₂ X Y) (hφ₁ : φ₀.fst (W := W).map (W := W) L sorry = φ.fst (W := W).map (W := W) L sorry)
  (hφ₂ : φ₀.snd (W := W).map (W := W) L sorry = φ.snd (W := W).map (W := W) L sorry)
  (hφ₀ :
    add' W (φ₀.fst (W := W).map (W := W) L sorry) (φ₀.snd (W := W).map (W := W) L sorry) = φ₀.add (W := W).map (W := W) L sorry),
  add' W (φ₀.fst (W := W).map (W := W) L sorry) (φ₀.snd (W := W).map (W := W) L sorry) = φ.add (W := W).map (W := W) L sorry
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⟩
Cleared hypotheses: f₁, f₂, hφ₁, hφ₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (goal)
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 ⋯
⊢ add' W (φ₀.fst (W := W).map (W := W) L ⋯) (φ₀.snd (W := W).map (W := W) L ⋯) = φ.add (W := W).map (W := W) L ⋯
have 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 sorry) (φ₀.snd (W := W).map (W := W) L sorry) = φ.add (W := W).map (W := W) L sorry
Tactic: obtain ⟨Z, t₁, t₂, hst, hft, hft', ht⟩ := (LeftFraction₂.map_eq_iff L W φ₀ φ).1 ⟨hφ₁, hφ₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (hypothesis)
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₁)
⊢ add' W (φ₀.fst (W := W).map (W := W) L ⋯) (φ₀.snd (W := W).map (W := W) L ⋯) = φ.add (W := W).map (W := W) L ⋯
have this : IsIso (L.map (φ₀.s (W := W) ≫ t₁))
Tactic: have := inverts L W _ ht
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (goal)
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₁))
⊢ add' W (φ₀.fst (W := W).map (W := W) L ⋯) (φ₀.snd (W := W).map (W := W) L ⋯) = φ.add (W := W).map (W := W) L ⋯
have rw : φ₀.add (W := W).map (W := W) L sorry ≫ L.map (φ₀.s (W := W) ≫ t₁) =
  φ.add (W := W).map (W := W) L sorry ≫ L.map (φ₀.s (W := W) ≫ t₁)
Tactic: rw [hφ₀, ← cancel_mono (L.map (φ₀.s ≫ t₁))]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (goal)
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₁))
⊢ φ₀.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₁)
have nth_rw : φ₀.add (W := W).map (W := W) L sorry ≫ L.map (φ₀.s (W := W) ≫ t₁) =
  φ.add (W := W).map (W := W) L sorry ≫ L.map (φ.s (W := W) ≫ t₂)
Tactic: nth_rw 2 [hst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (goal)
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₁))
⊢ φ₀.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₂)
have rw : φ₀.add (W := W).map (W := W) L sorry ≫ L.map (φ₀.s (W := W)) ≫ L.map t₁ =
  φ.add (W := W).map (W := W) L sorry ≫ 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']
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (goal)
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₂)
⊢ φ₀.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₂)
have rw₁ : φ₀.add (W := W).map (W := W) L sorry ≫ L.map (φ₀.s (W := W)) ≫ L.map t₁ =
  φ.add (W := W).map (W := W) L sorry ≫ L.map (φ.s (W := W)) ≫ L.map 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']
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (goal)
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₂
⊢ φ₀.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₂)
have rw₂ : L.map (φ₀.add (W := W).f (W := W)) ≫ L.map t₁ = φ.add (W := W).map (W := W) L sorry ≫ L.map (φ.s (W := W)) ≫ L.map 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']
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (goal)
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₂
⊢ φ₀.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₂)
have rw₃ : L.map (φ₀.add (W := W).f (W := W)) ≫ L.map t₁ = L.map (φ.add (W := W).f (W := W)) ≫ L.map 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']
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (goal)
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₂
⊢ φ₀.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₂)
have rw₄ : L.map (φ₀.add (W := W).f (W := W) ≫ t₁) = L.map (φ.add (W := W).f (W := W)) ≫ L.map 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']
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (goal)
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₂
⊢ φ₀.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₂)
have rw₅ : L.map (φ₀.add (W := W).f (W := W) ≫ t₁) = L.map (φ.add (W := W).f (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']
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive (goal)
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₂)
⊢ φ₀.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₂)
have rw₆ : L.map (φ₀.f (W := W) ≫ t₁ + φ₀.f' (W := W) ≫ t₁) = L.map (φ.add (W := W).f (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']