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))
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)) ⋯
fac₁'₁ : b.f (W := W) ≫ z₁.s (W := W) ≫ w₁.s (W := W) = a₁.s (W := W) ≫ t₁ ≫ w₁.f (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₂'
-- 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₁.comp (W := W) b = a₂.comp (W := W) b
have refine_2 : mk (W := W) (a₁.comp₀ (W := W) b z₁) = mk (W := W) (a₂.comp₀ (W := W) b z₂)
Tactic: rw [comp_eq _ _ z₁ fac₁, comp_eq _ _ z₂ fac₂]
-- 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)
⊢ mk (W := W) (a₁.comp₀ (W := W) b z₁) = mk (W := W) (a₂.comp₀ (W := W) b z₂)
have refine_2 : 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 : 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) (a₁.comp₀ (W := W) b z₁) (a₂.comp₀ (W := W) b z₂)
have refine_2 : LeftFractionRel (W := W) (a₁.comp₀ (W := W) b z₁) p₁
Tactic: refine LeftFractionRel.trans ?_ ((?_ : LeftFractionRel p₁ p₂).trans ?_)
-- 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)
refine_2 : LeftFractionRel (W := W) (a₁.comp₀ (W := W) b z₁) p₁
⊢ LeftFractionRel (W := W) (a₁.comp₀ (W := W) b z₁) (a₂.comp₀ (W := W) b z₂)
have refine_2₁ : LeftFractionRel (W := W) p₁ p₂
Tactic: refine LeftFractionRel.trans ?_ ((?_ : LeftFractionRel p₁ p₂).trans ?_)
-- 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)
refine_2 : LeftFractionRel (W := W) (a₁.comp₀ (W := W) b z₁) p₁
refine_2₁ : LeftFractionRel (W := W) p₁ p₂
⊢ LeftFractionRel (W := W) (a₁.comp₀ (W := W) b z₁) (a₂.comp₀ (W := W) b z₂)
have refine_2₂ : LeftFractionRel (W := W) p₂ (a₂.comp₀ (W := W) b z₂)
Tactic: refine LeftFractionRel.trans ?_ ((?_ : LeftFractionRel p₁ p₂).trans ?_)
-- 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₁]
-- 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) (a₁.comp₀ (W := W) b z₁) p₁
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) (a₁.comp₀ (W := W) b z₁) p₁
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) (a₁.comp₀ (W := W) b z₁) p₁
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) (a₁.comp₀ (W := W) b z₁) p₁
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) (a₁.comp₀ (W := W) b z₁) p₁
have refine_2 : (a₁.comp₀ (W := W) b z₁).s (W := W) ≫ w₁.s (W := W) ≫ u = p₁.s (W := W) ≫ u
Tactic: refine ⟨Z, w₁.s ≫ u, 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 : (a₁.comp₀ (W := W) b z₁).s (W := W) ≫ w₁.s (W := W) ≫ u = p₁.s (W := W) ≫ u
⊢ LeftFractionRel (W := W) (a₁.comp₀ (W := W) b z₁) p₁
have refine_2₁ : (a₁.comp₀ (W := W) b z₁).f (W := W) ≫ w₁.s (W := W) ≫ u = p₁.f (W := W) ≫ u
Tactic: refine ⟨Z, w₁.s ≫ u, 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 : (a₁.comp₀ (W := W) b z₁).s (W := W) ≫ w₁.s (W := W) ≫ u = p₁.s (W := W) ≫ u
refine_2₁ : (a₁.comp₀ (W := W) b z₁).f (W := W) ≫ w₁.s (W := W) ≫ u = p₁.f (W := W) ≫ u
⊢ LeftFractionRel (W := W) (a₁.comp₀ (W := W) b z₁) p₁
have refine_2₂ : W ((a₁.comp₀ (W := W) b z₁).s (W := W) ≫ w₁.s (W := W) ≫ u)
Tactic: refine ⟨Z, w₁.s ≫ u, u, ?_, ?_, ?_⟩