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 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 ⋯
⊢ add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
have obtain : ∀ (γ : W.LeftFraction (α.Y' (W := W)) (β.Y' (W := W)))
  (hγ :
    (RightFraction.mk (W := W) (α.s (W := W)) sorry (β.f (W := W))).f (W := W) ≫ γ.s (W := W) =
      (RightFraction.mk (W := W) (α.s (W := W)) sorry (β.f (W := W))).s (W := W) ≫ γ.f (W := W)),
  add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
Tactic: obtain ⟨γ, hγ⟩ := (RightFraction.mk _ α.hs β.f).exists_leftFraction
-- 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 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)
⊢ add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
have rw : α.add (W := W).map (W := W) L sorry ≫ g =
  (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W)) (β.s (W := W) ≫ γ.s (W := W))
            sorry).add
        (W := W).map
    (W := W) L sorry
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))]
-- 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 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 ⋯
⊢ add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
have 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))
            sorry).fst
        (W := W).map
    (W := W) L sorry
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))]
-- 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 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 ⋯
⊢ add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
have 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))
            sorry).snd
        (W := W).map
    (W := W) L sorry
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))]
-- 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 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)
⊢ 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 ⋯
have hφ₁ : α.fst (W := W).map (W := W) L sorry ≫ β.map (W := W) L sorry =
  (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W)) (β.s (W := W) ≫ γ.s (W := W))
            sorry).fst
        (W := W).map
    (W := W) L sorry
Tactic: rw [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 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)
⊢ 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 ⋯
have hφ₂ : α.snd (W := W).map (W := W) L sorry ≫ β.map (W := W) L sorry =
  (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W)) (β.s (W := W) ≫ γ.s (W := W))
            sorry).snd
        (W := W).map
    (W := W) L sorry
Tactic: rw [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 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)
⊢ α.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 ⋯
have rw : (α.add (W := W).comp₀ (W := W) β γ).map (W := W) L sorry =
  (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f' (W := W) ≫ γ.f (W := W)) (β.s (W := W) ≫ γ.s (W := W))
            sorry).add
        (W := W).map
    (W := W) L sorry
Tactic: rw [hβ, LeftFraction.map_comp_map_eq_map _ _ γ 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 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)
⊢ (α.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 ⋯
have dsimp : (LeftFraction.mk (W := W) ((α.f (W := W) + α.f' (W := W)) ≫ γ.f (W := W)) (β.s (W := W) ≫ γ.s (W := W)) sorry).map (W := W)
    L sorry =
  (LeftFraction.mk (W := W) (α.f (W := W) ≫ γ.f (W := W) + α.f' (W := W) ≫ γ.f (W := W)) (β.s (W := W) ≫ γ.s (W := W))
        sorry).map
    (W := W) L sorry
Tactic: dsimp [LeftFraction₂.add]
-- 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 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)
⊢ (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 ⋯
have rw : (LeftFraction.mk (W := W) (α.f (W := W) ≫ γ.f (W := W) + α.f' (W := W) ≫ γ.f (W := W)) (β.s (W := W) ≫ γ.s (W := W))
        sorry).map
    (W := W) L sorry =
  (LeftFraction.mk (W := W) (α.f (W := W) ≫ γ.f (W := W) + α.f' (W := W) ≫ γ.f (W := W)) (β.s (W := W) ≫ γ.s (W := W))
        sorry).map
    (W := W) L sorry
Tactic: rw [add_comp]
-- 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 Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)
have obtain : ∀ (α : W.LeftFraction X Y) (hα : f = α.map (W := W) L sorry), f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)
Tactic: obtain ⟨α, hα⟩ := exists_leftFraction L W f
-- 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 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 ⋯
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)
have obtain : ∀ (β : W.LeftFraction₂ Y Z) (hβ₁ : g₁ = β.fst (W := W).map (W := W) L sorry) (hβ₂ : g₂ = β.snd (W := W).map (W := W) L sorry),
  f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)
Tactic: obtain ⟨β, hβ₁, hβ₂⟩ := exists_leftFraction₂ L W g₁ g₂
-- 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 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 ⋯
⊢ f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)
have obtain : ∀ (γ : W.LeftFraction₂ (α.Y' (W := W)) (β.Y' (W := W)))
  (hγ₁ :
    (RightFraction₂.mk (W := W) (α.s (W := W)) sorry (β.f (W := W)) (β.f' (W := W))).f (W := W) ≫ γ.s (W := W) =
      (RightFraction₂.mk (W := W) (α.s (W := W)) sorry (β.f (W := W)) (β.f' (W := W))).s (W := W) ≫ γ.f (W := W))
  (hγ₂ :
    (RightFraction₂.mk (W := W) (α.s (W := W)) sorry (β.f (W := W)) (β.f' (W := W))).f' (W := W) ≫ γ.s (W := W) =
      (RightFraction₂.mk (W := W) (α.s (W := W)) sorry (β.f (W := W)) (β.f' (W := W))).s (W := W) ≫ γ.f' (W := W)),
  f ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)
Tactic: obtain ⟨γ, hγ₁, hγ₂⟩ := (RightFraction₂.mk _ α.hs β.f β.f').exists_leftFraction₂
-- 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 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 ≫ add' W g₁ g₂ = add' W (f ≫ g₁) (f ≫ g₂)
have rw : (α.comp₀ (W := W) (β.add (W := W)) (γ.add (W := W))).map (W := W) L sorry =
  (LeftFraction₂.mk (W := W) (α.f (W := W) ≫ γ.f (W := W)) (α.f (W := W) ≫ γ.f' (W := W)) (β.s (W := W) ≫ γ.s (W := W))
            sorry).add
        (W := W).map
    (W := W) L sorry
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])]
-- 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 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)
⊢ (α.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 ⋯
have dsimp : LeftFraction.map (W := W)
    (LeftFraction.mk (W := W) (α.f (W := W) ≫ (γ.f (W := W) + γ.f' (W := W))) (β.s (W := W) ≫ γ.s (W := W)) sorry) L sorry =
  (LeftFraction.mk (W := W) (α.f (W := W) ≫ γ.f (W := W) + α.f (W := W) ≫ γ.f' (W := W)) (β.s (W := W) ≫ γ.s (W := W))
        sorry).map
    (W := W) L sorry
Tactic: dsimp [LeftFraction₂.add]
-- 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 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)
⊢ 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 ⋯
have 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))
      sorry)
    L sorry =
  (LeftFraction.mk (W := W) (α.f (W := W) ≫ γ.f (W := W) + α.f (W := W) ≫ γ.f' (W := W)) (β.s (W := W) ≫ γ.s (W := W))
        sorry).map
    (W := W) L sorry
Tactic: rw [comp_add]
-- 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 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'
⊢ add W eX eY f₁ f₂ ≫ g = add W eX eZ (f₁ ≫ g) (f₂ ≫ g)
have 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)
Tactic: obtain ⟨g, rfl⟩ := (homEquiv eY eZ).symm.surjective g
Cleared hypotheses: g
-- 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 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'
⊢ f ≫ add W eY eZ g₁ g₂ = add W eX eZ (f ≫ g₁) (f ≫ g₂)
have 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₂)
Tactic: obtain ⟨f, rfl⟩ := (homEquiv eX eY).symm.surjective f
Cleared hypotheses: f
-- 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
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'
⊢ add W eX eY f₁ f₂ = add W eX' eY' f₁ f₂
have h₁ : 𝟙 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₂
-- 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
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₂ = add W eX' eY' f₁ f₂
have h₂ : 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₂ (𝟙 _)
-- 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
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₂
have h₃ : add W eX eY f₁ f₂ = add W eX' eY f₁ f₂
Tactic: simp only [id_comp] at h₁
Cleared hypotheses: 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
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₂
have h₃ : add W eX' eY f₁ f₂ = add W eX' eY' f₁ f₂
Tactic: simp only [comp_id] at h₂
Cleared hypotheses: 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
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₂
⊢ add W eX eY f₁ f₂ = add W eX' eY' f₁ f₂
have rw₁ : add W eX' eY' f₁ f₂ = add W eX' eY' f₁ f₂
Tactic: rw [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 Z : C
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
⊢ AddCommGroup (X' ⟶ Y')
have this : L.EssSurj
Tactic: have := Localization.essSurj L W