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
E : Type u_3
inst_5 : Category.{v_3, u_3} E
inst_6 : Preadditive.{v_3, u_3} E
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : L.Additive
G : Functor.{v_2, v_3, u_2, u_3} D E
h : (L ⋙ G).Additive
X Y : C
φ : W.LeftFraction₂ X Y
mpr :
  G.map (φ.add (W := W).map (W := W) L ⋯) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)
mpr₁ :
  G.map (φ.add (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W))) =
    (G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)) ≫ G.map (L.map (φ.s (W := W)))
mpr₂ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    (G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)) ≫ G.map (L.map (φ.s (W := W)))
mpr₃ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W)))
mpr₄ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W)))
mpr₅ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
⊢ G.map (φ.fst (W := W).map (W := W) L ⋯ + φ.snd (W := W).map (W := W) L ⋯) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)
have mpr₆ : G.map (L.map (φ.add (W := W).f (W := W))) =
  G.map (φ.fst (W := W).map (W := W) L sorry ≫ L.map (φ.s (W := W))) +
    G.map (φ.snd (W := W).map (W := W) L sorry ≫ L.map (φ.s (W := W)))
Tactic: rw [← φ.map_add L (inverts L W), ← cancel_mono (G.map (L.map φ.s)), ← G.map_comp,
      add_comp, ← G.map_comp, ← G.map_comp, LeftFraction.map_comp_map_s,
      LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, ← Functor.comp_map,
      Functor.map_add, Functor.comp_map, Functor.comp_map]
-- 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
E : Type u_3
inst_5 : Category.{v_3, u_3} E
inst_6 : Preadditive.{v_3, u_3} E
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : L.Additive
G : Functor.{v_2, v_3, u_2, u_3} D E
h : (L ⋙ G).Additive
X Y : C
φ : W.LeftFraction₂ X Y
mpr :
  G.map (φ.add (W := W).map (W := W) L ⋯) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)
mpr₁ :
  G.map (φ.add (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W))) =
    (G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)) ≫ G.map (L.map (φ.s (W := W)))
mpr₂ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    (G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)) ≫ G.map (L.map (φ.s (W := W)))
mpr₃ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W)))
mpr₄ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W)))
mpr₅ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
mpr₆ :
  G.map (L.map (φ.add (W := W).f (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
⊢ G.map (φ.fst (W := W).map (W := W) L ⋯ + φ.snd (W := W).map (W := W) L ⋯) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)
have mpr₇ : G.map (L.map (φ.add (W := W).f (W := W))) =
  G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (φ.snd (W := W).map (W := W) L sorry ≫ L.map (φ.s (W := W)))
Tactic: rw [← φ.map_add L (inverts L W), ← cancel_mono (G.map (L.map φ.s)), ← G.map_comp,
      add_comp, ← G.map_comp, ← G.map_comp, LeftFraction.map_comp_map_s,
      LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, ← Functor.comp_map,
      Functor.map_add, Functor.comp_map, Functor.comp_map]
-- 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
E : Type u_3
inst_5 : Category.{v_3, u_3} E
inst_6 : Preadditive.{v_3, u_3} E
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : L.Additive
G : Functor.{v_2, v_3, u_2, u_3} D E
h : (L ⋙ G).Additive
X Y : C
φ : W.LeftFraction₂ X Y
mpr :
  G.map (φ.add (W := W).map (W := W) L ⋯) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)
mpr₁ :
  G.map (φ.add (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W))) =
    (G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)) ≫ G.map (L.map (φ.s (W := W)))
mpr₂ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    (G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)) ≫ G.map (L.map (φ.s (W := W)))
mpr₃ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W)))
mpr₄ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W)))
mpr₅ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
mpr₆ :
  G.map (L.map (φ.add (W := W).f (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
mpr₇ :
  G.map (L.map (φ.add (W := W).f (W := W))) =
    G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
⊢ G.map (φ.fst (W := W).map (W := W) L ⋯ + φ.snd (W := W).map (W := W) L ⋯) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)
have mpr₈ : G.map (L.map (φ.add (W := W).f (W := W))) =
  G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (L.map (φ.snd (W := W).f (W := W)))
Tactic: rw [← φ.map_add L (inverts L W), ← cancel_mono (G.map (L.map φ.s)), ← G.map_comp,
      add_comp, ← G.map_comp, ← G.map_comp, LeftFraction.map_comp_map_s,
      LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, ← Functor.comp_map,
      Functor.map_add, Functor.comp_map, Functor.comp_map]
-- 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
E : Type u_3
inst_5 : Category.{v_3, u_3} E
inst_6 : Preadditive.{v_3, u_3} E
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : L.Additive
G : Functor.{v_2, v_3, u_2, u_3} D E
h : (L ⋙ G).Additive
X Y : C
φ : W.LeftFraction₂ X Y
mpr :
  G.map (φ.add (W := W).map (W := W) L ⋯) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)
mpr₁ :
  G.map (φ.add (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W))) =
    (G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)) ≫ G.map (L.map (φ.s (W := W)))
mpr₂ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    (G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)) ≫ G.map (L.map (φ.s (W := W)))
mpr₃ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W)))
mpr₄ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W)))
mpr₅ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
mpr₆ :
  G.map (L.map (φ.add (W := W).f (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
mpr₇ :
  G.map (L.map (φ.add (W := W).f (W := W))) =
    G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
mpr₈ :
  G.map (L.map (φ.add (W := W).f (W := W))) =
    G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (L.map (φ.snd (W := W).f (W := W)))
⊢ G.map (φ.fst (W := W).map (W := W) L ⋯ + φ.snd (W := W).map (W := W) L ⋯) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)
have mpr₉ : (L ⋙ G).map (φ.add (W := W).f (W := W)) =
  G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (L.map (φ.snd (W := W).f (W := W)))
Tactic: rw [← φ.map_add L (inverts L W), ← cancel_mono (G.map (L.map φ.s)), ← G.map_comp,
      add_comp, ← G.map_comp, ← G.map_comp, LeftFraction.map_comp_map_s,
      LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, ← Functor.comp_map,
      Functor.map_add, Functor.comp_map, Functor.comp_map]
-- 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
E : Type u_3
inst_5 : Category.{v_3, u_3} E
inst_6 : Preadditive.{v_3, u_3} E
inst_7 : Preadditive.{v_2, u_2} D
inst_8 : L.Additive
G : Functor.{v_2, v_3, u_2, u_3} D E
h : (L ⋙ G).Additive
X Y : C
φ : W.LeftFraction₂ X Y
mpr :
  G.map (φ.add (W := W).map (W := W) L ⋯) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)
mpr₁ :
  G.map (φ.add (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W))) =
    (G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)) ≫ G.map (L.map (φ.s (W := W)))
mpr₂ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    (G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)) ≫ G.map (L.map (φ.s (W := W)))
mpr₃ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W)))
mpr₄ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯) ≫ G.map (L.map (φ.s (W := W)))
mpr₅ :
  G.map (φ.add (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
mpr₆ :
  G.map (L.map (φ.add (W := W).f (W := W))) =
    G.map (φ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W))) +
      G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
mpr₇ :
  G.map (L.map (φ.add (W := W).f (W := W))) =
    G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (φ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ.s (W := W)))
mpr₈ :
  G.map (L.map (φ.add (W := W).f (W := W))) =
    G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (L.map (φ.snd (W := W).f (W := W)))
mpr₉ :
  (L ⋙ G).map (φ.add (W := W).f (W := W)) =
    G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (L.map (φ.snd (W := W).f (W := W)))
⊢ G.map (φ.fst (W := W).map (W := W) L ⋯ + φ.snd (W := W).map (W := W) L ⋯) =
    G.map (φ.fst (W := W).map (W := W) L ⋯) + G.map (φ.snd (W := W).map (W := W) L ⋯)
have mpr₁₀ : (L ⋙ G).map (φ.f (W := W)) + (L ⋙ G).map (φ.f' (W := W)) =
  G.map (L.map (φ.fst (W := W).f (W := W))) + G.map (L.map (φ.snd (W := W).f (W := W)))
Tactic: rw [← φ.map_add L (inverts L W), ← cancel_mono (G.map (L.map φ.s)), ← G.map_comp,
      add_comp, ← G.map_comp, ← G.map_comp, LeftFraction.map_comp_map_s,
      LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, ← Functor.comp_map,
      Functor.map_add, Functor.comp_map, Functor.comp_map]
-- 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
E : Type u_3
inst_4 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_5 : W.HasLeftCalculusOfFractions
inst_6 : Preadditive.{v_2, u_2} D
inst_7 : Preadditive.{v_3, u_3} E
inst_8 : L.Additive
inst_9 : F.Additive
h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0
X₁ X₂ : C
f g : X₁ ⟶ X₂
hfg : F.map (L.map f) = F.map (L.map g)
⊢ L.map f = L.map g
have rw : L.map (f - g) = 0
Tactic: rw [← sub_eq_zero, ← L.map_sub]
-- 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
E : Type u_3
inst_4 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_5 : W.HasLeftCalculusOfFractions
inst_6 : Preadditive.{v_2, u_2} D
inst_7 : Preadditive.{v_3, u_3} E
inst_8 : L.Additive
inst_9 : F.Additive
h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0
X₁ X₂ : C
f g : X₁ ⟶ X₂
hfg : F.map (L.map f) = F.map (L.map g)
⊢ F.map (L.map (f - g)) = 0
have rw : F.map (L.map f - L.map g) = 0
Tactic: rw [L.map_sub, F.map_sub, hfg, sub_self]
-- 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
E : Type u_3
inst_4 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_5 : W.HasLeftCalculusOfFractions
inst_6 : Preadditive.{v_2, u_2} D
inst_7 : Preadditive.{v_3, u_3} E
inst_8 : L.Additive
inst_9 : F.Additive
h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0
X₁ X₂ : C
f g : X₁ ⟶ X₂
hfg : F.map (L.map f) = F.map (L.map g)
rw : F.map (L.map f - L.map g) = 0
⊢ F.map (L.map (f - g)) = 0
have rw₁ : F.map (L.map f) - F.map (L.map g) = 0
Tactic: rw [L.map_sub, F.map_sub, hfg, sub_self]
-- 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
E : Type u_3
inst_4 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_5 : W.HasLeftCalculusOfFractions
inst_6 : Preadditive.{v_2, u_2} D
inst_7 : Preadditive.{v_3, u_3} E
inst_8 : L.Additive
inst_9 : F.Additive
h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0
X₁ X₂ : C
f g : X₁ ⟶ X₂
hfg : F.map (L.map f) = F.map (L.map g)
rw : F.map (L.map f - L.map g) = 0
rw₁ : F.map (L.map f) - F.map (L.map g) = 0
⊢ F.map (L.map (f - g)) = 0
have rw₂ : F.map (L.map g) - F.map (L.map g) = 0
Tactic: rw [L.map_sub, F.map_sub, hfg, sub_self]
-- 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
E : Type u_3
inst_4 : Category.{v_3, u_3} E
F : Functor.{v_2, v_3, u_2, u_3} D E
inst_5 : W.HasLeftCalculusOfFractions
inst_6 : Preadditive.{v_2, u_2} D
inst_7 : Preadditive.{v_3, u_3} E
inst_8 : L.Additive
inst_9 : F.Additive
h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0
X₁ X₂ : C
f g : X₁ ⟶ X₂
hfg : F.map (L.map f) = F.map (L.map g)
rw : F.map (L.map f - L.map g) = 0
rw₁ : F.map (L.map f) - F.map (L.map g) = 0
rw₂ : F.map (L.map g) - F.map (L.map g) = 0
⊢ F.map (L.map (f - g)) = 0
have rw₃ : Eq.{v_3 + 1} (α := F.obj (L.obj X₁) ⟶ F.obj (L.obj X₂)) 0 0
Tactic: rw [L.map_sub, F.map_sub, hfg, sub_self]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ : W.LeftFraction X Y
h : LeftFractionRel (W := W) z₁ z₂
⊢ LeftFractionRel (W := W) z₂ z₁
have obtain : ∀ (Z : C) (t₁ : z₁.Y' (W := W) ⟶ Z) (t₂ : z₂.Y' (W := W) ⟶ Z) (hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂)
  (hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂) (ht : W (z₁.s (W := W) ≫ t₁)), LeftFractionRel (W := W) z₂ z₁
Tactic: obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
h₁₂ : LeftFractionRel (W := W) z₁ z₂
h₂₃ : LeftFractionRel (W := W) z₂ z₃
⊢ LeftFractionRel (W := W) z₁ z₃
have obtain : ∀ (Z₄ : C) (t₁ : z₁.Y' (W := W) ⟶ Z₄) (t₂ : z₂.Y' (W := W) ⟶ Z₄) (hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂)
  (hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂) (ht : W (z₁.s (W := W) ≫ t₁)), LeftFractionRel (W := W) z₁ z₃
Tactic: obtain ⟨Z₄, t₁, t₂, hst, hft, ht⟩ := h₁₂
Cleared hypotheses: h₁₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
h₂₃ : LeftFractionRel (W := W) z₂ z₃
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
⊢ LeftFractionRel (W := W) z₁ z₃
have obtain : ∀ (Z₅ : C) (u₂ : z₂.Y' (W := W) ⟶ Z₅) (u₃ : z₃.Y' (W := W) ⟶ Z₅) (hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃)
  (hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃) (hu : W (z₂.s (W := W) ≫ u₂)), LeftFractionRel (W := W) z₁ z₃
Tactic: obtain ⟨Z₅, u₂, u₃, hsu, hfu, hu⟩ := h₂₃
Cleared hypotheses: h₂₃
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
⊢ LeftFractionRel (W := W) z₁ z₃
have obtain : ∀ {Y' : C} (v₄ : Z₄ ⟶ Y') (v₅ : Z₅ ⟶ Y') (hv₅ : W v₅)
  (fac :
    (RightFraction.mk (W := W) (z₁.s (W := W) ≫ t₁) ht (z₃.s (W := W) ≫ u₃)).f (W := W) ≫
        (LeftFraction.mk (W := W) v₄ v₅ hv₅).s (W := W) =
      (RightFraction.mk (W := W) (z₁.s (W := W) ≫ t₁) ht (z₃.s (W := W) ≫ u₃)).s (W := W) ≫
        (LeftFraction.mk (W := W) v₄ v₅ hv₅).f (W := W)),
  LeftFractionRel (W := W) z₁ z₃
Tactic: obtain ⟨⟨v₄, v₅, hv₅⟩, fac⟩ := HasLeftCalculusOfFractions.exists_leftFraction
    (RightFraction.mk (z₁.s ≫ t₁) ht (z₃.s ≫ u₃))
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac :
  (RightFraction.mk (W := W) (z₁.s (W := W) ≫ t₁) ht (z₃.s (W := W) ≫ u₃)).f (W := W) ≫
      (LeftFraction.mk (W := W) v₄ v₅ hv₅).s (W := W) =
    (RightFraction.mk (W := W) (z₁.s (W := W) ≫ t₁) ht (z₃.s (W := W) ≫ u₃)).s (W := W) ≫
      (LeftFraction.mk (W := W) v₄ v₅ hv₅).f (W := W)
⊢ LeftFractionRel (W := W) z₁ z₃
have fac₁ : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
Tactic: simp only [Category.assoc] at fac
Cleared hypotheses: fac
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
⊢ LeftFractionRel (W := W) z₁ z₃
have eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Tactic: have eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄ := by
    simpa only [← reassoc_of% hsu, reassoc_of% hst] using fac
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
⊢ LeftFractionRel (W := W) z₁ z₃
have obtain : ∀ (Z₇ : C) (w : Y' ⟶ Z₇) (hw : W w) (fac' : (u₂ ≫ v₅) ≫ w = (t₂ ≫ v₄) ≫ w), LeftFractionRel (W := W) z₁ z₃
Tactic: obtain ⟨Z₇, w, hw, fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ z₂.hs eq