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
f₁ f₂ : X ⟶ Y
⊢ L.map (f₁ + f₂) = L.map f₁ + L.map f₂
have rw : L.map (f₁ + f₂) = add W (Iso.refl (L.obj X)) (Iso.refl (L.obj Y)) (L.map f₁) (L.map f₂)
Tactic: rw [add_eq W (Iso.refl _) (Iso.refl _) (L.map f₁) (L.map 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
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
⊢ G.Additive ↔ (L ⋙ G).Additive
have mp : G.Additive → (L ⋙ G).Additive
Tactic: constructor
-- 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
mp : G.Additive → (L ⋙ G).Additive
⊢ G.Additive ↔ (L ⋙ G).Additive
have mpr : (L ⋙ G).Additive → G.Additive
Tactic: constructor
-- 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
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
⊢ G.Additive
have refine : ∀ {X Y : D} {f g : X ⟶ Y}, G.map (f + g) = G.map f + G.map g
Tactic: refine ⟨fun {X Y f g} => ?_⟩
-- 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
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
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
⊢ G.map (f + g) = G.map f + G.map g
have hL : L.EssSurj
Tactic: have hL := essSurj L W
-- 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
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
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
⊢ G.map (f + g) = G.map f + G.map g
have eq : G.map
    (HAdd.hAdd (α := L.obj (L.objPreimage X) ⟶ L.obj (L.objPreimage Y))
      (Iso.hom (L.objObjPreimageIso X) ≫ f ≫ Iso.inv (L.objObjPreimageIso Y))
      (Iso.hom (L.objObjPreimageIso X) ≫ g ≫ Iso.inv (L.objObjPreimageIso Y))) =
  HAdd.hAdd (α := G.obj (L.obj (L.objPreimage X)) ⟶ G.obj (L.obj (L.objPreimage Y)))
    (G.map (Iso.hom (L.objObjPreimageIso X) ≫ f ≫ Iso.inv (L.objObjPreimageIso Y)))
    (G.map (Iso.hom (L.objObjPreimageIso X) ≫ g ≫ Iso.inv (L.objObjPreimageIso Y)))
Tactic: have eq := this ((L.objObjPreimageIso X).hom ≫ f ≫ (L.objObjPreimageIso Y).inv)
        ((L.objObjPreimageIso X).hom ≫ g ≫ (L.objObjPreimageIso Y).inv)
-- 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
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
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  G.map
      (HAdd.hAdd (α := L.obj (L.objPreimage X) ⟶ L.obj (L.objPreimage Y))
        (Iso.hom (L.objObjPreimageIso X) ≫ f ≫ Iso.inv (L.objObjPreimageIso Y))
        (Iso.hom (L.objObjPreimageIso X) ≫ g ≫ Iso.inv (L.objObjPreimageIso Y))) =
    HAdd.hAdd (α := G.obj (L.obj (L.objPreimage X)) ⟶ G.obj (L.obj (L.objPreimage Y)))
      (G.map (Iso.hom (L.objObjPreimageIso X) ≫ f ≫ Iso.inv (L.objObjPreimageIso Y)))
      (G.map (Iso.hom (L.objObjPreimageIso X) ≫ g ≫ Iso.inv (L.objObjPreimageIso Y)))
⊢ G.map (f + g) = G.map f + G.map g
have eq₁ : Eq (α := G.obj (L.obj (L.objPreimage X)) ⟶ G.obj (L.obj (L.objPreimage Y)))
  (G.map (Iso.hom (L.objObjPreimageIso X)) ≫ G.map (f + g) ≫ G.map (Iso.inv (L.objObjPreimageIso Y)))
  (G.map (Iso.hom (L.objObjPreimageIso X)) ≫ (G.map f + G.map g) ≫ G.map (Iso.inv (L.objObjPreimageIso Y)))
Tactic: rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp,
        ← comp_add, ← comp_add, ← add_comp, ← add_comp, Functor.map_comp, Functor.map_comp] at eq
Cleared hypotheses: eq
-- 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
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  Eq (α := G.obj (L.obj (L.objPreimage X)) ⟶ G.obj (L.obj (L.objPreimage Y)))
    (G.map (Iso.hom (L.objObjPreimageIso X)) ≫ G.map (f + g) ≫ G.map (Iso.inv (L.objObjPreimageIso Y)))
    (G.map (Iso.hom (L.objObjPreimageIso X)) ≫ (G.map f + G.map g) ≫ G.map (Iso.inv (L.objObjPreimageIso Y)))
⊢ G.map (f + g) = G.map f + G.map g
have rw : Eq (α := G.obj X ⟶ G.obj (L.obj (L.objPreimage Y))) (G.map (f + g) ≫ G.map (Iso.inv (L.objObjPreimageIso Y)))
  ((G.map f + G.map g) ≫ G.map (Iso.inv (L.objObjPreimageIso Y)))
Tactic: rw [← cancel_mono (G.map (L.objObjPreimageIso Y).inv),
        ← cancel_epi (G.map (L.objObjPreimageIso X).hom), eq]
-- 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
this : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
X Y : D
f g : X ⟶ Y
hL : L.EssSurj
eq :
  Eq (α := G.obj (L.obj (L.objPreimage X)) ⟶ G.obj (L.obj (L.objPreimage Y)))
    (G.map (Iso.hom (L.objObjPreimageIso X)) ≫ G.map (f + g) ≫ G.map (Iso.inv (L.objObjPreimageIso Y)))
    (G.map (Iso.hom (L.objObjPreimageIso X)) ≫ (G.map f + G.map g) ≫ G.map (Iso.inv (L.objObjPreimageIso Y)))
rw :
  Eq (α := G.obj X ⟶ G.obj (L.obj (L.objPreimage Y))) (G.map (f + g) ≫ G.map (Iso.inv (L.objObjPreimageIso Y)))
    ((G.map f + G.map g) ≫ G.map (Iso.inv (L.objObjPreimageIso Y)))
rw₁ :
  Eq (α := G.obj (L.obj (L.objPreimage X)) ⟶ G.obj (L.obj (L.objPreimage Y)))
    (G.map (Iso.hom (L.objObjPreimageIso X)) ≫ G.map (f + g) ≫ G.map (Iso.inv (L.objObjPreimageIso Y)))
    (G.map (Iso.hom (L.objObjPreimageIso X)) ≫ (G.map f + G.map g) ≫ G.map (Iso.inv (L.objObjPreimageIso Y)))
⊢ G.map (f + g) = G.map f + G.map g
have rw₂ : Eq (α := G.obj (L.obj (L.objPreimage X)) ⟶ G.obj (L.obj (L.objPreimage Y)))
  (G.map (Iso.hom (L.objObjPreimageIso X)) ≫ (G.map f + G.map g) ≫ G.map (Iso.inv (L.objObjPreimageIso Y)))
  (G.map (Iso.hom (L.objObjPreimageIso X)) ≫ (G.map f + G.map g) ≫ G.map (Iso.inv (L.objObjPreimageIso Y)))
Tactic: rw [← cancel_mono (G.map (L.objObjPreimageIso Y).inv),
        ← cancel_epi (G.map (L.objObjPreimageIso X).hom), eq]
-- 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
⊢ G.Additive
have mpr : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
Tactic: suffices ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g by
      refine ⟨fun {X Y f g} => ?_⟩
      have hL := essSurj L W
      have eq := this ((L.objObjPreimageIso X).hom ≫ f ≫ (L.objObjPreimageIso Y).inv)
        ((L.objObjPreimageIso X).hom ≫ g ≫ (L.objObjPreimageIso Y).inv)
      rw [Functor.map_comp, Functor.map_comp, Functor.map_comp, Functor.map_comp,
        ← comp_add, ← comp_add, ← add_comp, ← add_comp, Functor.map_comp, Functor.map_comp] at eq
      rw [← cancel_mono (G.map (L.objObjPreimageIso Y).inv),
        ← cancel_epi (G.map (L.objObjPreimageIso X).hom), eq]
-- 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
f g : L.obj X ⟶ L.obj Y
⊢ G.map (f + g) = G.map f + G.map g
have mpr : ∀ (φ : W.LeftFraction₂ X Y),
  G.map (φ.fst (W := W).map (W := W) L sorry + φ.snd (W := W).map (W := W) L sorry) =
    G.map (φ.fst (W := W).map (W := W) L sorry) + G.map (φ.snd (W := W).map (W := W) L sorry)
Tactic: obtain ⟨φ, rfl, rfl⟩ := exists_leftFraction₂ L W f g
Cleared hypotheses: f, 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
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
⊢ 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 (φ.add (W := W).map (W := W) L sorry) =
  G.map (φ.fst (W := W).map (W := W) L sorry) + G.map (φ.snd (W := W).map (W := W) L sorry)
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 ⋯)
⊢ 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 (φ.add (W := W).map (W := W) L sorry) ≫ G.map (L.map (φ.s (W := W))) =
  (G.map (φ.fst (W := W).map (W := W) L sorry) + G.map (φ.snd (W := W).map (W := W) L sorry)) ≫ G.map (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)))
⊢ 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 (φ.add (W := W).map (W := W) L sorry ≫ L.map (φ.s (W := W))) =
  (G.map (φ.fst (W := W).map (W := W) L sorry) + G.map (φ.snd (W := W).map (W := W) L sorry)) ≫ G.map (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)))
⊢ 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 (φ.add (W := W).map (W := W) L sorry ≫ L.map (φ.s (W := W))) =
  G.map (φ.fst (W := W).map (W := W) L sorry) ≫ G.map (L.map (φ.s (W := W))) +
    G.map (φ.snd (W := W).map (W := W) L sorry) ≫ G.map (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)))
⊢ 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 (φ.add (W := W).map (W := W) L sorry ≫ L.map (φ.s (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) ≫ G.map (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)))
⊢ 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 (φ.add (W := W).map (W := W) L sorry ≫ L.map (φ.s (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]