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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ :
  (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ (z₂.f (W := W))).f (W := W) ≫ z₁₂.s (W := W) =
    (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ (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₃)
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)
-- 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₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ :
  (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ (z₂.f (W := W))).f (W := W) ≫ z₁₂.s (W := W) =
    (RightFraction.mk (W := W) (z₁.s (W := W)) ⋯ (z₂.f (W := W))).s (W := W) ≫ z₁₂.f (W := W)
z₂₃ : W.LeftFraction (z₂.Y' (W := W)) (z₃.Y' (W := W))
fac₂₃ :
  (RightFraction.mk (W := W) (z₂.s (W := W)) ⋯ (z₃.f (W := W))).f (W := W) ≫ z₂₃.s (W := W) =
    (RightFraction.mk (W := W) (z₂.s (W := W)) ⋯ (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₃)
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)
-- 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₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ : 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₃.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₂₃.f (W := W) ≫ z'.s (W := W) = z₁₂.s (W := W) ≫ z'.f (W := W)
⊢ z₃.f (W := W) ≫ (mk (W := W) (z'.f (W := W)) (z₂₃.s (W := W) ≫ z'.s (W := W)) ⋯).s (W := W) =
    (mk (W := W) (z₁.f (W := W) ≫ z₁₂.f (W := W)) (z₂.s (W := W) ≫ z₁₂.s (W := W)) ⋯).s (W := W) ≫
      (mk (W := W) (z'.f (W := W)) (z₂₃.s (W := W) ≫ z'.s (W := W)) ⋯).f (W := W)
have dsimp : z₃.f (W := W) ≫ z₂₃.s (W := W) ≫ z'.s (W := W) = (z₂.s (W := W) ≫ z₁₂.s (W := W)) ≫ z'.f (W := W)
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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ : 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₃.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₂₃.f (W := W) ≫ z'.s (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₁₂.s (W := W)) ≫ z'.f (W := W)
have rw : z₃.f (W := W) ≫ z₂₃.s (W := W) ≫ z'.s (W := W) = z₂.s (W := W) ≫ z₁₂.s (W := W) ≫ z'.f (W := W)
Tactic: rw [assoc, reassoc_of% 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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ : 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₃.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₂₃.f (W := W) ≫ z'.s (W := W) = z₁₂.s (W := W) ≫ z'.f (W := W)
rw : z₃.f (W := W) ≫ z₂₃.s (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'.s (W := W) = (z₂.s (W := W) ≫ z₁₂.s (W := W)) ≫ z'.f (W := W)
have rw₁ : z₂.s (W := W) ≫ z₂₃.f (W := W) ≫ z'.s (W := W) = z₂.s (W := W) ≫ z₁₂.s (W := W) ≫ z'.f (W := W)
Tactic: rw [assoc, reassoc_of% 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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ : 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₃.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₂₃.f (W := W) ≫ z'.s (W := W) = z₁₂.s (W := W) ≫ z'.f (W := W)
rw : z₃.f (W := W) ≫ z₂₃.s (W := W) ≫ z'.s (W := W) = z₂.s (W := W) ≫ z₁₂.s (W := W) ≫ z'.f (W := W)
rw₁ : z₂.s (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'.s (W := W) = (z₂.s (W := W) ≫ z₁₂.s (W := W)) ≫ z'.f (W := W)
have rw₂ : z₂.s (W := W) ≫ z₁₂.s (W := W) ≫ z'.f (W := W) = z₂.s (W := W) ≫ z₁₂.s (W := W) ≫ z'.f (W := W)
Tactic: rw [assoc, reassoc_of% 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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ : 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₃.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₂₃.f (W := W) ≫ z'.s (W := W) = z₁₂.s (W := W) ≫ z'.f (W := W)
⊢ (mk (W := W) (z₂.f (W := W) ≫ z₂₃.f (W := W)) (z₃.s (W := W) ≫ z₂₃.s (W := W)) ⋯).f (W := W) ≫
      (mk (W := W) (z₁₂.f (W := W) ≫ z'.f (W := W)) (z'.s (W := W)) ⋯).s (W := W) =
    z₁.s (W := W) ≫ (mk (W := W) (z₁₂.f (W := W) ≫ z'.f (W := W)) (z'.s (W := W)) ⋯).f (W := W)
have dsimp : (z₂.f (W := W) ≫ z₂₃.f (W := W)) ≫ z'.s (W := W) = z₁.s (W := W) ≫ z₁₂.f (W := W) ≫ z'.f (W := W)
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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ : 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₃.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₂₃.f (W := W) ≫ z'.s (W := W) = z₁₂.s (W := W) ≫ z'.f (W := W)
⊢ (z₂.f (W := W) ≫ z₂₃.f (W := W)) ≫ z'.s (W := W) = z₁.s (W := W) ≫ z₁₂.f (W := W) ≫ z'.f (W := W)
have rw : z₂.f (W := W) ≫ z₂₃.f (W := W) ≫ z'.s (W := W) = z₁.s (W := W) ≫ z₁₂.f (W := W) ≫ z'.f (W := W)
Tactic: rw [assoc, ← reassoc_of% 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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ : 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₃.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₂₃.f (W := W) ≫ z'.s (W := W) = z₁₂.s (W := W) ≫ z'.f (W := W)
rw : z₂.f (W := W) ≫ z₂₃.f (W := W) ≫ z'.s (W := W) = z₁.s (W := W) ≫ z₁₂.f (W := W) ≫ z'.f (W := W)
⊢ (z₂.f (W := W) ≫ z₂₃.f (W := W)) ≫ z'.s (W := W) = z₁.s (W := W) ≫ z₁₂.f (W := W) ≫ z'.f (W := W)
have rw₁ : z₂.f (W := W) ≫ z₂₃.f (W := W) ≫ z'.s (W := W) = z₂.f (W := W) ≫ z₁₂.s (W := W) ≫ z'.f (W := W)
Tactic: rw [assoc, ← reassoc_of% 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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ : 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₃.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₂₃.f (W := W) ≫ z'.s (W := W) = z₁₂.s (W := W) ≫ z'.f (W := W)
rw : z₂.f (W := W) ≫ z₂₃.f (W := W) ≫ z'.s (W := W) = z₁.s (W := W) ≫ z₁₂.f (W := W) ≫ z'.f (W := W)
rw₁ : z₂.f (W := W) ≫ z₂₃.f (W := W) ≫ z'.s (W := W) = z₂.f (W := W) ≫ z₁₂.s (W := W) ≫ z'.f (W := W)
⊢ (z₂.f (W := W) ≫ z₂₃.f (W := W)) ≫ z'.s (W := W) = z₁.s (W := W) ≫ z₁₂.f (W := W) ≫ z'.f (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 [assoc, ← reassoc_of% 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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction (z₁.Y' (W := W)) (z₂.Y' (W := W))
fac₁₂ : 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₃.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₂₃.f (W := W) ≫ z'.s (W := W) = z₁₂.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₃)
have rw : Hom.mk (W := W)
    ((mk (W := W) (z₁.f (W := W) ≫ z₁₂.f (W := W)) (z₂.s (W := W) ≫ z₁₂.s (W := W)) sorry).comp₀ (W := W) z₃
      (mk (W := W) (z'.f (W := W)) (z₂₃.s (W := W) ≫ z'.s (W := W)) sorry)) =
  Hom.mk (W := W)
    (z₁.comp₀ (W := W) (mk (W := W) (z₂.f (W := W) ≫ z₂₃.f (W := W)) (z₃.s (W := W) ≫ z₂₃.s (W := W)) sorry)
      (mk (W := W) (z₁₂.f (W := W) ≫ z'.f (W := W)) (z'.s (W := W)) sorry))
Tactic: rw [comp_eq z₁ z₂ z₁₂ fac₁₂, comp_eq z₂ z₃ z₂₃ fac₂₃, comp₀, comp₀,
      Hom.comp_eq, Hom.comp_eq,
      comp_eq _ z₃ (mk z'.f (z₂₃.s ≫ z'.s) (W.comp_mem _ _ z₂₃.hs z'.hs))
        (by dsimp; rw [assoc, reassoc_of% fac₂₃, fac]),
      comp_eq z₁ _ (mk (z₁₂.f ≫ z'.f) z'.s z'.hs)
        (by dsimp; rw [assoc, ← reassoc_of% 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
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.mk (W := W) (ofHom W (f ≫ g)) = (Hom.mk (W := W) (ofHom W f)).comp (W := W) (Hom.mk (W := W) (ofHom W g))
have rw : Hom.mk (W := W) (ofHom W (f ≫ g)) = Hom.mk (W := W) ((ofHom W f).comp₀ (W := W) (ofHom W g) (ofHom W g))
Tactic: rw [Hom.comp_eq, comp_eq (ofHom W f) (ofHom W g) (ofHom W g) (by simp)]
-- 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₃ : 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)
⊢ Eq (α := Hom W (Functor.obj (Q W) X) (Functor.obj (Q W) Z))
    (Hom.comp (W := W) (homMk (W := W) z₁) (homMk (W := W) z₂)) (homMk (W := W) (z₁.comp₀ (W := W) z₂ z₃))
have rw : z₁.comp (W := W) z₂ = homMk (W := W) (z₁.comp₀ (W := W) z₂ z₃)
Tactic: rw [Hom.comp_eq, comp_eq z₁ z₂ z₃ h₃]
-- 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₃ : 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)
rw : z₁.comp (W := W) z₂ = homMk (W := W) (z₁.comp₀ (W := W) z₂ z₃)
⊢ Eq (α := Hom W (Functor.obj (Q W) X) (Functor.obj (Q W) Z))
    (Hom.comp (W := W) (homMk (W := W) z₁) (homMk (W := W) z₂)) (homMk (W := W) (z₁.comp₀ (W := W) z₂ z₃))
have rw₁ : Hom.mk (W := W) (z₁.comp₀ (W := W) z₂ z₃) = homMk (W := W) (z₁.comp₀ (W := W) z₂ z₃)
Tactic: rw [Hom.comp_eq, comp_eq z₁ z₂ z₃ h₃]
-- 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 Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (Functor.map (Q W) f ≫ Qinv (W := W) s hs)
    (homMk (W := W) (mk (W := W) f s hs))
have dsimp : Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y) (homMk (W := W) (ofHom W f) ≫ homMk (W := W) (ofInv (W := W) s hs))
  (homMk (W := W) (mk (W := W) f s hs))
Tactic: dsimp only [Q_map, Qinv]
-- 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 Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y)
    (homMk (W := W) (ofHom W f) ≫ homMk (W := W) (ofInv (W := W) s hs)) (homMk (W := W) (mk (W := W) f s hs))
have rw : Eq (α := Functor.obj (Q W) X ⟶ Functor.obj (Q W) Y)
  (homMk (W := W) ((ofHom W f).comp₀ (W := W) (ofInv (W := W) s hs) (ofHom W (𝟙 ((ofHom W f).Y' (W := W))))))
  (homMk (W := W) (mk (W := W) f s hs))
Tactic: rw [homMk_comp_homMk (ofHom W f) (ofInv s hs) (ofHom W (𝟙 _)) (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
s : X ⟶ Y
hs : W s
⊢ Functor.map (Q W) s ≫ Qinv (W := W) s hs = 𝟙 (Functor.obj (Q W) X)
have rw : homMk (W := W) (mk (W := W) s s hs) = 𝟙 (Functor.obj (Q W) X)
Tactic: rw [Q_map_comp_Qinv]
-- 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
s : X ⟶ Y
hs : W s
⊢ homMk (W := W) (mk (W := W) s s hs) = 𝟙 (Functor.obj (Q W) X)
have h : LeftFractionRel (W := W) (mk (W := W) s s hs) (ofHom W (𝟙 (Functor.obj (Q W) X)))
Tactic: apply homMk_eq_of_leftFractionRel
-- 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
s : X ⟶ Y
hs : W s
⊢ Qinv (W := W) s hs ≫ Functor.map (Q W) s = 𝟙 (Functor.obj (Q W) Y)
have dsimp : homMk (W := W) (ofInv (W := W) s hs) ≫ homMk (W := W) (ofHom W s) = 𝟙 (Functor.obj (Q W) Y)
Tactic: dsimp only [Qinv, Q_map]
-- 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
s : X ⟶ Y
hs : W s
⊢ homMk (W := W) (ofInv (W := W) s hs) ≫ homMk (W := W) (ofHom W s) = 𝟙 (Functor.obj (Q W) Y)
have rw : homMk (W := W) ((ofInv (W := W) s hs).comp₀ (W := W) (ofHom W s) (ofHom W (𝟙 Y))) = 𝟙 (Functor.obj (Q W) Y)
Tactic: rw [homMk_comp_homMk (ofInv s hs) (ofHom W s) (ofHom W (𝟙 Y)) (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
s : X ⟶ Y
hs : W s
⊢ homMk (W := W) ((ofInv (W := W) s hs).comp₀ (W := W) (ofHom W s) (ofHom W (𝟙 Y))) = 𝟙 (Functor.obj (Q W) Y)
have h : LeftFractionRel (W := W) ((ofInv (W := W) s hs).comp₀ (W := W) (ofHom W s) (ofHom W (𝟙 Y)))
  (ofHom W (𝟙 (Functor.obj (Q W) Y)))
Tactic: apply homMk_eq_of_leftFractionRel
-- 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
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
⊢ ∀ (a : LeftFractionRel (W := W) a₁ a₂),
    Eq.{v_3 + 1} (α := F.obj X ⟶ F.obj Y) ((fun (f : W.LeftFraction X Y) ↦ f.map (W := W) F hF) a₁)
      ((fun (f : W.LeftFraction X Y) ↦ f.map (W := W) F hF) a₂)
have this : ∀ (Z : C) (t₁ : a₁.Y' (W := W) ⟶ Z) (t₂ : a₂.Y' (W := W) ⟶ Z) (hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂)
  (hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂) (h : W (a₁.s (W := W) ≫ t₁)),
  Eq.{v_3 + 1} (α := F.obj X ⟶ F.obj Y) ((fun (f : W.LeftFraction X Y) ↦ f.map (W := W) F hF) a₁)
    ((fun (f : W.LeftFraction X Y) ↦ f.map (W := W) F hF) a₂)
Tactic: ⟨Z, t₁, t₂, hst, hft, h⟩
-- 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
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' (W := W) ⟶ Z
t₂ : a₂.Y' (W := W) ⟶ Z
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
h : W (a₁.s (W := W) ≫ t₁)
⊢ a₁.map (W := W) F hF = a₂.map (W := W) F hF
have this : IsIso (F.map (a₁.s (W := W) ≫ t₁))
Tactic: have := hF _ h
-- 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
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' (W := W) ⟶ Z
t₂ : a₂.Y' (W := W) ⟶ Z
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
h : W (a₁.s (W := W) ≫ t₁)
this : IsIso (F.map (a₁.s (W := W) ≫ t₁))
⊢ a₁.map (W := W) F hF = a₂.map (W := W) F hF
have rw : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
Tactic: rw [← cancel_mono (F.map (a₁.s ≫ t₁)), F.map_comp, map_comp_map_s_assoc,
      ← F.map_comp, ← F.map_comp, hst, hft, F.map_comp,
      F.map_comp, map_comp_map_s_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
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' (W := W) ⟶ Z
t₂ : a₂.Y' (W := W) ⟶ Z
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
h : W (a₁.s (W := W) ≫ t₁)
this : IsIso (F.map (a₁.s (W := W) ≫ t₁))
rw : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
⊢ a₁.map (W := W) F hF = a₂.map (W := W) F hF
have rw₁ : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
Tactic: rw [← cancel_mono (F.map (a₁.s ≫ t₁)), F.map_comp, map_comp_map_s_assoc,
      ← F.map_comp, ← F.map_comp, hst, hft, F.map_comp,
      F.map_comp, map_comp_map_s_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
E : Type u_3
inst_3 : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : Functor.{v_1, v_3, u_1, u_3} C E
hF : W.IsInvertedBy F
a₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' (W := W) ⟶ Z
t₂ : a₂.Y' (W := W) ⟶ Z
hst : a₁.s (W := W) ≫ t₁ = a₂.s (W := W) ≫ t₂
hft : a₁.f (W := W) ≫ t₁ = a₂.f (W := W) ≫ t₂
h : W (a₁.s (W := W) ≫ t₁)
this : IsIso (F.map (a₁.s (W := W) ≫ t₁))
rw : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁) = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W) ≫ t₁)
rw₁ : a₁.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
⊢ a₁.map (W := W) F hF = a₂.map (W := W) F hF
have rw₂ : F.map (a₁.f (W := W)) ≫ F.map t₁ = a₂.map (W := W) F hF ≫ F.map (a₁.s (W := W)) ≫ F.map t₁
Tactic: rw [← cancel_mono (F.map (a₁.s ≫ t₁)), F.map_comp, map_comp_map_s_assoc,
      ← F.map_comp, ← F.map_comp, hst, hft, F.map_comp,
      F.map_comp, map_comp_map_s_assoc]