awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁_1 : Hom W X Y
z₂ : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ :
  (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).f (W := W) ≫ z₁.s (W := W) =
    (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).s (W := W) ≫ z₁.f (W := W)
⊢ 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₂)
have refine_1 : ∀ (z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W)))
  (fac₂ :
    (RightFraction.mk (W := W) (a.s (W := W)) sorry (b₂.f (W := W))).f (W := W) ≫ z₂.s (W := W) =
      (RightFraction.mk (W := W) (a.s (W := W)) sorry (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₂)
Tactic: obtain ⟨z₂, fac₂⟩ := exists_leftFraction (RightFraction.mk a.s a.hs b₂.f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ :
  (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).f (W := W) ≫ z₁.s (W := W) =
    (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ :
  (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₂.f (W := W))).f (W := W) ≫ z₂.s (W := W) =
    (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₂.f (W := W))).s (W := W) ≫ z₂.f (W := W)
⊢ 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₂)
have refine_1 : ∀ (w₁ : W.LeftFraction (z₁.Y' (W := W)) U)
  (fac₁' :
    (RightFraction.mk (W := W) (z₁.s (W := W)) sorry t₁).f (W := W) ≫ w₁.s (W := W) =
      (RightFraction.mk (W := W) (z₁.s (W := W)) sorry t₁).s (W := W) ≫ w₁.f (W := W)),
  Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
    ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)
Tactic: obtain ⟨w₁, fac₁'⟩ := exists_leftFraction (RightFraction.mk z₁.s z₁.hs t₁)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ :
  (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).f (W := W) ≫ z₁.s (W := W) =
    (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ :
  (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₂.f (W := W))).f (W := W) ≫ z₂.s (W := W) =
    (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₂.f (W := W))).s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' :
  (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ t₁).f (W := W) ≫ w₁.s (W := W) =
    (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ t₁).s (W := W) ≫ w₁.f (W := W)
⊢ 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₂)
have refine_1 : ∀ (w₂ : W.LeftFraction (z₂.Y' (W := W)) U)
  (fac₂' :
    (RightFraction.mk (W := W) (z₂.s (W := W)) sorry t₂).f (W := W) ≫ w₂.s (W := W) =
      (RightFraction.mk (W := W) (z₂.s (W := W)) sorry t₂).s (W := W) ≫ w₂.f (W := W)),
  Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
    ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)
Tactic: obtain ⟨w₂, fac₂'⟩ := exists_leftFraction (RightFraction.mk z₂.s z₂.hs t₂)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ :
  (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).f (W := W) ≫ z₁.s (W := W) =
    (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₁.f (W := W))).s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ :
  (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₂.f (W := W))).f (W := W) ≫ z₂.s (W := W) =
    (RightFraction.mk (W := W) (a.s (W := W)) ⋯ (b₂.f (W := W))).s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' :
  (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ t₁).f (W := W) ≫ w₁.s (W := W) =
    (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ t₁).s (W := W) ≫ w₁.f (W := W)
w₂ : W.LeftFraction (z₂.Y' (W := W)) U
fac₂' :
  (RightFraction.mk (W := W) (z₂.s (W := W)) ⋯ t₂).f (W := W) ≫ w₂.s (W := W) =
    (RightFraction.mk (W := W) (z₂.s (W := W)) ⋯ t₂).s (W := W) ≫ w₂.f (W := W)
⊢ 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₂)
have refine_1 : ∀ (u : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W)))
  (fac₃ :
    (RightFraction.mk (W := W) (w₁.s (W := W)) sorry (w₂.s (W := W))).f (W := W) ≫ u.s (W := W) =
      (RightFraction.mk (W := W) (w₁.s (W := W)) sorry (w₂.s (W := W))).s (W := W) ≫ u.f (W := W)),
  Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
    ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)
Tactic: obtain ⟨u, fac₃⟩ := exists_leftFraction (RightFraction.mk w₁.s w₁.hs w₂.s)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ : b₁.f (W := W) ≫ z₁.s (W := W) = a.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ : b₂.f (W := W) ≫ z₂.s (W := W) = a.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' : t₁ ≫ w₁.s (W := W) = z₁.s (W := W) ≫ w₁.f (W := W)
w₂ : W.LeftFraction (z₂.Y' (W := W)) U
fac₂' : t₂ ≫ w₂.s (W := W) = z₂.s (W := W) ≫ w₂.f (W := W)
u : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : w₂.s (W := W) ≫ u.s (W := W) = w₁.s (W := W) ≫ u.f (W := W)
⊢ a.s (W := W) ≫ z₁.f (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    a.s (W := W) ≫ z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
have rw : b₁.f (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
  a.s (W := W) ≫ z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
Tactic: rw [← reassoc_of% fac₁, ← reassoc_of% fac₂, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
        reassoc_of% hft, fac₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ : b₁.f (W := W) ≫ z₁.s (W := W) = a.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ : b₂.f (W := W) ≫ z₂.s (W := W) = a.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' : t₁ ≫ w₁.s (W := W) = z₁.s (W := W) ≫ w₁.f (W := W)
w₂ : W.LeftFraction (z₂.Y' (W := W)) U
fac₂' : t₂ ≫ w₂.s (W := W) = z₂.s (W := W) ≫ w₂.f (W := W)
u : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : w₂.s (W := W) ≫ u.s (W := W) = w₁.s (W := W) ≫ u.f (W := W)
rw :
  b₁.f (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    a.s (W := W) ≫ z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
⊢ 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)
have rw₁ : b₁.f (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
  b₂.f (W := W) ≫ z₂.s (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
Tactic: rw [← reassoc_of% fac₁, ← reassoc_of% fac₂, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
        reassoc_of% hft, fac₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ : b₁.f (W := W) ≫ z₁.s (W := W) = a.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ : b₂.f (W := W) ≫ z₂.s (W := W) = a.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' : t₁ ≫ w₁.s (W := W) = z₁.s (W := W) ≫ w₁.f (W := W)
w₂ : W.LeftFraction (z₂.Y' (W := W)) U
fac₂' : t₂ ≫ w₂.s (W := W) = z₂.s (W := W) ≫ w₂.f (W := W)
u : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : w₂.s (W := W) ≫ u.s (W := W) = w₁.s (W := W) ≫ u.f (W := W)
rw :
  b₁.f (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    a.s (W := W) ≫ z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
rw₁ :
  b₁.f (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    b₂.f (W := W) ≫ z₂.s (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
⊢ 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)
have rw₂ : b₁.f (W := W) ≫ t₁ ≫ w₁.s (W := W) ≫ u.f (W := W) = b₂.f (W := W) ≫ z₂.s (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
Tactic: rw [← reassoc_of% fac₁, ← reassoc_of% fac₂, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
        reassoc_of% hft, fac₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ : b₁.f (W := W) ≫ z₁.s (W := W) = a.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ : b₂.f (W := W) ≫ z₂.s (W := W) = a.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' : t₁ ≫ w₁.s (W := W) = z₁.s (W := W) ≫ w₁.f (W := W)
w₂ : W.LeftFraction (z₂.Y' (W := W)) U
fac₂' : t₂ ≫ w₂.s (W := W) = z₂.s (W := W) ≫ w₂.f (W := W)
u : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : w₂.s (W := W) ≫ u.s (W := W) = w₁.s (W := W) ≫ u.f (W := W)
rw :
  b₁.f (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    a.s (W := W) ≫ z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
rw₁ :
  b₁.f (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    b₂.f (W := W) ≫ z₂.s (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
rw₂ : b₁.f (W := W) ≫ t₁ ≫ w₁.s (W := W) ≫ u.f (W := W) = b₂.f (W := W) ≫ z₂.s (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
⊢ 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)
have rw₃ : b₁.f (W := W) ≫ t₁ ≫ w₁.s (W := W) ≫ u.f (W := W) = b₂.f (W := W) ≫ t₂ ≫ w₂.s (W := W) ≫ u.s (W := W)
Tactic: rw [← reassoc_of% fac₁, ← reassoc_of% fac₂, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
        reassoc_of% hft, fac₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ : b₁.f (W := W) ≫ z₁.s (W := W) = a.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ : b₂.f (W := W) ≫ z₂.s (W := W) = a.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' : t₁ ≫ w₁.s (W := W) = z₁.s (W := W) ≫ w₁.f (W := W)
w₂ : W.LeftFraction (z₂.Y' (W := W)) U
fac₂' : t₂ ≫ w₂.s (W := W) = z₂.s (W := W) ≫ w₂.f (W := W)
u : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : w₂.s (W := W) ≫ u.s (W := W) = w₁.s (W := W) ≫ u.f (W := W)
rw :
  b₁.f (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    a.s (W := W) ≫ z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
rw₁ :
  b₁.f (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    b₂.f (W := W) ≫ z₂.s (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
rw₂ : b₁.f (W := W) ≫ t₁ ≫ w₁.s (W := W) ≫ u.f (W := W) = b₂.f (W := W) ≫ z₂.s (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
rw₃ : b₁.f (W := W) ≫ t₁ ≫ w₁.s (W := W) ≫ u.f (W := W) = b₂.f (W := W) ≫ t₂ ≫ w₂.s (W := W) ≫ u.s (W := W)
⊢ 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)
have rw₄ : b₂.f (W := W) ≫ t₂ ≫ w₁.s (W := W) ≫ u.f (W := W) = b₂.f (W := W) ≫ t₂ ≫ w₂.s (W := W) ≫ u.s (W := W)
Tactic: rw [← reassoc_of% fac₁, ← reassoc_of% fac₂, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
        reassoc_of% hft, fac₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ : b₁.f (W := W) ≫ z₁.s (W := W) = a.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ : b₂.f (W := W) ≫ z₂.s (W := W) = a.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' : t₁ ≫ w₁.s (W := W) = z₁.s (W := W) ≫ w₁.f (W := W)
w₂ : W.LeftFraction (z₂.Y' (W := W)) U
fac₂' : t₂ ≫ w₂.s (W := W) = z₂.s (W := W) ≫ w₂.f (W := W)
u : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : w₂.s (W := W) ≫ u.s (W := W) = w₁.s (W := W) ≫ u.f (W := W)
rw :
  b₁.f (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    a.s (W := W) ≫ z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
rw₁ :
  b₁.f (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    b₂.f (W := W) ≫ z₂.s (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
rw₂ : b₁.f (W := W) ≫ t₁ ≫ w₁.s (W := W) ≫ u.f (W := W) = b₂.f (W := W) ≫ z₂.s (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
rw₃ : b₁.f (W := W) ≫ t₁ ≫ w₁.s (W := W) ≫ u.f (W := W) = b₂.f (W := W) ≫ t₂ ≫ w₂.s (W := W) ≫ u.s (W := W)
rw₄ : b₂.f (W := W) ≫ t₂ ≫ w₁.s (W := W) ≫ u.f (W := W) = b₂.f (W := W) ≫ t₂ ≫ w₂.s (W := W) ≫ u.s (W := W)
⊢ 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)
have rw₅ : b₂.f (W := W) ≫ t₂ ≫ w₁.s (W := W) ≫ u.f (W := W) = b₂.f (W := W) ≫ t₂ ≫ w₁.s (W := W) ≫ u.f (W := W)
Tactic: rw [← reassoc_of% fac₁, ← reassoc_of% fac₂, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
        reassoc_of% hft, fac₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (hypothesis)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ : b₁.f (W := W) ≫ z₁.s (W := W) = a.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ : b₂.f (W := W) ≫ z₂.s (W := W) = a.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' : t₁ ≫ w₁.s (W := W) = z₁.s (W := W) ≫ w₁.f (W := W)
w₂ : W.LeftFraction (z₂.Y' (W := W)) U
fac₂' : t₂ ≫ w₂.s (W := W) = z₂.s (W := W) ≫ w₂.f (W := W)
u : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : w₂.s (W := W) ≫ u.s (W := W) = w₁.s (W := W) ≫ u.f (W := W)
⊢ a.comp (W := W) b₁ = a.comp (W := W) b₂
have 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)
Tactic: have eq : a.s ≫ z₁.f ≫ w₁.f ≫ u.f = a.s ≫ z₂.f ≫ w₂.f ≫ u.s := by
      rw [← reassoc_of% fac₁, ← reassoc_of% fac₂, ← reassoc_of% fac₁', ← reassoc_of% fac₂',
        reassoc_of% hft, fac₃]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
W : MorphismProperty.{v_1, u_1} C
inst_2 : W.HasLeftCalculusOfFractions
X Y Z : C
z₁_1 : Hom W X Y
z₂_1 : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' (W := W) ⟶ U
t₂ : b₂.Y' (W := W) ⟶ U
hst : b₁.s (W := W) ≫ t₁ = b₂.s (W := W) ≫ t₂
hft : b₁.f (W := W) ≫ t₁ = b₂.f (W := W) ≫ t₂
ht : W (b₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a.Y' (W := W)) (b₁.Y' (W := W))
fac₁ : b₁.f (W := W) ≫ z₁.s (W := W) = a.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a.Y' (W := W)) (b₂.Y' (W := W))
fac₂ : b₂.f (W := W) ≫ z₂.s (W := W) = a.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction (z₁.Y' (W := W)) U
fac₁' : t₁ ≫ w₁.s (W := W) = z₁.s (W := W) ≫ w₁.f (W := W)
w₂ : W.LeftFraction (z₂.Y' (W := W)) U
fac₂' : t₂ ≫ w₂.s (W := W) = z₂.s (W := W) ≫ w₂.f (W := W)
u : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : w₂.s (W := W) ≫ u.s (W := W) = w₁.s (W := W) ≫ u.f (W := W)
eq :
  a.s (W := W) ≫ z₁.f (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) =
    a.s (W := W) ≫ z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)
⊢ a.comp (W := W) b₁ = a.comp (W := W) b₂
have refine_1 : ∀ (Z_1 : C) (p : u.Y' (W := W) ⟶ Z_1) (hp : W p)
  (fac₄ : (z₁.f (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W)) ≫ p = (z₂.f (W := W) ≫ w₂.f (W := W) ≫ u.s (W := W)) ≫ p),
  a.comp (W := W) b₁ = a.comp (W := W) b₂
Tactic: obtain ⟨Z, p, hp, fac₄⟩ := HasLeftCalculusOfFractions.ext _ _ _ a.hs eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (hypothesis)
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.comp (W := W) b₁ = a.comp (W := W) b₂
have 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
Tactic: simp only [assoc] at fac₄
Cleared hypotheses: fac₄
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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.comp (W := W) b₁ = a.comp (W := W) b₂
have refine_1 : mk (W := W) (a.comp₀ (W := W) b₁ z₁) = mk (W := W) (a.comp₀ (W := W) b₂ z₂)
Tactic: rw [comp_eq _ _ z₁ fac₁, comp_eq _ _ z₂ fac₂]