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
X Y : C
z₁ z₂ : W.LeftFraction X Y
Z : C
t₁ : z₁.Y' (W := W) ⟶ Z
t₂ : z₂.Y' (W := W) ⟶ Z
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
⊢ LeftFractionRel (W := W) z₂ z₁

Tactic:
exact ⟨Z, t₂, t₁, hst.symm, hft.symm, by simpa only [← hst] using ht⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
h₁₂ : LeftFractionRel (W := W) z₁ z₂
h₂₃ : LeftFractionRel (W := W) z₂ z₃
obtain :
  ∀ (Z₄ : C) (t₁ : z₁.Y' (W := W) ⟶ Z₄) (t₂ : z₂.Y' (W := W) ⟶ Z₄) (hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂)
    (hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂) (ht : W (z₁.s (W := W) ≫ t₁)), LeftFractionRel (W := W) z₁ z₃
⊢ LeftFractionRel (W := W) z₁ z₃

Tactic:
obtain ⟨Z₄, t₁, t₂, hst, hft, ht⟩ := 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
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
h₂₃ : LeftFractionRel (W := W) z₂ z₃
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
obtain :
  ∀ (Z₅ : C) (u₂ : z₂.Y' (W := W) ⟶ Z₅) (u₃ : z₃.Y' (W := W) ⟶ Z₅) (hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃)
    (hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃) (hu : W (z₂.s (W := W) ≫ u₂)), LeftFractionRel (W := W) z₁ z₃
⊢ LeftFractionRel (W := W) z₁ z₃

Tactic:
obtain ⟨Z₅, u₂, u₃, hsu, hfu, hu⟩ := 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
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
obtain :
  ∀ {Y' : C} (v₄ : Z₄ ⟶ Y') (v₅ : Z₅ ⟶ Y') (hv₅ : W v₅)
    (fac :
      (RightFraction.mk (W := W) (z₁.s (W := W) ≫ t₁) ht (z₃.s (W := W) ≫ u₃)).f (W := W) ≫
          (LeftFraction.mk (W := W) v₄ v₅ hv₅).s (W := W) =
        (RightFraction.mk (W := W) (z₁.s (W := W) ≫ t₁) ht (z₃.s (W := W) ≫ u₃)).s (W := W) ≫
          (LeftFraction.mk (W := W) v₄ v₅ hv₅).f (W := W)),
    LeftFractionRel (W := W) z₁ z₃
⊢ LeftFractionRel (W := W) z₁ z₃

Tactic:
obtain ⟨⟨v₄, v₅, hv₅⟩, fac⟩ := HasLeftCalculusOfFractions.exists_leftFraction
    (RightFraction.mk (z₁.s ≫ t₁) ht (z₃.s ≫ u₃))

Premises used: CategoryTheory.MorphismProperty.RightFraction.mk, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac :
  (RightFraction.mk (W := W) (z₁.s (W := W) ≫ t₁) ht (z₃.s (W := W) ≫ u₃)).f (W := W) ≫
      (LeftFraction.mk (W := W) v₄ v₅ hv₅).s (W := W) =
    (RightFraction.mk (W := W) (z₁.s (W := W) ≫ t₁) ht (z₃.s (W := W) ≫ u₃)).s (W := W) ≫
      (LeftFraction.mk (W := W) v₄ v₅ hv₅).f (W := W)
⊢ z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄

Tactic:
simp only [Category.assoc] at fac

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
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
⊢ z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄

Tactic:
simpa only [← reassoc_of% hsu, reassoc_of% hst] using fac
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
⊢ z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄

Tactic:
have eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄ := by
    simpa only [← reassoc_of% hsu, reassoc_of% hst] using fac
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
obtain : ∀ (Z₇ : C) (w : Y' ⟶ Z₇) (hw : W w) (fac' : (u₂ ≫ v₅) ≫ w = (t₂ ≫ v₄) ≫ w), LeftFractionRel (W := W) z₁ z₃
⊢ LeftFractionRel (W := W) z₁ z₃

Tactic:
obtain ⟨Z₇, w, hw, fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ z₂.hs eq

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.ext
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : (u₂ ≫ v₅) ≫ w = (t₂ ≫ v₄) ≫ w
⊢ u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w

Tactic:
simp only [Category.assoc] at fac'

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
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ LeftFractionRel (W := W) z₁ z₃

Tactic:
⟨Z₇, t₁ ≫ v₄ ≫ w, u₃ ≫ v₅ ≫ w, ?_, ?_, ?_⟩

Premises used: CategoryTheory.MorphismProperty.LeftFractionRel, Exists.intro, CategoryTheory.CategoryStruct.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
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
refine_1 : z₁.s (W := W) ≫ t₁ ≫ v₄ ≫ w = z₃.s (W := W) ≫ u₃ ≫ v₅ ≫ w
refine_2 : z₁.f (W := W) ≫ t₁ ≫ v₄ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
refine_3 : W (z₁.s (W := W) ≫ t₁ ≫ v₄ ≫ w)
⊢ LeftFractionRel (W := W) z₁ z₃

Tactic:
refine ⟨Z₇, t₁ ≫ v₄ ≫ w, u₃ ≫ v₅ ≫ w, ?_, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
refine_1 refine_1₁ : z₁.s (W := W) ≫ t₁ ≫ v₄ ≫ w = z₁.s (W := W) ≫ t₁ ≫ v₄ ≫ w
⊢ z₁.s (W := W) ≫ t₁ ≫ v₄ ≫ w = z₃.s (W := W) ≫ u₃ ≫ v₅ ≫ w

Tactic:
rw [reassoc_of% fac]
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
refine_2 : z₂.f (W := W) ≫ t₂ ≫ v₄ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
refine_2₁ : z₂.f (W := W) ≫ u₂ ≫ v₅ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
refine_2₂ refine_2₃ : z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
⊢ z₁.f (W := W) ≫ t₁ ≫ v₄ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w

Tactic:
rw [reassoc_of% hft, ← fac', reassoc_of% hfu]
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
refine_3 : W ((z₂.s (W := W) ≫ u₂) ≫ v₅ ≫ w)
⊢ W (z₁.s (W := W) ≫ t₁ ≫ v₄ ≫ w)

Tactic:
rw [← reassoc_of% fac, ← reassoc_of% hsu, ← Category.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
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ W ((z₂.s (W := W) ≫ u₂) ≫ v₅ ≫ w)

Tactic:
W.comp_mem _ _ hu (W.comp_mem _ _ hv₅ hw)

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ W ((z₂.s (W := W) ≫ u₂) ≫ v₅ ≫ w)

Tactic:
exact W.comp_mem _ _ hu (W.comp_mem _ _ hv₅ hw)

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- 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 Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
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)
h₃' : z₂.f (W := W) ≫ z₃'.s (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W)
obtain :
  ∀ (z₄ : W.LeftFraction (z₃.Y' (W := W)) (z₃'.Y' (W := W)))
    (fac :
      (RightFraction.mk (W := W) (z₃.s (W := W)) ⋯ (z₃'.s (W := W))).f (W := W) ≫ z₄.s (W := W) =
        (RightFraction.mk (W := W) (z₃.s (W := W)) ⋯ (z₃'.s (W := W))).s (W := W) ≫ z₄.f (W := W)),
    LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')
⊢ LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')

Tactic:
obtain ⟨z₄, fac⟩ := exists_leftFraction (RightFraction.mk z₃.s z₃.hs z₃'.s)

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.RightFraction.mk, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.exists_leftFraction
-- 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 Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
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)
h₃' : z₂.f (W := W) ≫ z₃'.s (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W)
z₄ : W.LeftFraction (z₃.Y' (W := W)) (z₃'.Y' (W := W))
fac : z₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
rw : z₂.f (W := W) ≫ z₃.s (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
rw₁ : z₂.f (W := W) ≫ z₃.s (W := W) ≫ z₄.f (W := W) = z₂.f (W := W) ≫ z₃'.s (W := W) ≫ z₄.s (W := W)
rw₂ rw₃ : z₂.f (W := W) ≫ z₃.s (W := W) ≫ z₄.f (W := W) = z₂.f (W := W) ≫ z₃.s (W := W) ≫ z₄.f (W := W)
⊢ z₁.s (W := W) ≫ z₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)

Tactic:
rw [← reassoc_of% h₃, ← reassoc_of% h₃', fac]
-- 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 Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
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)
h₃' : z₂.f (W := W) ≫ z₃'.s (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W)
z₄ : W.LeftFraction (z₃.Y' (W := W)) (z₃'.Y' (W := W))
fac : z₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
⊢ z₁.s (W := W) ≫ z₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)

Tactic:
have eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s := by
    rw [← reassoc_of% h₃, ← reassoc_of% h₃', fac]
-- 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 Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
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)
h₃' : z₂.f (W := W) ≫ z₃'.s (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W)
z₄ : W.LeftFraction (z₃.Y' (W := W)) (z₃'.Y' (W := W))
fac : z₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
eq : z₁.s (W := W) ≫ z₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
obtain :
  ∀ (Y_1 : C) (t : z₄.Y' (W := W) ⟶ Y_1) (ht : W t)
    (fac' : (z₃.f (W := W) ≫ z₄.f (W := W)) ≫ t = (z₃'.f (W := W) ≫ z₄.s (W := W)) ≫ t),
    LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')
⊢ LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')

Tactic:
obtain ⟨Y, t, ht, fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ z₁.hs eq

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.ext
-- 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_1 Z : C
z₁ : W.LeftFraction X Y_1
z₂ : W.LeftFraction Y_1 Z
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)
h₃' : z₂.f (W := W) ≫ z₃'.s (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W)
z₄ : W.LeftFraction (z₃.Y' (W := W)) (z₃'.Y' (W := W))
fac : z₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
eq : z₁.s (W := W) ≫ z₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
Y : C
t : z₄.Y' (W := W) ⟶ Y
ht : W t
fac' : (z₃.f (W := W) ≫ z₄.f (W := W)) ≫ t = (z₃'.f (W := W) ≫ z₄.s (W := W)) ≫ t
⊢ z₃.f (W := W) ≫ z₄.f (W := W) ≫ t = z₃'.f (W := W) ≫ z₄.s (W := W) ≫ t

Tactic:
simp only [assoc] at fac'

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
X Y_1 Z : C
z₁ : W.LeftFraction X Y_1
z₂ : W.LeftFraction Y_1 Z
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)
h₃' : z₂.f (W := W) ≫ z₃'.s (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W)
z₄ : W.LeftFraction (z₃.Y' (W := W)) (z₃'.Y' (W := W))
fac : z₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
eq : z₁.s (W := W) ≫ z₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
Y : C
t : z₄.Y' (W := W) ⟶ Y
ht : W t
fac' : z₃.f (W := W) ≫ z₄.f (W := W) ≫ t = z₃'.f (W := W) ≫ z₄.s (W := W) ≫ t
⊢ LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')

Tactic:
⟨Y, z₄.f ≫ t, z₄.s ≫ t, ?_, ?_, ?_⟩

Premises used: CategoryTheory.MorphismProperty.LeftFractionRel, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.LeftFraction.f, CategoryTheory.MorphismProperty.LeftFraction.s
-- 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_1 Z : C
z₁ : W.LeftFraction X Y_1
z₂ : W.LeftFraction Y_1 Z
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)
h₃' : z₂.f (W := W) ≫ z₃'.s (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W)
z₄ : W.LeftFraction (z₃.Y' (W := W)) (z₃'.Y' (W := W))
fac : z₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
eq : z₁.s (W := W) ≫ z₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
Y : C
t : z₄.Y' (W := W) ⟶ Y
ht : W t
fac' : z₃.f (W := W) ≫ z₄.f (W := W) ≫ t = z₃'.f (W := W) ≫ z₄.s (W := W) ≫ t
refine_1 :
  (z₁.comp₀ (W := W) z₂ z₃).s (W := W) ≫ z₄.f (W := W) ≫ t = (z₁.comp₀ (W := W) z₂ z₃').s (W := W) ≫ z₄.s (W := W) ≫ t
refine_2 :
  (z₁.comp₀ (W := W) z₂ z₃).f (W := W) ≫ z₄.f (W := W) ≫ t = (z₁.comp₀ (W := W) z₂ z₃').f (W := W) ≫ z₄.s (W := W) ≫ t
refine_3 : W ((z₁.comp₀ (W := W) z₂ z₃).s (W := W) ≫ z₄.f (W := W) ≫ t)
⊢ LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')

Tactic:
refine ⟨Y, z₄.f ≫ t, z₄.s ≫ t, ?_, ?_, ?_⟩
-- 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_1 Z : C
z₁ : W.LeftFraction X Y_1
z₂ : W.LeftFraction Y_1 Z
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)
h₃' : z₂.f (W := W) ≫ z₃'.s (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W)
z₄ : W.LeftFraction (z₃.Y' (W := W)) (z₃'.Y' (W := W))
fac : z₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
eq : z₁.s (W := W) ≫ z₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
Y : C
t : z₄.Y' (W := W) ⟶ Y
ht : W t
fac' : z₃.f (W := W) ≫ z₄.f (W := W) ≫ t = z₃'.f (W := W) ≫ z₄.s (W := W) ≫ t
⊢ (z₁.comp₀ (W := W) z₂ z₃).s (W := W) ≫ z₄.f (W := W) ≫ t = (z₁.comp₀ (W := W) z₂ z₃').s (W := W) ≫ z₄.s (W := W) ≫ t

Tactic:
simp only [comp₀, assoc, reassoc_of% fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MorphismProperty.LeftFraction.comp₀