awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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 : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
rw : Hom.map (W := W) (homMk (W := W) (ofHom W f)) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
⊢ Hom.map (W := W) (Functor.map (Q W) f) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
have rw₁ : (ofHom W f).map (W := W) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
Tactic: rw [Q_map, Hom.map_mk, id_comp, comp_id, map_ofHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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 : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
rw : Hom.map (W := W) (homMk (W := W) (ofHom W f)) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
rw₁ : (ofHom W f).map (W := W) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
⊢ Hom.map (W := W) (Functor.map (Q W) f) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
have rw₂ : (ofHom W f).map (W := W) F hF = F.map f ≫ 𝟙 (F.obj Y)
Tactic: rw [Q_map, Hom.map_mk, id_comp, comp_id, map_ofHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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 : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
rw : Hom.map (W := W) (homMk (W := W) (ofHom W f)) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
rw₁ : (ofHom W f).map (W := W) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
rw₂ : (ofHom W f).map (W := W) F hF = F.map f ≫ 𝟙 (F.obj Y)
⊢ Hom.map (W := W) (Functor.map (Q W) f) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
have rw₃ : (ofHom W f).map (W := W) F hF = F.map f
Tactic: rw [Q_map, Hom.map_mk, id_comp, comp_id, map_ofHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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 : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
rw : Hom.map (W := W) (homMk (W := W) (ofHom W f)) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
rw₁ : (ofHom W f).map (W := W) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
rw₂ : (ofHom W f).map (W := W) F hF = F.map f ≫ 𝟙 (F.obj Y)
rw₃ : (ofHom W f).map (W := W) F hF = F.map f
⊢ Hom.map (W := W) (Functor.map (Q W) f) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
have rw₄ : F.map f = F.map f
Tactic: rw [Q_map, Hom.map_mk, id_comp, comp_id, map_ofHom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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 : X ⟶ Y
⊢ F₁.map f = eqToHom ⋯ ≫ F₂.map f ≫ eqToHom ⋯
have obtain : ∀ (f : W.LeftFraction X Y), F₁.map (Hom.mk (W := W) f) = eqToHom sorry ≫ F₂.map (Hom.mk (W := W) f) ≫ eqToHom sorry
Tactic: obtain ⟨f, rfl⟩ := Hom.mk_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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
⊢ F₁.map (Hom.mk (W := W) f) = eqToHom ⋯ ≫ F₂.map (Hom.mk (W := W) f) ≫ eqToHom ⋯
have rw : F₁.map (Functor.map (Q W) (f.f (W := W))) ≫ F₁.map (Qinv (W := W) (f.s (W := W)) sorry) =
  eqToHom sorry ≫ F₂.map (Functor.map (Q W) (f.f (W := W))) ≫ F₂.map (Qinv (W := W) (f.s (W := W)) sorry) ≫ eqToHom sorry
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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
⊢ 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 ⋯
have erw : (eqToHom sorry ≫ (Q W ⋙ F₂).map (f.f (W := W)) ≫ eqToHom sorry) ≫ F₁.map (Qinv (W := W) (f.s (W := W)) sorry) =
  eqToHom sorry ≫ F₂.map (Functor.map (Q W) (f.f (W := W))) ≫ F₂.map (Qinv (W := W) (f.s (W := W)) sorry) ≫ eqToHom sorry
Tactic: erw [Functor.congr_hom h f.f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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
⊢ (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 ⋯
have rw : eqToHom sorry ≫ (Q W ⋙ F₂).map (f.f (W := W)) ≫ eqToHom sorry ≫ F₁.map (Qinv (W := W) (f.s (W := W)) sorry) =
  eqToHom sorry ≫ F₂.map (Functor.map (Q W) (f.f (W := W))) ≫ F₂.map (Qinv (W := W) (f.s (W := W)) sorry) ≫ eqToHom sorry
Tactic: rw [assoc, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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
⊢ 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 ⋯
have e_a : eqToHom sorry ≫ F₁.map (Qinv (W := W) (f.s (W := W)) sorry) = F₂.map (Qinv (W := W) (f.s (W := W)) sorry) ≫ eqToHom sorry
Tactic: congr 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (hypothesis)
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
⊢ eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) = F₂.map (Qinv (W := W) (f.s (W := W)) ⋯) ≫ eqToHom ⋯
have this : IsIso (X := Functor.obj (Q W) Y) (Functor.map (Q W) (f.s (W := W)))
Tactic: have := inverts W _ f.hs
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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)))
⊢ eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) = F₂.map (Qinv (W := W) (f.s (W := W)) ⋯) ≫ eqToHom ⋯
have e_a : F₂.map (Functor.map (Q W) (f.s (W := W))) ≫ eqToHom sorry ≫ F₁.map (Qinv (W := W) (f.s (W := W)) sorry) = eqToHom sorry
Tactic: rw [← cancel_epi (F₂.map ((Q W).map f.s)), ← F₂.map_comp_assoc,
      Qiso_hom_inv_id, Functor.map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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)))
⊢ F₂.map (Functor.map (Q W) (f.s (W := W))) ≫ eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) = eqToHom ⋯
have e_a : (eqToHom sorry ≫ (Q W ⋙ F₁).map (f.s (W := W)) ≫ eqToHom sorry) ≫ eqToHom sorry ≫ F₁.map (Qinv (W := W) (f.s (W := W)) sorry) =
  eqToHom sorry
Tactic: erw [Functor.congr_hom h.symm f.s]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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)))
⊢ (eqToHom ⋯ ≫ (Q W ⋙ F₁).map (f.s (W := W)) ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) =
    eqToHom ⋯
have e_a : (eqToHom sorry ≫ F₁.map (Functor.map (Q W) (f.s (W := W))) ≫ eqToHom sorry) ≫
    eqToHom sorry ≫ F₁.map (Qinv (W := W) (f.s (W := W)) sorry) =
  eqToHom sorry
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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)))
⊢ (eqToHom ⋯ ≫ F₁.map (Functor.map (Q W) (f.s (W := W))) ≫ eqToHom ⋯) ≫
      eqToHom ⋯ ≫ F₁.map (Qinv (W := W) (f.s (W := W)) ⋯) =
    eqToHom ⋯
have e_a : eqToHom sorry ≫ F₁.map (𝟙 (Functor.obj (Q W) Y)) = eqToHom sorry
Tactic: rw [assoc, assoc, eqToHom_trans_assoc, eqToHom_refl, id_comp, ← F₁.map_comp,
      Qiso_hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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)))
⊢ eqToHom ⋯ ≫ F₁.map (𝟙 (Functor.obj (Q W) Y)) = eqToHom ⋯
have e_a : eqToHom sorry ≫ F₁.map (𝟙 Y) = eqToHom sorry
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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)))
⊢ eqToHom ⋯ ≫ F₁.map (𝟙 Y) = eqToHom ⋯
have e_a : Eq.{v_3 + 1} (α := F₂.obj Y ⟶ F₁.obj Y) (eqToHom sorry ≫ 𝟙 (F₁.obj Y)) (eqToHom sorry)
Tactic: rw [F₁.map_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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 ⋯)
⊢ eqToHom ⋯ ≫ F₁.map (𝟙 Y) = eqToHom ⋯
have e_a₁ : Eq.{v_3 + 1} (α := F₂.obj Y ⟶ F₁.obj Y) (eqToHom sorry) (eqToHom sorry)
Tactic: rw [F₁.map_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (homMk (W := W) f) (f.map (W := W) (Q W) ⋯)
have 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)) sorry)
  (f.map (W := W) (Q W) sorry)
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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) ⋯)
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (homMk (W := W) f) (f.map (W := W) (Q W) ⋯)
have 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)) sorry) ≫ Functor.map (Q W) (f.s (W := W)))
  (f.map (W := W) (Q W) sorry ≫ Functor.map (Q W) (f.s (W := 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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)))
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (homMk (W := W) f) (f.map (W := W) (Q W) ⋯)
have 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)) sorry ≫ Functor.map (Q W) (f.s (W := W)))
  (f.map (W := W) (Q W) sorry ≫ Functor.map (Q W) (f.s (W := 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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)))
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (homMk (W := W) f) (f.map (W := W) (Q W) ⋯)
have rw₃ : Functor.map (Q W) (f.f (W := W)) ≫ 𝟙 (Functor.obj (Q W) (f.Y' (W := W))) =
  f.map (W := W) (Q W) sorry ≫ Functor.map (Q W) (f.s (W := 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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))
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (homMk (W := W) f) (f.map (W := W) (Q W) ⋯)
have 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) sorry ≫ Functor.map (Q W) (f.s (W := 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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)))
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (homMk (W := W) f) (f.map (W := W) (Q W) ⋯)
have 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)))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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
⊢ 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
have mp : Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) ((Hom.mk (W := W) f).map (W := W) (Q W) sorry)
    ((Hom.mk (W := W) g).map (W := W) (Q W) sorry) →
  LeftFractionRel (W := W) f g
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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
⊢ 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
have 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) sorry)
    ((Hom.mk (W := W) g).map (W := W) (Q W) sorry)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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) ⋯)
⊢ LeftFractionRel (W := W) f g
have mp : Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (f.map (W := W) (Q W) sorry) (g.map (W := W) (Q W) sorry)
Tactic: rw [← homMk_eq_iff_leftFractionRel, homMk_eq, homMk_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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
⊢ 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) ⋯)
have mpr : Hom.mk (W := W) f = Hom.mk (W := W) g
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (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
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₁ ⋯) =
    NatTrans.app (Iso.hom (Localization.compUniqFunctor L₁ L₂ W)) X ≫
      φ.map (W := W) L₂ ⋯ ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₁ L₂ W)) Y
have rw : (Localization.uniq L₁ L₂ W).functor.map (φ.map (W := W) L₁ sorry) ≫
    (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: 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (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
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₁ ⋯
⊢ φ₁.map (W := W) L₂ ⋯ = φ₂.map (W := W) L₂ ⋯
have a : (Localization.uniq L₂ L₁ W).functor.map (φ₁.map (W := W) L₂ sorry) =
  (Localization.uniq L₂ L₁ W).functor.map (φ₂.map (W := W) L₂ sorry)
Tactic: apply (Localization.uniq L₂ L₁ W).functor.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (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
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₁ ⋯
⊢ (Localization.uniq L₂ L₁ W).functor.map (φ₁.map (W := W) L₂ ⋯) =
    (Localization.uniq L₂ L₁ W).functor.map (φ₂.map (W := W) L₂ ⋯)
have a : NatTrans.app (Iso.hom (Localization.compUniqFunctor L₂ L₁ W)) X ≫
    φ₁.map (W := W) L₁ sorry ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₂ L₁ W)) Y =
  (Localization.uniq L₂ L₁ W).functor.map (φ₂.map (W := W) L₂ sorry)
Tactic: rw [map_compatibility φ₁ L₂ L₁, map_compatibility φ₂ L₂ L₁, h]