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 : C
s : X ⟶ Y
hs : W s
h : LeftFractionRel (W := W) (mk (W := W) s s hs) (ofHom W (𝟙 (Functor.obj (Q W) X)))
⊢ homMk (W := W) (mk (W := W) s s hs) = 𝟙 (Functor.obj (Q W) X)

Tactic:
apply homMk_eq_of_leftFractionRel

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_of_leftFractionRel
-- 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 : C
s : X ⟶ Y
hs : W s
⊢ (mk (W := W) s s hs).s (W := W) ≫ 𝟙 Y = (ofHom W (𝟙 (Functor.obj (Q W) X))).s (W := W) ≫ s

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
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
⊢ (mk (W := W) s s hs).f (W := W) ≫ 𝟙 Y = (ofHom W (𝟙 (Functor.obj (Q W) X))).f (W := W) ≫ s

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
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
⊢ W ((mk (W := W) s s hs).s (W := W) ≫ 𝟙 Y)

Tactic:
simpa using hs
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
⊢ LeftFractionRel (W := W) (mk (W := W) s s hs) (ofHom W (𝟙 (Functor.obj (Q W) X)))

Tactic:
exact ⟨_, 𝟙 Y, s, by simp, by simp, by simpa using hs⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
dsimp : homMk (W := W) (ofInv (W := W) s hs) ≫ homMk (W := W) (ofHom W s) = 𝟙 (Functor.obj (Q W) Y)
⊢ Qinv (W := W) s hs ≫ Functor.map (Q W) s = 𝟙 (Functor.obj (Q W) Y)

Tactic:
dsimp only [Qinv, Q_map]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv, CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
⊢ (ofHom W s).f (W := W) ≫ (ofHom W (𝟙 Y)).s (W := W) = (ofInv (W := W) s hs).s (W := W) ≫ (ofHom W (𝟙 Y)).f (W := W)

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
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
rw : homMk (W := W) ((ofInv (W := W) s hs).comp₀ (W := W) (ofHom W s) (ofHom W (𝟙 Y))) = 𝟙 (Functor.obj (Q W) Y)
⊢ homMk (W := W) (ofInv (W := W) s hs) ≫ homMk (W := W) (ofHom W s) = 𝟙 (Functor.obj (Q W) Y)

Tactic:
rw [homMk_comp_homMk (ofInv s hs) (ofHom W s) (ofHom W (𝟙 Y)) (by simp)]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_comp_homMk, CategoryTheory.CategoryStruct.id, CategoryTheory.MorphismProperty.LeftFraction.ofHom, CategoryTheory.MorphismProperty.LeftFraction.ofInv
-- 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 : C
s : X ⟶ Y
hs : W s
h :
  LeftFractionRel (W := W) ((ofInv (W := W) s hs).comp₀ (W := W) (ofHom W s) (ofHom W (𝟙 Y)))
    (ofHom W (𝟙 (Functor.obj (Q W) Y)))
⊢ homMk (W := W) ((ofInv (W := W) s hs).comp₀ (W := W) (ofHom W s) (ofHom W (𝟙 Y))) = 𝟙 (Functor.obj (Q W) Y)

Tactic:
apply homMk_eq_of_leftFractionRel

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_of_leftFractionRel
-- 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 : C
s : X ⟶ Y
hs : W s
⊢ ((ofInv (W := W) s hs).comp₀ (W := W) (ofHom W s) (ofHom W (𝟙 Y))).s (W := W) ≫ 𝟙 Y =
    (ofHom W (𝟙 (Functor.obj (Q W) Y))).s (W := W) ≫ 𝟙 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
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
⊢ ((ofInv (W := W) s hs).comp₀ (W := W) (ofHom W s) (ofHom W (𝟙 Y))).f (W := W) ≫ 𝟙 Y =
    (ofHom W (𝟙 (Functor.obj (Q W) Y))).f (W := W) ≫ 𝟙 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
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
⊢ W (((ofInv (W := W) s hs).comp₀ (W := W) (ofHom W s) (ofHom W (𝟙 Y))).s (W := W) ≫ 𝟙 Y)

Tactic:
simpa using W.id_mem Y

Premises used: CategoryTheory.MorphismProperty.id_mem
-- 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 : C
s : X ⟶ Y
hs : W s
⊢ LeftFractionRel (W := W) ((ofInv (W := W) s hs).comp₀ (W := W) (ofHom W s) (ofHom W (𝟙 Y)))
    (ofHom W (𝟙 (Functor.obj (Q W) Y)))

Tactic:
exact ⟨_, 𝟙 Y, 𝟙 Y, by simp, by simp, by simpa using W.id_mem Y⟩
-- 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
s : X ⟶ Y
hs : W s
⊢ Functor.map (Q W) s ≫ Qinv (W := W) s hs = 𝟙 (Functor.obj (Q W) X)

Tactic:
(Qiso s hs).hom_inv_id

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk, CategoryTheory.Iso.hom_inv_id, CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv, CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso
-- 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
s : X ⟶ Y
hs : W s
⊢ Qinv (W := W) s hs ≫ Functor.map (Q W) s = 𝟙 (Functor.obj (Q W) Y)

Tactic:
(Qiso s hs).inv_hom_id

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk, CategoryTheory.Iso.inv_hom_id, CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv, CategoryTheory.MorphismProperty.LeftFraction.Localization.Qiso
-- 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 : C
s : X ⟶ Y
hs : W s
⊢ IsIso (Qinv (W := W) s hs)

Tactic:
inferInstanceAs <| IsIso (Qiso s hs).inv

Premises used: _private.0.CategoryTheory.MorphismProperty.LeftFraction.Localization.instIsIsoQinv._proof_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
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
this :
  ∀ (Z : C) (t₁ : a₁.Y' (W := W) ⟶ Z) (t₂ : a₂.Y' (W := W) ⟶ Z) (hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂)
    (hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂) (h : W (a₁.s (W := W) ≫ t₁)),
    Eq.{v_3 + 1} (α := F.obj X ⟶ F.obj Y) ((fun (f : W.LeftFraction X Y) ↦ f.map (W := W) F hF) a₁)
      ((fun (f : W.LeftFraction X Y) ↦ f.map (W := W) F hF) a₂)
⊢ ∀ (a : LeftFractionRel (W := W) a₁ a₂),
    Eq.{v_3 + 1} (α := F.obj X ⟶ F.obj Y) ((fun (f : W.LeftFraction X Y) ↦ f.map (W := W) F hF) a₁)
      ((fun (f : W.LeftFraction X Y) ↦ f.map (W := W) F hF) a₂)

Tactic:
⟨Z, t₁, t₂, hst, hft, 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
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' (W := W) ⟶ Z
t₂ : a₂.Y' (W := W) ⟶ Z
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
h : W (a₁.s (W := W) ≫ t₁)
⊢ IsIso (F.map (a₁.s (W := W) ≫ t₁))

Tactic:
have := hF _ 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
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' (W := W) ⟶ Z
t₂ : a₂.Y' (W := W) ⟶ Z
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
h : W (a₁.s (W := W) ≫ t₁)
this : IsIso (F.map (a₁.s (W := W) ≫ t₁))
rw : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
rw₁ : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₂ : F.map (a₁.f (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₃ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
rw₄ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
rw₅ : F.map (a₁.f (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
rw₆ : F.map (a₂.f (W := W) ≫ t₂) = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
rw₇ : F.map (a₂.f (W := W)) ≫ F.map t₂ = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W) ≫ t₂)
rw₈ : F.map (a₂.f (W := W)) ≫ F.map t₂ = a₂.map (W := W) F hF ≫ F.map (a₂.s (W := W)) ≫ F.map t₂
rw₉ rw₁₀ : F.map (a₂.f (W := W)) ≫ F.map t₂ = F.map (a₂.f (W := W)) ≫ F.map t₂
⊢ a₁.map (W := W) F hF = a₂.map (W := W) F hF

Tactic:
rw [← cancel_mono (F.map (a₁.s ≫ t₁)), F.map_comp, map_comp_map_s_assoc,
      ← F.map_comp, ← F.map_comp, hst, hft, F.map_comp,
      F.map_comp, map_comp_map_s_assoc]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
E : Type u_3
inst_1 : Category.{v_3, u_3} E
W : MorphismProperty.{v_1, u_1} C
X Y : C
f : W.LeftFraction X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
⊢ (mk (W := W) f).map (W := W) F hF = f.map (W := W) F hF

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map, 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
⊢ W.IsInvertedBy (Q W)

Tactic:
fun _ _ s hs =>
  inferInstanceAs <| IsIso (Qiso s hs).hom

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy, _private.0.CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.inverts._proof_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
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X : C
rw : (ofHom W (𝟙 X)).map (W := W) F hF = 𝟙 (F.obj X)
rw₁ : F.map (𝟙 X) = 𝟙 (F.obj X)
rw₂ rw₃ : Eq.{v_3 + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) (𝟙 (F.obj X))
⊢ (Hom.mk (W := W) (ofHom W (𝟙 X))).map (W := W) F hF = 𝟙 (F.obj X)

Tactic:
rw [Hom.map_mk, map_ofHom, F.map_id]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map_mk, CategoryTheory.MorphismProperty.LeftFraction.map_ofHom, 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
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
obtain :
  ∀ (f : W.LeftFraction X Y),
    Hom.map (W := W) (Hom.mk (W := W) f ≫ g) F hF = (Hom.mk (W := W) f).map (W := W) F hF ≫ Hom.map (W := W) g F hF
⊢ Hom.map (W := W) (f ≫ g) F hF = Hom.map (W := W) f F hF ≫ Hom.map (W := W) g F hF

Tactic:
obtain ⟨f, rfl⟩ := Hom.mk_surjective f

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
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
g : Y ⟶ Z
f : W.LeftFraction X Y
obtain :
  ∀ (g : W.LeftFraction Y Z),
    Hom.map (W := W) (Hom.mk (W := W) f ≫ Hom.mk (W := W) g) F hF =
      (Hom.mk (W := W) f).map (W := W) F hF ≫ (Hom.mk (W := W) g).map (W := W) F hF
⊢ Hom.map (W := W) (Hom.mk (W := W) f ≫ g) F hF = (Hom.mk (W := W) f).map (W := W) F hF ≫ Hom.map (W := W) g F hF

Tactic:
obtain ⟨g, rfl⟩ := 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
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
dsimp : Hom.map (W := W) (Hom.mk (W := W) f ≫ Hom.mk (W := W) g) F hF = f.map (W := W) F hF ≫ g.map (W := W) F hF
⊢ Hom.map (W := W) (Hom.mk (W := W) f ≫ Hom.mk (W := W) g) F hF =
    (Hom.mk (W := W) f).map (W := W) F hF ≫ (Hom.mk (W := W) g).map (W := W) F hF

Tactic:
dsimp
-- 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
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
obtain :
  ∀ (z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W)))
    (fac :
      (RightFraction.mk (W := W) (f.s (W := W)) ⋯ (g.f (W := W))).f (W := W) ≫ z.s (W := W) =
        (RightFraction.mk (W := W) (f.s (W := W)) ⋯ (g.f (W := W))).s (W := W) ≫ z.f (W := W)),
    Hom.map (W := W) (Hom.mk (W := W) f ≫ Hom.mk (W := W) g) F hF = f.map (W := W) F hF ≫ g.map (W := W) F hF
⊢ Hom.map (W := W) (Hom.mk (W := W) f ≫ Hom.mk (W := W) g) F hF = f.map (W := W) F hF ≫ g.map (W := W) F hF

Tactic:
obtain ⟨z, fac⟩ := HasLeftCalculusOfFractions.exists_leftFraction
      (RightFraction.mk f.s f.hs g.f)

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.RightFraction.mk, CategoryTheory.MorphismProperty.LeftFraction.f, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction
-- 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
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W))
fac :
  (RightFraction.mk (W := W) (f.s (W := W)) ⋯ (g.f (W := W))).f (W := W) ≫ z.s (W := W) =
    (RightFraction.mk (W := W) (f.s (W := W)) ⋯ (g.f (W := W))).s (W := W) ≫ z.f (W := W)
rw : (f.comp₀ (W := W) g z).map (W := W) F hF = f.map (W := W) F hF ≫ g.map (W := W) F hF
⊢ Hom.map (W := W) (Hom.mk (W := W) f ≫ Hom.mk (W := W) g) F hF = f.map (W := W) F hF ≫ g.map (W := W) F hF

Tactic:
rw [homMk_comp_homMk f g z fac, Hom.map_mk]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_comp_homMk, CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map_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
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W))
fac : g.f (W := W) ≫ z.s (W := W) = f.s (W := W) ≫ z.f (W := W)
⊢ IsIso (F.map (g.s (W := W)))

Tactic:
have := hF _ g.hs
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W))
fac : g.f (W := W) ≫ z.s (W := W) = f.s (W := W) ≫ z.f (W := W)
this : IsIso (F.map (g.s (W := W)))
⊢ IsIso (F.map (z.s (W := W)))

Tactic:
have := hF _ z.hs
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
E : Type u_3
inst_3 : Category.{v_3, u_3} E
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W))
fac : g.f (W := W) ≫ z.s (W := W) = f.s (W := W) ≫ z.f (W := W)
this_1 : IsIso (F.map (g.s (W := W)))
this : IsIso (F.map (z.s (W := W)))
rw :
  F.map ((mk (W := W) (f.f (W := W) ≫ z.f (W := W)) (g.s (W := W) ≫ z.s (W := W)) ⋯).f (W := W)) =
    f.map (W := W) F hF ≫ F.map (f.s (W := W) ≫ z.f (W := W))
⊢ (mk (W := W) (f.f (W := W) ≫ z.f (W := W)) (g.s (W := W) ≫ z.s (W := W)) ⋯).map (W := W) F hF =
    f.map (W := W) F hF ≫ g.map (W := W) F hF

Tactic:
rw [← cancel_mono (F.map g.s), assoc, map_comp_map_s,
      ← cancel_mono (F.map z.s), assoc, assoc, ← F.map_comp,
      ← F.map_comp, map_comp_map_s, fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.MorphismProperty.LeftFraction.s
-- 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
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W))
fac : g.f (W := W) ≫ z.s (W := W) = f.s (W := W) ≫ z.f (W := W)
this_1 : IsIso (F.map (g.s (W := W)))
this : IsIso (F.map (z.s (W := W)))
dsimp : F.map (f.f (W := W) ≫ z.f (W := W)) = f.map (W := W) F hF ≫ F.map (f.s (W := W) ≫ z.f (W := W))
⊢ F.map ((mk (W := W) (f.f (W := W) ≫ z.f (W := W)) (g.s (W := W) ≫ z.s (W := W)) ⋯).f (W := W)) =
    f.map (W := W) F hF ≫ F.map (f.s (W := W) ≫ z.f (W := W))

Tactic:
dsimp
-- 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
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction (f.Y' (W := W)) (g.Y' (W := W))
fac : g.f (W := W) ≫ z.s (W := W) = f.s (W := W) ≫ z.f (W := W)
this_1 : IsIso (F.map (g.s (W := W)))
this : IsIso (F.map (z.s (W := W)))
rw : F.map (f.f (W := W)) ≫ F.map (z.f (W := W)) = f.map (W := W) F hF ≫ F.map (f.s (W := W) ≫ z.f (W := W))
rw₁ : F.map (f.f (W := W)) ≫ F.map (z.f (W := W)) = f.map (W := W) F hF ≫ F.map (f.s (W := W)) ≫ F.map (z.f (W := W))
rw₂ rw₃ : F.map (f.f (W := W)) ≫ F.map (z.f (W := W)) = F.map (f.f (W := W)) ≫ F.map (z.f (W := W))
⊢ F.map (f.f (W := W) ≫ z.f (W := W)) = f.map (W := W) F hF ≫ F.map (f.s (W := W) ≫ z.f (W := W))

Tactic:
rw [F.map_comp, F.map_comp, map_comp_map_s_assoc]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_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 : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
dsimp : Hom.map (W := W) (Functor.map (Q W) f) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
⊢ (Q W ⋙ lift (W := W) F hF).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
dsimp [lift]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.StrictUniversalPropertyFixedTarget.lift
-- 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 : 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
rw₄ rw₅ : F.map f = F.map f
⊢ Hom.map (W := W) (Functor.map (Q W) f) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)

Tactic:
rw [Q_map, Hom.map_mk, id_comp, comp_id, map_ofHom]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.map_mk, CategoryTheory.MorphismProperty.LeftFraction.map_ofHom, CategoryTheory.Category.comp_id, CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map, 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 : X ⟶ Y
obtain : ∀ (f : W.LeftFraction X Y), F₁.map (Hom.mk (W := W) f) = eqToHom ⋯ ≫ F₂.map (Hom.mk (W := W) f) ≫ eqToHom ⋯
⊢ F₁.map f = eqToHom ⋯ ≫ F₂.map f ≫ eqToHom ⋯

Tactic:
obtain ⟨f, rfl⟩ := Hom.mk_surjective f

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk_surjective, rfl