awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' (W := W) ⟶ Z
t₂ : ψ.Y' (W := W) ⟶ Z
hst : φ.s (W := W) ≫ t₁ = ψ.s (W := W) ≫ t₂
hft : φ.f (W := W) ≫ t₁ = ψ.f (W := W) ≫ t₂
ht : W (φ.s (W := W) ≫ t₁)
Z' : C
t₁' : φ.Y' (W := W) ⟶ Z'
t₂' : ψ.Y' (W := W) ⟶ Z'
hst' : φ.s (W := W) ≫ t₁' = ψ.s (W := W) ≫ t₂'
hft' : φ.f' (W := W) ≫ t₁' = ψ.f' (W := W) ≫ t₂'
ht' : W (φ.s (W := W) ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)
Z'' : C
u : α.Y' (W := W) ⟶ Z''
hu : W u
hα' : ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac : t₁' ≫ α.s (W := W) ≫ u = t₁ ≫ α.f (W := W) ≫ u
fac' : t₂ ≫ α.f (W := W) ≫ u ≫ u' = t₂' ≫ α.s (W := W) ≫ u ≫ u'
⊢ W ((φ.s (W := W) ≫ t₁') ≫ α.s (W := W) ≫ u ≫ u')

Tactic:
exact W.comp_mem _ _ ht' (W.comp_mem _ _ α.hs (W.comp_mem _ _ hu hu'))

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
h : LeftFraction₂Rel (W := W) φ ψ
⊢ LeftFractionRel (W := W) (φ.fst (W := W)) (ψ.fst (W := W)) ∧
    LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W))

Tactic:
⟨h.fst, h.snd⟩

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂Rel.snd, CategoryTheory.MorphismProperty.LeftFraction₂Rel.fst, And.intro
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
h : LeftFraction₂Rel (W := W) φ ψ
⊢ LeftFractionRel (W := W) (φ.fst (W := W)) (ψ.fst (W := W)) ∧
    LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W))

Tactic:
exact ⟨h.fst, h.snd⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.RightFraction₂ X Y
inst_1 : W.HasLeftCalculusOfFractions
obtain :
  ∀ (ψ₁ : W.LeftFraction X Y)
    (hψ₁ : φ.fst (W := W).f (W := W) ≫ ψ₁.s (W := W) = φ.fst (W := W).s (W := W) ≫ ψ₁.f (W := W)),
    ∃ (ψ : W.LeftFraction₂ X Y),
      φ.f (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f (W := W) ∧
        φ.f' (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f' (W := W)
⊢ ∃ (ψ : W.LeftFraction₂ X Y),
    φ.f (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f (W := W) ∧
      φ.f' (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f' (W := W)

Tactic:
obtain ⟨ψ₁, hψ₁⟩ := φ.fst.exists_leftFraction

Premises used: CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction, CategoryTheory.MorphismProperty.RightFraction₂.fst
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.RightFraction₂ X Y
inst_1 : W.HasLeftCalculusOfFractions
ψ₁ : W.LeftFraction X Y
hψ₁ : φ.fst (W := W).f (W := W) ≫ ψ₁.s (W := W) = φ.fst (W := W).s (W := W) ≫ ψ₁.f (W := W)
obtain :
  ∀ (ψ₂ : W.LeftFraction X Y)
    (hψ₂ : φ.snd (W := W).f (W := W) ≫ ψ₂.s (W := W) = φ.snd (W := W).s (W := W) ≫ ψ₂.f (W := W)),
    ∃ (ψ : W.LeftFraction₂ X Y),
      φ.f (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f (W := W) ∧
        φ.f' (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f' (W := W)
⊢ ∃ (ψ : W.LeftFraction₂ X Y),
    φ.f (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f (W := W) ∧
      φ.f' (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f' (W := W)

Tactic:
obtain ⟨ψ₂, hψ₂⟩ := φ.snd.exists_leftFraction

Premises used: CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction, CategoryTheory.MorphismProperty.RightFraction₂.snd
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.RightFraction₂ X Y
inst_1 : W.HasLeftCalculusOfFractions
ψ₁ : W.LeftFraction X Y
hψ₁ : φ.fst (W := W).f (W := W) ≫ ψ₁.s (W := W) = φ.fst (W := W).s (W := W) ≫ ψ₁.f (W := W)
ψ₂ : W.LeftFraction X Y
hψ₂ : φ.snd (W := W).f (W := W) ≫ ψ₂.s (W := W) = φ.snd (W := W).s (W := W) ≫ ψ₂.f (W := W)
obtain :
  ∀ (α : W.LeftFraction (ψ₁.Y' (W := W)) (ψ₂.Y' (W := W)))
    (hα :
      (RightFraction.mk (W := W) (ψ₁.s (W := W)) ⋯ (ψ₂.s (W := W))).f (W := W) ≫ α.s (W := W) =
        (RightFraction.mk (W := W) (ψ₁.s (W := W)) ⋯ (ψ₂.s (W := W))).s (W := W) ≫ α.f (W := W)),
    ∃ (ψ : W.LeftFraction₂ X Y),
      φ.f (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f (W := W) ∧
        φ.f' (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f' (W := W)
⊢ ∃ (ψ : W.LeftFraction₂ X Y),
    φ.f (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f (W := W) ∧
      φ.f' (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f' (W := W)

Tactic:
obtain ⟨α, hα⟩ := (RightFraction.mk _ ψ₁.hs ψ₂.s).exists_leftFraction

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.RightFraction.mk, CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction, CategoryTheory.MorphismProperty.LeftFraction.s
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.RightFraction₂ X Y
inst_1 : W.HasLeftCalculusOfFractions
ψ₁ : W.LeftFraction X Y
hψ₁ : φ.f (W := W) ≫ ψ₁.s (W := W) = φ.s (W := W) ≫ ψ₁.f (W := W)
ψ₂ : W.LeftFraction X Y
hψ₂ : φ.f' (W := W) ≫ ψ₂.s (W := W) = φ.s (W := W) ≫ ψ₂.f (W := W)
α : W.LeftFraction (ψ₁.Y' (W := W)) (ψ₂.Y' (W := W))
hα : ψ₂.s (W := W) ≫ α.s (W := W) = ψ₁.s (W := W) ≫ α.f (W := W)
⊢ ∃ (ψ : W.LeftFraction₂ X Y),
    φ.f (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f (W := W) ∧
      φ.f' (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f' (W := W)

Tactic:
⟨LeftFraction₂.mk (ψ₁.f ≫ α.f) (ψ₂.f ≫ α.s) (ψ₂.s ≫ α.s)
      (W.comp_mem _ _ ψ₂.hs α.hs), ?_, ?_⟩

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.comp_mem, And.intro, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.LeftFraction.f, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.LeftFraction₂.mk
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.RightFraction₂ X Y
inst_1 : W.HasLeftCalculusOfFractions
ψ₁ : W.LeftFraction X Y
hψ₁ : φ.f (W := W) ≫ ψ₁.s (W := W) = φ.s (W := W) ≫ ψ₁.f (W := W)
ψ₂ : W.LeftFraction X Y
hψ₂ : φ.f' (W := W) ≫ ψ₂.s (W := W) = φ.s (W := W) ≫ ψ₂.f (W := W)
α : W.LeftFraction (ψ₁.Y' (W := W)) (ψ₂.Y' (W := W))
hα : ψ₂.s (W := W) ≫ α.s (W := W) = ψ₁.s (W := W) ≫ α.f (W := W)
refine_1 :
  φ.f (W := W) ≫
      (LeftFraction₂.mk (W := W) (ψ₁.f (W := W) ≫ α.f (W := W)) (ψ₂.f (W := W) ≫ α.s (W := W))
            (ψ₂.s (W := W) ≫ α.s (W := W)) ⋯).s
        (W := W) =
    φ.s (W := W) ≫
      (LeftFraction₂.mk (W := W) (ψ₁.f (W := W) ≫ α.f (W := W)) (ψ₂.f (W := W) ≫ α.s (W := W))
            (ψ₂.s (W := W) ≫ α.s (W := W)) ⋯).f
        (W := W)
refine_2 :
  φ.f' (W := W) ≫
      (LeftFraction₂.mk (W := W) (ψ₁.f (W := W) ≫ α.f (W := W)) (ψ₂.f (W := W) ≫ α.s (W := W))
            (ψ₂.s (W := W) ≫ α.s (W := W)) ⋯).s
        (W := W) =
    φ.s (W := W) ≫
      (LeftFraction₂.mk (W := W) (ψ₁.f (W := W) ≫ α.f (W := W)) (ψ₂.f (W := W) ≫ α.s (W := W))
            (ψ₂.s (W := W) ≫ α.s (W := W)) ⋯).f'
        (W := W)
⊢ ∃ (ψ : W.LeftFraction₂ X Y),
    φ.f (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f (W := W) ∧
      φ.f' (W := W) ≫ ψ.s (W := W) = φ.s (W := W) ≫ ψ.f' (W := W)

Tactic:
refine ⟨LeftFraction₂.mk (ψ₁.f ≫ α.f) (ψ₂.f ≫ α.s) (ψ₂.s ≫ α.s)
      (W.comp_mem _ _ ψ₂.hs α.hs), ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.RightFraction₂ X Y
inst_1 : W.HasLeftCalculusOfFractions
ψ₁ : W.LeftFraction X Y
hψ₁ : φ.f (W := W) ≫ ψ₁.s (W := W) = φ.s (W := W) ≫ ψ₁.f (W := W)
ψ₂ : W.LeftFraction X Y
hψ₂ : φ.f' (W := W) ≫ ψ₂.s (W := W) = φ.s (W := W) ≫ ψ₂.f (W := W)
α : W.LeftFraction (ψ₁.Y' (W := W)) (ψ₂.Y' (W := W))
hα : ψ₂.s (W := W) ≫ α.s (W := W) = ψ₁.s (W := W) ≫ α.f (W := W)
refine_1 : φ.f (W := W) ≫ ψ₂.s (W := W) ≫ α.s (W := W) = φ.s (W := W) ≫ ψ₁.f (W := W) ≫ α.f (W := W)
⊢ φ.f (W := W) ≫
      (LeftFraction₂.mk (W := W) (ψ₁.f (W := W) ≫ α.f (W := W)) (ψ₂.f (W := W) ≫ α.s (W := W))
            (ψ₂.s (W := W) ≫ α.s (W := W)) ⋯).s
        (W := W) =
    φ.s (W := W) ≫
      (LeftFraction₂.mk (W := W) (ψ₁.f (W := W) ≫ α.f (W := W)) (ψ₂.f (W := W) ≫ α.s (W := W))
            (ψ₂.s (W := W) ≫ α.s (W := W)) ⋯).f
        (W := W)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.RightFraction₂ X Y
inst_1 : W.HasLeftCalculusOfFractions
ψ₁ : W.LeftFraction X Y
hψ₁ : φ.f (W := W) ≫ ψ₁.s (W := W) = φ.s (W := W) ≫ ψ₁.f (W := W)
ψ₂ : W.LeftFraction X Y
hψ₂ : φ.f' (W := W) ≫ ψ₂.s (W := W) = φ.s (W := W) ≫ ψ₂.f (W := W)
α : W.LeftFraction (ψ₁.Y' (W := W)) (ψ₂.Y' (W := W))
hα : ψ₂.s (W := W) ≫ α.s (W := W) = ψ₁.s (W := W) ≫ α.f (W := W)
refine_1 : φ.f (W := W) ≫ ψ₁.s (W := W) ≫ α.f (W := W) = φ.s (W := W) ≫ ψ₁.f (W := W) ≫ α.f (W := W)
refine_1₁ refine_1₂ : φ.s (W := W) ≫ ψ₁.f (W := W) ≫ α.f (W := W) = φ.s (W := W) ≫ ψ₁.f (W := W) ≫ α.f (W := W)
⊢ φ.f (W := W) ≫ ψ₂.s (W := W) ≫ α.s (W := W) = φ.s (W := W) ≫ ψ₁.f (W := W) ≫ α.f (W := W)

Tactic:
rw [hα, reassoc_of% hψ₁]
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X Y : C
φ : W.RightFraction₂ X Y
inst_1 : W.HasLeftCalculusOfFractions
ψ₁ : W.LeftFraction X Y
hψ₁ : φ.f (W := W) ≫ ψ₁.s (W := W) = φ.s (W := W) ≫ ψ₁.f (W := W)
ψ₂ : W.LeftFraction X Y
hψ₂ : φ.f' (W := W) ≫ ψ₂.s (W := W) = φ.s (W := W) ≫ ψ₂.f (W := W)
α : W.LeftFraction (ψ₁.Y' (W := W)) (ψ₂.Y' (W := W))
hα : ψ₂.s (W := W) ≫ α.s (W := W) = ψ₁.s (W := W) ≫ α.f (W := W)
refine_2 refine_2₁ :
  φ.s (W := W) ≫ ψ₂.f (W := W) ≫ α.s (W := W) =
    φ.s (W := W) ≫
      (LeftFraction₂.mk (W := W) (ψ₁.f (W := W) ≫ α.f (W := W)) (ψ₂.f (W := W) ≫ α.s (W := W))
            (ψ₂.s (W := W) ≫ α.s (W := W)) ⋯).f'
        (W := W)
⊢ φ.f' (W := W) ≫
      (LeftFraction₂.mk (W := W) (ψ₁.f (W := W) ≫ α.f (W := W)) (ψ₂.f (W := W) ≫ α.s (W := W))
            (ψ₂.s (W := W) ≫ α.s (W := W)) ⋯).s
        (W := W) =
    φ.s (W := W) ≫
      (LeftFraction₂.mk (W := W) (ψ₁.f (W := W) ≫ α.f (W := W)) (ψ₂.f (W := W) ≫ α.s (W := W))
            (ψ₂.s (W := W) ≫ α.s (W := W)) ⋯).f'
        (W := W)

Tactic:
rw [reassoc_of% hψ₂]
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
have :
  ∀ (φ : W.LeftFraction X Y) (hφ : f = φ.map (W := W) L ⋯),
    ∃ (φ : W.LeftFraction₂ X Y), f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯
⊢ ∃ (φ : W.LeftFraction₂ X Y), f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯

Tactic:
have ⟨φ, hφ⟩ := exists_leftFraction L W f
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map (W := W) L ⋯
have :
  ∀ (φ' : W.LeftFraction X Y) (hφ' : f' = φ'.map (W := W) L ⋯),
    ∃ (φ : W.LeftFraction₂ X Y), f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯
⊢ ∃ (φ : W.LeftFraction₂ X Y), f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯

Tactic:
have ⟨φ', hφ'⟩ := exists_leftFraction L W f'
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map (W := W) L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map (W := W) L ⋯
obtain :
  ∀ (α : W.LeftFraction (φ.Y' (W := W)) (φ'.Y' (W := W)))
    (hα :
      (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).f (W := W) ≫ α.s (W := W) =
        (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).s (W := W) ≫ α.f (W := W)),
    ∃ (φ : W.LeftFraction₂ X Y), f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯
⊢ ∃ (φ : W.LeftFraction₂ X Y), f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯

Tactic:
obtain ⟨α, hα⟩ := (RightFraction.mk _ φ.hs φ'.s).exists_leftFraction

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.RightFraction.mk, CategoryTheory.MorphismProperty.RightFraction.exists_leftFraction, CategoryTheory.MorphismProperty.LeftFraction.s
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map (W := W) L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map (W := W) L ⋯
α : W.LeftFraction (φ.Y' (W := W)) (φ'.Y' (W := W))
hα :
  (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).f (W := W) ≫ α.s (W := W) =
    (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).s (W := W) ≫ α.f (W := W)
ψ : W.LeftFraction₂ X Y :=
  LeftFraction₂.mk (W := W) (φ.f (W := W) ≫ α.f (W := W)) (φ'.f (W := W) ≫ α.s (W := W)) (φ'.s (W := W) ≫ α.s (W := W))
    ⋯
rw : IsIso (L.map (φ'.s (W := W)) ≫ L.map (α.s (W := W)))
⊢ IsIso (L.map (φ'.s (W := W) ≫ α.s (W := W)))

Tactic:
rw [L.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map (W := W) L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map (W := W) L ⋯
α : W.LeftFraction (φ.Y' (W := W)) (φ'.Y' (W := W))
hα :
  (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).f (W := W) ≫ α.s (W := W) =
    (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).s (W := W) ≫ α.f (W := W)
ψ : W.LeftFraction₂ X Y :=
  LeftFraction₂.mk (W := W) (φ.f (W := W) ≫ α.f (W := W)) (φ'.f (W := W) ≫ α.s (W := W)) (φ'.s (W := W) ≫ α.s (W := W))
    ⋯
⊢ IsIso (L.map (φ'.s (W := W)) ≫ L.map (α.s (W := W)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map (W := W) L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map (W := W) L ⋯
α : W.LeftFraction (φ.Y' (W := W)) (φ'.Y' (W := W))
hα :
  (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).f (W := W) ≫ α.s (W := W) =
    (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).s (W := W) ≫ α.f (W := W)
ψ : W.LeftFraction₂ X Y :=
  LeftFraction₂.mk (W := W) (φ.f (W := W) ≫ α.f (W := W)) (φ'.f (W := W) ≫ α.s (W := W)) (φ'.s (W := W) ≫ α.s (W := W))
    ⋯
⊢ IsIso (L.map (φ'.s (W := W) ≫ α.s (W := W)))

Tactic:
have : IsIso (L.map (φ'.s ≫ α.s)) := by
    rw [L.map_comp]
    infer_instance
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map (W := W) L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map (W := W) L ⋯
α : W.LeftFraction (φ.Y' (W := W)) (φ'.Y' (W := W))
hα :
  (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).f (W := W) ≫ α.s (W := W) =
    (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).s (W := W) ≫ α.f (W := W)
ψ : W.LeftFraction₂ X Y :=
  LeftFraction₂.mk (W := W) (φ.f (W := W) ≫ α.f (W := W)) (φ'.f (W := W) ≫ α.s (W := W)) (φ'.s (W := W) ≫ α.s (W := W))
    ⋯
this : IsIso (L.map (φ'.s (W := W) ≫ α.s (W := W)))
⊢ ∃ (φ : W.LeftFraction₂ X Y), f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯

Tactic:
⟨ψ, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map (W := W) L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map (W := W) L ⋯
α : W.LeftFraction (φ.Y' (W := W)) (φ'.Y' (W := W))
hα :
  (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).f (W := W) ≫ α.s (W := W) =
    (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).s (W := W) ≫ α.f (W := W)
ψ : W.LeftFraction₂ X Y :=
  LeftFraction₂.mk (W := W) (φ.f (W := W) ≫ α.f (W := W)) (φ'.f (W := W) ≫ α.s (W := W)) (φ'.s (W := W) ≫ α.s (W := W))
    ⋯
this : IsIso (L.map (φ'.s (W := W) ≫ α.s (W := W)))
refine_1 : f = ψ.fst (W := W).map (W := W) L ⋯
refine_2 : f' = ψ.snd (W := W).map (W := W) L ⋯
⊢ ∃ (φ : W.LeftFraction₂ X Y), f = φ.fst (W := W).map (W := W) L ⋯ ∧ f' = φ.snd (W := W).map (W := W) L ⋯

Tactic:
refine ⟨ψ, ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map (W := W) L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map (W := W) L ⋯
α : W.LeftFraction (φ.Y' (W := W)) (φ'.Y' (W := W))
hα :
  (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).f (W := W) ≫ α.s (W := W) =
    (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).s (W := W) ≫ α.f (W := W)
ψ : W.LeftFraction₂ X Y :=
  LeftFraction₂.mk (W := W) (φ.f (W := W) ≫ α.f (W := W)) (φ'.f (W := W) ≫ α.s (W := W)) (φ'.s (W := W) ≫ α.s (W := W))
    ⋯
this : IsIso (L.map (φ'.s (W := W) ≫ α.s (W := W)))
refine_1 :
  f ≫ L.map (φ'.s (W := W) ≫ α.s (W := W)) = ψ.fst (W := W).map (W := W) L ⋯ ≫ L.map (φ'.s (W := W) ≫ α.s (W := W))
refine_1₁ : f ≫ L.map (φ'.s (W := W) ≫ α.s (W := W)) = L.map (ψ.fst (W := W).f (W := W))
refine_1₂ :
  f ≫ L.map ((RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).s (W := W) ≫ α.f (W := W)) =
    L.map (ψ.fst (W := W).f (W := W))
refine_1₃ :
  f ≫ L.map ((RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).s (W := W)) ≫ L.map (α.f (W := W)) =
    L.map (ψ.fst (W := W).f (W := W))
refine_1₄ :
  φ.map (W := W) L ⋯ ≫
      L.map ((RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).s (W := W)) ≫ L.map (α.f (W := W)) =
    L.map (ψ.fst (W := W).f (W := W))
refine_1₅ : L.map (φ.f (W := W)) ≫ L.map (α.f (W := W)) = L.map (ψ.fst (W := W).f (W := W))
refine_1₆ refine_1₇ : L.map (φ.f (W := W)) ≫ L.map (α.f (W := W)) = L.map (φ.f (W := W)) ≫ L.map (α.f (W := W))
⊢ f = ψ.fst (W := W).map (W := W) L ⋯

Tactic:
rw [← cancel_mono (L.map (φ'.s ≫ α.s)), LeftFraction.map_comp_map_s,
      hα, L.map_comp, hφ, LeftFraction.map_comp_map_s_assoc,
      L.map_comp]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s, CategoryTheory.MorphismProperty.LeftFraction.s, CategoryTheory.MorphismProperty.LeftFraction.map_comp_map_s_assoc
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map (W := W) L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map (W := W) L ⋯
α : W.LeftFraction (φ.Y' (W := W)) (φ'.Y' (W := W))
hα :
  (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).f (W := W) ≫ α.s (W := W) =
    (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).s (W := W) ≫ α.f (W := W)
ψ : W.LeftFraction₂ X Y :=
  LeftFraction₂.mk (W := W) (φ.f (W := W) ≫ α.f (W := W)) (φ'.f (W := W) ≫ α.s (W := W)) (φ'.s (W := W) ≫ α.s (W := W))
    ⋯
this : IsIso (L.map (φ'.s (W := W) ≫ α.s (W := W)))
refine_2 :
  φ'.map (W := W) L ⋯ ≫ L.map (φ'.s (W := W) ≫ α.s (W := W)) =
    ψ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ'.s (W := W) ≫ α.s (W := W))
⊢ f' = ψ.snd (W := W).map (W := W) L ⋯

Tactic:
rw [← cancel_mono (L.map (φ'.s ≫ α.s)), hφ']

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.LeftFraction.s
-- Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
inst_3 : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map (W := W) L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map (W := W) L ⋯
α : W.LeftFraction (φ.Y' (W := W)) (φ'.Y' (W := W))
hα :
  (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).f (W := W) ≫ α.s (W := W) =
    (RightFraction.mk (W := W) (φ.s (W := W)) ⋯ (φ'.s (W := W))).s (W := W) ≫ α.f (W := W)
ψ : W.LeftFraction₂ X Y :=
  LeftFraction₂.mk (W := W) (φ.f (W := W) ≫ α.f (W := W)) (φ'.f (W := W) ≫ α.s (W := W)) (φ'.s (W := W) ≫ α.s (W := W))
    ⋯
this : IsIso (L.map (φ'.s (W := W) ≫ α.s (W := W)))
refine_2 :
  φ'.map (W := W) L ⋯ ≫ L.map (φ'.s (W := W)) ≫ L.map (α.s (W := W)) =
    ψ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ'.s (W := W) ≫ α.s (W := W))
⊢ φ'.map (W := W) L ⋯ ≫ L.map (φ'.s (W := W) ≫ α.s (W := W)) =
    ψ.snd (W := W).map (W := W) L ⋯ ≫ L.map (φ'.s (W := W) ≫ α.s (W := W))

Tactic:
nth_rw 1 [L.map_comp]

Premises used: CategoryTheory.Functor.map_comp