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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a₁.Y' (W := W)) (b.Y' (W := W))
fac₁ : b.f (W := W) ≫ z₁.s (W := W) = a₁.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a₂.Y' (W := W)) (b.Y' (W := W))
fac₂ : b.f (W := W) ≫ z₂.s (W := W) = a₂.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
⊢ LeftFractionRel (W := W) p₁ p₂
have refine_2 : p₁.s (W := W) ≫ q.f (W := W) ≫ u = p₂.s (W := W) ≫ q.s (W := W) ≫ u
Tactic: refine ⟨Z, q.f ≫ u, q.s ≫ u, ?_, ?_, ?_⟩
-- 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a₁.Y' (W := W)) (b.Y' (W := W))
fac₁ : b.f (W := W) ≫ z₁.s (W := W) = a₁.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a₂.Y' (W := W)) (b.Y' (W := W))
fac₂ : b.f (W := W) ≫ z₂.s (W := W) = a₂.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2 : p₁.s (W := W) ≫ q.f (W := W) ≫ u = p₂.s (W := W) ≫ q.s (W := W) ≫ u
⊢ LeftFractionRel (W := W) p₁ p₂
have refine_2₁ : p₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
Tactic: refine ⟨Z, q.f ≫ u, q.s ≫ u, ?_, ?_, ?_⟩
-- 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a₁.Y' (W := W)) (b.Y' (W := W))
fac₁ : b.f (W := W) ≫ z₁.s (W := W) = a₁.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a₂.Y' (W := W)) (b.Y' (W := W))
fac₂ : b.f (W := W) ≫ z₂.s (W := W) = a₂.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2 : p₁.s (W := W) ≫ q.f (W := W) ≫ u = p₂.s (W := W) ≫ q.s (W := W) ≫ u
refine_2₁ : p₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
⊢ LeftFractionRel (W := W) p₁ p₂
have refine_2₂ : W (p₁.s (W := W) ≫ q.f (W := W) ≫ u)
Tactic: refine ⟨Z, q.f ≫ u, q.s ≫ u, ?_, ?_, ?_⟩
-- 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a₁.Y' (W := W)) (b.Y' (W := W))
fac₁ : b.f (W := W) ≫ z₁.s (W := W) = a₁.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a₂.Y' (W := W)) (b.Y' (W := W))
fac₂ : b.f (W := W) ≫ z₂.s (W := W) = a₂.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
⊢ p₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
have refine_2 : a₁.f (W := W) ≫ (t₁ ≫ w₁.f (W := W)) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
Tactic: rw [assoc, assoc, assoc, assoc, fac₄, reassoc_of% hft]
-- 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a₁.Y' (W := W)) (b.Y' (W := W))
fac₁ : b.f (W := W) ≫ z₁.s (W := W) = a₁.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a₂.Y' (W := W)) (b.Y' (W := W))
fac₂ : b.f (W := W) ≫ z₂.s (W := W) = a₂.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2 : a₁.f (W := W) ≫ (t₁ ≫ w₁.f (W := W)) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
⊢ p₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
have refine_2₁ : a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
Tactic: rw [assoc, assoc, assoc, assoc, fac₄, reassoc_of% hft]
-- 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a₁.Y' (W := W)) (b.Y' (W := W))
fac₁ : b.f (W := W) ≫ z₁.s (W := W) = a₁.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a₂.Y' (W := W)) (b.Y' (W := W))
fac₂ : b.f (W := W) ≫ z₂.s (W := W) = a₂.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2 : a₁.f (W := W) ≫ (t₁ ≫ w₁.f (W := W)) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2₁ : a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
⊢ p₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
have refine_2₂ : a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = a₂.f (W := W) ≫ (t₂ ≫ w₂.f (W := W)) ≫ q.s (W := W) ≫ u
Tactic: rw [assoc, assoc, assoc, assoc, fac₄, reassoc_of% hft]
-- 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a₁.Y' (W := W)) (b.Y' (W := W))
fac₁ : b.f (W := W) ≫ z₁.s (W := W) = a₁.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a₂.Y' (W := W)) (b.Y' (W := W))
fac₂ : b.f (W := W) ≫ z₂.s (W := W) = a₂.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2 : a₁.f (W := W) ≫ (t₁ ≫ w₁.f (W := W)) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2₁ : a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2₂ :
  a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = a₂.f (W := W) ≫ (t₂ ≫ w₂.f (W := W)) ≫ q.s (W := W) ≫ u
⊢ p₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
have refine_2₃ : a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
Tactic: rw [assoc, assoc, assoc, assoc, fac₄, reassoc_of% hft]
-- 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a₁.Y' (W := W)) (b.Y' (W := W))
fac₁ : b.f (W := W) ≫ z₁.s (W := W) = a₁.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a₂.Y' (W := W)) (b.Y' (W := W))
fac₂ : b.f (W := W) ≫ z₂.s (W := W) = a₂.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2 : a₁.f (W := W) ≫ (t₁ ≫ w₁.f (W := W)) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2₁ : a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2₂ :
  a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = a₂.f (W := W) ≫ (t₂ ≫ w₂.f (W := W)) ≫ q.s (W := W) ≫ u
refine_2₃ :
  a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
⊢ p₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
have refine_2₄ : a₁.f (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u = a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
Tactic: rw [assoc, assoc, assoc, assoc, fac₄, reassoc_of% hft]
-- 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a₁.Y' (W := W)) (b.Y' (W := W))
fac₁ : b.f (W := W) ≫ z₁.s (W := W) = a₁.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a₂.Y' (W := W)) (b.Y' (W := W))
fac₂ : b.f (W := W) ≫ z₂.s (W := W) = a₂.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2 : a₁.f (W := W) ≫ (t₁ ≫ w₁.f (W := W)) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2₁ : a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2₂ :
  a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = a₂.f (W := W) ≫ (t₂ ≫ w₂.f (W := W)) ≫ q.s (W := W) ≫ u
refine_2₃ :
  a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
refine_2₄ :
  a₁.f (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u = a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
⊢ p₁.f (W := W) ≫ q.f (W := W) ≫ u = p₂.f (W := W) ≫ q.s (W := W) ≫ u
have refine_2₅ : a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u = a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
Tactic: rw [assoc, assoc, assoc, assoc, fac₄, reassoc_of% hft]
-- 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z_1
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a₁.Y' (W := W)) (b.Y' (W := W))
fac₁ : b.f (W := W) ≫ z₁.s (W := W) = a₁.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a₂.Y' (W := W)) (b.Y' (W := W))
fac₂ : b.f (W := W) ≫ z₂.s (W := W) = a₂.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z_1 :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
q : W.LeftFraction (w₁.Y' (W := W)) (w₂.Y' (W := W))
fac₃ : z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) = z₁.s (W := W) ≫ w₁.s (W := W) ≫ q.f (W := W)
eq : a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₂.f (W := W) ≫ q.s (W := W)
Z : C
u : q.Y' (W := W) ⟶ Z
hu : W u
fac₄ : t₁ ≫ w₁.f (W := W) ≫ q.f (W := W) ≫ u = t₁ ≫ w₂.f (W := W) ≫ q.s (W := W) ≫ u
⊢ W (p₁.s (W := W) ≫ q.f (W := W) ≫ u)
have refine_2 : W (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) ≫ q.s (W := W) ≫ u)
Tactic: simp only [p₁, assoc, ← reassoc_of% 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a₁.Y' (W := W)) (b.Y' (W := W))
fac₁ : b.f (W := W) ≫ z₁.s (W := W) = a₁.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a₂.Y' (W := W)) (b.Y' (W := W))
fac₂ : b.f (W := W) ≫ z₂.s (W := W) = a₂.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
⊢ a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
have rw : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)
Tactic: rw [← fac₂', reassoc_of% 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₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' (W := W) ⟶ U
t₂ : a₂.Y' (W := W) ⟶ U
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
ht : W (a₁.s (W := W) ≫ t₁)
z₁ : W.LeftFraction (a₁.Y' (W := W)) (b.Y' (W := W))
fac₁ : b.f (W := W) ≫ z₁.s (W := W) = a₁.s (W := W) ≫ z₁.f (W := W)
z₂ : W.LeftFraction (a₂.Y' (W := W)) (b.Y' (W := W))
fac₂ : b.f (W := W) ≫ z₂.s (W := W) = a₂.s (W := W) ≫ z₂.f (W := W)
w₁ : W.LeftFraction U (z₁.Y' (W := W))
w₂ : W.LeftFraction U (z₂.Y' (W := W))
p₁ : W.LeftFraction X Z :=
  LeftFraction.mk (W := W) (a₁.f (W := W) ≫ t₁ ≫ w₁.f (W := W)) (b.s (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W)) ⋯
p₂ : W.LeftFraction X Z :=
  LeftFraction.mk (W := W) (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ⋯
fac₁' : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (W := W)
fac₂' : b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
rw : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = b.f (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)
⊢ a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
have rw₁ : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W)
Tactic: rw [← fac₂', reassoc_of% fac₂]