awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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))
⊢ 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 ⋯
have 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))
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]
-- 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
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
⊢ ∃ (φ : W.LeftFraction X Y), f = φ.map (W := W) L ⋯
have 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 sorry
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⟩
Cleared hypotheses: f
-- 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
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
⊢ ∃ (φ : W.LeftFraction X Y), e.inv.app X ≫ f' ≫ e.hom.app Y = φ.map (W := W) L ⋯
have obtain : ∀ (g : X ⟶ Y), ∃ (φ : W.LeftFraction X Y), e.inv.app X ≫ E.functor.map g ≫ e.hom.app Y = φ.map (W := W) L sorry
Tactic: obtain ⟨g, rfl⟩ := E.functor.map_surjective f'
Cleared hypotheses: f'
-- 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
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
⊢ ∃ (φ : W.LeftFraction X Y), e.inv.app X ≫ E.functor.map g ≫ e.hom.app Y = φ.map (W := W) L ⋯
have 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 sorry
Tactic: obtain ⟨g, rfl⟩ := MorphismProperty.LeftFraction.Localization.Hom.mk_surjective g
Cleared hypotheses: g
-- 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
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 ⋯
have 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 sorry
Tactic: refine ⟨g, ?_⟩
-- 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
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
⊢ e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk (W := W) g) ≫ e.hom.app Y =
    g.map (W := W) L ⋯
have rw : e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.homMk (W := W) g) ≫ e.hom.app Y =
  g.map (W := W) L sorry
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]
-- 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
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 ⋯
⊢ e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk (W := W) g) ≫ e.hom.app Y =
    g.map (W := W) L ⋯
have rw₁ : e.inv.app X ≫ E.functor.map (g.map (W := W) (MorphismProperty.LeftFraction.Localization.Q W) sorry) ≫ e.hom.app Y =
  g.map (W := W) L sorry
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]
-- 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
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 ⋯
⊢ e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk (W := W) g) ≫ e.hom.app Y =
    g.map (W := W) L ⋯
have rw₂ : e.inv.app X ≫
    (NatTrans.app (Iso.hom (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) X ≫
        g.map (W := W) L sorry ≫
          NatTrans.app (Iso.inv (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) Y) ≫
      e.hom.app Y =
  g.map (W := W) L sorry
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]
-- 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
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 ⋯
⊢ e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk (W := W) g) ≫ e.hom.app Y =
    g.map (W := W) L ⋯
have rw₃ : e.inv.app X ≫
    NatTrans.app (Iso.hom (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) X ≫
      (g.map (W := W) L sorry ≫
          NatTrans.app (Iso.inv (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) Y) ≫
        e.hom.app Y =
  g.map (W := W) L sorry
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]
-- 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
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 ⋯
⊢ e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk (W := W) g) ≫ e.hom.app Y =
    g.map (W := W) L ⋯
have rw₄ : e.inv.app X ≫
    NatTrans.app (Iso.hom (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) X ≫
      g.map (W := W) L sorry ≫
        NatTrans.app (Iso.inv (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) Y ≫ e.hom.app Y =
  g.map (W := W) L sorry
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]
-- 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
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 ⋯
⊢ e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk (W := W) g) ≫ e.hom.app Y =
    g.map (W := W) L ⋯
have rw₅ : e.inv.app X ≫
    NatTrans.app (Iso.hom (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) X ≫
      g.map (W := W) L sorry ≫ 𝟙 (L.obj Y) =
  g.map (W := W) L sorry
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]
-- 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
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 ⋯
⊢ e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk (W := W) g) ≫ e.hom.app Y =
    g.map (W := W) L ⋯
have rw₆ : e.inv.app X ≫
    NatTrans.app (Iso.hom (compUniqFunctor (MorphismProperty.LeftFraction.Localization.Q W) L W)) X ≫
      g.map (W := W) L sorry =
  g.map (W := W) L sorry
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]
-- 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
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 ⋯
⊢ e.inv.app X ≫ E.functor.map (MorphismProperty.LeftFraction.Localization.Hom.mk (W := W) g) ≫ e.hom.app Y =
    g.map (W := W) L ⋯
have rw₇ : g.map (W := W) L sorry = g.map (W := W) L sorry
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]
-- 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
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
⊢ φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯ ↔ LeftFractionRel (W := W) φ ψ
have mp : φ.map (W := W) L sorry = ψ.map (W := W) L sorry → LeftFractionRel (W := W) φ ψ
Tactic: constructor
-- 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
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) φ ψ
⊢ φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯ ↔ LeftFractionRel (W := W) φ ψ
have mpr : LeftFractionRel (W := W) φ ψ → φ.map (W := W) L sorry = ψ.map (W := W) L sorry
Tactic: constructor
-- 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
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 ⋯
⊢ LeftFractionRel (W := W) φ ψ
have mp : Eq (α := Functor.obj (Localization.Q W) X ⟶ Functor.obj (Localization.Q W) Y) (φ.map (W := W) (Localization.Q W) sorry)
  (ψ.map (W := W) (Localization.Q W) sorry)
Tactic: rw [← MorphismProperty.LeftFraction.Localization.map_eq_iff]