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
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) φ ψ
⊢ (Localization.Hom.mk (W := W) φ).map (W := W) L ⋯ = (Localization.Hom.mk (W := W) ψ).map (W := W) L ⋯
have mpr : Localization.Hom.mk (W := W) φ = Localization.Hom.mk (W := W) ψ
Tactic: congr 1
-- 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
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₂ : X ⟶ Y
⊢ L.map f₁ = L.map f₂ ↔ ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s
have mp : L.map f₁ = L.map f₂ → ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s
Tactic: constructor
-- 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
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₂ : X ⟶ Y
mp : L.map f₁ = L.map f₂ → ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s
⊢ L.map f₁ = L.map f₂ ↔ ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s
have mpr : (∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s) → L.map f₁ = L.map f₂
Tactic: constructor
-- 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
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₂ : X ⟶ Y
h : L.map f₁ = L.map f₂
⊢ ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s
have h₁ : LeftFractionRel (W := W) (LeftFraction.ofHom W f₁) (LeftFraction.ofHom W f₂)
Tactic: rw [← LeftFraction.map_ofHom W _ L (Localization.inverts _ _),
      ← LeftFraction.map_ofHom W _ L (Localization.inverts _ _),
      LeftFraction.map_eq_iff] at h
Cleared hypotheses: 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
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₂ : X ⟶ Y
h : LeftFractionRel (W := W) (LeftFraction.ofHom W f₁) (LeftFraction.ofHom W f₂)
⊢ ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s
have mp : ∀ (Z : C) (t₁ : (LeftFraction.ofHom W f₁).Y' (W := W) ⟶ Z) (t₂ : (LeftFraction.ofHom W f₂).Y' (W := W) ⟶ Z)
  (hst : (LeftFraction.ofHom W f₁).s (W := W) ≫ t₁ = (LeftFraction.ofHom W f₂).s (W := W) ≫ t₂)
  (hft : (LeftFraction.ofHom W f₁).f (W := W) ≫ t₁ = (LeftFraction.ofHom W f₂).f (W := W) ≫ t₂)
  (ht : W ((LeftFraction.ofHom W f₁).s (W := W) ≫ t₁)), ∃ (Z : C) (s : Y ⟶ Z) (_ : W s), f₁ ≫ s = f₂ ≫ s
Tactic: obtain ⟨Z, t₁, t₂, hst, hft, ht⟩ := h
Cleared hypotheses: 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
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
f : Arrow.{v_2, u_2} D
⊢ L.mapArrow.essImage f
have this : L.EssSurj
Tactic: have := Localization.essSurj L W
-- 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
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
f : Arrow.{v_2, u_2} D
this : L.EssSurj
⊢ L.mapArrow.essImage f
have obtain : ∀ (X : C) (eX : L.obj X ≅ f.left), L.mapArrow.essImage f
Tactic: obtain ⟨X, ⟨eX⟩⟩ : ∃ (X : C), Nonempty (L.obj X ≅ f.left) :=
      ⟨_, ⟨L.objObjPreimageIso f.left⟩⟩
-- 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
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
f : Arrow.{v_2, u_2} D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
⊢ L.mapArrow.essImage f
have obtain : ∀ (Y : C) (eY : L.obj Y ≅ f.right), L.mapArrow.essImage f
Tactic: obtain ⟨Y, ⟨eY⟩⟩ : ∃ (Y : C), Nonempty (L.obj Y ≅ f.right) :=
      ⟨_, ⟨L.objObjPreimageIso f.right⟩⟩
-- 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
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
f : Arrow.{v_2, u_2} D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
⊢ L.mapArrow.essImage f
have obtain : ∀ (φ : W.LeftFraction X Y) (hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map (W := W) L sorry), L.mapArrow.essImage f
Tactic: obtain ⟨φ, hφ⟩ := Localization.exists_leftFraction L W (eX.hom ≫ f.hom ≫ eY.inv)
-- 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
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
f : Arrow.{v_2, u_2} D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map (W := W) L ⋯
⊢ L.mapArrow.essImage f
have refine : f ≅ L.mapArrow.obj (Arrow.mk (φ.f (W := W)))
Tactic: refine ⟨Arrow.mk φ.f, ⟨Iso.symm ?_⟩⟩
-- 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
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
f : Arrow.{v_2, u_2} D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map (W := W) L ⋯
⊢ f ≅ L.mapArrow.obj (Arrow.mk (φ.f (W := W)))
have refine : eX.symm.hom ≫ (L.mapArrow.obj (Arrow.mk (φ.f (W := W)))).hom = f.hom ≫ (eY.symm ≪≫ isoOfHom L W (φ.s (W := W)) sorry).hom
Tactic: refine Arrow.isoMk eX.symm (eY.symm ≪≫ Localization.isoOfHom L W φ.s φ.hs) ?_
-- 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
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
f : Arrow.{v_2, u_2} D
this : L.EssSurj
X : C
eX : L.obj X ≅ f.left
Y : C
eY : L.obj Y ≅ f.right
φ : W.LeftFraction X Y
hφ : eX.hom ≫ f.hom ≫ eY.inv = φ.map (W := W) L ⋯
⊢ eX.symm.hom ≫ (L.mapArrow.obj (Arrow.mk (φ.f (W := W)))).hom = f.hom ≫ (eY.symm ≪≫ isoOfHom L W (φ.s (W := W)) ⋯).hom
have dsimp : eX.inv ≫ L.map (φ.f (W := W)) = f.hom ≫ eY.inv ≫ L.map (φ.s (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
X Y : C
φ : W.RightFraction X Y
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
⊢ (φ.map (W := W) L hL).op = φ.op (W := W).map (W := W.op) L.op ⋯
have dsimp : Eq.{v_2 + 1} (α := Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
  ((L.map (φ.f (W := W))).op ≫ (inv (L.map (φ.s (W := W)))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
  ((L.map (φ.f (W := W))).op ≫ inv (L.map (φ.s (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
Tactic: dsimp [map, LeftFraction.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
X Y : C
φ : W.RightFraction X Y
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
⊢ Eq.{v_2 + 1} (α := Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    ((L.map (φ.f (W := W))).op ≫ (inv (L.map (φ.s (W := W)))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    ((L.map (φ.f (W := W))).op ≫ inv (L.map (φ.s (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
have rw : Eq.{v_2 + 1} (α := Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
  ((L.map (φ.f (W := W))).op ≫ inv (L.map (φ.s (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
  ((L.map (φ.f (W := W))).op ≫ inv (L.map (φ.s (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
Tactic: rw [op_inv]
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
⊢ (φ.map (W := W) L hL).op = φ.op (W := W).map (W := W.op) L.op ⋯
have dsimp : Eq.{v_2 + 1} (α := Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
  ((inv (L.map (φ.s (W := W)))).op ≫ (L.map (φ.f (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
  (inv (L.map (φ.s (W := W))).op ≫ (L.map (φ.f (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
Tactic: dsimp [map, RightFraction.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
X Y : C
φ : W.LeftFraction X Y
L : Functor.{v_1, v_2, u_1, u_2} C D
hL : W.IsInvertedBy L
⊢ Eq.{v_2 + 1} (α := Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    ((inv (L.map (φ.s (W := W)))).op ≫ (L.map (φ.f (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
    (inv (L.map (φ.s (W := W))).op ≫ (L.map (φ.f (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
have rw : Eq.{v_2 + 1} (α := Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
  (inv (L.map (φ.s (W := W))).op ≫ (L.map (φ.f (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
  (inv (L.map (φ.s (W := W))).op ≫ (L.map (φ.f (W := W))).op : Opposite.op (L.obj Y) ⟶ Opposite.op (L.obj X))
Tactic: rw [op_inv]
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
h : W.HasLeftCalculusOfFractions
X Y : Cᵒᵖ
φ : LeftFraction.{v_1, u_1} W.op X Y
⊢ ∃ (ψ : RightFraction.{v_1, u_1} W.op X Y), ψ.s (W := W.op) ≫ φ.f (W := W.op) = ψ.f (W := W.op) ≫ φ.s (W := W.op)
have obtain : ∀ (ψ : W.LeftFraction (Opposite.unop Y) (Opposite.unop X))
  (eq : φ.unop (W := W.op).f (W := W) ≫ ψ.s (W := W) = φ.unop (W := W.op).s (W := W) ≫ ψ.f (W := W)),
  ∃ (ψ : RightFraction.{v_1, u_1} W.op X Y), ψ.s (W := W.op) ≫ φ.f (W := W.op) = ψ.f (W := W.op) ≫ φ.s (W := W.op)
Tactic: obtain ⟨ψ, eq⟩ := h.exists_leftFraction φ.unop
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
h : W.HasLeftCalculusOfFractions
X Y Y' : Cᵒᵖ
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : W.op s
eq : f₁ ≫ s = f₂ ≫ s
⊢ ∃ (X' : Cᵒᵖ) (t : X' ⟶ X) (_ : W.op t), t ≫ f₁ = t ≫ f₂
have obtain : ∀ (X' : C) (t : Opposite.unop X ⟶ X') (ht : W t) (fac : f₁.unop ≫ t = f₂.unop ≫ t),
  ∃ (X' : Cᵒᵖ) (t : X' ⟶ X) (_ : W.op t), t ≫ f₁ = t ≫ f₂
Tactic: obtain ⟨X', t, ht, fac⟩ := h.ext f₁.unop f₂.unop s.unop hs (Quiver.Hom.op_inj eq)
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
h : W.HasRightCalculusOfFractions
X Y : Cᵒᵖ
φ : RightFraction.{v_1, u_1} W.op X Y
⊢ ∃ (ψ : LeftFraction.{v_1, u_1} W.op X Y), φ.f (W := W.op) ≫ ψ.s (W := W.op) = φ.s (W := W.op) ≫ ψ.f (W := W.op)
have obtain : ∀ (ψ : W.RightFraction (Opposite.unop Y) (Opposite.unop X))
  (eq : ψ.s (W := W) ≫ φ.unop (W := W.op).f (W := W) = ψ.f (W := W) ≫ φ.unop (W := W.op).s (W := W)),
  ∃ (ψ : LeftFraction.{v_1, u_1} W.op X Y), φ.f (W := W.op) ≫ ψ.s (W := W.op) = φ.s (W := W.op) ≫ ψ.f (W := W.op)
Tactic: obtain ⟨ψ, eq⟩ := h.exists_rightFraction φ.unop
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
h : W.HasRightCalculusOfFractions
X' X Y : Cᵒᵖ
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : W.op s
eq : s ≫ f₁ = s ≫ f₂
⊢ ∃ (Y' : Cᵒᵖ) (t : Y ⟶ Y') (_ : W.op t), f₁ ≫ t = f₂ ≫ t
have obtain : ∀ (Y' : C) (t : Y' ⟶ Opposite.unop Y) (ht : W t) (fac : t ≫ f₁.unop = t ≫ f₂.unop),
  ∃ (Y' : Cᵒᵖ) (t : Y ⟶ Y') (_ : W.op t), f₁ ≫ t = f₂ ≫ t
Tactic: obtain ⟨Y', t, ht, fac⟩ := h.ext f₁.unop f₂.unop s.unop hs (Quiver.Hom.op_inj eq)
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasLeftCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X Y : C
φ : W.unop.LeftFraction X Y
⊢ ∃ (ψ : W.unop.RightFraction X Y), ψ.s (W := W.unop) ≫ φ.f (W := W.unop) = ψ.f (W := W.unop) ≫ φ.s (W := W.unop)
have obtain : ∀ (ψ : LeftFraction.{v_1, u_1} W (Opposite.op Y) (Opposite.op X))
  (eq : φ.op (W := W.unop).f (W := W) ≫ ψ.s (W := W) = φ.op (W := W.unop).s (W := W) ≫ ψ.f (W := W)),
  ∃ (ψ : W.unop.RightFraction X Y), ψ.s (W := W.unop) ≫ φ.f (W := W.unop) = ψ.f (W := W.unop) ≫ φ.s (W := W.unop)
Tactic: obtain ⟨ψ, eq⟩ := h.exists_leftFraction φ.op
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasLeftCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X Y Y' : C
f₁ f₂ : X ⟶ Y
s : Y ⟶ Y'
hs : W.unop s
eq : f₁ ≫ s = f₂ ≫ s
⊢ ∃ (X' : C) (t : X' ⟶ X) (_ : W.unop t), t ≫ f₁ = t ≫ f₂
have obtain : ∀ (X' : Cᵒᵖ) (t : Opposite.op X ⟶ X') (ht : W t) (fac : Eq (α := Opposite.op Y ⟶ X') (f₁.op ≫ t) (f₂.op ≫ t)),
  ∃ (X' : C) (t : X' ⟶ X) (_ : W.unop t), t ≫ f₁ = t ≫ f₂
Tactic: obtain ⟨X', t, ht, fac⟩ := h.ext f₁.op f₂.op s.op hs (Quiver.Hom.unop_inj eq)
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasRightCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X Y : C
φ : W.unop.RightFraction X Y
⊢ ∃ (ψ : W.unop.LeftFraction X Y), φ.f (W := W.unop) ≫ ψ.s (W := W.unop) = φ.s (W := W.unop) ≫ ψ.f (W := W.unop)
have obtain : ∀ (ψ : RightFraction.{v_1, u_1} W (Opposite.op Y) (Opposite.op X))
  (eq : ψ.s (W := W) ≫ φ.op (W := W.unop).f (W := W) = ψ.f (W := W) ≫ φ.op (W := W.unop).s (W := W)),
  ∃ (ψ : W.unop.LeftFraction X Y), φ.f (W := W.unop) ≫ ψ.s (W := W.unop) = φ.s (W := W.unop) ≫ ψ.f (W := W.unop)
Tactic: obtain ⟨ψ, eq⟩ := h.exists_rightFraction φ.op
-- 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
L : Functor.{v_1, v_2, u_1, u_2} C D
W_1 : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W_1
W : MorphismProperty.{v_1, u_1} Cᵒᵖ
h : HasRightCalculusOfFractions.{v_1, u_1} (C := Cᵒᵖ) W
X' X Y : C
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : W.unop s
eq : s ≫ f₁ = s ≫ f₂
⊢ ∃ (Y' : C) (t : Y ⟶ Y') (_ : W.unop t), f₁ ≫ t = f₂ ≫ t
have obtain : ∀ (Y' : Cᵒᵖ) (t : Y' ⟶ Opposite.op Y) (ht : W t) (fac : t ≫ f₁.op = t ≫ f₂.op),
  ∃ (Y' : C) (t : Y ⟶ Y') (_ : W.unop t), f₁ ≫ t = f₂ ≫ t
Tactic: obtain ⟨Y', t, ht, fac⟩ := h.ext f₁.op f₂.op s.op hs (Quiver.Hom.unop_inj eq)
-- 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
X Y : C
z₁ z₂ : W.RightFraction X Y
h : RightFractionRel (W := W) z₁ z₂
⊢ LeftFractionRel (W := W.op) (z₁.op (W := W)) (z₂.op (W := W))
have obtain : ∀ (Z : C) (t₁ : Z ⟶ z₁.X' (W := W)) (t₂ : Z ⟶ z₂.X' (W := W)) (hs : t₁ ≫ z₁.s (W := W) = t₂ ≫ z₂.s (W := W))
  (hf : t₁ ≫ z₁.f (W := W) = t₂ ≫ z₂.f (W := W)) (ht : W (t₁ ≫ z₁.s (W := W))),
  LeftFractionRel (W := W.op) (z₁.op (W := W)) (z₂.op (W := W))
Tactic: obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h
Cleared hypotheses: 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ᵒᵖ
X Y : Cᵒᵖ
z₁ z₂ : RightFraction.{v_1, u_1} W X Y
h : RightFractionRel (W := W) z₁ z₂
⊢ LeftFractionRel (W := W.unop) (z₁.unop (W := W)) (z₂.unop (W := W))
have obtain : ∀ (Z : Cᵒᵖ) (t₁ : Z ⟶ z₁.X' (W := W)) (t₂ : Z ⟶ z₂.X' (W := W)) (hs : t₁ ≫ z₁.s (W := W) = t₂ ≫ z₂.s (W := W))
  (hf : t₁ ≫ z₁.f (W := W) = t₂ ≫ z₂.f (W := W)) (ht : W (t₁ ≫ z₁.s (W := W))),
  LeftFractionRel (W := W.unop) (z₁.unop (W := W)) (z₂.unop (W := W))
Tactic: obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h
Cleared hypotheses: 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
X Y : C
z₁ z₂ : W.LeftFraction X Y
h : LeftFractionRel (W := W) z₁ z₂
⊢ RightFractionRel (W := W.op) (z₁.op (W := W)) (z₂.op (W := W))
have obtain : ∀ (Z : C) (t₁ : z₁.Y' (W := W) ⟶ Z) (t₂ : z₂.Y' (W := W) ⟶ Z) (hs : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂)
  (hf : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂) (ht : W (z₁.s (W := W) ≫ t₁)),
  RightFractionRel (W := W.op) (z₁.op (W := W)) (z₂.op (W := W))
Tactic: obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h
Cleared hypotheses: 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ᵒᵖ
X Y : Cᵒᵖ
z₁ z₂ : LeftFraction.{v_1, u_1} W X Y
h : LeftFractionRel (W := W) z₁ z₂
⊢ RightFractionRel (W := W.unop) (z₁.unop (W := W)) (z₂.unop (W := W))
have obtain : ∀ (Z : Cᵒᵖ) (t₁ : z₁.Y' (W := W) ⟶ Z) (t₂ : z₂.Y' (W := W) ⟶ Z) (hs : z₁.s (W := W) ≫ t₁ = z₂.s (W := W) ≫ t₂)
  (hf : z₁.f (W := W) ≫ t₁ = z₂.f (W := W) ≫ t₂) (ht : W (z₁.s (W := W) ≫ t₁)),
  RightFractionRel (W := W.unop) (z₁.unop (W := W)) (z₂.unop (W := W))
Tactic: obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h
Cleared hypotheses: 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
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.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ ∃ (φ : W.RightFraction X Y), f = φ.map (W := W) L ⋯
have obtain : ∀ (φ : MorphismProperty.LeftFraction.{v_1, u_1} W.op (Opposite.op Y) (Opposite.op X))
  (eq : f.op = φ.map (W := W.op) L.op sorry), ∃ (φ : W.RightFraction X Y), f = φ.map (W := W) L sorry
Tactic: obtain ⟨φ, eq⟩ := Localization.exists_leftFraction L.op W.op f.op
-- 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
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.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : MorphismProperty.LeftFraction.{v_1, u_1} W.op (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map (W := W.op) L.op ⋯
⊢ ∃ (φ : W.RightFraction X Y), f = φ.map (W := W) L ⋯
have refine : f.op = (φ.unop (W := W.op).map (W := W) L sorry).op
Tactic: refine ⟨φ.unop, Quiver.Hom.op_inj ?_⟩
-- 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
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.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : MorphismProperty.LeftFraction.{v_1, u_1} W.op (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map (W := W.op) L.op ⋯
⊢ f.op = (φ.unop (W := W.op).map (W := W) L ⋯).op
have rw : φ.map (W := W.op) L.op sorry = φ.unop (W := W.op).op (W := W).map (W := W.op) L.op sorry
Tactic: rw [eq, MorphismProperty.RightFraction.op_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
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.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯ ↔ RightFractionRel (W := W) φ ψ
have rw : φ.map (W := W) L sorry = ψ.map (W := W) L sorry ↔ (φ.map (W := W) L sorry).op = (ψ.map (W := W) L sorry).op
Tactic: rw [← leftFractionRel_op_iff, ← LeftFraction.map_eq_iff L.op W.op φ.op ψ.op,
    ← φ.op_map L (Localization.inverts _ _), ← ψ.op_map L (Localization.inverts _ _)]
-- 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
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.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯ ↔ (φ.map (W := W) L ⋯).op = (ψ.map (W := W) L ⋯).op
have mp : φ.map (W := W) L sorry = ψ.map (W := W) L sorry → (φ.map (W := W) L sorry).op = (ψ.map (W := W) L sorry).op
Tactic: constructor
-- 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
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.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
mp : φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯ → (φ.map (W := W) L ⋯).op = (ψ.map (W := W) L ⋯).op
⊢ φ.map (W := W) L ⋯ = ψ.map (W := W) L ⋯ ↔ (φ.map (W := W) L ⋯).op = (ψ.map (W := W) L ⋯).op
have mpr : (φ.map (W := W) L sorry).op = (ψ.map (W := W) L sorry).op → φ.map (W := W) L sorry = ψ.map (W := W) L sorry
Tactic: constructor
-- 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
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.HasRightCalculusOfFractions
Y Z : C
f₁ f₂ : Y ⟶ Z
⊢ L.map f₁ = L.map f₂ ↔ ∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂
have mp : L.map f₁ = L.map f₂ → ∃ (X : C) (s : X ⟶ Y) (_ : W s), s ≫ f₁ = s ≫ f₂
Tactic: constructor