awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
h₃ : z₂.f (W := W) ≫ z₃.s (W := W) = z₁.s (W := W) ≫ z₃.f (W := W)
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization W
this : IsIso (L.map (z₂.s (W := W) ≫ z₃.s (W := W)))
rw :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯ ≫
      L.map (z₂.s (W := W) ≫ z₃.s (W := W))
rw₁ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₂ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₃ :
  z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₄ :
  z₁.map (W := W) L ⋯ ≫ L.map (z₂.f (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₅ :
  z₁.map (W := W) L ⋯ ≫ L.map (z₂.f (W := W) ≫ z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₆ :
  z₁.map (W := W) L ⋯ ≫ L.map (z₁.s (W := W) ≫ z₃.f (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₇ :
  z₁.map (W := W) L ⋯ ≫ L.map (z₁.s (W := W)) ≫ L.map (z₃.f (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₈ :
  L.map (z₁.f (W := W)) ≫ L.map (z₃.f (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₉ rw₁₀ : L.map (z₁.f (W := W)) ≫ L.map (z₃.f (W := W)) = L.map (z₁.f (W := W)) ≫ L.map (z₃.f (W := W))
⊢ z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯

Tactic:
rw [← cancel_mono (L.map (z₂.s ≫ z₃.s)), map_comp_map_s,
    L.map_comp, assoc, map_comp_map_s_assoc, ← L.map_comp, h₃,
    L.map_comp, map_comp_map_s_assoc, L.map_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W
e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L :=
  compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W
⊢ f = e.inv.app X ≫ (e.hom.app X ≫ f ≫ e.inv.app Y) ≫ e.hom.app Y

Tactic:
simp
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W
e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L :=
  compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W
obtain :
  ∀ (f' : E.functor.obj X ⟶ E.functor.obj Y),
    ∃ (φ : W.LeftFraction X Y), e.inv.app X ≫ f' ≫ e.hom.app Y = φ.map (W := W) L ⋯
⊢ ∃ (φ : W.LeftFraction X Y), f = φ.map (W := W) L ⋯

Tactic:
obtain ⟨f', rfl⟩ : ∃ (f' : E.functor.obj X ⟶ E.functor.obj Y),
      f = e.inv.app _ ≫ f' ≫ e.hom.app _ := ⟨e.hom.app _ ≫ f ≫ e.inv.app _, by simp⟩

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W
e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L :=
  compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W
f' : E.functor.obj X ⟶ E.functor.obj Y
obtain : ∀ (g : X ⟶ Y), ∃ (φ : W.LeftFraction X Y), e.inv.app X ≫ E.functor.map g ≫ e.hom.app Y = φ.map (W := W) L ⋯
⊢ ∃ (φ : W.LeftFraction X Y), e.inv.app X ≫ f' ≫ e.hom.app Y = φ.map (W := W) L ⋯

Tactic:
obtain ⟨g, rfl⟩ := E.functor.map_surjective f'

Premises used: CategoryTheory.Equivalence.functor, rfl, CategoryTheory.Functor.map_surjective
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W
e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L :=
  compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W
g : X ⟶ Y
obtain :
  ∀ (g : W.LeftFraction X Y),
    ∃ (φ : W.LeftFraction X Y),
      e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk (W := W) g) ≫ e.hom.app Y =
        φ.map (W := W) L ⋯
⊢ ∃ (φ : W.LeftFraction X Y), e.inv.app X ≫ E.functor.map g ≫ e.hom.app Y = φ.map (W := W) L ⋯

Tactic:
obtain ⟨g, rfl⟩ := MorphismProperty.LeftFraction.Localization.Hom.mk_surjective g

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk_surjective, 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W
e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L :=
  compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W
g : W.LeftFraction X Y
⊢ ∃ (φ : W.LeftFraction X Y),
    e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk (W := W) g) ≫ e.hom.app Y =
      φ.map (W := W) L ⋯

Tactic:
⟨g, ?_⟩

Premises used: Exists.intro
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W
e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L :=
  compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W
g : W.LeftFraction X Y
refine :
  e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk (W := W) g) ≫ e.hom.app Y =
    g.map (W := W) L ⋯
⊢ ∃ (φ : W.LeftFraction X Y),
    e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk (W := W) g) ≫ e.hom.app Y =
      φ.map (W := W) L ⋯

Tactic:
refine ⟨g, ?_⟩
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
E : MorphismProperty.LeftFraction.Localization W ≌ D := uniq (MorphismProperty.LeftFraction.Localization.Q W) L W
e : MorphismProperty.LeftFraction.Localization.Q W ⋙ E.functor ≅ L :=
  compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W
g : W.LeftFraction X Y
rw :
  e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.homMk (W := W) g) ≫ e.hom.app Y =
    g.map (W := W) L ⋯
rw₁ :
  e.inv.app X ≫ E.functor.map (g.map (W := W) (MorphismProperty.LeftFraction.Localization.Q W) ⋯) ≫ e.hom.app Y =
    g.map (W := W) L ⋯
rw₂ :
  e.inv.app X ≫
      (NatTrans.app (Iso.hom (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) X ≫
          g.map (W := W) L ⋯ ≫
            NatTrans.app (Iso.inv (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) Y) ≫
        e.hom.app Y =
    g.map (W := W) L ⋯
rw₃ :
  e.inv.app X ≫
      NatTrans.app (Iso.hom (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) X ≫
        (g.map (W := W) L ⋯ ≫
            NatTrans.app (Iso.inv (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) Y) ≫
          e.hom.app Y =
    g.map (W := W) L ⋯
rw₄ :
  e.inv.app X ≫
      NatTrans.app (Iso.hom (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) X ≫
        g.map (W := W) L ⋯ ≫
          NatTrans.app (Iso.inv (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) Y ≫
            e.hom.app Y =
    g.map (W := W) L ⋯
rw₅ :
  e.inv.app X ≫
      NatTrans.app (Iso.hom (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) X ≫
        g.map (W := W) L ⋯ ≫ 𝟙 (L.obj Y) =
    g.map (W := W) L ⋯
rw₆ :
  e.inv.app X ≫
      NatTrans.app (Iso.hom (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) X ≫
        g.map (W := W) L ⋯ =
    g.map (W := W) L ⋯
rw₇ rw₈ : g.map (W := W) L ⋯ = g.map (W := W) L ⋯
⊢ e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk (W := W) g) ≫ e.hom.app Y =
    g.map (W := W) L ⋯

Tactic:
rw [← MorphismProperty.LeftFraction.Localization.homMk_eq_hom_mk,
    MorphismProperty.LeftFraction.Localization.homMk_eq g,
    g.map_compatibility (MorphismProperty.LeftFraction.Localization.Q W) L,
    assoc, assoc, Iso.inv_hom_id_app, comp_id, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map_compatibility, CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.MorphismProperty.LeftFraction.Localization.Q, CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_hom_mk, CategoryTheory.Iso.inv_hom_id_app_assoc
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
mp : φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯ → LeftFractionRel (W := W) φ ψ
mpr : LeftFractionRel (W := W) φ ψ → φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯
⊢ φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯ ↔ LeftFractionRel (W := W) φ ψ

Tactic:
constructor
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
h : φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯
mp :
  Eq (α := Functor.obj (Localization.Q W) X ⟶ Functor.obj (Localization.Q W) Y) (φ.map (W := W) (Localization.Q W) ⋯)
    (ψ.map (W := W) (Localization.Q W) ⋯)
⊢ LeftFractionRel (W := W) φ ψ

Tactic:
rw [← MorphismProperty.LeftFraction.Localization.map_eq_iff]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.map_eq_iff
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
h : φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯
⊢ Eq (α := Functor.obj (Localization.Q W) X ⟶ Functor.obj (Localization.Q W) Y) (φ.map (W := W) (Localization.Q W) ⋯)
    (ψ.map (W := W) (Localization.Q W) ⋯)

Tactic:
apply map_eq_of_map_eq _ _ _ _ h

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map_eq_of_map_eq
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
h : LeftFractionRel (W := W) φ ψ
mpr : Localization.Hom.mk (W := W) φ = Localization.Hom.mk (W := W) ψ
⊢ (Localization.Hom.mk (W := W) φ).map (W := W) L ⋯ = (Localization.Hom.mk (W := W) ψ).map (W := W) L ⋯

Tactic:
congr 1
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
h : LeftFractionRel (W := W) φ ψ
⊢ Localization.Hom.mk (W := W) φ = Localization.Hom.mk (W := W) ψ

Tactic:
Quot.sound h

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk, Quot.sound, CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction X Y
h : LeftFractionRel (W := W) φ ψ
⊢ Localization.Hom.mk (W := W) φ = Localization.Hom.mk (W := W) ψ

Tactic:
exact Quot.sound h

Premises used: Quot.sound
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
mp : L.map f₁ = L.map f₂ → ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s
mpr : (∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s) → L.map f₁ = L.map f₂
⊢ L.map f₁ = L.map f₂ ↔ ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s

Tactic:
constructor
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
h : L.map f₁ = L.map f₂
⊢ LeftFractionRel (W := W) (LeftFraction.ofHom W f₁) (LeftFraction.ofHom W f₂)

Tactic:
rw [← LeftFraction.map_ofHom W _ L (Localization.inverts _ _),
      ← LeftFraction.map_ofHom W _ L (Localization.inverts _ _),
      LeftFraction.map_eq_iff] at h

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map_ofHom, CategoryTheory.MorphismProperty.LeftFraction.map_eq_iff, 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
h : LeftFractionRel (W := W) (LeftFraction.ofHom W f₁) (LeftFraction.ofHom W f₂)
mp :
  ∀ (Z : C) (t₁ : (LeftFraction.ofHom W f₁).Y' (W := W) ⟶ Z) (t₂ : (LeftFraction.ofHom W f₂).Y' (W := W) ⟶ Z)
    (hst : (LeftFraction.ofHom W f₁).s (W := W) ≫ t₁ = (LeftFraction.ofHom W f₂).s (W := W) ≫ t₂)
    (hft : (LeftFraction.ofHom W f₁).f (W := W) ≫ t₁ = (LeftFraction.ofHom W f₂).f (W := W) ≫ t₂)
    (ht : W ((LeftFraction.ofHom W f₁).s (W := W) ≫ t₁)), ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s
⊢ ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
Z : C
t₁ t₂ : Y ⟶ Z
hst : 𝟙 Y ≫ t₁ = 𝟙 Y ≫ t₂
hft : f₁ ≫ t₁ = f₂ ≫ t₂
ht : W (𝟙 Y ≫ t₁)
⊢ ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s

Tactic:
grind
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
Z : C
s : Y ⟶ Z
hs : W s
fac : f₁ ≫ s = f₂ ≫ s
⊢ L.map f₁ = L.map f₂

Tactic:
simp only [← cancel_mono (Localization.isoOfHom L W s hs).hom,
      Localization.isoOfHom_hom, ← L.map_comp, fac]

Premises used: CategoryTheory.Localization.isoOfHom_hom, CategoryTheory.cancel_mono, CategoryTheory.Localization.isoOfHom, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.hom
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
f : Arrow.{v_2, u_2} D
⊢ L.EssSurj

Tactic:
have := Localization.essSurj L W
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.EssSurj
⊢ ∃ (X : C), Nonempty.{v_2 + 1} (L.obj X ≅ f.left)

Tactic:
⟨_, ⟨L.objObjPreimageIso f.left⟩⟩

Premises used: CategoryTheory.Arrow.left, Nonempty.intro, CategoryTheory.Functor.objObjPreimageIso, Exists.intro
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.EssSurj
obtain : ∀ (X : C) (eX : L.obj X ≅ f.left), L.mapArrow.essImage f
⊢ L.mapArrow.essImage f

Tactic:
obtain ⟨X, ⟨eX⟩⟩ : ∃ (X : C), Nonempty (L.obj X ≅ f.left) :=
      ⟨_, ⟨L.objObjPreimageIso f.left⟩⟩
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
⊢ ∃ (Y : C), Nonempty.{v_2 + 1} (L.obj Y ≅ f.right)

Tactic:
⟨_, ⟨L.objObjPreimageIso f.right⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Functor.objObjPreimageIso, Exists.intro, CategoryTheory.Arrow.right
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
obtain : ∀ (Y : C) (eY : L.obj Y ≅ f.right), L.mapArrow.essImage f
⊢ L.mapArrow.essImage f

Tactic:
obtain ⟨Y, ⟨eY⟩⟩ : ∃ (Y : C), Nonempty (L.obj Y ≅ f.right) :=
      ⟨_, ⟨L.objObjPreimageIso f.right⟩⟩
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
obtain : ∀ (φ : W.LeftFraction X Y) (hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map (W := W) L ⋯), L.mapArrow.essImage f
⊢ L.mapArrow.essImage f

Tactic:
obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L W (eX.hom ≫ f.hom ≫ eY.inv)

Premises used: CategoryTheory.Arrow.hom, CategoryTheory.Localization.exists_leftFraction, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map (W := W) L ⋯
⊢ L.mapArrow.essImage f

Tactic:
⟨Arrow.mk φ.f, ⟨Iso.symm ?_⟩⟩

Premises used: CategoryTheory.Functor.essImage, Nonempty.intro, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.MorphismProperty.LeftFraction.f, CategoryTheory.Arrow.mk
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map (W := W) L ⋯
refine : f ≅ L.mapArrow.obj (Arrow.mk (φ.f (W := W)))
⊢ L.mapArrow.essImage f

Tactic:
refine ⟨Arrow.mk φ.f, ⟨Iso.symm ?_⟩⟩
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
f : Arrow.{v_2, u_2} D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map (W := W) L ⋯
refine :
  eX.symm.hom ≫ (L.mapArrow.obj (Arrow.mk (φ.f (W := W)))).hom = f.hom ≫ (eY.symm ≪≫ isoOfHom L W (φ.s (W := W)) ⋯).hom
⊢ f ≅ L.mapArrow.obj (Arrow.mk (φ.f (W := W)))

Tactic:
refine Arrow.isoMk eX.symm (eY.symm ≪≫ Localization.isoOfHom L W φ.s φ.hs) ?_

Premises used: CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Arrow.isoMk