awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ Hom.mk (W := W) f = homMk (W := W) (mk (W := W) (f.f (W := W)) (f.s (W := W)) ⋯)

Tactic:
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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
rw :
  F₁.map (Functor.map (Q W) (f.f (W := W))) ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) =
    eqToHom ⋯ ≫ F₂.map (Functor.map (Q W) (f.f (W := W))) ≫ F₂.map (Qinv (W := W) (f.s (W := W)) ⋯) ≫ eqToHom ⋯
⊢ F₁.map (Hom.mk (W := W) f) = eqToHom ⋯ ≫ F₂.map (Hom.mk (W := W) f) ≫ eqToHom ⋯

Tactic:
rw [show Hom.mk f = homMk (mk f.f f.s f.hs) by rfl,
      ← Q_map_comp_Qinv f.f f.s f.hs, F₁.map_comp, F₂.map_comp, assoc]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.Category.assoc, CategoryTheory.MorphismProperty.LeftFraction.f, CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map_comp_Qinv
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
erw :
  (eqToHom ⋯ ≫ (Q W ⋙ F₂).map (f.f (W := W)) ≫ eqToHom ⋯) ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) =
    eqToHom ⋯ ≫ F₂.map (Functor.map (Q W) (f.f (W := W))) ≫ F₂.map (Qinv (W := W) (f.s (W := W)) ⋯) ≫ eqToHom ⋯
⊢ F₁.map (Functor.map (Q W) (f.f (W := W))) ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) =
    eqToHom ⋯ ≫ F₂.map (Functor.map (Q W) (f.f (W := W))) ≫ F₂.map (Qinv (W := W) (f.s (W := W)) ⋯) ≫ eqToHom ⋯

Tactic:
erw [Functor.congr_hom h f.f]

Premises used: CategoryTheory.Functor.congr_hom, CategoryTheory.MorphismProperty.LeftFraction.f
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
rw :
  eqToHom ⋯ ≫ (Q W ⋙ F₂).map (f.f (W := W)) ≫ eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) =
    eqToHom ⋯ ≫ F₂.map (Functor.map (Q W) (f.f (W := W))) ≫ F₂.map (Qinv (W := W) (f.s (W := W)) ⋯) ≫ eqToHom ⋯
⊢ (eqToHom ⋯ ≫ (Q W ⋙ F₂).map (f.f (W := W)) ≫ eqToHom ⋯) ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) =
    eqToHom ⋯ ≫ F₂.map (Functor.map (Q W) (f.f (W := W))) ≫ F₂.map (Qinv (W := W) (f.s (W := W)) ⋯) ≫ eqToHom ⋯

Tactic:
rw [assoc, assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
e_a : eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) = F₂.map (Qinv (W := W) (f.s (W := W)) ⋯) ≫ eqToHom ⋯
⊢ eqToHom ⋯ ≫ (Q W ⋙ F₂).map (f.f (W := W)) ≫ eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) =
    eqToHom ⋯ ≫ F₂.map (Functor.map (Q W) (f.f (W := W))) ≫ F₂.map (Qinv (W := W) (f.s (W := W)) ⋯) ≫ eqToHom ⋯

Tactic:
congr 2
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ IsIso (X := Functor.obj (Q W) Y) (Functor.map (Q W) (f.s (W := W)))

Tactic:
have := inverts W _ f.hs
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso (X := Functor.obj (Q W) Y) (Functor.map (Q W) (f.s (W := W)))
e_a : F₂.map (Functor.map (Q W) (f.s (W := W))) ≫ eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) = eqToHom ⋯
⊢ eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) = F₂.map (Qinv (W := W) (f.s (W := W)) ⋯) ≫ eqToHom ⋯

Tactic:
rw [← cancel_epi (F₂.map ((Q W).map f.s)), ← F₂.map_comp_assoc,
      Qiso_hom_inv_id, Functor.map_id, id_comp]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_hom_inv_id, CategoryTheory.MorphismProperty.LeftFraction.Localization.Q, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_id, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.cancel_epi, CategoryTheory.Category.id_comp
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso (X := Functor.obj (Q W) Y) (Functor.map (Q W) (f.s (W := W)))
e_a :
  (eqToHom ⋯ ≫ (Q W ⋙ F₁).map (f.s (W := W)) ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) =
    eqToHom ⋯
⊢ F₂.map (Functor.map (Q W) (f.s (W := W))) ≫ eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) = eqToHom ⋯

Tactic:
erw [Functor.congr_hom h.symm f.s]

Premises used: CategoryTheory.Functor.congr_hom, CategoryTheory.MorphismProperty.LeftFraction.s, Eq.symm
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso (X := Functor.obj (Q W) Y) (Functor.map (Q W) (f.s (W := W)))
e_a :
  (eqToHom ⋯ ≫ F₁.map (Functor.map (Q W) (f.s (W := W))) ≫ eqToHom ⋯) ≫
      eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) =
    eqToHom ⋯
⊢ (eqToHom ⋯ ≫ (Q W ⋙ F₁).map (f.s (W := W)) ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) =
    eqToHom ⋯

Tactic:
dsimp
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso (X := Functor.obj (Q W) Y) (Functor.map (Q W) (f.s (W := W)))
e_a : eqToHom ⋯ ≫ F₁.map (𝟙 (Functor.obj (Q W) Y)) = eqToHom ⋯
⊢ (eqToHom ⋯ ≫ F₁.map (Functor.map (Q W) (f.s (W := W))) ≫ eqToHom ⋯) ≫
      eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) =
    eqToHom ⋯

Tactic:
rw [assoc, assoc, eqToHom_trans_assoc, eqToHom_refl, id_comp, ← F₁.map_comp,
      Qiso_hom_inv_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_hom_inv_id, CategoryTheory.eqToHom_refl, CategoryTheory.Functor.map_comp, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.Category.id_comp
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso (X := Functor.obj (Q W) Y) (Functor.map (Q W) (f.s (W := W)))
e_a : eqToHom ⋯ ≫ F₁.map (𝟙 Y) = eqToHom ⋯
⊢ eqToHom ⋯ ≫ F₁.map (𝟙 (Functor.obj (Q W) Y)) = eqToHom ⋯

Tactic:
dsimp
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso (X := Functor.obj (Q W) Y) (Functor.map (Q W) (f.s (W := W)))
e_a : Eq.{v_3 + 1} (α := F₂.obj Y ⟶ F₁.obj Y) (eqToHom ⋯ ≫ 𝟙 (F₁.obj Y)) (eqToHom ⋯)
e_a₁ e_a₂ : Eq.{v_3 + 1} (α := F₂.obj Y ⟶ F₁.obj Y) (eqToHom ⋯) (eqToHom ⋯)
⊢ eqToHom ⋯ ≫ F₁.map (𝟙 Y) = eqToHom ⋯

Tactic:
rw [F₁.map_id, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id
-- 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
E : Type u_3
inst_3 : Category.{v_3, u_3} E
⊢ Functor.IsLocalization (Q W) W

Tactic:
Functor.IsLocalization.mk' _ _
    (strictUniversalPropertyFixedTarget W _)
    (strictUniversalPropertyFixedTarget W _)

Premises used: CategoryTheory.Functor.IsLocalization.mk', CategoryTheory.MorphismProperty.LeftFraction.Localization.strictUniversalPropertyFixedTarget
-- 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
f : W.LeftFraction X Y
rw :
  Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y)
    (Functor.map (Q W) (f.f (W := W)) ≫ Qinv (W := W) (f.s (W := W)) ⋯) (f.map (W := W) (Q W) ⋯)
rw₁ :
  Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) (f.Y' (W := W)))
    ((Functor.map (Q W) (f.f (W := W)) ≫ Qinv (W := W) (f.s (W := W)) ⋯) ≫ Functor.map (Q W) (f.s (W := W)))
    (f.map (W := W) (Q W) ⋯ ≫ Functor.map (Q W) (f.s (W := W)))
rw₂ :
  Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) (f.Y' (W := W)))
    (Functor.map (Q W) (f.f (W := W)) ≫ Qinv (W := W) (f.s (W := W)) ⋯ ≫ Functor.map (Q W) (f.s (W := W)))
    (f.map (W := W) (Q W) ⋯ ≫ Functor.map (Q W) (f.s (W := W)))
rw₃ :
  Functor.map (Q W) (f.f (W := W)) ≫ 𝟙 (Functor.obj (Q W) (f.Y' (W := W))) =
    f.map (W := W) (Q W) ⋯ ≫ Functor.map (Q W) (f.s (W := W))
rw₄ :
  Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) (f.Y' (W := W))) (Functor.map (Q W) (f.f (W := W)))
    (f.map (W := W) (Q W) ⋯ ≫ Functor.map (Q W) (f.s (W := W)))
rw₅ rw₆ :
  Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) (f.Y' (W := W))) (Functor.map (Q W) (f.f (W := W)))
    (Functor.map (Q W) (f.f (W := W)))
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (homMk (W := W) f) (f.map (W := W) (Q W) ⋯)

Tactic:
rw [← Q_map_comp_Qinv f.f f.s f.hs, ← cancel_mono ((Q W).map f.s),
    assoc, Qiso_inv_hom_id, comp_id, map_comp_map_s]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.MorphismProperty.LeftFraction.Localization.Q, CategoryTheory.Functor.map, CategoryTheory.MorphismProperty.LeftFraction.f, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso_inv_hom_id, CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map_comp_Qinv
-- 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
f g : W.LeftFraction X Y
mp :
  Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) ((Hom.mk (W := W) f).map (W := W) (Q W) ⋯)
      ((Hom.mk (W := W) g).map (W := W) (Q W) ⋯) →
    LeftFractionRel (W := W) f g
mpr :
  LeftFractionRel (W := W) f g →
    Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) ((Hom.mk (W := W) f).map (W := W) (Q W) ⋯)
      ((Hom.mk (W := W) g).map (W := W) (Q W) ⋯)
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) ((Hom.mk (W := W) f).map (W := W) (Q W) ⋯)
      ((Hom.mk (W := W) g).map (W := W) (Q W) ⋯) ↔
    LeftFractionRel (W := W) f g

Tactic:
constructor
-- 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
f g : W.LeftFraction X Y
h :
  Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) ((Hom.mk (W := W) f).map (W := W) (Q W) ⋯)
    ((Hom.mk (W := W) g).map (W := W) (Q W) ⋯)
mp : Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (f.map (W := W) (Q W) ⋯) (g.map (W := W) (Q W) ⋯)
⊢ LeftFractionRel (W := W) f g

Tactic:
rw [← homMk_eq_iff_leftFractionRel, homMk_eq, homMk_eq]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_iff_leftFractionRel, CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq
-- 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
f g : W.LeftFraction X Y
h :
  Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) ((Hom.mk (W := W) f).map (W := W) (Q W) ⋯)
    ((Hom.mk (W := W) g).map (W := W) (Q W) ⋯)
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (f.map (W := W) (Q W) ⋯) (g.map (W := W) (Q W) ⋯)

Tactic:
h

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.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
inst_1 : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h :
  Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) ((Hom.mk (W := W) f).map (W := W) (Q W) ⋯)
    ((Hom.mk (W := W) g).map (W := W) (Q W) ⋯)
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (f.map (W := W) (Q W) ⋯) (g.map (W := W) (Q W) ⋯)

Tactic:
exact 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
inst_1 : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : LeftFractionRel (W := W) f g
mpr : Hom.mk (W := W) f = Hom.mk (W := W) g
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) ((Hom.mk (W := W) f).map (W := W) (Q W) ⋯)
    ((Hom.mk (W := W) g).map (W := W) (Q W) ⋯)

Tactic:
congr 1
-- 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
f g : W.LeftFraction X Y
h : LeftFractionRel (W := W) f g
⊢ Hom.mk (W := W) f = Hom.mk (W := W) g

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
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : LeftFractionRel (W := W) f g
⊢ Hom.mk (W := W) f = Hom.mk (W := W) g

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
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
inst_2 : L.IsLocalization W
⊢ φ.map (W := W) L ⋯ = L.map (φ.f (W := W)) ≫ (Localization.isoOfHom L W (φ.s (W := W)) ⋯).inv

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map, 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
φ : W.LeftFraction X Y
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L₁ : Functor.{v_1, v_2, u_1, u_2} C D
L₂ : Functor.{v_1, v_3, u_1, u_3} C E
inst_3 : L₁.IsLocalization W
inst_4 : L₂.IsLocalization W
e : L₁ ⋙ (Localization.uniq L₁ L₂ W).functor ≅ L₂ := Localization.compUniqFunctor L₁ L₂ W
rw :
  (Localization.uniq L₁ L₂ W).functor.map (φ.map (W := W) L₁ ⋯) ≫
      (L₁ ⋙ (Localization.uniq L₁ L₂ W).functor).map (φ.s (W := W)) ≫ e.hom.app (φ.Y' (W := W)) =
    NatTrans.app (Iso.hom (Localization.compUniqFunctor L₁ L₂ W)) X ≫ L₂.map (φ.f (W := W))
⊢ (Localization.uniq L₁ L₂ W).functor.map (φ.map (W := W) L₁ ⋯) =
    NatTrans.app (Iso.hom (Localization.compUniqFunctor L₁ L₂ W)) X ≫
      φ.map (W := W) L₂ ⋯ ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₁ L₂ W)) Y

Tactic:
rw [← cancel_mono (e.hom.app Y), assoc, assoc, e.inv_hom_id_app, comp_id,
    ← cancel_mono (L₂.map φ.s), assoc, assoc, map_comp_map_s, ← e.hom.naturality]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map, CategoryTheory.NatTrans.naturality, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.Iso.inv_hom_id_app, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L₁ : Functor.{v_1, v_2, u_1, u_2} C D
L₂ : Functor.{v_1, v_3, u_1, u_3} C E
inst_3 : L₁.IsLocalization W
inst_4 : L₂.IsLocalization W
e : L₁ ⋙ (Localization.uniq L₁ L₂ W).functor ≅ L₂ := Localization.compUniqFunctor L₁ L₂ W
⊢ (Localization.uniq L₁ L₂ W).functor.map (φ.map (W := W) L₁ ⋯) ≫
      (L₁ ⋙ (Localization.uniq L₁ L₂ W).functor).map (φ.s (W := W)) ≫ e.hom.app (φ.Y' (W := W)) =
    NatTrans.app (Iso.hom (Localization.compUniqFunctor L₁ L₂ W)) X ≫ L₂.map (φ.f (W := W))

Tactic:
simpa [← Functor.map_comp_assoc, map_comp_map_s] using e.hom.naturality φ.f

Premises used: CategoryTheory.Functor.map_comp_assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.MorphismProperty.LeftFraction.f, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, 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
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ₁ φ₂ : W.LeftFraction X Y
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L₁ : Functor.{v_1, v_2, u_1, u_2} C D
L₂ : Functor.{v_1, v_3, u_1, u_3} C E
inst_3 : L₁.IsLocalization W
inst_4 : L₂.IsLocalization W
h : φ₁.map (W := W) L₁ ⋯ = φ₂.map (W := W) L₁ ⋯
a :
  (Localization.uniq L₂ L₁ W).functor.map (φ₁.map (W := W) L₂ ⋯) =
    (Localization.uniq L₂ L₁ W).functor.map (φ₂.map (W := W) L₂ ⋯)
⊢ φ₁.map (W := W) L₂ ⋯ = φ₂.map (W := W) L₂ ⋯

Tactic:
apply (Localization.uniq L₂ L₁ W).functor.map_injective

Premises used: CategoryTheory.Localization.uniq, CategoryTheory.Equivalence.functor, CategoryTheory.Functor.map_injective
-- 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
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L₁ : Functor.{v_1, v_2, u_1, u_2} C D
L₂ : Functor.{v_1, v_3, u_1, u_3} C E
inst_3 : L₁.IsLocalization W
inst_4 : L₂.IsLocalization W
h : φ₁.map (W := W) L₁ ⋯ = φ₂.map (W := W) L₁ ⋯
a :
  NatTrans.app (Iso.hom (Localization.compUniqFunctor L₂ L₁ W)) X ≫
      φ₁.map (W := W) L₁ ⋯ ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₂ L₁ W)) Y =
    (Localization.uniq L₂ L₁ W).functor.map (φ₂.map (W := W) L₂ ⋯)
a₁ :
  Eq (α := (Localization.uniq L₂ L₁ W).functor.obj (L₂.obj X) ⟶ (Localization.uniq L₂ L₁ W).functor.obj (L₂.obj Y))
    (NatTrans.app (Iso.hom (Localization.compUniqFunctor L₂ L₁ W)) X ≫
        φ₁.map (W := W) L₁ ⋯ ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₂ L₁ W)) Y :
      (L₂ ⋙ (Localization.uniq L₂ L₁ W).functor).obj X ⟶ (L₂ ⋙ (Localization.uniq L₂ L₁ W).functor).obj Y)
    (NatTrans.app (Iso.hom (Localization.compUniqFunctor L₂ L₁ W)) X ≫
      φ₂.map (W := W) L₁ ⋯ ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₂ L₁ W)) Y)
a₂ a₃ :
  Eq (α := (Localization.uniq L₂ L₁ W).functor.obj (L₂.obj X) ⟶ (Localization.uniq L₂ L₁ W).functor.obj (L₂.obj Y))
    (NatTrans.app (Iso.hom (Localization.compUniqFunctor L₂ L₁ W)) X ≫
        φ₂.map (W := W) L₁ ⋯ ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₂ L₁ W)) Y :
      (L₂ ⋙ (Localization.uniq L₂ L₁ W).functor).obj X ⟶ (L₂ ⋙ (Localization.uniq L₂ L₁ W).functor).obj Y)
    (NatTrans.app (Iso.hom (Localization.compUniqFunctor L₂ L₁ W)) X ≫
      φ₂.map (W := W) L₁ ⋯ ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₂ L₁ W)) Y)
⊢ (Localization.uniq L₂ L₁ W).functor.map (φ₁.map (W := W) L₂ ⋯) =
    (Localization.uniq L₂ L₁ W).functor.map (φ₂.map (W := W) L₂ ⋯)

Tactic:
rw [map_compatibility φ₁ L₂ L₁, map_compatibility φ₂ L₂ L₁, h]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map_compatibility
-- 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
rw : IsIso (L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)))
⊢ IsIso (L.map (z₂.s (W := W) ≫ z₃.s (W := W)))

Tactic:
rw [L.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- 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
⊢ IsIso (L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)))

Tactic:
infer_instance
-- 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
⊢ IsIso (L.map (z₂.s (W := W) ≫ z₃.s (W := W)))

Tactic:
have : IsIso (L.map (z₂.s ≫ z₃.s)) := by
    rw [L.map_comp]
    infer_instance