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 Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.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 U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
⊢ a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)

Tactic:
have eq : a₁.s ≫ t₁ ≫ w₁.f ≫ q.f = a₁.s ≫ t₁ ≫ w₂.f ≫ q.s := by
        rw [← reassoc_of% fac₁', ← fac₃, reassoc_of% hst, reassoc_of% 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.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 U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
refine_2 :
  ∀ (Z_1 : C) (u : q.Y' (W := W) ⟶ Z_1) (hu : W u)
    (fac₄ : (t₁ ≫ w₁.f (W := W) ≫ q.f (W := W)) ≫ u = (t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)) ≫ u),
    LeftFractionRel (W := W) p₁ p₂
⊢ LeftFractionRel (W := W) p₁ p₂

Tactic:
obtain ⟨Z, u, hu, 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.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 U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : (t₁ ≫ w₁.f (W := W) ≫ q.f (W := W)) ≫ u = (t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)) ≫ u
⊢ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u

Tactic:
simp only [assoc] at fac₄

Premises used: CategoryTheory.Category.assoc
-- 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.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 U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
⊢ LeftFractionRel (W := W) p₁ p₂

Tactic:
⟨Z, q.f ≫ u, q.s ≫ u, ?_, ?_, ?_⟩

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
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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.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 U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2 : p₁.s (W := W) ≫ q.f (W := W) ≫ u = p₂.s (W := W) ≫ q.s (W := W) ≫ u
refine_2₁ : p₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2₂ : W (p₁.s (W := W) ≫ q.f (W := W) ≫ u)
⊢ LeftFractionRel (W := W) p₁ p₂

Tactic:
refine ⟨Z, q.f ≫ u, q.s ≫ u, ?_, ?_, ?_⟩
-- 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.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 U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
⊢ p₁.s (W := W) ≫ q.f (W := W) ≫ u = p₂.s (W := W) ≫ q.s (W := W) ≫ u

Tactic:
simp only [p₁, p₂, assoc, reassoc_of% fac₃]

Premises used: CategoryTheory.Category.assoc
-- 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.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 U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2 : a₁.f (W := W) ≫ (t₁ ≫ w₁.f (W := W)) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2₁ : a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2₂ :
  a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = a₂.f (W := W) ≫ (t₂ ≫ w₂.f (W := W)) ≫ q.s (W := W) ≫ u
refine_2₃ :
  a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2₄ :
  a₁.f (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u = a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2₅ refine_2₆ :
  a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u = a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
⊢ p₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u

Tactic:
rw [assoc, assoc, assoc, assoc, fac₄, reassoc_of% hft]

Premises used: CategoryTheory.Category.assoc
-- 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.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 U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2 : W (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) ≫ u)
⊢ W (p₁.s (W := W) ≫ q.f (W := W) ≫ u)

Tactic:
simp only [p₁, assoc, ← reassoc_of% fac₃]

Premises used: CategoryTheory.Category.assoc
-- 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.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 U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
⊢ W (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) ≫ u)

Tactic:
W.comp_mem _ _ b.hs (W.comp_mem _ _ z₂.hs
          (W.comp_mem _ _ w₂.hs (W.comp_mem _ _ q.hs hu)))

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.comp_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 Z_1 : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z_1
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.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 U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
⊢ W (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) ≫ u)

Tactic:
exact W.comp_mem _ _ b.hs (W.comp_mem _ _ z₂.hs
          (W.comp_mem _ _ w₂.hs (W.comp_mem _ _ q.hs hu)))

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.comp_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 Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.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 U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
rw : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)
rw₁ rw₂ : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W)
⊢ a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)

Tactic:
rw [← fac₂', reassoc_of% 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.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 U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
⊢ a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)

Tactic:
have eq : a₂.s ≫ z₂.f ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f := by
        rw [← fac₂', reassoc_of% fac₂]