awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
inst_1 : W.HasLeftCalculusOfFractions
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₃).f (W := W) ≫ z₄.f (W := W) ≫ t = (z₁.comp₀ (W := W) z₂ z₃').f (W := W) ≫ z₄.s (W := W) ≫ t

Tactic:
simp only [comp₀, assoc, fac']

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MorphismProperty.LeftFraction.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
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_3 : W (z₂.s (W := W) ≫ z₃'.s (W := W) ≫ z₄.s (W := W) ≫ t)
⊢ W ((z₁.comp₀ (W := W) z₂ z₃).s (W := W) ≫ z₄.f (W := W) ≫ t)

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MorphismProperty.LeftFraction.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
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
⊢ W (z₂.s (W := W) ≫ z₃'.s (W := W) ≫ z₄.s (W := W) ≫ t)

Tactic:
W.comp_mem _ _ z₂.hs (W.comp_mem _ _ z₃'.hs (W.comp_mem _ _ z₄.hs ht))

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, 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_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
⊢ W (z₂.s (W := W) ≫ z₃'.s (W := W) ≫ z₄.s (W := W) ≫ t)

Tactic:
exact W.comp_mem _ _ z₂.hs (W.comp_mem _ _ z₃'.hs (W.comp_mem _ _ z₄.hs ht))

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, 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
f : Hom W X Y
mk :
  ∀ (z : W.LeftFraction X Y), ∃ (z_1 : W.LeftFraction X Y), Quot.mk (LeftFractionRel (W := W)) z = Hom.mk (W := W) z_1
⊢ ∃ (z : W.LeftFraction X Y), f = Hom.mk (W := W) z

Tactic:
obtain ⟨z⟩ := f
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
f : Hom W X Y
z : W.LeftFraction X Y
⊢ ∃ (z_1 : W.LeftFraction X Y), Quot.mk (LeftFractionRel (W := W)) z = mk (W := W) z_1

Tactic:
⟨z, rfl⟩

Premises used: Exists.intro, 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
X Y : C
f : Hom W X Y
z : W.LeftFraction X Y
⊢ ∃ (z_1 : W.LeftFraction X Y), Quot.mk (LeftFractionRel (W := W)) z = mk (W := W) z_1

Tactic:
exact ⟨z, 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
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)
⊢ z₁.comp (W := W) z₂ = Localization.Hom.mk (W := W) (z₁.comp₀ (W := W) z₂ z₃)

Tactic:
Quot.sound (LeftFraction.comp₀_rel _ _ _ _
    (RightFraction.leftFraction_fac (RightFraction.mk z₁.s z₁.hs z₂.f)) h₃)

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.RightFraction.leftFraction_fac, CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk, Quot.sound, CategoryTheory.MorphismProperty.RightFraction.mk, CategoryTheory.MorphismProperty.LeftFraction.comp, CategoryTheory.MorphismProperty.LeftFraction.comp₀_rel, CategoryTheory.MorphismProperty.LeftFraction.f, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : Hom W X Y
z₂ : Hom W Y Z
refine_1 :
  ∀ (a : W.LeftFraction X Y) (b₁ b₂ : W.LeftFraction Y Z),
    LeftFractionRel (W := W) b₁ b₂ →
      Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
        ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)
refine_2 :
  ∀ (a₁ a₂ : W.LeftFraction X Y) (b : W.LeftFraction Y Z),
    LeftFractionRel (W := W) a₁ a₂ →
      Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a₁ b)
        ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a₂ b)
⊢ Hom W X Z

Tactic:
refine Quot.lift₂ (fun a b => a.comp b) ?_ ?_ z₁ z₂

Premises used: Quot.lift₂
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : Hom W X Y
z₂ : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
refine_1 :
  ∀ (z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W)))
    (fac₁ :
      (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).f (W := W) ≫ z₁.s (W := W) =
        (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).s (W := W) ≫ z₁.f (W := W)),
    Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
      ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)
⊢ Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
    ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)

Tactic:
obtain ⟨z₁, fac₁⟩ := exists_leftFraction (RightFraction.mk a.s a.hs b₁.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
X Y Z : C
z₁_1 : Hom W X Y
z₂ : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ :
  (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).f (W := W) ≫ z₁.s (W := W) =
    (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).s (W := W) ≫ z₁.f (W := W)
refine_1 :
  ∀ (z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W)))
    (fac₂ :
      (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₂.f (W := W))).f (W := W) ≫ z₂.s (W := W) =
        (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₂.f (W := W))).s (W := W) ≫ z₂.f (W := W)),
    Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
      ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)
⊢ Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
    ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)

Tactic:
obtain ⟨z₂, fac₂⟩ := exists_leftFraction (RightFraction.mk a.s a.hs b₂.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
X Y Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ :
  (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).f (W := W) ≫ z₁.s (W := W) =
    (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ :
  (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₂.f (W := W))).f (W := W) ≫ z₂.s (W := W) =
    (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₂.f (W := W))).s (W := W) ≫ z₂.f (W := W)
refine_1 :
  ∀ (w₁ : W.LeftFraction (z₁.Y' (W := W)) U)
    (fac₁' :
      (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ t₁).f (W := W) ≫ w₁.s (W := W) =
        (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ t₁).s (W := W) ≫ w₁.f (W := W)),
    Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
      ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)
⊢ Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
    ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)

Tactic:
obtain ⟨w₁, fac₁'⟩ := exists_leftFraction (RightFraction.mk z₁.s z₁.hs t₁)

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
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₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ :
  (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).f (W := W) ≫ z₁.s (W := W) =
    (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ :
  (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₂.f (W := W))).f (W := W) ≫ z₂.s (W := W) =
    (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₂.f (W := W))).s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' :
  (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ t₁).f (W := W) ≫ w₁.s (W := W) =
    (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ t₁).s (W := W) ≫ w₁.f (W := W)
refine_1 :
  ∀ (w₂ : W.LeftFraction (z₂.Y' (W := W)) U)
    (fac₂' :
      (RightFraction.mk (W := W) (z₂.s (W := W)) ⋯ t₂).f (W := W) ≫ w₂.s (W := W) =
        (RightFraction.mk (W := W) (z₂.s (W := W)) ⋯ t₂).s (W := W) ≫ w₂.f (W := W)),
    Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
      ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)
⊢ Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
    ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)

Tactic:
obtain ⟨w₂, fac₂'⟩ := exists_leftFraction (RightFraction.mk z₂.s z₂.hs t₂)

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
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₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ :
  (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).f (W := W) ≫ z₁.s (W := W) =
    (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ :
  (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₂.f (W := W))).f (W := W) ≫ z₂.s (W := W) =
    (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₂.f (W := W))).s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' :
  (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ t₁).f (W := W) ≫ w₁.s (W := W) =
    (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ t₁).s (W := W) ≫ w₁.f (W := W)
w₂ : W.LeftFraction (z₂.Y' (W := W)) U
fac₂' :
  (RightFraction.mk (W := W) (z₂.s (W := W)) ⋯ t₂).f (W := W) ≫ w₂.s (W := W) =
    (RightFraction.mk (W := W) (z₂.s (W := W)) ⋯ t₂).s (W := W) ≫ w₂.f (W := W)
refine_1 :
  ∀ (u : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W)))
    (fac₃ :
      (RightFraction.mk (W := W) (w₁.s (W := W)) ⋯ (w₂.s (W := W))).f (W := W) ≫ u.s (W := W) =
        (RightFraction.mk (W := W) (w₁.s (W := W)) ⋯ (w₂.s (W := W))).s (W := W) ≫ u.f (W := W)),
    Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
      ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)
⊢ Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
    ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)

Tactic:
obtain ⟨u, fac₃⟩ := exists_leftFraction (RightFraction.mk w₁.s w₁.hs w₂.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
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₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ : b₁.f (W := W) ≫ z₁.s (W := W) = a.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ : b₂.f (W := W) ≫ z₂.s (W := W) = a.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' : t₁ ≫ w₁.s (W := W) = z₁.s (W := W) ≫ w₁.f (W := W)
w₂ : W.LeftFraction (z₂.Y' (W := W)) U
fac₂' : t₂ ≫ w₂.s (W := W) = z₂.s (W := W) ≫ w₂.f (W := W)
u : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : w₂.s (W := W) ≫ u.s (W := W) = w₁.s (W := W) ≫ u.f (W := W)
rw :
  b₁.f (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    a.s (W := W) ≫ z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
rw₁ :
  b₁.f (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    b₂.f (W := W) ≫ z₂.s (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
rw₂ : b₁.f (W := W) ≫ t₁ ≫ w₁.s (W := W) ≫ u.f (W := W) = b₂.f (W := W) ≫ z₂.s (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
rw₃ : b₁.f (W := W) ≫ t₁ ≫ w₁.s (W := W) ≫ u.f (W := W) = b₂.f (W := W) ≫ t₂ ≫ w₂.s (W := W) ≫ u.s (W := W)
rw₄ : b₂.f (W := W) ≫ t₂ ≫ w₁.s (W := W) ≫ u.f (W := W) = b₂.f (W := W) ≫ t₂ ≫ w₂.s (W := W) ≫ u.s (W := W)
rw₅ rw₆ : b₂.f (W := W) ≫ t₂ ≫ w₁.s (W := W) ≫ u.f (W := W) = b₂.f (W := W) ≫ t₂ ≫ w₁.s (W := W) ≫ u.f (W := W)
⊢ a.s (W := W) ≫ z₁.f (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    a.s (W := W) ≫ z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)

Tactic:
rw [← reassoc_of% fac₁, ← reassoc_of% fac₂, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
        reassoc_of% hft, fac₃]
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ : b₁.f (W := W) ≫ z₁.s (W := W) = a.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ : b₂.f (W := W) ≫ z₂.s (W := W) = a.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' : t₁ ≫ w₁.s (W := W) = z₁.s (W := W) ≫ w₁.f (W := W)
w₂ : W.LeftFraction (z₂.Y' (W := W)) U
fac₂' : t₂ ≫ w₂.s (W := W) = z₂.s (W := W) ≫ w₂.f (W := W)
u : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : w₂.s (W := W) ≫ u.s (W := W) = w₁.s (W := W) ≫ u.f (W := W)
⊢ a.s (W := W) ≫ z₁.f (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    a.s (W := W) ≫ z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)

Tactic:
have eq : a.s ≫ z₁.f ≫ w₁.f ≫ u.f = a.s ≫ z₂.f ≫ w₂.f ≫ u.s := by
      rw [← reassoc_of% fac₁, ← reassoc_of% fac₂, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
        reassoc_of% hft, fac₃]
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ : b₁.f (W := W) ≫ z₁.s (W := W) = a.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ : b₂.f (W := W) ≫ z₂.s (W := W) = a.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' : t₁ ≫ w₁.s (W := W) = z₁.s (W := W) ≫ w₁.f (W := W)
w₂ : W.LeftFraction (z₂.Y' (W := W)) U
fac₂' : t₂ ≫ w₂.s (W := W) = z₂.s (W := W) ≫ w₂.f (W := W)
u : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : w₂.s (W := W) ≫ u.s (W := W) = w₁.s (W := W) ≫ u.f (W := W)
eq :
  a.s (W := W) ≫ z₁.f (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    a.s (W := W) ≫ z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
refine_1 :
  ∀ (Z_1 : C) (p : u.Y' (W := W) ⟶ Z_1) (hp : W p)
    (fac₄ : (z₁.f (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W)) ≫ p = (z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)) ≫ p),
    a.comp (W := W) b₁ = a.comp (W := W) b₂
⊢ a.comp (W := W) b₁ = a.comp (W := W) b₂

Tactic:
obtain ⟨Z, p, hp, fac₄⟩ := HasLeftCalculusOfFractions.ext _ _ _ a.hs eq

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.ext
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z_1 : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z_1
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z_1
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ : b₁.f (W := W) ≫ z₁.s (W := W) = a.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ : b₂.f (W := W) ≫ z₂.s (W := W) = a.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' : t₁ ≫ w₁.s (W := W) = z₁.s (W := W) ≫ w₁.f (W := W)
w₂ : W.LeftFraction (z₂.Y' (W := W)) U
fac₂' : t₂ ≫ w₂.s (W := W) = z₂.s (W := W) ≫ w₂.f (W := W)
u : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : w₂.s (W := W) ≫ u.s (W := W) = w₁.s (W := W) ≫ u.f (W := W)
eq :
  a.s (W := W) ≫ z₁.f (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    a.s (W := W) ≫ z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
Z : C
p : u.Y' (W := W) ⟶ Z
hp : W p
fac₄ : (z₁.f (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W)) ≫ p = (z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)) ≫ p
⊢ z₁.f (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p = z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W) ≫ p

Tactic:
simp only [assoc] at fac₄

Premises used: CategoryTheory.Category.assoc