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φ₁ : φ₀.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₂)
⊢ φ₀.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 (φ.f (W := W) ≫ t₂ + φ.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₂)
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₂)
⊢ φ₀.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 (φ.f (W := W) ≫ t₂ + φ.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₂)
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₂)
⊢ φ₀.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 (φ.f (W := W) ≫ t₂ + φ.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
f₁ f₂ : L.obj X ⟶ L.obj Y
⊢ add' W f₁ f₂ = add' W f₂ f₁
have obtain : ∀ (α : W.LeftFraction₂ X Y) (h₁ : f₁ = α.fst (W := W).map (W := W) L sorry) (h₂ : f₂ = α.snd (W := W).map (W := W) L sorry),
  add' W f₁ f₂ = add' W f₂ f₁
Tactic: obtain ⟨α, h₁, h₂⟩ := exists_leftFraction₂ L W f₁ 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 : 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 f₂ f₁
have rw : α.add (W := W).map (W := W) L sorry = add' W f₂ f₁
Tactic: rw [add'_eq W f₁ f₂ α h₁ h₂, add'_eq W f₂ f₁ α.symm h₂ h₁, α.symm_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 : 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₁
⊢ add' W f₁ f₂ = add' W f₂ f₁
have rw₁ : α.add (W := W).map (W := W) L sorry = α.symm (W := W).add (W := W).map (W := W) L sorry
Tactic: rw [add'_eq W f₁ f₂ α h₁ h₂, add'_eq W f₂ f₁ α.symm h₂ h₁, α.symm_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 : 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 ⋯
⊢ add' W f₁ f₂ = add' W f₂ f₁
have rw₂ : α.add (W := W).map (W := W) L sorry = α.add (W := W).map (W := W) L sorry
Tactic: rw [add'_eq W f₁ f₂ α h₁ h₂, add'_eq W f₂ f₁ α.symm h₂ h₁, α.symm_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 : C
f : L.obj X ⟶ L.obj Y
⊢ add' W f (L.map 0) = f
have obtain : ∀ (α : W.LeftFraction X Y) (hα : f = α.map (W := W) L sorry), add' W f (L.map 0) = f
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 : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
⊢ add' W f (L.map 0) = f
have rw : (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) sorry).add (W := W).map (W := W) L sorry = α.map (W := W) L sorry
Tactic: rw [add'_eq W f (L.map 0) (LeftFraction₂.mk α.f 0 α.s α.hs) 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
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 ⋯
⊢ add' W f (L.map 0) = f
have rw₁ : L.map 0 = (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) sorry).snd (W := W).map (W := W) L sorry
Tactic: rw [add'_eq W f (L.map 0) (LeftFraction₂.mk α.f 0 α.s α.hs) 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
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
⊢ L.map 0 = (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).map (W := W) L ⋯
have rw : L.map 0 ≫ L.map (α.s (W := W)) =
  (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) sorry).snd (W := W).map (W := W) L sorry ≫ L.map (α.s (W := W))
Tactic: rw [← cancel_mono (L.map α.s), ← L.map_comp, Limits.zero_comp,
      LeftFraction.map_comp_map_s]
-- 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 : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
rw :
  L.map 0 ≫ L.map (α.s (W := W)) =
    (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).map (W := W) L ⋯ ≫ L.map (α.s (W := W))
⊢ L.map 0 = (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).map (W := W) L ⋯
have rw₁ : L.map (0 ≫ α.s (W := W)) =
  (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) sorry).snd (W := W).map (W := W) L sorry ≫ L.map (α.s (W := W))
Tactic: rw [← cancel_mono (L.map α.s), ← L.map_comp, Limits.zero_comp,
      LeftFraction.map_comp_map_s]
-- 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 : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
rw :
  L.map 0 ≫ L.map (α.s (W := W)) =
    (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).map (W := W) L ⋯ ≫ L.map (α.s (W := W))
rw₁ :
  L.map (0 ≫ α.s (W := W)) =
    (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).map (W := W) L ⋯ ≫ L.map (α.s (W := W))
⊢ L.map 0 = (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).map (W := W) L ⋯
have rw₂ : L.map 0 =
  (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) sorry).snd (W := W).map (W := W) L sorry ≫ L.map (α.s (W := W))
Tactic: rw [← cancel_mono (L.map α.s), ← L.map_comp, Limits.zero_comp,
      LeftFraction.map_comp_map_s]
-- 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 : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
rw :
  L.map 0 ≫ L.map (α.s (W := W)) =
    (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).map (W := W) L ⋯ ≫ L.map (α.s (W := W))
rw₁ :
  L.map (0 ≫ α.s (W := W)) =
    (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).map (W := W) L ⋯ ≫ L.map (α.s (W := W))
rw₂ :
  L.map 0 =
    (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).map (W := W) L ⋯ ≫ L.map (α.s (W := W))
⊢ L.map 0 = (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).snd (W := W).map (W := W) L ⋯
have rw₃ : L.map 0 = L.map ((LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) sorry).snd (W := W).f (W := W))
Tactic: rw [← cancel_mono (L.map α.s), ← L.map_comp, Limits.zero_comp,
      LeftFraction.map_comp_map_s]
-- 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 : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
⊢ (LeftFraction₂.mk (W := W) (α.f (W := W)) 0 (α.s (W := W)) ⋯).add (W := W).map (W := W) L ⋯ = α.map (W := W) L ⋯
have dsimp : (LeftFraction.mk (W := W) (α.f (W := W) + 0) (α.s (W := W)) sorry).map (W := W) L 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 : C
f : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map (W := W) L ⋯
⊢ (LeftFraction.mk (W := W) (α.f (W := W) + 0) (α.s (W := W)) ⋯).map (W := W) L ⋯ = α.map (W := W) L ⋯
have rw : (LeftFraction.mk (W := W) (α.f (W := W)) (α.s (W := W)) sorry).map (W := W) L sorry = α.map (W := W) L sorry
Tactic: rw [add_zero]
-- 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 : L.obj X ⟶ L.obj Y
⊢ add' W (L.map 0) f = f
have rw : add' W f (L.map 0) = f
Tactic: rw [add'_comm, add'_zero]
-- 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 : L.obj X ⟶ L.obj Y
rw : add' W f (L.map 0) = f
⊢ add' W (L.map 0) f = f
have rw₁ : f = f
Tactic: rw [add'_comm, add'_zero]
-- 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₂ f₃ : L.obj X ⟶ L.obj Y
⊢ add' W (add' W f₁ f₂) f₃ = add' W f₁ (add' W f₂ f₃)
have obtain : ∀ (α : W.LeftFraction₃ X Y) (h₁ : f₁ = α.fst (W := W).map (W := W) L sorry) (h₂ : f₂ = α.snd (W := W).map (W := W) L sorry)
  (h₃ : f₃ = α.thd (W := W).map (W := W) L sorry), add' W (add' W f₁ f₂) f₃ = add' W f₁ (add' W f₂ f₃)
Tactic: obtain ⟨α, h₁, h₂, h₃⟩ := exists_leftFraction₃ L W f₁ f₂ f₃
-- 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₂ f₃ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₃ X Y
h₁ : f₁ = α.fst (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
h₃ : f₃ = α.thd (W := W).map (W := W) L ⋯
⊢ add' W (add' W f₁ f₂) f₃ = add' W f₁ (add' W f₂ f₃)
have rw : (LeftFraction₂.mk (W := W) (α.f (W := W) + α.f' (W := W)) (α.f'' (W := W)) (α.s (W := W)) sorry).add (W := W).map (W := W) L
    sorry =
  (LeftFraction₂.mk (W := W) (α.f (W := W)) (α.f' (W := W) + α.f'' (W := W)) (α.s (W := W)) sorry).add (W := W).map (W := W)
    L sorry
Tactic: rw [add'_eq W f₁ f₂ α.forgetThd h₁ h₂, add'_eq W f₂ f₃ α.forgetFst h₂ h₃,
    add'_eq W _ _ (LeftFraction₂.mk (α.f + α.f') α.f'' α.s α.hs) rfl h₃,
    add'_eq W _ _ (LeftFraction₂.mk α.f (α.f' + α.f'') α.s α.hs) h₁ rfl]
-- 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₂ f₃ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₃ X Y
h₁ : f₁ = α.fst (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
h₃ : f₃ = α.thd (W := W).map (W := W) L ⋯
⊢ (LeftFraction₂.mk (W := W) (α.f (W := W) + α.f' (W := W)) (α.f'' (W := W)) (α.s (W := W)) ⋯).add (W := W).map (W := W)
      L ⋯ =
    (LeftFraction₂.mk (W := W) (α.f (W := W)) (α.f' (W := W) + α.f'' (W := W)) (α.s (W := W)) ⋯).add (W := W).map (W :=
      W) L ⋯
have dsimp : (LeftFraction.mk (W := W) (α.f (W := W) + α.f' (W := W) + α.f'' (W := W)) (α.s (W := W)) sorry).map (W := W) L sorry =
  (LeftFraction.mk (W := W) (α.f (W := W) + (α.f' (W := W) + α.f'' (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 : C
f₁ f₂ f₃ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₃ X Y
h₁ : f₁ = α.fst (W := W).map (W := W) L ⋯
h₂ : f₂ = α.snd (W := W).map (W := W) L ⋯
h₃ : f₃ = α.thd (W := W).map (W := W) L ⋯
⊢ (LeftFraction.mk (W := W) (α.f (W := W) + α.f' (W := W) + α.f'' (W := W)) (α.s (W := W)) ⋯).map (W := W) L ⋯ =
    (LeftFraction.mk (W := W) (α.f (W := W) + (α.f' (W := W) + α.f'' (W := W))) (α.s (W := W)) ⋯).map (W := W) L ⋯
have rw : (LeftFraction.mk (W := W) (α.f (W := W) + (α.f' (W := W) + α.f'' (W := W))) (α.s (W := W)) sorry).map (W := W) L sorry =
  (LeftFraction.mk (W := W) (α.f (W := W) + (α.f' (W := W) + α.f'' (W := W))) (α.s (W := W)) sorry).map (W := W) L sorry
Tactic: rw [add_assoc]
-- 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
⊢ add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
have obtain : ∀ (α : W.LeftFraction₂ X Y) (h₁ : f₁ = α.fst (W := W).map (W := W) L sorry) (h₂ : f₂ = α.snd (W := W).map (W := W) L sorry),
  add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
Tactic: obtain ⟨α, h₁, h₂⟩ := exists_leftFraction₂ L W f₁ 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₁ 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 ⋯
⊢ add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
have obtain : ∀ (β : W.LeftFraction Y Z) (hβ : g = β.map (W := W) L sorry), add' W f₁ f₂ ≫ g = add' W (f₁ ≫ g) (f₂ ≫ g)
Tactic: obtain ⟨β, hβ⟩ := exists_leftFraction L W g