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

Tactic:
rw [Hom.comp_eq, comp_eq z (ofHom W (𝟙 Y)) (ofInv z.s z.hs) (by simp)]

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

Tactic:
dsimp [comp₀]

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

Tactic:
simp only [comp_id, id_comp]

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₁ X₂ X₃ X₄ : C
f₁ : Hom W X₁ X₂
f₂ : Hom W X₂ X₃
f₃ : Hom W X₃ X₄
obtain :
  ∀ (z₁ : W.LeftFraction X₁ X₂),
    ((Hom.mk (W := W) z₁).comp (W := W) f₂).comp (W := W) f₃ = (Hom.mk (W := W) z₁).comp (W := W) (f₂.comp (W := W) f₃)
⊢ (f₁.comp (W := W) f₂).comp (W := W) f₃ = f₁.comp (W := W) (f₂.comp (W := W) 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₁ X₂ X₃ X₄ : C
f₂ : Hom W X₂ X₃
f₃ : Hom W X₃ X₄
z₁ : W.LeftFraction X₁ X₂
obtain :
  ∀ (z₂ : W.LeftFraction X₂ X₃),
    ((Hom.mk (W := W) z₁).comp (W := W) (Hom.mk (W := W) z₂)).comp (W := W) f₃ =
      (Hom.mk (W := W) z₁).comp (W := W) ((Hom.mk (W := W) z₂).comp (W := W) f₃)
⊢ ((Hom.mk (W := W) z₁).comp (W := W) f₂).comp (W := W) f₃ = (Hom.mk (W := W) z₁).comp (W := W) (f₂.comp (W := W) 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₁ X₂ X₃ X₄ : C
f₃ : Hom W X₃ X₄
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
obtain :
  ∀ (z₃ : W.LeftFraction X₃ X₄),
    ((Hom.mk (W := W) z₁).comp (W := W) (Hom.mk (W := W) z₂)).comp (W := W) (Hom.mk (W := W) z₃) =
      (Hom.mk (W := W) z₁).comp (W := W) ((Hom.mk (W := W) z₂).comp (W := W) (Hom.mk (W := W) z₃))
⊢ ((Hom.mk (W := W) z₁).comp (W := W) (Hom.mk (W := W) z₂)).comp (W := W) f₃ =
    (Hom.mk (W := W) z₁).comp (W := W) ((Hom.mk (W := W) z₂).comp (W := W) 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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
obtain :
  ∀ (z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W)))
    (fac₁₂ :
      (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ (z₂.f (W := W))).f (W := W) ≫ z₁₂.s (W := W) =
        (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ (z₂.f (W := W))).s (W := W) ≫ z₁₂.f (W := W)),
    (z₁.comp (W := W) z₂).comp (W := W) (Hom.mk (W := W) z₃) = (Hom.mk (W := W) z₁).comp (W := W) (z₂.comp (W := W) z₃)
⊢ (z₁.comp (W := W) z₂).comp (W := W) (Hom.mk (W := W) z₃) = (Hom.mk (W := W) z₁).comp (W := W) (z₂.comp (W := W) z₃)

Tactic:
obtain ⟨z₁₂, fac₁₂⟩ := exists_leftFraction (RightFraction.mk z₁.s z₁.hs z₂.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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ :
  (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ (z₂.f (W := W))).f (W := W) ≫ z₁₂.s (W := W) =
    (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ (z₂.f (W := W))).s (W := W) ≫ z₁₂.f (W := W)
obtain :
  ∀ (z₂₃ : W.LeftFraction (z₂.Y' (W := W)) (z₃.Y' (W := W)))
    (fac₂₃ :
      (RightFraction.mk (W := W) (z₂.s (W := W)) ⋯ (z₃.f (W := W))).f (W := W) ≫ z₂₃.s (W := W) =
        (RightFraction.mk (W := W) (z₂.s (W := W)) ⋯ (z₃.f (W := W))).s (W := W) ≫ z₂₃.f (W := W)),
    (z₁.comp (W := W) z₂).comp (W := W) (Hom.mk (W := W) z₃) = (Hom.mk (W := W) z₁).comp (W := W) (z₂.comp (W := W) z₃)
⊢ (z₁.comp (W := W) z₂).comp (W := W) (Hom.mk (W := W) z₃) = (Hom.mk (W := W) z₁).comp (W := W) (z₂.comp (W := W) z₃)

Tactic:
obtain ⟨z₂₃, fac₂₃⟩ := exists_leftFraction (RightFraction.mk z₂.s z₂.hs z₃.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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ :
  (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ (z₂.f (W := W))).f (W := W) ≫ z₁₂.s (W := W) =
    (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ (z₂.f (W := W))).s (W := W) ≫ z₁₂.f (W := W)
z₂₃ : W.LeftFraction (z₂.Y' (W := W)) (z₃.Y' (W := W))
fac₂₃ :
  (RightFraction.mk (W := W) (z₂.s (W := W)) ⋯ (z₃.f (W := W))).f (W := W) ≫ z₂₃.s (W := W) =
    (RightFraction.mk (W := W) (z₂.s (W := W)) ⋯ (z₃.f (W := W))).s (W := W) ≫ z₂₃.f (W := W)
obtain :
  ∀ (z' : W.LeftFraction (z₁₂.Y' (W := W)) (z₂₃.Y' (W := W)))
    (fac :
      (RightFraction.mk (W := W) (z₁₂.s (W := W)) ⋯ (z₂₃.f (W := W))).f (W := W) ≫ z'.s (W := W) =
        (RightFraction.mk (W := W) (z₁₂.s (W := W)) ⋯ (z₂₃.f (W := W))).s (W := W) ≫ z'.f (W := W)),
    (z₁.comp (W := W) z₂).comp (W := W) (Hom.mk (W := W) z₃) = (Hom.mk (W := W) z₁).comp (W := W) (z₂.comp (W := W) z₃)
⊢ (z₁.comp (W := W) z₂).comp (W := W) (Hom.mk (W := W) z₃) = (Hom.mk (W := W) z₁).comp (W := W) (z₂.comp (W := W) z₃)

Tactic:
obtain ⟨z', fac⟩ := exists_leftFraction (RightFraction.mk z₁₂.s z₁₂.hs z₂₃.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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ : 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₃.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₂₃.f (W := W) ≫ z'.s (W := W) = z₁₂.s (W := W) ≫ z'.f (W := W)
dsimp : z₃.f (W := W) ≫ z₂₃.s (W := W) ≫ z'.s (W := W) = (z₂.s (W := W) ≫ z₁₂.s (W := W)) ≫ z'.f (W := W)
⊢ z₃.f (W := W) ≫ (mk (W := W) (z'.f (W := W)) (z₂₃.s (W := W) ≫ z'.s (W := W)) ⋯).s (W := W) =
    (mk (W := W) (z₁.f (W := W) ≫ z₁₂.f (W := W)) (z₂.s (W := W) ≫ z₁₂.s (W := W)) ⋯).s (W := W) ≫
      (mk (W := W) (z'.f (W := W)) (z₂₃.s (W := W) ≫ z'.s (W := W)) ⋯).f (W := W)

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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ : 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₃.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₂₃.f (W := W) ≫ z'.s (W := W) = z₁₂.s (W := W) ≫ z'.f (W := W)
rw : z₃.f (W := W) ≫ z₂₃.s (W := W) ≫ z'.s (W := W) = z₂.s (W := W) ≫ z₁₂.s (W := W) ≫ z'.f (W := W)
rw₁ : z₂.s (W := W) ≫ z₂₃.f (W := W) ≫ z'.s (W := W) = z₂.s (W := W) ≫ z₁₂.s (W := W) ≫ z'.f (W := W)
rw₂ rw₃ : z₂.s (W := W) ≫ z₁₂.s (W := W) ≫ z'.f (W := W) = z₂.s (W := W) ≫ z₁₂.s (W := W) ≫ z'.f (W := W)
⊢ z₃.f (W := W) ≫ z₂₃.s (W := W) ≫ z'.s (W := W) = (z₂.s (W := W) ≫ z₁₂.s (W := W)) ≫ z'.f (W := W)

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

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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ : 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₃.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₂₃.f (W := W) ≫ z'.s (W := W) = z₁₂.s (W := W) ≫ z'.f (W := W)
rw : z₂.f (W := W) ≫ z₂₃.f (W := W) ≫ z'.s (W := W) = z₁.s (W := W) ≫ z₁₂.f (W := W) ≫ z'.f (W := W)
rw₁ : z₂.f (W := W) ≫ z₂₃.f (W := W) ≫ z'.s (W := W) = z₂.f (W := W) ≫ z₁₂.s (W := W) ≫ z'.f (W := W)
rw₂ rw₃ : z₂.f (W := W) ≫ z₁₂.s (W := W) ≫ z'.f (W := W) = z₂.f (W := W) ≫ z₁₂.s (W := W) ≫ z'.f (W := W)
⊢ (z₂.f (W := W) ≫ z₂₃.f (W := W)) ≫ z'.s (W := W) = z₁.s (W := W) ≫ z₁₂.f (W := W) ≫ z'.f (W := W)

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

Tactic:
rw [comp_eq z₁ z₂ z₁₂ fac₁₂, comp_eq z₂ z₃ z₂₃ fac₂₃, comp₀, comp₀,
      Hom.comp_eq, Hom.comp_eq,
      comp_eq _ z₃ (mk z'.f (z₂₃.s ≫ z'.s) (W.comp_mem _ _ z₂₃.hs z'.hs))
        (by dsimp; rw [assoc, reassoc_of% fac₂₃, fac]),
      comp_eq z₁ _ (mk (z₁₂.f ≫ z'.f) z'.s z'.hs)
        (by dsimp; rw [assoc, ← reassoc_of% fac₁₂, fac])]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.LeftFraction.mk, CategoryTheory.MorphismProperty.LeftFraction.comp₀, CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.comp_eq, CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.LeftFraction.comp_eq, 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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ : 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₃.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₂₃.f (W := W) ≫ z'.s (W := W) = z₁₂.s (W := W) ≫ z'.f (W := W)
⊢ Hom.mk (W := W)
      ((mk (W := W) (z₁.f (W := W) ≫ z₁₂.f (W := W)) (z₂.s (W := W) ≫ z₁₂.s (W := W)) ⋯).comp₀ (W := W) z₃
        (mk (W := W) (z'.f (W := W)) (z₂₃.s (W := W) ≫ z'.s (W := W)) ⋯)) =
    Hom.mk (W := W)
      (z₁.comp₀ (W := W) (mk (W := W) (z₂.f (W := W) ≫ z₂₃.f (W := W)) (z₃.s (W := W) ≫ z₂₃.s (W := W)) ⋯)
        (mk (W := W) (z₁₂.f (W := W) ≫ z'.f (W := W)) (z'.s (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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (ofHom W g).f (W := W) ≫ (ofHom W g).s (W := W) = (ofHom W f).s (W := W) ≫ (ofHom W g).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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
rw : Hom.mk (W := W) (ofHom W (f ≫ g)) = Hom.mk (W := W) ((ofHom W f).comp₀ (W := W) (ofHom W g) (ofHom W g))
⊢ Hom.mk (W := W) (ofHom W (f ≫ g)) = (Hom.mk (W := W) (ofHom W f)).comp (W := W) (Hom.mk (W := W) (ofHom W g))

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

Premises used: CategoryTheory.MorphismProperty.LeftFraction.ofHom, CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.comp_eq, 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 : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.mk (W := W) (ofHom W (f ≫ g)) = Hom.mk (W := W) ((ofHom W f).comp₀ (W := W) (ofHom W g) (ofHom W g))

Tactic:
simp only [ofHom, comp₀, comp_id]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.ofHom, CategoryTheory.Category.comp_id, 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 : C
f : W.LeftFraction X Y
⊢ homMk (W := W) f = Hom.mk (W := W) f

Tactic:
rfl

Premises used: 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 : C
f : X ⟶ Y
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (Functor.map (Q W) f) (homMk (W := W) (ofHom W f))

Tactic:
rfl

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk, 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)
rw : z₁.comp (W := W) z₂ = homMk (W := W) (z₁.comp₀ (W := W) z₂ z₃)
rw₁ rw₂ : Hom.mk (W := W) (z₁.comp₀ (W := W) z₂ z₃) = homMk (W := W) (z₁.comp₀ (W := W) z₂ z₃)
⊢ Eq (α := Hom W (Functor.obj (Q W) X) (Functor.obj (Q W) Z))
    (Hom.comp (W := W) (homMk (W := W) z₁) (homMk (W := W) z₂)) (homMk (W := W) (z₁.comp₀ (W := W) z₂ z₃))

Tactic:
rw [Hom.comp_eq, comp_eq z₁ z₂ z₃ h₃]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.comp_eq, CategoryTheory.MorphismProperty.LeftFraction.comp_eq
-- 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 : C
z₁ z₂ : W.LeftFraction X Y
h : LeftFractionRel (W := W) z₁ z₂
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (homMk (W := W) z₁) (homMk (W := W) z₂)

Tactic:
Quot.sound h

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk, Quot.sound, CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom
-- 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 : C
z₁ z₂ : W.LeftFraction X Y
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (homMk (W := W) z₁) (homMk (W := W) z₂) ↔
    LeftFractionRel (W := W) z₁ z₂

Tactic:
@Equivalence.quot_mk_eq_iff _ _ (equivalenceLeftFractionRel W X Y) _ _

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk, CategoryTheory.MorphismProperty.equivalenceLeftFractionRel, Equivalence.quot_mk_eq_iff, CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom
-- 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 Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
dsimp :
  Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y)
    (homMk (W := W) (ofHom W f) ≫ homMk (W := W) (ofInv (W := W) s hs)) (homMk (W := W) (mk (W := W) f s hs))
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (Functor.map (Q W) f ≫ Qinv (W := W) s hs)
    (homMk (W := W) (mk (W := W) f s hs))

Tactic:
dsimp only [Q_map, Qinv]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv, CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map
-- 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 Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ (ofInv (W := W) s hs).f (W := W) ≫ (ofHom W (𝟙 ((ofHom W f).Y' (W := W)))).s (W := W) =
    (ofHom W f).s (W := W) ≫ (ofHom W (𝟙 ((ofHom W f).Y' (W := W)))).f (W := W)

Tactic:
simp
-- 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 Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
rw :
  Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y)
    (homMk (W := W) ((ofHom W f).comp₀ (W := W) (ofInv (W := W) s hs) (ofHom W (𝟙 ((ofHom W f).Y' (W := W))))))
    (homMk (W := W) (mk (W := W) f s hs))
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y)
    (homMk (W := W) (ofHom W f) ≫ homMk (W := W) (ofInv (W := W) s hs)) (homMk (W := W) (mk (W := W) f s hs))

Tactic:
rw [homMk_comp_homMk (ofHom W f) (ofInv s hs) (ofHom W (𝟙 _)) (by simp)]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_comp_homMk, CategoryTheory.CategoryStruct.id, CategoryTheory.MorphismProperty.LeftFraction.ofHom, CategoryTheory.MorphismProperty.LeftFraction.ofInv
-- 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 Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y)
    (homMk (W := W) ((ofHom W f).comp₀ (W := W) (ofInv (W := W) s hs) (ofHom W (𝟙 ((ofHom W f).Y' (W := W))))))
    (homMk (W := W) (mk (W := W) f s hs))

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
s : X ⟶ Y
hs : W s
rw : homMk (W := W) (mk (W := W) s s hs) = 𝟙 (Functor.obj (Q W) X)
⊢ Functor.map (Q W) s ≫ Qinv (W := W) s hs = 𝟙 (Functor.obj (Q W) X)

Tactic:
rw [Q_map_comp_Qinv]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map_comp_Qinv