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_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
⊢ mk (W := W) (a.comp₀ (W := W) b₁ z₁) = mk (W := W) (a.comp₀ (W := W) b₂ z₂)
have refine_1 : LeftFractionRel (W := W) (a.comp₀ (W := W) b₁ z₁) (a.comp₀ (W := W) b₂ z₂)
Tactic: apply Quot.sound
-- 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
⊢ LeftFractionRel (W := W) (a.comp₀ (W := W) b₁ z₁) (a.comp₀ (W := W) b₂ z₂)
have 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
Tactic: refine ⟨Z, w₁.f ≫ u.f ≫ p, w₂.f ≫ u.s ≫ p, ?_, ?_, ?_⟩
-- 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
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
⊢ LeftFractionRel (W := W) (a.comp₀ (W := W) b₁ z₁) (a.comp₀ (W := W) b₂ z₂)
have 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
Tactic: refine ⟨Z, w₁.f ≫ u.f ≫ p, w₂.f ≫ u.s ≫ p, ?_, ?_, ?_⟩
-- 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
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
⊢ LeftFractionRel (W := W) (a.comp₀ (W := W) b₁ z₁) (a.comp₀ (W := W) b₂ z₂)
have refine_1₂ : W ((a.comp₀ (W := W) b₁ z₁).s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p)
Tactic: refine ⟨Z, w₁.f ≫ u.f ≫ p, w₂.f ≫ u.s ≫ p, ?_, ?_, ?_⟩
-- 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₁ 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
have 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
Tactic: dsimp
-- 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₁ 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
have 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
Tactic: dsimp
-- 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
⊢ W ((a.comp₀ (W := W) b₁ z₁).s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p)
have refine_1 : W ((b₁.s (W := W) ≫ z₁.s (W := W)) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p)
Tactic: dsimp
-- 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
⊢ W ((b₁.s (W := W) ≫ z₁.s (W := W)) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p)
have refine_1 : W (b₁.s (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p)
Tactic: simp only [assoc]
-- 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
⊢ W (b₁.s (W := W) ≫ z₁.s (W := W) ≫ w₁.f (W := W) ≫ u.f (W := W) ≫ p)
have refine_1 : W ((b₁.s (W := W) ≫ t₁) ≫ w₂.s (W := W) ≫ u.s (W := W) ≫ p)
Tactic: rw [← reassoc_of% fac₁', ← reassoc_of% fac₃, ← assoc]
-- 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₁ : 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₁)
⊢ 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_2 : ∀ (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₂ : 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)
⊢ 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_2 : ∀ (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₁ 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)
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_2 : ∀ (w₁ : W.LeftFraction U (z₁.Y' (W := W)))
  (fac₁' :
    (RightFraction.mk (W := W) (a₁.s (W := W) ≫ t₁) ht (b.f (W := W) ≫ z₁.s (W := W))).f (W := W) ≫ w₁.s (W := W) =
      (RightFraction.mk (W := W) (a₁.s (W := W) ≫ t₁) ht (b.f (W := W) ≫ z₁.s (W := W))).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 (a₁.s ≫ t₁) ht (b.f ≫ z₁.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₁ 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)
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 U (z₁.Y' (W := W))
fac₁' :
  (RightFraction.mk (W := W) (a₁.s (W := W) ≫ t₁) ht (b.f (W := W) ≫ z₁.s (W := W))).f (W := W) ≫ w₁.s (W := W) =
    (RightFraction.mk (W := W) (a₁.s (W := W) ≫ t₁) ht (b.f (W := W) ≫ z₁.s (W := W))).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_2 : ∀ (w₂ : W.LeftFraction U (z₂.Y' (W := W)))
  (fac₂' :
    Eq (α :=
      RightFraction.X' (W := W) (RightFraction.mk (W := W) (a₂.s (W := W) ≫ t₂) sorry (b.f (W := W) ≫ z₂.s (W := W))) ⟶
        w₂.Y' (W := W))
      (RightFraction.f (W := W) (RightFraction.mk (W := W) (a₂.s (W := W) ≫ t₂) sorry (b.f (W := W) ≫ z₂.s (W := W))) ≫
        w₂.s (W := W))
      (RightFraction.s (W := W) (RightFraction.mk (W := W) (a₂.s (W := W) ≫ t₂) sorry (b.f (W := W) ≫ z₂.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 (a₂.s ≫ t₂)
      (show W _ by rw [← hst]; exact ht) (b.f ≫ z₂.s))
-- 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₁ 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))
fac₁' : (b.f (W := W) ≫ z₁.s (W := W)) ≫ w₁.s (W := W) = (a₁.s (W := W) ≫ t₁) ≫ w₁.f (W := W)
w₂ : W.LeftFraction U (z₂.Y' (W := W))
fac₂' : (b.f (W := W) ≫ z₂.s (W := W)) ≫ w₂.s (W := W) = (a₂.s (W := W) ≫ t₂) ≫ w₂.f (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)) ⋯
⊢ a₁.comp (W := W) b = a₂.comp (W := W) b
have fac₁'₁ : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
Tactic: simp only [assoc] at fac₁' fac₂'
Cleared hypotheses: fac₁', fac₂'