awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
z₁ z₂ : W.LeftFraction₂ X Y
h : LeftFraction₂Rel (W := W) z₁ z₂
obtain :
  ∀ (Z : C) (t₁ : z₁.Y' (W := W) ⟶ Z) (t₂ : z₂.Y' (W := W) ⟶ Z) (hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂),
    z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂ →
      ∀ (hft' : z₁.f' (W := W) ≫ t₁ = z₂.f' (W := W) ≫ t₂) (ht : W (z₁.s (W := W) ≫ t₁)),
        LeftFractionRel (W := W) (z₁.snd (W := W)) (z₂.snd (W := W))
⊢ LeftFractionRel (W := W) (z₁.snd (W := W)) (z₂.snd (W := W))

Tactic:
obtain ⟨Z, t₁, t₂, hst, _, hft', ht⟩ := 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
z₁ z₂ : W.LeftFraction₂ X Y
Z : C
t₁ : z₁.Y' (W := W) ⟶ Z
t₂ : z₂.Y' (W := W) ⟶ Z
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
w : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
hft' : z₁.f' (W := W) ≫ t₁ = z₂.f' (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
⊢ LeftFractionRel (W := W) (z₁.snd (W := W)) (z₂.snd (W := W))

Tactic:
⟨Z, t₁, t₂, hst, hft', ht⟩

Premises used: CategoryTheory.MorphismProperty.LeftFractionRel, Exists.intro
-- 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
z₁ z₂ : W.LeftFraction₂ X Y
Z : C
t₁ : z₁.Y' (W := W) ⟶ Z
t₂ : z₂.Y' (W := W) ⟶ Z
hst : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂
w : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂
hft' : z₁.f' (W := W) ≫ t₁ = z₂.f' (W := W) ≫ t₂
ht : W (z₁.s (W := W) ≫ t₁)
⊢ LeftFractionRel (W := W) (z₁.snd (W := W)) (z₂.snd (W := W))

Tactic:
exact ⟨Z, t₁, t₂, hst, hft', ht⟩
-- 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
simp :
  LeftFractionRel (W := W) (φ.fst (W := W)) (ψ.fst (W := W)) ∧
      LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W)) ↔
    LeftFraction₂Rel (W := W) φ ψ
⊢ φ.fst (W := W).map (W := W) L ⋯ = ψ.fst (W := W).map (W := W) L ⋯ ∧
      φ.snd (W := W).map (W := W) L ⋯ = ψ.snd (W := W).map (W := W) L ⋯ ↔
    LeftFraction₂Rel (W := W) φ ψ

Tactic:
simp only [LeftFraction.map_eq_iff L W]

Premises used: CategoryTheory.MorphismProperty.LeftFraction.map_eq_iff
-- 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
mp :
  LeftFractionRel (W := W) (φ.fst (W := W)) (ψ.fst (W := W)) ∧
      LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W)) →
    LeftFraction₂Rel (W := W) φ ψ
mpr :
  LeftFraction₂Rel (W := W) φ ψ →
    LeftFractionRel (W := W) (φ.fst (W := W)) (ψ.fst (W := W)) ∧
      LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W))
⊢ LeftFractionRel (W := W) (φ.fst (W := W)) (ψ.fst (W := W)) ∧
      LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W)) ↔
    LeftFraction₂Rel (W := W) φ ψ

Tactic:
constructor
-- 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 : LeftFractionRel (W := W) (φ.fst (W := W)) (ψ.fst (W := W))
h' : LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W))
mp :
  ∀ (Z : C) (t₁ : φ.fst (W := W).Y' (W := W) ⟶ Z) (t₂ : ψ.fst (W := W).Y' (W := W) ⟶ Z)
    (hst : φ.fst (W := W).s (W := W) ≫ t₁ = ψ.fst (W := W).s (W := W) ≫ t₂)
    (hft : φ.fst (W := W).f (W := W) ≫ t₁ = ψ.fst (W := W).f (W := W) ≫ t₂) (ht : W (φ.fst (W := W).s (W := W) ≫ t₁)),
    LeftFraction₂Rel (W := W) φ ψ
⊢ LeftFraction₂Rel (W := W) φ ψ

Tactic:
obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := 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
φ ψ : W.LeftFraction₂ X Y
h' : LeftFractionRel (W := W) (φ.snd (W := W)) (ψ.snd (W := W))
Z : C
t₁ : φ.fst (W := W).Y' (W := W) ⟶ Z
t₂ : ψ.fst (W := W).Y' (W := W) ⟶ Z
hst : φ.fst (W := W).s (W := W) ≫ t₁ = ψ.fst (W := W).s (W := W) ≫ t₂
hft : φ.fst (W := W).f (W := W) ≫ t₁ = ψ.fst (W := W).f (W := W) ≫ t₂
ht : W (φ.fst (W := W).s (W := W) ≫ t₁)
mp :
  ∀ (Z' : C) (t₁' : φ.snd (W := W).Y' (W := W) ⟶ Z') (t₂' : ψ.snd (W := W).Y' (W := W) ⟶ Z')
    (hst' : φ.snd (W := W).s (W := W) ≫ t₁' = ψ.snd (W := W).s (W := W) ≫ t₂')
    (hft' : φ.snd (W := W).f (W := W) ≫ t₁' = ψ.snd (W := W).f (W := W) ≫ t₂')
    (ht' : W (φ.snd (W := W).s (W := W) ≫ t₁')), LeftFraction₂Rel (W := W) φ ψ
⊢ LeftFraction₂Rel (W := W) φ ψ

Tactic:
obtain ⟨Z', t₁', t₂', hst', hft', ht'⟩ := 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
φ ψ : 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₁')
mp :
  ∀ (α : W.LeftFraction Z Z')
    (hα :
      (RightFraction.mk (W := W) (φ.s (W := W) ≫ t₁) ht (φ.s (W := W) ≫ t₁')).f (W := W) ≫ α.s (W := W) =
        (RightFraction.mk (W := W) (φ.s (W := W) ≫ t₁) ht (φ.s (W := W) ≫ t₁')).s (W := W) ≫ α.f (W := W)),
    LeftFraction₂Rel (W := W) φ ψ
⊢ LeftFraction₂Rel (W := W) φ ψ

Tactic:
have ⟨α, hα⟩ := (RightFraction.mk _ ht (φ.s ≫ t₁')).exists_leftFraction
-- 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α :
  (RightFraction.mk (W := W) (φ.s (W := W) ≫ t₁) ht (φ.s (W := W) ≫ t₁')).f (W := W) ≫ α.s (W := W) =
    (RightFraction.mk (W := W) (φ.s (W := W) ≫ t₁) ht (φ.s (W := W) ≫ t₁')).s (W := W) ≫ α.f (W := W)
⊢ φ.s (W := W) ≫ t₁' ≫ α.s (W := W) = φ.s (W := W) ≫ t₁ ≫ α.f (W := W)

Tactic:
simp only [Category.assoc] at hα

Premises used: CategoryTheory.Category.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
φ ψ : 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)
mp :
  ∀ (Z'' : C) (u : α.Y' (W := W) ⟶ Z'') (hu : W u) (fac : (t₁' ≫ α.s (W := W)) ≫ u = (t₁ ≫ α.f (W := W)) ≫ u),
    LeftFraction₂Rel (W := W) φ ψ
⊢ LeftFraction₂Rel (W := W) φ ψ

Tactic:
obtain ⟨Z'', u, hu, fac⟩ := HasLeftCalculusOfFractions.ext _ _ _ φ.hs hα

Premises used: CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.ext, CategoryTheory.MorphismProperty.LeftFraction₂.hs
-- 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
fac : (t₁' ≫ α.s (W := W)) ≫ u = (t₁ ≫ α.f (W := W)) ≫ u
rw : φ.s (W := W) ≫ t₁ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
rw₁ : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
rw₂ rw₃ : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u = φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u
⊢ ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u

Tactic:
rw [← reassoc_of% hst, ← reassoc_of% hα, ← reassoc_of% hst']
-- 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
fac : (t₁' ≫ α.s (W := W)) ≫ u = (t₁ ≫ α.f (W := W)) ≫ u
⊢ ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u

Tactic:
have hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u := by
      rw [← reassoc_of% hst, ← reassoc_of% hα, ← reassoc_of% hst']
-- 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
fac : (t₁' ≫ α.s (W := W)) ≫ u = (t₁ ≫ α.f (W := W)) ≫ u
hα' : ψ.s (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u
mp :
  ∀ (Z''' : C) (u' : Z'' ⟶ Z''') (hu' : W u') (fac' : (t₂ ≫ α.f (W := W) ≫ u) ≫ u' = (t₂' ≫ α.s (W := W) ≫ u) ≫ u'),
    LeftFraction₂Rel (W := W) φ ψ
⊢ LeftFraction₂Rel (W := W) φ ψ

Tactic:
obtain ⟨Z''', u', hu', fac'⟩ := HasLeftCalculusOfFractions.ext _ _ _ ψ.hs hα'

Premises used: CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.ext, CategoryTheory.MorphismProperty.LeftFraction₂.hs
-- 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
fac : (t₁' ≫ α.s (W := W)) ≫ u = (t₁ ≫ α.f (W := 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₂ ≫ α.f (W := W) ≫ u) ≫ u' = (t₂' ≫ α.s (W := W) ≫ u) ≫ u'
⊢ t₁' ≫ α.s (W := W) ≫ u = t₁ ≫ α.f (W := W) ≫ u

Tactic:
simp only [Category.assoc] at fac fac'

Premises used: CategoryTheory.Category.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
φ ψ : 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
fac : (t₁' ≫ α.s (W := W)) ≫ u = (t₁ ≫ α.f (W := 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₂ ≫ α.f (W := W) ≫ u) ≫ u' = (t₂' ≫ α.s (W := W) ≫ u) ≫ u'
fac₁ : t₁' ≫ α.s (W := W) ≫ u = t₁ ≫ α.f (W := W) ≫ u
⊢ t₂ ≫ α.f (W := W) ≫ u ≫ u' = t₂' ≫ α.s (W := W) ≫ u ≫ u'

Tactic:
simp only [Category.assoc] at fac fac'

Premises used: CategoryTheory.Category.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
φ ψ : 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'
⊢ LeftFraction₂Rel (W := W) φ ψ

Tactic:
⟨Z''', t₁' ≫ α.s ≫ u ≫ u', t₂' ≫ α.s ≫ u ≫ u', ?_, ?_, ?_, ?_⟩

Premises used: CategoryTheory.MorphismProperty.LeftFraction₂Rel, Exists.intro, 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
φ ψ : 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'
mp : φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
mp₁ : φ.f (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.f (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
mp₂ : φ.f' (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.f' (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
mp₃ : W (φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u')
⊢ LeftFraction₂Rel (W := W) φ ψ

Tactic:
refine ⟨Z''', t₁' ≫ α.s ≫ u ≫ u', t₂' ≫ α.s ≫ u ≫ u', ?_, ?_, ?_, ?_⟩
-- 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'
mp mp₁ : ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u' = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
⊢ φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.s (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'

Tactic:
rw [reassoc_of% hst']
-- 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'
mp : φ.f (W := W) ≫ t₁ ≫ α.f (W := W) ≫ u ≫ u' = ψ.f (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
mp₁ : ψ.f (W := W) ≫ t₂ ≫ α.f (W := W) ≫ u ≫ u' = ψ.f (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
mp₂ mp₃ : ψ.f (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u' = ψ.f (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
⊢ φ.f (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.f (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'

Tactic:
rw [reassoc_of% fac, reassoc_of% hft, fac']
-- 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'
mp mp₁ : ψ.f' (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u' = ψ.f' (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'
⊢ φ.f' (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u' = ψ.f' (W := W) ≫ t₂' ≫ α.s (W := W) ≫ u ≫ u'

Tactic:
rw [reassoc_of% hft']
-- 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'
mp : W ((φ.s (W := W) ≫ t₁') ≫ α.s (W := W) ≫ u ≫ u')
⊢ W (φ.s (W := W) ≫ t₁' ≫ α.s (W := W) ≫ u ≫ u')

Tactic:
rw [← Category.assoc]

Premises used: CategoryTheory.Category.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
φ ψ : 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:
W.comp_mem _ _ ht' (W.comp_mem _ _ α.hs (W.comp_mem _ _ hu hu'))

Premises used: CategoryTheory.MorphismProperty.LeftFraction.hs, CategoryTheory.MorphismProperty.comp_mem