awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : (u₂ ≫ v₅) ≫ w = (t₂ ≫ v₄) ≫ w
⊢ LeftFractionRel (W := W) z₁ z₃
have fac'₁ : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
Tactic: simp only [Category.assoc] at fac'
Cleared hypotheses: fac'
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ LeftFractionRel (W := W) z₁ z₃
have refine_1 : z₁.s (W := W) ≫ t₁ ≫ v₄ ≫ w = z₃.s (W := W) ≫ u₃ ≫ v₅ ≫ w
Tactic: refine ⟨Z₇, t₁ ≫ v₄ ≫ w, u₃ ≫ v₅ ≫ w, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
refine_1 : z₁.s (W := W) ≫ t₁ ≫ v₄ ≫ w = z₃.s (W := W) ≫ u₃ ≫ v₅ ≫ w
⊢ LeftFractionRel (W := W) z₁ z₃
have refine_2 : z₁.f (W := W) ≫ t₁ ≫ v₄ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
Tactic: refine ⟨Z₇, t₁ ≫ v₄ ≫ w, u₃ ≫ v₅ ≫ w, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
refine_1 : z₁.s (W := W) ≫ t₁ ≫ v₄ ≫ w = z₃.s (W := W) ≫ u₃ ≫ v₅ ≫ w
refine_2 : z₁.f (W := W) ≫ t₁ ≫ v₄ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
⊢ LeftFractionRel (W := W) z₁ z₃
have refine_3 : W (z₁.s (W := W) ≫ t₁ ≫ v₄ ≫ w)
Tactic: refine ⟨Z₇, t₁ ≫ v₄ ≫ w, u₃ ≫ v₅ ≫ w, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ z₁.s (W := W) ≫ t₁ ≫ v₄ ≫ w = z₃.s (W := W) ≫ u₃ ≫ v₅ ≫ w
have refine_1 : z₁.s (W := W) ≫ t₁ ≫ v₄ ≫ w = z₁.s (W := W) ≫ t₁ ≫ v₄ ≫ w
Tactic: rw [reassoc_of% fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ z₁.f (W := W) ≫ t₁ ≫ v₄ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
have refine_2 : z₂.f (W := W) ≫ t₂ ≫ v₄ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
Tactic: rw [reassoc_of% hft, ← fac', reassoc_of% hfu]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
refine_2 : z₂.f (W := W) ≫ t₂ ≫ v₄ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
⊢ z₁.f (W := W) ≫ t₁ ≫ v₄ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
have refine_2₁ : z₂.f (W := W) ≫ u₂ ≫ v₅ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
Tactic: rw [reassoc_of% hft, ← fac', reassoc_of% hfu]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
refine_2 : z₂.f (W := W) ≫ t₂ ≫ v₄ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
refine_2₁ : z₂.f (W := W) ≫ u₂ ≫ v₅ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
⊢ z₁.f (W := W) ≫ t₁ ≫ v₄ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
have refine_2₂ : z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w = z₃.f (W := W) ≫ u₃ ≫ v₅ ≫ w
Tactic: rw [reassoc_of% hft, ← fac', reassoc_of% hfu]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst_1 : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' (W := W) ⟶ Z₄
t₂ : z₂.Y' (W := W) ⟶ Z₄
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
hft : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
Z₅ : C
u₂ : z₂.Y' (W := W) ⟶ Z₅
u₃ : z₃.Y' (W := W) ⟶ Z₅
hsu : z₂.s (W := W) ≫ u₂ = z₃.s (W := W) ≫ u₃
hfu : z₂.f (W := W) ≫ u₂ = z₃.f (W := W) ≫ u₃
hu : W (z₂.s (W := W) ≫ u₂)
Y' : C
v₄ : Z₄ ⟶ Y'
v₅ : Z₅ ⟶ Y'
hv₅ : W v₅
fac : z₃.s (W := W) ≫ u₃ ≫ v₅ = z₁.s (W := W) ≫ t₁ ≫ v₄
eq : z₂.s (W := W) ≫ u₂ ≫ v₅ = z₂.s (W := W) ≫ t₂ ≫ v₄
Z₇ : C
w : Y' ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ W (z₁.s (W := W) ≫ t₁ ≫ v₄ ≫ w)
have refine_3 : W ((z₂.s (W := W) ≫ u₂) ≫ v₅ ≫ w)
Tactic: rw [← reassoc_of% fac, ← reassoc_of% hsu, ← Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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₃ 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)
h₃' : z₂.f (W := W) ≫ z₃'.s (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W)
⊢ LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')
have obtain : ∀ (z₄ : W.LeftFraction (z₃.Y' (W := W)) (z₃'.Y' (W := W)))
  (fac :
    (RightFraction.mk (W := W) (z₃.s (W := W)) sorry (z₃'.s (W := W))).f (W := W) ≫ z₄.s (W := W) =
      (RightFraction.mk (W := W) (z₃.s (W := W)) sorry (z₃'.s (W := W))).s (W := W) ≫ z₄.f (W := W)),
  LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')
Tactic: obtain ⟨z₄, fac⟩ := exists_leftFraction (RightFraction.mk z₃.s z₃.hs z₃'.s)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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₃ 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)
h₃' : 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₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ 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₄.s (W := W)
have rw : z₂.f (W := W) ≫ z₃.s (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
Tactic: rw [← reassoc_of% h₃, ← reassoc_of% h₃', fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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₃ 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)
h₃' : 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₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
rw : z₂.f (W := W) ≫ z₃.s (W := W) ≫ z₄.f (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₃'.f (W := W) ≫ z₄.s (W := W)
have rw₁ : z₂.f (W := W) ≫ z₃.s (W := W) ≫ z₄.f (W := W) = z₂.f (W := W) ≫ z₃'.s (W := W) ≫ z₄.s (W := W)
Tactic: rw [← reassoc_of% h₃, ← reassoc_of% h₃', fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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₃ 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)
h₃' : 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₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
rw : z₂.f (W := W) ≫ z₃.s (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
rw₁ : z₂.f (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₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
have 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)
Tactic: rw [← reassoc_of% h₃, ← reassoc_of% h₃', fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (hypothesis)
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₃ 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)
h₃' : 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₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
⊢ LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')
have eq : z₁.s (W := W) ≫ z₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
Tactic: have eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s := by
    rw [← reassoc_of% h₃, ← reassoc_of% h₃', fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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₃ 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)
h₃' : 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₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
eq : z₁.s (W := W) ≫ z₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
⊢ LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')
have obtain : ∀ (Y_1 : C) (t : z₄.Y' (W := W) ⟶ Y_1) (ht : W t)
  (fac' : (z₃.f (W := W) ≫ z₄.f (W := W)) ≫ t = (z₃'.f (W := W) ≫ z₄.s (W := W)) ≫ t),
  LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')
Tactic: obtain ⟨Y, t, ht, fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ z₁.hs eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (hypothesis)
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_1 Z : C
z₁ : W.LeftFraction X Y_1
z₂ : W.LeftFraction Y_1 Z
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)
h₃' : 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₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
eq : z₁.s (W := W) ≫ z₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
Y : C
t : z₄.Y' (W := W) ⟶ Y
ht : W t
fac' : (z₃.f (W := W) ≫ z₄.f (W := W)) ≫ t = (z₃'.f (W := W) ≫ z₄.s (W := W)) ≫ t
⊢ LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')
have fac'₁ : z₃.f (W := W) ≫ z₄.f (W := W) ≫ t = z₃'.f (W := W) ≫ z₄.s (W := W) ≫ t
Tactic: simp only [assoc] at fac'
Cleared hypotheses: fac'
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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_1 Z : C
z₁ : W.LeftFraction X Y_1
z₂ : W.LeftFraction Y_1 Z
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)
h₃' : 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₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
eq : z₁.s (W := W) ≫ z₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
Y : C
t : z₄.Y' (W := W) ⟶ Y
ht : W t
fac' : z₃.f (W := W) ≫ z₄.f (W := W) ≫ t = z₃'.f (W := W) ≫ z₄.s (W := W) ≫ t
⊢ LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')
have refine_1 : (z₁.comp₀ (W := W) z₂ z₃).s (W := W) ≫ z₄.f (W := W) ≫ t = (z₁.comp₀ (W := W) z₂ z₃').s (W := W) ≫ z₄.s (W := W) ≫ t
Tactic: refine ⟨Y, z₄.f ≫ t, z₄.s ≫ t, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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_1 Z : C
z₁ : W.LeftFraction X Y_1
z₂ : W.LeftFraction Y_1 Z
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)
h₃' : 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₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
eq : z₁.s (W := W) ≫ z₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
Y : C
t : z₄.Y' (W := W) ⟶ Y
ht : W t
fac' : z₃.f (W := W) ≫ z₄.f (W := W) ≫ t = z₃'.f (W := W) ≫ z₄.s (W := W) ≫ t
refine_1 :
  (z₁.comp₀ (W := W) z₂ z₃).s (W := W) ≫ z₄.f (W := W) ≫ t = (z₁.comp₀ (W := W) z₂ z₃').s (W := W) ≫ z₄.s (W := W) ≫ t
⊢ LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')
have refine_2 : (z₁.comp₀ (W := W) z₂ z₃).f (W := W) ≫ z₄.f (W := W) ≫ t = (z₁.comp₀ (W := W) z₂ z₃').f (W := W) ≫ z₄.s (W := W) ≫ t
Tactic: refine ⟨Y, z₄.f ≫ t, z₄.s ≫ t, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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_1 Z : C
z₁ : W.LeftFraction X Y_1
z₂ : W.LeftFraction Y_1 Z
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)
h₃' : 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₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
eq : z₁.s (W := W) ≫ z₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
Y : C
t : z₄.Y' (W := W) ⟶ Y
ht : W t
fac' : z₃.f (W := W) ≫ z₄.f (W := W) ≫ t = z₃'.f (W := W) ≫ z₄.s (W := W) ≫ t
refine_1 :
  (z₁.comp₀ (W := W) z₂ z₃).s (W := W) ≫ z₄.f (W := W) ≫ t = (z₁.comp₀ (W := W) z₂ z₃').s (W := W) ≫ z₄.s (W := W) ≫ t
refine_2 :
  (z₁.comp₀ (W := W) z₂ z₃).f (W := W) ≫ z₄.f (W := W) ≫ t = (z₁.comp₀ (W := W) z₂ z₃').f (W := W) ≫ z₄.s (W := W) ≫ t
⊢ LeftFractionRel (W := W) (z₁.comp₀ (W := W) z₂ z₃) (z₁.comp₀ (W := W) z₂ z₃')
have refine_3 : W ((z₁.comp₀ (W := W) z₂ z₃).s (W := W) ≫ z₄.f (W := W) ≫ t)
Tactic: refine ⟨Y, z₄.f ≫ t, z₄.s ≫ t, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
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_1 Z : C
z₁ : W.LeftFraction X Y_1
z₂ : W.LeftFraction Y_1 Z
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)
h₃' : 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₃'.s (W := W) ≫ z₄.s (W := W) = z₃.s (W := W) ≫ z₄.f (W := W)
eq : z₁.s (W := W) ≫ z₃.f (W := W) ≫ z₄.f (W := W) = z₁.s (W := W) ≫ z₃'.f (W := W) ≫ z₄.s (W := W)
Y : C
t : z₄.Y' (W := W) ⟶ Y
ht : W t
fac' : z₃.f (W := W) ≫ z₄.f (W := W) ≫ t = z₃'.f (W := W) ≫ z₄.s (W := W) ≫ t
⊢ W ((z₁.comp₀ (W := W) z₂ z₃).s (W := W) ≫ z₄.f (W := W) ≫ t)
have refine_3 : W (z₂.s (W := W) ≫ z₃'.s (W := W) ≫ z₄.s (W := W) ≫ t)
Tactic: simp only [comp₀, assoc, ← reassoc_of% fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.CalculusOfFractions (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
f : Hom W X Y
⊢ ∃ (z : W.LeftFraction X Y), f = mk (W := W) z
have mk : ∀ (z : W.LeftFraction X Y), ∃ (z_1 : W.LeftFraction X Y), Quot.mk (LeftFractionRel (W := W)) z = mk (W := W) z_1
Tactic: obtain ⟨z⟩ := 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₁ : Hom W X Y
z₂ : Hom W Y Z
⊢ Hom W X Z
have refine_1 : ∀ (a : W.LeftFraction X Y) (b₁ b₂ : W.LeftFraction Y Z),
  LeftFractionRel (W := W) b₁ b₂ →
    Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
      ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)
Tactic: refine Quot.lift₂ (fun a b => a.comp b) ?_ ?_ z₁ z₂
-- 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
refine_1 :
  ∀ (a : W.LeftFraction X Y) (b₁ b₂ : W.LeftFraction Y Z),
    LeftFractionRel (W := W) b₁ b₂ →
      Eq (α := Hom W X Z) ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₁)
        ((fun (a : W.LeftFraction X Y) (b : W.LeftFraction Y Z) ↦ a.comp (W := W) b) a b₂)
⊢ Hom W X Z
have refine_2 : ∀ (a₁ a₂ : W.LeftFraction X Y) (b : W.LeftFraction Y Z),
  LeftFractionRel (W := W) a₁ a₂ →
    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: refine Quot.lift₂ (fun a b => a.comp b) ?_ ?_ z₁ z₂
-- 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 : 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₁)
⊢ 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)