ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddGroup A<VAR>CategoryTheory.HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : A<GOAL>(CategoryTheory.shiftFunctor C i).map ((CategoryTheory.shiftFunctor C (-i)).map f) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C (-i) i ⋯).hom.app X) (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctorCompIsoId C (-i) i ⋯).inv.app Y))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddGroup A<VAR>CategoryTheory.HasShift C A<VAR>n : A<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map (CategoryTheory.shiftShiftNeg X n).inv) (CategoryTheory.shiftNegShift ((CategoryTheory.shiftFunctor C n).obj X) n).hom = CategoryTheory.CategoryStruct.id ((CategoryTheory.shiftFunctor C n).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddGroup A<VAR>CategoryTheory.HasShift C A<VAR>n m : A<VAR>h : n + m = 0<VAR>X : C<GOAL>(CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C n m h).hom.app X) = (CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app ((CategoryTheory.shiftFunctor C n).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddGroup A<VAR>CategoryTheory.HasShift C A<VAR>n m : A<VAR>h : n + m = 0<VAR>X : C<GOAL>(CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C n m h).inv.app X) = (CategoryTheory.shiftFunctorCompIsoId C m n ⋯).inv.app ((CategoryTheory.shiftFunctor C n).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddGroup A<VAR>CategoryTheory.HasShift C A<VAR>n : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).hom.app X) = (CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).hom.app ((CategoryTheory.shiftFunctor C n).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddGroup A<VAR>CategoryTheory.HasShift C A<VAR>n : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).inv.app X) = (CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).inv.app ((CategoryTheory.shiftFunctor C n).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddGroup A<VAR>CategoryTheory.HasShift C A<VAR>n : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctor C (-n)).map ((CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).hom.app X) = (CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).hom.app ((CategoryTheory.shiftFunctor C (-n)).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddGroup A<VAR>CategoryTheory.HasShift C A<VAR>n : A<VAR>X : C<GOAL>(CategoryTheory.shiftFunctor C (-n)).map ((CategoryTheory.shiftFunctorCompIsoId C (-n) n ⋯).inv.app X) = (CategoryTheory.shiftFunctorCompIsoId C n (-n) ⋯).inv.app ((CategoryTheory.shiftFunctor C (-n)).obj X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddGroup A<VAR>CategoryTheory.HasShift C A<VAR>CategoryTheory.Limits.HasZeroMorphisms C<VAR>X Y : C<VAR>n : A<GOAL>(CategoryTheory.shiftFunctor C n).map 0 = 0
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddCommMonoid A<VAR>CategoryTheory.HasShift C A<VAR>i j k : A<VAR>h : i + j = k<GOAL>CategoryTheory.shiftFunctorComm C i j = (CategoryTheory.shiftFunctorAdd' C i j k h).symm ≪≫ CategoryTheory.shiftFunctorAdd' C j i k ⋯
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddCommMonoid A<VAR>CategoryTheory.HasShift C A<VAR>i : A<GOAL>CategoryTheory.shiftFunctorComm C i i = CategoryTheory.Iso.refl ((CategoryTheory.shiftFunctor C i).comp (CategoryTheory.shiftFunctor C i))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddCommMonoid A<VAR>CategoryTheory.HasShift C A<VAR>i j : A<GOAL>(CategoryTheory.shiftFunctorComm C i j).symm = CategoryTheory.shiftFunctorComm C j i
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddCommMonoid A<VAR>CategoryTheory.HasShift C A<VAR>X : C<VAR>i j : A<GOAL>(CategoryTheory.shiftComm X i j).symm = CategoryTheory.shiftComm X j i
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddCommMonoid A<VAR>CategoryTheory.HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i j : A<GOAL>(CategoryTheory.shiftFunctor C j).map ((CategoryTheory.shiftFunctor C i).map f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm X i j).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C i).map ((CategoryTheory.shiftFunctor C j).map f)) (CategoryTheory.shiftComm Y j i).hom)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddCommMonoid A<VAR>CategoryTheory.HasShift C A<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i j : A<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm X i j).hom ((CategoryTheory.shiftFunctor C i).map ((CategoryTheory.shiftFunctor C j).map f)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C j).map ((CategoryTheory.shiftFunctor C i).map f)) (CategoryTheory.shiftComm Y i j).hom
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddCommMonoid A<VAR>CategoryTheory.HasShift C A<VAR>X : C<VAR>n : A<GOAL>(CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C n).obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C n 0).hom.app X) ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorZero C A).hom.app X))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddCommMonoid A<VAR>CategoryTheory.HasShift C A<VAR>X : C<VAR>n : A<GOAL>(CategoryTheory.shiftFunctorZero C A).inv.app ((CategoryTheory.shiftFunctor C n).obj X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorZero C A).inv.app X)) ((CategoryTheory.shiftFunctorComm C n 0).inv.app X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddCommMonoid A<VAR>CategoryTheory.HasShift C A<VAR>X : C<VAR>a : A<GOAL>(CategoryTheory.shiftFunctorComm C a 0).hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C a).obj X)) ((CategoryTheory.shiftFunctor C a).map ((CategoryTheory.shiftFunctorZero C A).inv.app X))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>AddCommMonoid A<VAR>CategoryTheory.HasShift C A<VAR>m₁ m₂ m₃ : A<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X) ((CategoryTheory.shiftFunctor C m₁).map ((CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C m₂ m₃).hom.app ((CategoryTheory.shiftFunctor C m₁).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C m₃).map ((CategoryTheory.shiftFunctorComm C m₁ m₂).hom.app X)) ((CategoryTheory.shiftFunctorComm C m₁ m₃).hom.app ((CategoryTheory.shiftFunctor C m₂).obj X)))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>s : A → CategoryTheory.Functor C C<VAR>i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)<VAR>X : C<GOAL>F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.zero hF s i).hom.app X) = CategoryTheory.CategoryStruct.comp ((i 0).hom.app X) ((CategoryTheory.shiftFunctorZero D A).hom.app (F.obj X))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>s : A → CategoryTheory.Functor C C<VAR>i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)<VAR>X : C<GOAL>F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.zero hF s i).inv.app X) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero D A).inv.app (F.obj X)) ((i 0).inv.app X)
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>s : A → CategoryTheory.Functor C C<VAR>i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)<VAR>a b : A<VAR>X : C<GOAL>F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.add hF s i a b).hom.app X) = CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).hom.app (F.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((i a).inv.app X)) ((i b).inv.app ((s a).obj X))))
<VAR>C : Type u<VAR>A : Type u_1<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_2} D<VAR>AddMonoid A<VAR>CategoryTheory.HasShift D A<VAR>F : CategoryTheory.Functor C D<VAR>hF : F.FullyFaithful<VAR>s : A → CategoryTheory.Functor C C<VAR>i : (i : A) → (s i).comp F ≅ F.comp (CategoryTheory.shiftFunctor D i)<VAR>a b : A<VAR>X : C<GOAL>F.map ((CategoryTheory.Functor.FullyFaithful.hasShift.add hF s i a b).inv.app X) = CategoryTheory.CategoryStruct.comp ((i b).hom.app ((s a).obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D b).map ((i a).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd D a b).inv.app (F.obj X)) ((i (a + b)).inv.app X)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : CategoryTheory.Limits.Fan fun i => f i.succ<VAR>c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt<VAR>X : CategoryTheory.Discrete (Fin (n + 1))<GOAL>(CategoryTheory.extendFan c₁ c₂).π.app X = Fin.cases c₂.fst (fun i => c₂.snd ≫ c₁.π.app { as := i }) X.as
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : CategoryTheory.Limits.Fan fun i => f i.succ<VAR>c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt<GOAL>(CategoryTheory.extendFan c₁ c₂).pt = c₂.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>CategoryTheory.Limits.HasTerminal C<VAR>n : ℕ<VAR>f : Fin n → C<GOAL>CategoryTheory.Limits.HasProduct f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryProducts C<VAR>CategoryTheory.Limits.HasTerminal C<GOAL>CategoryTheory.Limits.HasFiniteProducts C
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ<VAR>c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt<VAR>X : CategoryTheory.Discrete (Fin (n + 1))<GOAL>(CategoryTheory.extendCofan c₁ c₂).ι.app X = Fin.cases c₂.inl (fun i => c₁.ι.app { as := i } ≫ c₂.inr) X.as
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : CategoryTheory.Limits.Cofan fun i => f i.succ<VAR>c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt<GOAL>(CategoryTheory.extendCofan c₁ c₂).pt = c₂.pt
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>CategoryTheory.Limits.HasInitial C<VAR>n : ℕ<VAR>f : Fin n → C<GOAL>CategoryTheory.Limits.HasCoproduct f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasBinaryCoproducts C<VAR>CategoryTheory.Limits.HasInitial C<GOAL>CategoryTheory.Limits.HasFiniteCoproducts C
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>self : W.LeftFraction X Y<GOAL>W self.s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>W.ContainsIdentities<GOAL>(CategoryTheory.MorphismProperty.LeftFraction.ofHom W f).Y' = Y
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>W.ContainsIdentities<GOAL>(CategoryTheory.MorphismProperty.LeftFraction.ofHom W f).s = CategoryTheory.CategoryStruct.id Y
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>W.ContainsIdentities<GOAL>(CategoryTheory.MorphismProperty.LeftFraction.ofHom W f).f = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>s : Y ⟶ X<VAR>hs : W s<GOAL>(CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).Y' = X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>s : Y ⟶ X<VAR>hs : W s<GOAL>(CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).s = s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>s : Y ⟶ X<VAR>hs : W s<GOAL>(CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).f = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<VAR>L : CategoryTheory.Functor C D<VAR>hL : W.IsInvertedBy L<GOAL>CategoryTheory.CategoryStruct.comp (φ.map L hL) (L.map φ.s) = L.map φ.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>L : CategoryTheory.Functor C D<VAR>hL : W.IsInvertedBy L<VAR>W.ContainsIdentities<GOAL>(CategoryTheory.MorphismProperty.LeftFraction.ofHom W f).map L hL = L.map f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>s : Y ⟶ X<VAR>hs : W s<VAR>L : CategoryTheory.Functor C D<VAR>hL : W.IsInvertedBy L<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).map L hL) (L.map s) = CategoryTheory.CategoryStruct.id (L.obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>s : Y ⟶ X<VAR>hs : W s<VAR>L : CategoryTheory.Functor C D<VAR>hL : W.IsInvertedBy L<GOAL>CategoryTheory.CategoryStruct.comp (L.map s) ((CategoryTheory.MorphismProperty.LeftFraction.ofInv s hs).map L hL) = CategoryTheory.CategoryStruct.id (L.obj Y)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>α : W.LeftFraction X Y<GOAL>∃ Y' f s, ∃ (hs : W s), α = CategoryTheory.MorphismProperty.LeftFraction.mk f s hs
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>self : W.RightFraction X Y<GOAL>W self.s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>W.ContainsIdentities<GOAL>(CategoryTheory.MorphismProperty.RightFraction.ofHom W f).X' = X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>W.ContainsIdentities<GOAL>(CategoryTheory.MorphismProperty.RightFraction.ofHom W f).f = f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>W.ContainsIdentities<GOAL>(CategoryTheory.MorphismProperty.RightFraction.ofHom W f).s = CategoryTheory.CategoryStruct.id X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>s : Y ⟶ X<VAR>hs : W s<GOAL>(CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).s = s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>s : Y ⟶ X<VAR>hs : W s<GOAL>(CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).X' = Y
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>s : Y ⟶ X<VAR>hs : W s<GOAL>(CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).f = CategoryTheory.CategoryStruct.id Y
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>φ : W.RightFraction X Y<VAR>L : CategoryTheory.Functor C D<VAR>hL : W.IsInvertedBy L<GOAL>CategoryTheory.CategoryStruct.comp (L.map φ.s) (φ.map L hL) = L.map φ.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>L : CategoryTheory.Functor C D<VAR>hL : W.IsInvertedBy L<VAR>W.ContainsIdentities<GOAL>(CategoryTheory.MorphismProperty.RightFraction.ofHom W f).map L hL = L.map f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>s : Y ⟶ X<VAR>hs : W s<VAR>L : CategoryTheory.Functor C D<VAR>hL : W.IsInvertedBy L<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).map L hL) (L.map s) = CategoryTheory.CategoryStruct.id (L.obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>CategoryTheory.Category.{u_4, u_2} D<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>s : Y ⟶ X<VAR>hs : W s<VAR>L : CategoryTheory.Functor C D<VAR>hL : W.IsInvertedBy L<GOAL>CategoryTheory.CategoryStruct.comp (L.map s) ((CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).map L hL) = CategoryTheory.CategoryStruct.id (L.obj Y)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>α : W.RightFraction X Y<GOAL>∃ X' s, ∃ (hs : W s), ∃ f, α = CategoryTheory.MorphismProperty.RightFraction.mk s hs f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>self : W.HasLeftCalculusOfFractions<VAR>X' X Y : C<VAR>f₁ f₂ : X ⟶ Y<VAR>s : X' ⟶ X<GOAL>W s → CategoryTheory.CategoryStruct.comp s f₁ = CategoryTheory.CategoryStruct.comp s f₂ → ∃ Y' t, ∃ (_ : W t), CategoryTheory.CategoryStruct.comp f₁ t = CategoryTheory.CategoryStruct.comp f₂ t
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>self : W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>φ : W.RightFraction X Y<GOAL>∃ ψ, CategoryTheory.CategoryStruct.comp φ.f ψ.s = CategoryTheory.CategoryStruct.comp φ.s ψ.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>self : W.HasRightCalculusOfFractions<VAR>X Y Y' : C<VAR>f₁ f₂ : X ⟶ Y<VAR>s : Y ⟶ Y'<GOAL>W s → CategoryTheory.CategoryStruct.comp f₁ s = CategoryTheory.CategoryStruct.comp f₂ s → ∃ X' t, ∃ (_ : W t), CategoryTheory.CategoryStruct.comp t f₁ = CategoryTheory.CategoryStruct.comp t f₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>self : W.HasRightCalculusOfFractions<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<GOAL>∃ ψ, CategoryTheory.CategoryStruct.comp ψ.s φ.f = CategoryTheory.CategoryStruct.comp ψ.f φ.s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>φ : W.RightFraction X Y<GOAL>∃ ψ, CategoryTheory.CategoryStruct.comp φ.f ψ.s = CategoryTheory.CategoryStruct.comp φ.s ψ.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>φ : W.RightFraction X Y<GOAL>CategoryTheory.CategoryStruct.comp φ.f φ.leftFraction.s = CategoryTheory.CategoryStruct.comp φ.s φ.leftFraction.f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasRightCalculusOfFractions<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<GOAL>∃ ψ, CategoryTheory.CategoryStruct.comp ψ.s φ.f = CategoryTheory.CategoryStruct.comp ψ.f φ.s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasRightCalculusOfFractions<VAR>X Y : C<VAR>φ : W.LeftFraction X Y<GOAL>CategoryTheory.CategoryStruct.comp φ.rightFraction.s φ.f = CategoryTheory.CategoryStruct.comp φ.rightFraction.f φ.s
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>z : W.LeftFraction X Y<GOAL>CategoryTheory.MorphismProperty.LeftFractionRel z z
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ : W.LeftFraction X Y<VAR>h : CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂<GOAL>CategoryTheory.MorphismProperty.LeftFractionRel z₂ z₁
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>z₁ z₂ z₃ : W.LeftFraction X Y<VAR>W.HasLeftCalculusOfFractions<VAR>h₁₂ : CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂<VAR>h₂₃ : CategoryTheory.MorphismProperty.LeftFractionRel z₂ z₃<GOAL>CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₃
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<GOAL>Equivalence CategoryTheory.MorphismProperty.LeftFractionRel
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>z₁ : W.LeftFraction X Y<VAR>z₂ : W.LeftFraction Y Z<VAR>z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'<VAR>h₃ : CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f<VAR>h₃' : CategoryTheory.CategoryStruct.comp z₂.f z₃'.s = CategoryTheory.CategoryStruct.comp z₁.s z₃'.f<GOAL>CategoryTheory.MorphismProperty.LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>X Y : C<VAR>f : CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom W X Y<GOAL>∃ z, f = CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk z
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>z₁ : W.LeftFraction X Y<VAR>z₂ : W.LeftFraction Y Z<VAR>z₃ : W.LeftFraction z₁.Y' z₂.Y'<VAR>h₃ : CategoryTheory.CategoryStruct.comp z₂.f z₃.s = CategoryTheory.CategoryStruct.comp z₁.s z₃.f<GOAL>z₁.comp z₂ = CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk (z₁.comp₀ z₂ z₃)
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>z₁ : W.LeftFraction X Y<VAR>z₂ : W.LeftFraction Y Z<GOAL>(CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk z₁).comp (CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk z₂) = z₁.comp z₂
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X : C<GOAL>(CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).obj X = X
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f : W.LeftFraction X Y<GOAL>CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk f = CategoryTheory.MorphismProperty.LeftFraction.Localization.Hom.mk f
<VAR>C : Type u_1<VAR>CategoryTheory.Category.{u_3, u_1} C<VAR>W : CategoryTheory.MorphismProperty C<VAR>W.HasLeftCalculusOfFractions<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map f = CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk (CategoryTheory.MorphismProperty.LeftFraction.ofHom W f)