awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction (goal)
Goal:
C₁ : Type u_1
C₂ : Type u_2
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
inst_2 : F.Full
inst_3 : F.Faithful
adj : F ⊣ G
j : C₁
⊢ inverseImage (isomorphisms C₂) G (adj.counit.app j)
have simp : IsIso (G.map (adj.counit.app j))
Tactic: simp only [Functor.id_obj, Functor.comp_obj, inverseImage_iff, isomorphisms.iff]
-- 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
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.LeftFraction₂ X Y
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : W.IsInvertedBy F
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : F.Additive
⊢ φ.add (W := W).map (W := W) F hF = φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF
have this : IsIso (F.map (φ.s (W := W)))
Tactic: have := hF φ.s φ.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
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.LeftFraction₂ X Y
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : W.IsInvertedBy F
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : F.Additive
this : IsIso (F.map (φ.s (W := W)))
⊢ φ.add (W := W).map (W := W) F hF = φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF
have rw : φ.add (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) =
  (φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF) ≫ F.map (φ.s (W := W))
Tactic: rw [← cancel_mono (F.map φ.s), add_comp, LeftFraction.map_comp_map_s,
    LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, F.map_add]
-- 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
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.LeftFraction₂ X Y
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : W.IsInvertedBy F
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : F.Additive
this : IsIso (F.map (φ.s (W := W)))
rw :
  φ.add (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) =
    (φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF) ≫ F.map (φ.s (W := W))
⊢ φ.add (W := W).map (W := W) F hF = φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF
have rw₁ : φ.add (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) =
  φ.fst (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
Tactic: rw [← cancel_mono (F.map φ.s), add_comp, LeftFraction.map_comp_map_s,
    LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, F.map_add]
-- 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
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.LeftFraction₂ X Y
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : W.IsInvertedBy F
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : F.Additive
this : IsIso (F.map (φ.s (W := W)))
rw :
  φ.add (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) =
    (φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF) ≫ F.map (φ.s (W := W))
rw₁ :
  φ.add (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) =
    φ.fst (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
⊢ φ.add (W := W).map (W := W) F hF = φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF
have rw₂ : F.map (φ.add (W := W).f (W := W)) =
  φ.fst (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
Tactic: rw [← cancel_mono (F.map φ.s), add_comp, LeftFraction.map_comp_map_s,
    LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, F.map_add]
-- 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
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.LeftFraction₂ X Y
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : W.IsInvertedBy F
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : F.Additive
this : IsIso (F.map (φ.s (W := W)))
rw :
  φ.add (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) =
    (φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF) ≫ F.map (φ.s (W := W))
rw₁ :
  φ.add (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) =
    φ.fst (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
rw₂ :
  F.map (φ.add (W := W).f (W := W)) =
    φ.fst (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
⊢ φ.add (W := W).map (W := W) F hF = φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF
have rw₃ : F.map (φ.add (W := W).f (W := W)) =
  F.map (φ.fst (W := W).f (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
Tactic: rw [← cancel_mono (F.map φ.s), add_comp, LeftFraction.map_comp_map_s,
    LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, F.map_add]
-- 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
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.LeftFraction₂ X Y
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : W.IsInvertedBy F
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : F.Additive
this : IsIso (F.map (φ.s (W := W)))
rw :
  φ.add (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) =
    (φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF) ≫ F.map (φ.s (W := W))
rw₁ :
  φ.add (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) =
    φ.fst (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
rw₂ :
  F.map (φ.add (W := W).f (W := W)) =
    φ.fst (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
rw₃ :
  F.map (φ.add (W := W).f (W := W)) =
    F.map (φ.fst (W := W).f (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
⊢ φ.add (W := W).map (W := W) F hF = φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF
have rw₄ : F.map (φ.add (W := W).f (W := W)) = F.map (φ.fst (W := W).f (W := W)) + F.map (φ.snd (W := W).f (W := W))
Tactic: rw [← cancel_mono (F.map φ.s), add_comp, LeftFraction.map_comp_map_s,
    LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, F.map_add]
-- 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
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.LeftFraction₂ X Y
F : Functor.{v_1, v_2, u_1, u_2} C D
hF : W.IsInvertedBy F
inst_3 : Preadditive.{v_2, u_2} D
inst_4 : F.Additive
this : IsIso (F.map (φ.s (W := W)))
rw :
  φ.add (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) =
    (φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF) ≫ F.map (φ.s (W := W))
rw₁ :
  φ.add (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) =
    φ.fst (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
rw₂ :
  F.map (φ.add (W := W).f (W := W)) =
    φ.fst (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
rw₃ :
  F.map (φ.add (W := W).f (W := W)) =
    F.map (φ.fst (W := W).f (W := W)) + φ.snd (W := W).map (W := W) F hF ≫ F.map (φ.s (W := W))
rw₄ : F.map (φ.add (W := W).f (W := W)) = F.map (φ.fst (W := W).f (W := W)) + F.map (φ.snd (W := W).f (W := W))
⊢ φ.add (W := W).map (W := W) F hF = φ.fst (W := W).map (W := W) F hF + φ.snd (W := W).map (W := W) F hF
have rw₅ : F.map (φ.f (W := W)) + F.map (φ.f' (W := W)) = F.map (φ.fst (W := W).f (W := W)) + F.map (φ.snd (W := W).f (W := W))
Tactic: rw [← cancel_mono (F.map φ.s), add_comp, LeftFraction.map_comp_map_s,
    LeftFraction.map_comp_map_s, LeftFraction.map_comp_map_s, F.map_add]
-- 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 ⋯
⊢ neg' W f = φ.neg (W := W).map (W := W) L ⋯
have obtain : ∀ (φ₀ : W.LeftFraction X Y) (hφ : φ₀.map (W := W) L sorry = φ.map (W := W) L sorry)
  (hφ₀ : neg' W (φ₀.map (W := W) L sorry) = φ₀.neg (W := W).map (W := W) L sorry),
  neg' W (φ₀.map (W := W) L sorry) = φ.neg (W := W).map (W := W) L sorry
Tactic: obtain ⟨φ₀, rfl, hφ₀⟩ : ∃ (φ₀ : W.LeftFraction X Y)
    (_ : f = φ₀.map L (inverts L W)),
      neg' W f = φ₀.neg.map L (inverts L W) :=
    ⟨_, (exists_leftFraction L W f).choose_spec, rfl⟩
Cleared hypotheses: f, 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φ : φ₀.map (W := W) L ⋯ = φ.map (W := W) L ⋯
hφ₀ : neg' W (φ₀.map (W := W) L ⋯) = φ₀.neg (W := W).map (W := W) L ⋯
⊢ neg' W (φ₀.map (W := W) L ⋯) = φ.neg (W := W).map (W := W) L ⋯
have hφ₁ : LeftFractionRel (W := W) φ₀ φ
Tactic: rw [MorphismProperty.LeftFraction.map_eq_iff] at hφ
Cleared hypotheses: 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φ : LeftFractionRel (W := W) φ₀ φ
hφ₀ : neg' W (φ₀.map (W := W) L ⋯) = φ₀.neg (W := W).map (W := W) L ⋯
⊢ neg' W (φ₀.map (W := W) L ⋯) = φ.neg (W := W).map (W := W) L ⋯
have obtain : ∀ (Y' : C) (t₁ : φ₀.Y' (W := W) ⟶ Y') (t₂ : φ.Y' (W := W) ⟶ Y') (hst : φ₀.s (W := W) ≫ t₁ = φ.s (W := W) ≫ t₂)
  (hft : φ₀.f (W := W) ≫ t₁ = φ.f (W := W) ≫ t₂) (ht : W (φ₀.s (W := W) ≫ t₁)),
  neg' W (φ₀.map (W := W) L sorry) = φ.neg (W := W).map (W := W) L sorry
Tactic: obtain ⟨Y', t₁, t₂, hst, hft, ht⟩ := 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
φ φ₀ : 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₁)
⊢ neg' W (φ₀.map (W := W) L ⋯) = φ.neg (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φ₀ : 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₁))
⊢ neg' W (φ₀.map (W := W) L ⋯) = φ.neg (W := W).map (W := W) L ⋯
have rw : neg' W (φ₀.map (W := W) L sorry) ≫ L.map (φ₀.s (W := W) ≫ t₁) = φ.neg (W := W).map (W := W) L sorry ≫ L.map (φ₀.s (W := W) ≫ t₁)
Tactic: rw [← 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φ₀ : 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₁))
⊢ neg' W (φ₀.map (W := W) L ⋯) ≫ L.map (φ₀.s (W := W) ≫ t₁) =
    φ.neg (W := W).map (W := W) L ⋯ ≫ L.map (φ₀.s (W := W) ≫ t₁)
have nth_rw : neg' W (φ₀.map (W := W) L sorry) ≫ L.map (φ₀.s (W := W)) ≫ L.map t₁ =
  φ.neg (W := W).map (W := W) L sorry ≫ L.map (φ₀.s (W := W) ≫ t₁)
Tactic: nth_rw 1 [L.map_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 : 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₁))
⊢ 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 : φ₀.neg (W := W).map (W := W) L sorry ≫ L.map (φ₀.s (W := W)) ≫ L.map t₁ =
  φ.neg (W := W).map (W := W) L sorry ≫ L.map (φ₀.s (W := W) ≫ t₁)
Tactic: rw [hφ₀, hst, LeftFraction.map_comp_map_s_assoc, L.map_comp,
    LeftFraction.map_comp_map_s_assoc, ← L.map_comp, ← L.map_comp,
    neg_comp, neg_comp, hft]
-- 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₁)
⊢ 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₁ : φ₀.neg (W := W).map (W := W) L sorry ≫ L.map (φ₀.s (W := W)) ≫ L.map t₁ =
  φ.neg (W := W).map (W := W) L sorry ≫ L.map (φ.s (W := W) ≫ t₂)
Tactic: rw [hφ₀, hst, LeftFraction.map_comp_map_s_assoc, L.map_comp,
    LeftFraction.map_comp_map_s_assoc, ← L.map_comp, ← L.map_comp,
    neg_comp, neg_comp, hft]
-- 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₂)
⊢ 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 (φ₀.neg (W := W).f (W := W)) ≫ L.map t₁ = φ.neg (W := W).map (W := W) L sorry ≫ L.map (φ.s (W := W) ≫ t₂)
Tactic: rw [hφ₀, hst, LeftFraction.map_comp_map_s_assoc, L.map_comp,
    LeftFraction.map_comp_map_s_assoc, ← L.map_comp, ← L.map_comp,
    neg_comp, neg_comp, hft]
-- 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₂)
⊢ 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 (φ₀.neg (W := W).f (W := W)) ≫ L.map t₁ = φ.neg (W := W).map (W := W) L sorry ≫ L.map (φ.s (W := W)) ≫ L.map 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₂
⊢ 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 (φ₀.neg (W := W).f (W := W)) ≫ L.map t₁ = L.map (φ.neg (W := W).f (W := W)) ≫ L.map 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₂
⊢ 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 (φ₀.neg (W := W).f (W := W) ≫ t₁) = L.map (φ.neg (W := W).f (W := W)) ≫ L.map 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₂
⊢ 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 (φ₀.neg (W := W).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]