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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
refine_2 :
  ∀ (Z_1 : C) (u : w₂.Y' (W := W) ⟶ Z_1) (hu : W u)
    (fac₄ : (z₂.f (W := W) ≫ w₂.s (W := W)) ≫ u = (t₂ ≫ w₂.f (W := W)) ≫ u),
    LeftFractionRel (W := W) p₂ (a₂.comp₀ (W := W) b z₂)
⊢ LeftFractionRel (W := W) p₂ (a₂.comp₀ (W := W) b z₂)

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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : (z₂.f (W := W) ≫ w₂.s (W := W)) ≫ u = (t₂ ≫ w₂.f (W := W)) ≫ u
⊢ z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
⊢ LeftFractionRel (W := W) p₂ (a₂.comp₀ (W := W) b z₂)

Tactic:
⟨Z, u, w₂.s ≫ u, ?_, ?_, ?_⟩

Premises used: CategoryTheory.MorphismProperty.LeftFractionRel, Exists.intro, CategoryTheory.CategoryStruct.comp, 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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
refine_2 : p₂.s (W := W) ≫ u = (a₂.comp₀ (W := W) b z₂).s (W := W) ≫ w₂.s (W := W) ≫ u
refine_2₁ : p₂.f (W := W) ≫ u = (a₂.comp₀ (W := W) b z₂).f (W := W) ≫ w₂.s (W := W) ≫ u
refine_2₂ : W (p₂.s (W := W) ≫ u)
⊢ LeftFractionRel (W := W) p₂ (a₂.comp₀ (W := W) b z₂)

Tactic:
refine ⟨Z, u, w₂.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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
refine_2 : (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ≫ u = (b.s (W := W) ≫ z₂.s (W := W)) ≫ w₂.s (W := W) ≫ u
⊢ p₂.s (W := W) ≫ u = (a₂.comp₀ (W := W) b z₂).s (W := W) ≫ w₂.s (W := W) ≫ u

Tactic:
dsimp [p₁, p₂]
-- 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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
⊢ (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ≫ u = (b.s (W := W) ≫ z₂.s (W := W)) ≫ w₂.s (W := W) ≫ u

Tactic:
simp only [assoc]

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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
refine_2 : (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) ≫ u = (a₂.f (W := W) ≫ z₂.f (W := W)) ≫ w₂.s (W := W) ≫ u
⊢ p₂.f (W := W) ≫ u = (a₂.comp₀ (W := W) b z₂).f (W := W) ≫ w₂.s (W := W) ≫ u

Tactic:
dsimp [p₁, p₂]
-- 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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
⊢ (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) ≫ u = (a₂.f (W := W) ≫ z₂.f (W := W)) ≫ w₂.s (W := W) ≫ u

Tactic:
simp only [assoc, 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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
refine_2 : W ((b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ≫ u)
⊢ W (p₂.s (W := W) ≫ u)

Tactic:
dsimp [p₁, p₂]
-- 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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
refine_2 : W (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) ≫ u)
⊢ W ((b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ≫ u)

Tactic:
simp only [assoc]

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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
⊢ W (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) ≫ u)

Tactic:
W.comp_mem _ _ b.hs (W.comp_mem _ _ z₂.hs (W.comp_mem _ _ w₂.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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
⊢ W (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) ≫ u)

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

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 Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
⊢ (mk (W := W) z₁).comp (W := W) (mk (W := W) z₂) = z₁.comp (W := W) z₂

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk, Quot.lift₂, CategoryTheory.MorphismProperty.LeftFraction.comp, rfl, CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.comp
-- 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
f : Hom W X Y
obtain :
  ∀ (z : W.LeftFraction X Y), (Hom.mk (W := W) (ofHom W (𝟙 X))).comp (W := W) (Hom.mk (W := W) z) = Hom.mk (W := W) z
⊢ (Hom.mk (W := W) (ofHom W (𝟙 X))).comp (W := W) f = f

Tactic:
obtain ⟨z, 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
X Y : C
z : W.LeftFraction X Y
⊢ z.f (W := W) ≫ (ofHom W (z.f (W := W))).s (W := W) = (ofHom W (𝟙 X)).s (W := W) ≫ (ofHom W (z.f (W := W))).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
z : W.LeftFraction X Y
rw : Hom.mk (W := W) ((ofHom W (𝟙 X)).comp₀ (W := W) z (ofHom W (z.f (W := W)))) = Hom.mk (W := W) z
⊢ (Hom.mk (W := W) (ofHom W (𝟙 X))).comp (W := W) (Hom.mk (W := W) z) = Hom.mk (W := W) z

Tactic:
rw [Hom.comp_eq, comp_eq (ofHom W (𝟙 X)) z (ofHom W z.f) (by simp)]

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.MorphismProperty.LeftFraction.ofHom, CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.comp_eq, CategoryTheory.MorphismProperty.LeftFraction.comp_eq, CategoryTheory.MorphismProperty.LeftFraction.f
-- 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
z : W.LeftFraction X Y
dsimp : Hom.mk (W := W) (mk (W := W) (𝟙 X ≫ z.f (W := W)) (z.s (W := W) ≫ 𝟙 (z.Y' (W := W))) ⋯) = Hom.mk (W := W) z
⊢ Hom.mk (W := W) ((ofHom W (𝟙 X)).comp₀ (W := W) z (ofHom W (z.f (W := W)))) = Hom.mk (W := W) z

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
X Y : C
z : W.LeftFraction X Y
⊢ Hom.mk (W := W) (mk (W := W) (𝟙 X ≫ z.f (W := W)) (z.s (W := W) ≫ 𝟙 (z.Y' (W := W))) ⋯) = Hom.mk (W := W) z

Tactic:
simp only [id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- 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
f : Hom W X Y
obtain :
  ∀ (z : W.LeftFraction X Y), (Hom.mk (W := W) z).comp (W := W) (Hom.mk (W := W) (ofHom W (𝟙 Y))) = Hom.mk (W := W) z
⊢ f.comp (W := W) (Hom.mk (W := W) (ofHom W (𝟙 Y))) = f

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

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