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
X Y : C
φ₁ φ₂ : W.LeftFraction X Y
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L₁ : Functor.{v_1, v_2, u_1, u_2} C D
L₂ : Functor.{v_1, v_3, u_1, u_3} C E
inst_3 : L₁.IsLocalization W
inst_4 : L₂.IsLocalization W
h : φ₁.map (W := W) L₁ ⋯ = φ₂.map (W := W) L₁ ⋯
a :
  NatTrans.app (Iso.hom (Localization.compUniqFunctor L₂ L₁ W)) X ≫
      φ₁.map (W := W) L₁ ⋯ ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₂ L₁ W)) Y =
    (Localization.uniq L₂ L₁ W).functor.map (φ₂.map (W := W) L₂ ⋯)
⊢ (Localization.uniq L₂ L₁ W).functor.map (φ₁.map (W := W) L₂ ⋯) =
    (Localization.uniq L₂ L₁ W).functor.map (φ₂.map (W := W) L₂ ⋯)
have a₁ : Eq (α := (Localization.uniq L₂ L₁ W).functor.obj (L₂.obj X) ⟶ (Localization.uniq L₂ L₁ W).functor.obj (L₂.obj Y))
  (NatTrans.app (Iso.hom (Localization.compUniqFunctor L₂ L₁ W)) X ≫
      φ₁.map (W := W) L₁ sorry ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₂ L₁ W)) Y :
    (L₂ ⋙ (Localization.uniq L₂ L₁ W).functor).obj X ⟶ (L₂ ⋙ (Localization.uniq L₂ L₁ W).functor).obj Y)
  (NatTrans.app (Iso.hom (Localization.compUniqFunctor L₂ L₁ W)) X ≫
    φ₂.map (W := W) L₁ sorry ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₂ L₁ W)) Y)
Tactic: rw [map_compatibility φ₁ L₂ L₁, map_compatibility φ₂ L₂ L₁, 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
X Y : C
φ₁ φ₂ : W.LeftFraction X Y
E : Type u_3
inst_2 : Category.{v_3, u_3} E
L₁ : Functor.{v_1, v_2, u_1, u_2} C D
L₂ : Functor.{v_1, v_3, u_1, u_3} C E
inst_3 : L₁.IsLocalization W
inst_4 : L₂.IsLocalization W
h : φ₁.map (W := W) L₁ ⋯ = φ₂.map (W := W) L₁ ⋯
a :
  NatTrans.app (Iso.hom (Localization.compUniqFunctor L₂ L₁ W)) X ≫
      φ₁.map (W := W) L₁ ⋯ ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₂ L₁ W)) Y =
    (Localization.uniq L₂ L₁ W).functor.map (φ₂.map (W := W) L₂ ⋯)
a₁ :
  Eq (α := (Localization.uniq L₂ L₁ W).functor.obj (L₂.obj X) ⟶ (Localization.uniq L₂ L₁ W).functor.obj (L₂.obj Y))
    (NatTrans.app (Iso.hom (Localization.compUniqFunctor L₂ L₁ W)) X ≫
        φ₁.map (W := W) L₁ ⋯ ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₂ L₁ W)) Y :
      (L₂ ⋙ (Localization.uniq L₂ L₁ W).functor).obj X ⟶ (L₂ ⋙ (Localization.uniq L₂ L₁ W).functor).obj Y)
    (NatTrans.app (Iso.hom (Localization.compUniqFunctor L₂ L₁ W)) X ≫
      φ₂.map (W := W) L₁ ⋯ ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₂ L₁ W)) Y)
⊢ (Localization.uniq L₂ L₁ W).functor.map (φ₁.map (W := W) L₂ ⋯) =
    (Localization.uniq L₂ L₁ W).functor.map (φ₂.map (W := W) L₂ ⋯)
have a₂ : Eq (α := (Localization.uniq L₂ L₁ W).functor.obj (L₂.obj X) ⟶ (Localization.uniq L₂ L₁ W).functor.obj (L₂.obj Y))
  (NatTrans.app (Iso.hom (Localization.compUniqFunctor L₂ L₁ W)) X ≫
      φ₂.map (W := W) L₁ sorry ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₂ L₁ W)) Y :
    (L₂ ⋙ (Localization.uniq L₂ L₁ W).functor).obj X ⟶ (L₂ ⋙ (Localization.uniq L₂ L₁ W).functor).obj Y)
  (NatTrans.app (Iso.hom (Localization.compUniqFunctor L₂ L₁ W)) X ≫
    φ₂.map (W := W) L₁ sorry ≫ NatTrans.app (Iso.inv (Localization.compUniqFunctor L₂ L₁ W)) Y)
Tactic: rw [map_compatibility φ₁ L₂ L₁, map_compatibility φ₂ L₂ L₁, 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
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)
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization W
⊢ IsIso (L.map (z₂.s (W := W) ≫ z₃.s (W := W)))
have rw : IsIso (L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)))
Tactic: rw [L.map_comp]
-- 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₁ : 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)
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization W
⊢ z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ = (z₁.comp₀ (W := W) z₂ z₃).map (W := W) L ⋯
have this : IsIso (L.map (z₂.s (W := W) ≫ z₃.s (W := W)))
Tactic: have : IsIso (L.map (z₂.s ≫ z₃.s)) := by
    rw [L.map_comp]
    infer_instance
-- 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₁ : 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)
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization W
this : IsIso (L.map (z₂.s (W := W) ≫ z₃.s (W := W)))
⊢ z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯
have rw : (z₁.map (W := W) L sorry ≫ z₂.map (W := W) L sorry) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
  (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) sorry).map (W := W) L sorry ≫
    L.map (z₂.s (W := W) ≫ z₃.s (W := W))
Tactic: rw [← cancel_mono (L.map (z₂.s ≫ z₃.s)), map_comp_map_s,
    L.map_comp, assoc, map_comp_map_s_assoc, ← L.map_comp, h₃,
    L.map_comp, map_comp_map_s_assoc, L.map_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 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)
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization W
this : IsIso (L.map (z₂.s (W := W) ≫ z₃.s (W := W)))
rw :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯ ≫
      L.map (z₂.s (W := W) ≫ z₃.s (W := W))
⊢ z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯
have rw₁ : (z₁.map (W := W) L sorry ≫ z₂.map (W := W) L sorry) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
  L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) sorry).f (W := W))
Tactic: rw [← cancel_mono (L.map (z₂.s ≫ z₃.s)), map_comp_map_s,
    L.map_comp, assoc, map_comp_map_s_assoc, ← L.map_comp, h₃,
    L.map_comp, map_comp_map_s_assoc, L.map_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 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)
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization W
this : IsIso (L.map (z₂.s (W := W) ≫ z₃.s (W := W)))
rw :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯ ≫
      L.map (z₂.s (W := W) ≫ z₃.s (W := W))
rw₁ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
⊢ z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯
have rw₂ : (z₁.map (W := W) L sorry ≫ z₂.map (W := W) L sorry) ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
  L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) sorry).f (W := W))
Tactic: rw [← cancel_mono (L.map (z₂.s ≫ z₃.s)), map_comp_map_s,
    L.map_comp, assoc, map_comp_map_s_assoc, ← L.map_comp, h₃,
    L.map_comp, map_comp_map_s_assoc, L.map_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 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)
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization W
this : IsIso (L.map (z₂.s (W := W) ≫ z₃.s (W := W)))
rw :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯ ≫
      L.map (z₂.s (W := W) ≫ z₃.s (W := W))
rw₁ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₂ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
⊢ z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯
have rw₃ : z₁.map (W := W) L sorry ≫ z₂.map (W := W) L sorry ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
  L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) sorry).f (W := W))
Tactic: rw [← cancel_mono (L.map (z₂.s ≫ z₃.s)), map_comp_map_s,
    L.map_comp, assoc, map_comp_map_s_assoc, ← L.map_comp, h₃,
    L.map_comp, map_comp_map_s_assoc, L.map_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 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)
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization W
this : IsIso (L.map (z₂.s (W := W) ≫ z₃.s (W := W)))
rw :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯ ≫
      L.map (z₂.s (W := W) ≫ z₃.s (W := W))
rw₁ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₂ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₃ :
  z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
⊢ z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯
have rw₄ : z₁.map (W := W) L sorry ≫ L.map (z₂.f (W := W)) ≫ L.map (z₃.s (W := W)) =
  L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) sorry).f (W := W))
Tactic: rw [← cancel_mono (L.map (z₂.s ≫ z₃.s)), map_comp_map_s,
    L.map_comp, assoc, map_comp_map_s_assoc, ← L.map_comp, h₃,
    L.map_comp, map_comp_map_s_assoc, L.map_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 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)
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization W
this : IsIso (L.map (z₂.s (W := W) ≫ z₃.s (W := W)))
rw :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯ ≫
      L.map (z₂.s (W := W) ≫ z₃.s (W := W))
rw₁ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₂ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₃ :
  z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₄ :
  z₁.map (W := W) L ⋯ ≫ L.map (z₂.f (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
⊢ z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯
have rw₅ : z₁.map (W := W) L sorry ≫ L.map (z₂.f (W := W) ≫ z₃.s (W := W)) =
  L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) sorry).f (W := W))
Tactic: rw [← cancel_mono (L.map (z₂.s ≫ z₃.s)), map_comp_map_s,
    L.map_comp, assoc, map_comp_map_s_assoc, ← L.map_comp, h₃,
    L.map_comp, map_comp_map_s_assoc, L.map_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 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)
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization W
this : IsIso (L.map (z₂.s (W := W) ≫ z₃.s (W := W)))
rw :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯ ≫
      L.map (z₂.s (W := W) ≫ z₃.s (W := W))
rw₁ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₂ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₃ :
  z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₄ :
  z₁.map (W := W) L ⋯ ≫ L.map (z₂.f (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₅ :
  z₁.map (W := W) L ⋯ ≫ L.map (z₂.f (W := W) ≫ z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
⊢ z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯
have rw₆ : z₁.map (W := W) L sorry ≫ L.map (z₁.s (W := W) ≫ z₃.f (W := W)) =
  L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) sorry).f (W := W))
Tactic: rw [← cancel_mono (L.map (z₂.s ≫ z₃.s)), map_comp_map_s,
    L.map_comp, assoc, map_comp_map_s_assoc, ← L.map_comp, h₃,
    L.map_comp, map_comp_map_s_assoc, L.map_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 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)
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization W
this : IsIso (L.map (z₂.s (W := W) ≫ z₃.s (W := W)))
rw :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯ ≫
      L.map (z₂.s (W := W) ≫ z₃.s (W := W))
rw₁ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₂ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₃ :
  z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₄ :
  z₁.map (W := W) L ⋯ ≫ L.map (z₂.f (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₅ :
  z₁.map (W := W) L ⋯ ≫ L.map (z₂.f (W := W) ≫ z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₆ :
  z₁.map (W := W) L ⋯ ≫ L.map (z₁.s (W := W) ≫ z₃.f (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
⊢ z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯
have rw₇ : z₁.map (W := W) L sorry ≫ L.map (z₁.s (W := W)) ≫ L.map (z₃.f (W := W)) =
  L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) sorry).f (W := W))
Tactic: rw [← cancel_mono (L.map (z₂.s ≫ z₃.s)), map_comp_map_s,
    L.map_comp, assoc, map_comp_map_s_assoc, ← L.map_comp, h₃,
    L.map_comp, map_comp_map_s_assoc, L.map_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 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)
L : Functor.{v_1, v_2, u_1, u_2} C D
inst_3 : L.IsLocalization W
this : IsIso (L.map (z₂.s (W := W) ≫ z₃.s (W := W)))
rw :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯ ≫
      L.map (z₂.s (W := W) ≫ z₃.s (W := W))
rw₁ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W) ≫ z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₂ :
  (z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯) ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₃ :
  z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ ≫ L.map (z₂.s (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₄ :
  z₁.map (W := W) L ⋯ ≫ L.map (z₂.f (W := W)) ≫ L.map (z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₅ :
  z₁.map (W := W) L ⋯ ≫ L.map (z₂.f (W := W) ≫ z₃.s (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₆ :
  z₁.map (W := W) L ⋯ ≫ L.map (z₁.s (W := W) ≫ z₃.f (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
rw₇ :
  z₁.map (W := W) L ⋯ ≫ L.map (z₁.s (W := W)) ≫ L.map (z₃.f (W := W)) =
    L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).f (W := W))
⊢ z₁.map (W := W) L ⋯ ≫ z₂.map (W := W) L ⋯ =
    (mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) ⋯).map (W := W) L ⋯
have rw₈ : L.map (z₁.f (W := W)) ≫ L.map (z₃.f (W := W)) =
  L.map ((mk (W := W) (z₁.f (W := W) ≫ z₃.f (W := W)) (z₂.s (W := W) ≫ z₃.s (W := W)) sorry).f (W := W))
Tactic: rw [← cancel_mono (L.map (z₂.s ≫ z₃.s)), map_comp_map_s,
    L.map_comp, assoc, map_comp_map_s_assoc, ← L.map_comp, h₃,
    L.map_comp, map_comp_map_s_assoc, L.map_comp]