awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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
this : Preadditive.{v_2, u_2} D := preadditive L W
⊢ ∀ {X Y : C} {f g : X ⟶ Y}, L.map (f + g) = L.map f + L.map g

Tactic:
apply Preadditive.map_add

Premises used: CategoryTheory.Localization.Preadditive.map_add
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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
mpr : (L ⋙ G).Additive → G.Additive
⊢ G.Additive ↔ (L ⋙ G).Additive

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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 : G.Additive
⊢ (L ⋙ G).Additive

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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

Tactic:
⟨fun {X Y f g} => ?_⟩

Premises used: CategoryTheory.Functor.Additive.mk
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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
refine : ∀ {X Y : D} {f g : X ⟶ Y}, G.map (f + g) = G.map f + G.map g
⊢ G.Additive

Tactic:
refine ⟨fun {X Y f g} => ?_⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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
⊢ L.EssSurj

Tactic:
have hL := essSurj L W
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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
      (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)
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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)))
⊢ 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

Premises used: CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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)))
rw₂ 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)))
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
rw [← cancel_mono (G.map (L.objObjPreimageIso Y).inv),
        ← cancel_epi (G.map (L.objObjPreimageIso X).hom), eq]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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
mpr : ∀ ⦃X Y : C⦄ (f g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g
⊢ G.Additive

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]
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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
mpr :
  ∀ (φ : 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 ⋯)
⊢ G.map (f + g) = G.map f + G.map g

Tactic:
obtain ⟨φ, rfl, rfl⟩ := exists_leftFraction₂ L W f g

Premises used: CategoryTheory.Localization.exists_leftFraction₂, rfl
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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
⊢ W.Q.Additive

Tactic:
functor_additive W.Q W

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.functor_additive
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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
inst_5 : HasZeroObject.{v_1, u_1} C
⊢ HasZeroObject W.Localization

Tactic:
W.Q.hasZeroObject_of_additive

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.hasZeroObject_of_additive
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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
inst_5 : HasLocalization.{u_3, v_1, u_1} W
⊢ Functor.Additive.{v_1, u_1, u_3, u_1} (D := Localization'.{u_3, v_1, u_1} W) W.Q'

Tactic:
functor_additive W.Q' W

Premises used: CategoryTheory.MorphismProperty.Q', CategoryTheory.Localization.functor_additive
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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
inst_5 : HasLocalization.{u_3, v_1, u_1} W
inst_6 : HasZeroObject.{v_1, u_1} C
⊢ HasZeroObject.{u_3, u_1} (Localization'.{u_3, v_1, u_1} W)

Tactic:
W.Q'.hasZeroObject_of_additive

Premises used: CategoryTheory.Functor.hasZeroObject_of_additive, CategoryTheory.MorphismProperty.Q'
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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 : L.map (f - g) = 0
⊢ L.map f = L.map g

Tactic:
rw [← sub_eq_zero, ← L.map_sub]

Premises used: sub_eq_zero, CategoryTheory.Functor.map_sub
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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
rw₃ rw₄ : Eq.{v_3 + 1} (α := F.obj (L.obj X₁) ⟶ F.obj (L.obj X₂)) 0 0
⊢ F.map (L.map (f - g)) = 0

Tactic:
rw [L.map_sub, F.map_sub, hfg, sub_self]

Premises used: sub_self, CategoryTheory.Functor.map_sub
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
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 - g) = 0

Tactic:
exact h _ (by rw [L.map_sub, F.map_sub, hfg, sub_self])
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
X Y : C
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : L.IsLocalization W
z : W.LeftFraction X Y
⊢ IsIso (L.map (z.s (W := W)))

Tactic:
Localization.inverts L W _ z.hs

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.Localization.inverts
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.LeftFraction X Y
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
this : IsIso (L.map (φ.s (W := W))) := ⋯
⊢ φ.map (W := W) L hL ≫ L.map (φ.s (W := W)) = L.map (φ.f (W := W))

Tactic:
simp [map]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
X Y : C
f : X ⟶ Y
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
inst_2 : W.ContainsIdentities
⊢ (ofHom W f).map (W := W) L hL = L.map f

Tactic:
simp [map]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
X Y : C
s : Y ⟶ X
hs : W s
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
this : IsIso (L.map s) := ⋯
⊢ (ofInv (W := W) s hs).map (W := W) L hL ≫ L.map s = 𝟙 (L.obj X)

Tactic:
simp [map]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
X Y : C
s : Y ⟶ X
hs : W s
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
this : IsIso (L.map s) := ⋯
⊢ L.map s ≫ (ofInv (W := W) s hs).map (W := W) L hL = 𝟙 (L.obj Y)

Tactic:
simp [map]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
α : W.LeftFraction X Y
⊢ ∃ (Y' : C) (f : X ⟶ Y') (s : Y ⟶ Y') (hs : W s), α = mk (W := W) f s hs

Tactic:
⟨_, _, _, _, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
X Y : C
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_2 : L.IsLocalization W
z : W.RightFraction X Y
⊢ IsIso (L.map (z.s (W := W)))

Tactic:
Localization.inverts L W _ z.hs

Premises used: CategoryTheory.Localization.inverts, CategoryTheory.MorphismProperty.RightFraction.hs
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.RightFraction X Y
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
this : IsIso (L.map (φ.s (W := W))) := ⋯
⊢ L.map (φ.s (W := W)) ≫ φ.map (W := W) L hL = L.map (φ.f (W := W))

Tactic:
simp [map]

Premises used: CategoryTheory.MorphismProperty.RightFraction.map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
X Y : C
f : X ⟶ Y
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
inst_2 : W.ContainsIdentities
⊢ (ofHom W f).map (W := W) L hL = L.map f

Tactic:
simp [map]

Premises used: CategoryTheory.MorphismProperty.RightFraction.map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
X Y : C
s : Y ⟶ X
hs : W s
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
this : IsIso (L.map s) := ⋯
⊢ (ofInv (W := W) s hs).map (W := W) L hL ≫ L.map s = 𝟙 (L.obj X)

Tactic:
simp [map]

Premises used: CategoryTheory.MorphismProperty.RightFraction.map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
X Y : C
s : Y ⟶ X
hs : W s
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
this : IsIso (L.map s) := ⋯
⊢ L.map s ≫ (ofInv (W := W) s hs).map (W := W) L hL = 𝟙 (L.obj Y)

Tactic:
simp [map]

Premises used: CategoryTheory.MorphismProperty.RightFraction.map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
α : W.RightFraction X Y
⊢ ∃ (X' : C) (s : X' ⟶ X) (hs : W s) (f : X' ⟶ Y), α = mk (W := W) s hs f

Tactic:
⟨_, _, _, _, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.HasLeftCalculusOfFractions
X Y : C
φ : W.RightFraction X Y
⊢ ∃ (ψ : W.LeftFraction X Y), φ.f (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f (W := W)

Tactic:
HasLeftCalculusOfFractions.exists_leftFraction φ

Premises used: CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.HasLeftCalculusOfFractions
X Y : C
φ : W.RightFraction X Y
⊢ φ.f (W := W) ≫ φ.leftFraction (W := W).s (W := W) = φ.s (W := W) ≫ φ.leftFraction (W := W).f (W := W)

Tactic:
φ.exists_leftFraction.choose_spec

Premises used: Exists.choose_spec, CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.HasRightCalculusOfFractions
X Y : C
φ : W.LeftFraction X Y
⊢ ∃ (ψ : W.RightFraction X Y), ψ.s (W := W) ≫ φ.f (W := W) = ψ.f (W := W) ≫ φ.s (W := W)

Tactic:
HasRightCalculusOfFractions.exists_rightFraction φ

Premises used: CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.exists_rightFraction
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.HasRightCalculusOfFractions
X Y : C
φ : W.LeftFraction X Y
⊢ φ.rightFraction (W := W).s (W := W) ≫ φ.f (W := W) = φ.rightFraction (W := W).f (W := W) ≫ φ.s (W := W)

Tactic:
φ.exists_rightFraction.choose_spec

Premises used: Exists.choose_spec, CategoryTheory.MorphismProperty.LeftFraction.exists_rightFraction
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z : W.LeftFraction X Y
⊢ W (z.s (W := W) ≫ 𝟙 (z.Y' (W := W)))

Tactic:
simpa only [Category.comp_id] using z.hs

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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₂
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₁
⊢ LeftFractionRel (W := W) z₂ z₁

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
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
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₁)
⊢ W (z₂.s (W := W) ≫ t₂)

Tactic:
simpa only [← hst] using ht