awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
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)
⊢ LeftFractionRel (W := W) p₂ (a₂.comp₀ (W := W) b z₂)
have eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Tactic: have eq : a₂.s ≫ z₂.f ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f := by
        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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
⊢ LeftFractionRel (W := W) p₂ (a₂.comp₀ (W := W) b z₂)
have refine_2 : ∀ (Z_1 : C) (u : w₂.Y' (W := W) ⟶ Z_1) (hu : W u)
  (fac₄ : (z₂.f (W := W) ≫ w₂.s (W := W)) ≫ u = (t₂ ≫ w₂.f (W := W)) ≫ u),
  LeftFractionRel (W := W) p₂ (a₂.comp₀ (W := W) b z₂)
Tactic: obtain ⟨Z, u, hu, 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₁ 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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : (z₂.f (W := W) ≫ w₂.s (W := W)) ≫ u = (t₂ ≫ w₂.f (W := W)) ≫ u
⊢ LeftFractionRel (W := W) p₂ (a₂.comp₀ (W := W) b z₂)
have fac₅ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
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₁ 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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
⊢ LeftFractionRel (W := W) p₂ (a₂.comp₀ (W := W) b z₂)
have refine_2 : p₂.s (W := W) ≫ u = (a₂.comp₀ (W := W) b z₂).s (W := W) ≫ w₂.s (W := W) ≫ u
Tactic: refine ⟨Z, u, w₂.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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
refine_2 : p₂.s (W := W) ≫ u = (a₂.comp₀ (W := W) b z₂).s (W := W) ≫ w₂.s (W := W) ≫ u
⊢ LeftFractionRel (W := W) p₂ (a₂.comp₀ (W := W) b z₂)
have refine_2₁ : p₂.f (W := W) ≫ u = (a₂.comp₀ (W := W) b z₂).f (W := W) ≫ w₂.s (W := W) ≫ u
Tactic: refine ⟨Z, u, w₂.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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
refine_2 : p₂.s (W := W) ≫ u = (a₂.comp₀ (W := W) b z₂).s (W := W) ≫ w₂.s (W := W) ≫ u
refine_2₁ : p₂.f (W := W) ≫ u = (a₂.comp₀ (W := W) b z₂).f (W := W) ≫ w₂.s (W := W) ≫ u
⊢ LeftFractionRel (W := W) p₂ (a₂.comp₀ (W := W) b z₂)
have refine_2₂ : W (p₂.s (W := W) ≫ u)
Tactic: refine ⟨Z, u, w₂.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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
⊢ p₂.s (W := W) ≫ u = (a₂.comp₀ (W := W) b z₂).s (W := W) ≫ w₂.s (W := W) ≫ u
have refine_2 : (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ≫ u = (b.s (W := W) ≫ z₂.s (W := W)) ≫ w₂.s (W := W) ≫ u
Tactic: dsimp [p₁, 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₁ 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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
⊢ p₂.f (W := W) ≫ u = (a₂.comp₀ (W := W) b z₂).f (W := W) ≫ w₂.s (W := W) ≫ u
have refine_2 : (a₂.f (W := W) ≫ t₂ ≫ w₂.f (W := W)) ≫ u = (a₂.f (W := W) ≫ z₂.f (W := W)) ≫ w₂.s (W := W) ≫ u
Tactic: dsimp [p₁, 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₁ 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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
⊢ W (p₂.s (W := W) ≫ u)
have refine_2 : W ((b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ≫ u)
Tactic: dsimp [p₁, 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₁ 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)
eq : a₂.s (W := W) ≫ z₂.f (W := W) ≫ w₂.s (W := W) = a₂.s (W := W) ≫ t₂ ≫ w₂.f (W := W)
Z : C
u : w₂.Y' (W := W) ⟶ Z
hu : W u
fac₄ : z₂.f (W := W) ≫ w₂.s (W := W) ≫ u = t₂ ≫ w₂.f (W := W) ≫ u
⊢ W ((b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W)) ≫ u)
have refine_2 : W (b.s (W := W) ≫ z₂.s (W := W) ≫ w₂.s (W := W) ≫ u)
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 : C
f : Hom W X Y
⊢ (Hom.mk (W := W) (ofHom W (𝟙 X))).comp (W := W) f = f
have obtain : ∀ (z : W.LeftFraction X Y), (Hom.mk (W := W) (ofHom W (𝟙 X))).comp (W := W) (Hom.mk (W := W) z) = Hom.mk (W := W) z
Tactic: obtain ⟨z, rfl⟩ := Hom.mk_surjective f
Cleared hypotheses: 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 : C
z : W.LeftFraction X Y
⊢ (Hom.mk (W := W) (ofHom W (𝟙 X))).comp (W := W) (Hom.mk (W := W) z) = Hom.mk (W := W) z
have rw : Hom.mk (W := W) ((ofHom W (𝟙 X)).comp₀ (W := W) z (ofHom W (z.f (W := W)))) = Hom.mk (W := W) z
Tactic: rw [Hom.comp_eq, comp_eq (ofHom W (𝟙 X)) z (ofHom W z.f) (by simp)]
-- 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 : C
z : W.LeftFraction X Y
⊢ Hom.mk (W := W) ((ofHom W (𝟙 X)).comp₀ (W := W) z (ofHom W (z.f (W := W)))) = Hom.mk (W := W) z
have dsimp : Hom.mk (W := W) (mk (W := W) (𝟙 X ≫ z.f (W := W)) (z.s (W := W) ≫ 𝟙 (z.Y' (W := W))) sorry) = Hom.mk (W := W) z
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 : C
f : Hom W X Y
⊢ f.comp (W := W) (Hom.mk (W := W) (ofHom W (𝟙 Y))) = f
have obtain : ∀ (z : W.LeftFraction X Y), (Hom.mk (W := W) z).comp (W := W) (Hom.mk (W := W) (ofHom W (𝟙 Y))) = Hom.mk (W := W) z
Tactic: obtain ⟨z, rfl⟩ := Hom.mk_surjective f
Cleared hypotheses: 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 : C
z : W.LeftFraction X Y
⊢ (Hom.mk (W := W) z).comp (W := W) (Hom.mk (W := W) (ofHom W (𝟙 Y))) = Hom.mk (W := W) z
have rw : Hom.mk (W := W) (z.comp₀ (W := W) (ofHom W (𝟙 Y)) (ofInv (W := W) (z.s (W := W)) sorry)) = Hom.mk (W := W) z
Tactic: rw [Hom.comp_eq, comp_eq z (ofHom W (𝟙 Y)) (ofInv z.s z.hs) (by simp)]
-- 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 : C
z : W.LeftFraction X Y
⊢ Hom.mk (W := W) (z.comp₀ (W := W) (ofHom W (𝟙 Y)) (ofInv (W := W) (z.s (W := W)) ⋯)) = Hom.mk (W := W) z
have dsimp : Hom.mk (W := W) (mk (W := W) (z.f (W := W) ≫ 𝟙 (z.Y' (W := W))) (𝟙 Y ≫ z.s (W := W)) sorry) = Hom.mk (W := W) z
Tactic: dsimp [comp₀]
-- 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₁ X₂ X₃ X₄ : C
f₁ : Hom W X₁ X₂
f₂ : Hom W X₂ X₃
f₃ : Hom W X₃ X₄
⊢ (f₁.comp (W := W) f₂).comp (W := W) f₃ = f₁.comp (W := W) (f₂.comp (W := W) f₃)
have obtain : ∀ (z₁ : W.LeftFraction X₁ X₂),
  ((Hom.mk (W := W) z₁).comp (W := W) f₂).comp (W := W) f₃ = (Hom.mk (W := W) z₁).comp (W := W) (f₂.comp (W := W) f₃)
Tactic: obtain ⟨z₁, rfl⟩ := Hom.mk_surjective f₁
Cleared hypotheses: 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₁ X₂ X₃ X₄ : C
f₂ : Hom W X₂ X₃
f₃ : Hom W X₃ X₄
z₁ : W.LeftFraction X₁ X₂
⊢ ((Hom.mk (W := W) z₁).comp (W := W) f₂).comp (W := W) f₃ = (Hom.mk (W := W) z₁).comp (W := W) (f₂.comp (W := W) f₃)
have obtain : ∀ (z₂ : W.LeftFraction X₂ X₃),
  ((Hom.mk (W := W) z₁).comp (W := W) (Hom.mk (W := W) z₂)).comp (W := W) f₃ =
    (Hom.mk (W := W) z₁).comp (W := W) ((Hom.mk (W := W) z₂).comp (W := W) f₃)
Tactic: obtain ⟨z₂, rfl⟩ := Hom.mk_surjective f₂
Cleared hypotheses: 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₁ X₂ X₃ X₄ : C
f₃ : Hom W X₃ X₄
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
⊢ ((Hom.mk (W := W) z₁).comp (W := W) (Hom.mk (W := W) z₂)).comp (W := W) f₃ =
    (Hom.mk (W := W) z₁).comp (W := W) ((Hom.mk (W := W) z₂).comp (W := W) f₃)
have obtain : ∀ (z₃ : W.LeftFraction X₃ X₄),
  ((Hom.mk (W := W) z₁).comp (W := W) (Hom.mk (W := W) z₂)).comp (W := W) (Hom.mk (W := W) z₃) =
    (Hom.mk (W := W) z₁).comp (W := W) ((Hom.mk (W := W) z₂).comp (W := W) (Hom.mk (W := W) z₃))
Tactic: obtain ⟨z₃, rfl⟩ := Hom.mk_surjective f₃
Cleared hypotheses: 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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
⊢ (z₁.comp (W := W) z₂).comp (W := W) (Hom.mk (W := W) z₃) = (Hom.mk (W := W) z₁).comp (W := W) (z₂.comp (W := W) z₃)
have obtain : ∀ (z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W)))
  (fac₁₂ :
    (RightFraction.mk (W := W) (z₁.s (W := W)) sorry (z₂.f (W := W))).f (W := W) ≫ z₁₂.s (W := W) =
      (RightFraction.mk (W := W) (z₁.s (W := W)) sorry (z₂.f (W := W))).s (W := W) ≫ z₁₂.f (W := W)),
  (z₁.comp (W := W) z₂).comp (W := W) (Hom.mk (W := W) z₃) = (Hom.mk (W := W) z₁).comp (W := W) (z₂.comp (W := W) z₃)
Tactic: obtain ⟨z₁₂, fac₁₂⟩ := exists_leftFraction (RightFraction.mk z₁.s z₁.hs z₂.f)