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_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
refine_1 : mk (W := W) (a.comp₀ (W := W) b₁ z₁) = mk (W := W) (a.comp₀ (W := W) b₂ z₂)
⊢ a.comp (W := W) b₁ = a.comp (W := W) b₂

Tactic:
rw [comp_eq _ _ z₁ fac₁, comp_eq _ _ z₂ fac₂]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.comp_eq
-- 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
refine_1 : LeftFractionRel (W := W) (a.comp₀ (W := W) b₁ z₁) (a.comp₀ (W := W) b₂ z₂)
⊢ mk (W := W) (a.comp₀ (W := W) b₁ z₁) = mk (W := W) (a.comp₀ (W := W) b₂ z₂)

Tactic:
apply Quot.sound

Premises used: Quot.sound
-- 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
⊢ LeftFractionRel (W := W) (a.comp₀ (W := W) b₁ z₁) (a.comp₀ (W := W) b₂ z₂)

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

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 : 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
refine_1 :
  (a.comp₀ (W := W) b₁ z₁).s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p =
    (a.comp₀ (W := W) b₂ z₂).s (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W) ≫ p
refine_1₁ :
  (a.comp₀ (W := W) b₁ z₁).f (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p =
    (a.comp₀ (W := W) b₂ z₂).f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W) ≫ p
refine_1₂ : W ((a.comp₀ (W := W) b₁ z₁).s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p)
⊢ LeftFractionRel (W := W) (a.comp₀ (W := W) b₁ z₁) (a.comp₀ (W := W) b₂ z₂)

Tactic:
refine ⟨Z, w₁.f ≫ u.f ≫ p, w₂.f ≫ u.s ≫ 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 : 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
refine_1 :
  (b₁.s (W := W) ≫ z₁.s (W := W)) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p =
    (b₂.s (W := W) ≫ z₂.s (W := W)) ≫ w₂.f (W := W) ≫ u.s (W := W) ≫ p
⊢ (a.comp₀ (W := W) b₁ z₁).s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p =
    (a.comp₀ (W := W) b₂ z₂).s (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W) ≫ p

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 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
⊢ (b₁.s (W := W) ≫ z₁.s (W := W)) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p =
    (b₂.s (W := W) ≫ z₂.s (W := W)) ≫ w₂.f (W := W) ≫ u.s (W := W) ≫ p

Tactic:
simp only [assoc, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
        reassoc_of% hst, 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 : 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
refine_1 :
  (a.f (W := W) ≫ z₁.f (W := W)) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p =
    (a.f (W := W) ≫ z₂.f (W := W)) ≫ w₂.f (W := W) ≫ u.s (W := W) ≫ p
⊢ (a.comp₀ (W := W) b₁ z₁).f (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p =
    (a.comp₀ (W := W) b₂ z₂).f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W) ≫ p

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 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
⊢ (a.f (W := W) ≫ z₁.f (W := W)) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p =
    (a.f (W := W) ≫ z₂.f (W := W)) ≫ w₂.f (W := W) ≫ u.s (W := W) ≫ p

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 : 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
refine_1 : W ((b₁.s (W := W) ≫ z₁.s (W := W)) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p)
⊢ W ((a.comp₀ (W := W) b₁ z₁).s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p)

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 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
refine_1 : W (b₁.s (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p)
⊢ W ((b₁.s (W := W) ≫ z₁.s (W := W)) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p)

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 : 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
refine_1 : W ((b₁.s (W := W) ≫ t₁) ≫ w₂.s (W := W) ≫ u.s (W := W) ≫ p)
⊢ W (b₁.s (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p)

Tactic:
rw [← reassoc_of% fac₁', ← reassoc_of% fac₃, ← 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 : 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
⊢ W ((b₁.s (W := W) ≫ t₁) ≫ w₂.s (W := W) ≫ u.s (W := W) ≫ p)

Tactic:
W.comp_mem _ _ ht (W.comp_mem _ _ w₂.hs (W.comp_mem _ _ u.hs hp))

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 : 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
⊢ W ((b₁.s (W := W) ≫ t₁) ≫ w₂.s (W := W) ≫ u.s (W := W) ≫ p)

Tactic:
exact W.comp_mem _ _ ht (W.comp_mem _ _ w₂.hs (W.comp_mem _ _ u.hs hp))

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₁ : Hom W X Y
z₂ : 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₁)
refine_2 :
  ∀ (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₁ 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₁ :
  (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_2 :
  ∀ (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