ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>S : CategoryTheory.Functor C D<VAR>T : D<VAR>CategoryTheory.Limits.HasColimits C<VAR>CategoryTheory.Limits.PreservesColimits S<VAR>A : CategoryTheory.CostructuredArrow S T<VAR>P : (CategoryTheory.CostructuredArrow S T)ᵒᵖ<VAR>f : P ⟶ Opposite.op A<VAR>CategoryTheory.Mono f<GOAL>CategoryTheory.CostructuredArrow.projectQuotient (CategoryTheory.Subobject.mk f) = CategoryTheory.Subobject.mk f.unop.left.op
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>S : CategoryTheory.Functor C D<VAR>T : D<VAR>CategoryTheory.Limits.HasColimits C<VAR>CategoryTheory.Limits.PreservesColimits S<VAR>A : CategoryTheory.CostructuredArrow S T<VAR>P : CategoryTheory.Subobject (Opposite.op A)<GOAL>∃ q, CategoryTheory.CategoryStruct.comp (S.map (CategoryTheory.CostructuredArrow.projectQuotient P).arrow.unop) q = A.hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>S : CategoryTheory.Functor C D<VAR>T : D<VAR>A : CategoryTheory.CostructuredArrow S T<VAR>P : (CategoryTheory.CostructuredArrow S T)ᵒᵖ<VAR>f : P ⟶ Opposite.op A<VAR>CategoryTheory.Mono f.unop.left.op<GOAL>CategoryTheory.CategoryStruct.comp f.unop.left (CategoryTheory.Subobject.underlyingIso f.unop.left.op).hom.unop = (CategoryTheory.Subobject.mk f.unop.left.op).arrow.unop
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>S : CategoryTheory.Functor C D<VAR>T : D<VAR>CategoryTheory.Limits.HasColimits C<VAR>CategoryTheory.Limits.PreservesColimits S<VAR>A : CategoryTheory.CostructuredArrow S T<VAR>P : CategoryTheory.Subobject (Opposite.op A)<VAR>q : S.obj (Opposite.unop (CategoryTheory.Subobject.underlying.obj (CategoryTheory.CostructuredArrow.projectQuotient P))) ⟶ (CategoryTheory.Functor.fromPUnit T).obj A.right<VAR>hq : CategoryTheory.CategoryStruct.comp (S.map (CategoryTheory.CostructuredArrow.projectQuotient P).arrow.unop) q = A.hom<GOAL>CategoryTheory.CostructuredArrow.liftQuotient (CategoryTheory.CostructuredArrow.projectQuotient P) hq = P
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v, u₁} C<VAR>D : Type u₂<VAR>CategoryTheory.Category.{v, u₂} D<VAR>S : CategoryTheory.Functor C D<VAR>T : D<VAR>A : CategoryTheory.CostructuredArrow S T<VAR>P Q : (CategoryTheory.CostructuredArrow S T)ᵒᵖ<VAR>f : P ⟶ Opposite.op A<VAR>g : Q ⟶ Opposite.op A<VAR>CategoryTheory.Mono f.unop.left.op<VAR>CategoryTheory.Mono g.unop.left.op<VAR>h : CategoryTheory.Subobject.mk f.unop.left.op ≤ CategoryTheory.Subobject.mk g.unop.left.op<GOAL>CategoryTheory.CategoryStruct.comp g.unop.left (CategoryTheory.Subobject.ofMkLEMk f.unop.left.op g.unop.left.op h).unop = f.unop.left
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id A) ((CategoryTheory.exp.coev A).app B)) ((CategoryTheory.exp.ev A).app (A ⨯ B)) = CategoryTheory.CategoryStruct.id (A ⨯ B)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp.coev A).app (A ⟹ B)) ((CategoryTheory.exp A).map ((CategoryTheory.exp.ev A).app B)) = CategoryTheory.CategoryStruct.id (A ⟹ B)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A X Y : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>f : A ⨯ Y ⟶ X<GOAL>((CategoryTheory.exp.adjunction A).homEquiv Y X) f = CategoryTheory.CartesianClosed.curry f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A X Y : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>f : Y ⟶ A ⟹ X<GOAL>((CategoryTheory.exp.adjunction A).homEquiv Y X).symm f = CategoryTheory.CartesianClosed.uncurry f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A X X' Y : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>f : X ⟶ X'<VAR>g : A ⨯ X' ⟶ Y<GOAL>CategoryTheory.CartesianClosed.curry (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id A) f) g) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CartesianClosed.curry g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A X Y Y' : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>f : A ⨯ X ⟶ Y<VAR>g : Y ⟶ Y'<GOAL>CategoryTheory.CartesianClosed.curry (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianClosed.curry f) ((CategoryTheory.exp A).map g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A X Y Y' : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>f : X ⟶ A ⟹ Y<VAR>g : Y ⟶ Y'<GOAL>CategoryTheory.CartesianClosed.uncurry (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.exp A).map g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianClosed.uncurry f) g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A X X' Y : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>f : X ⟶ X'<VAR>g : X' ⟶ A ⟹ Y<GOAL>CategoryTheory.CartesianClosed.uncurry (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id A) f) (CategoryTheory.CartesianClosed.uncurry g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A X Y : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>f : A ⨯ X ⟶ Y<GOAL>CategoryTheory.CartesianClosed.uncurry (CategoryTheory.CartesianClosed.curry f) = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A X Y : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>f : X ⟶ A ⟹ Y<GOAL>CategoryTheory.CartesianClosed.curry (CategoryTheory.CartesianClosed.uncurry f) = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A X Y : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>f : A ⨯ Y ⟶ X<VAR>g : Y ⟶ A ⟹ X<GOAL>CategoryTheory.CartesianClosed.curry f = g ↔ f = CategoryTheory.CartesianClosed.uncurry g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A X Y : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>f : A ⨯ Y ⟶ X<VAR>g : Y ⟶ A ⟹ X<GOAL>g = CategoryTheory.CartesianClosed.curry f ↔ CategoryTheory.CartesianClosed.uncurry g = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A X Y : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>g : Y ⟶ A ⟹ X<GOAL>CategoryTheory.CartesianClosed.uncurry g = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id A) g) ((CategoryTheory.exp.ev A).app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A X Y : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>g : A ⨯ Y ⟶ X<GOAL>CategoryTheory.CartesianClosed.curry g = CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp.coev A).app Y) ((CategoryTheory.exp A).map g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>A X : C<VAR>CategoryTheory.Exponentiable A<GOAL>CategoryTheory.CartesianClosed.uncurry (CategoryTheory.CategoryStruct.id (A ⟹ X)) = (CategoryTheory.exp.ev A).app X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>A X : C<VAR>CategoryTheory.Exponentiable A<GOAL>CategoryTheory.CartesianClosed.curry (CategoryTheory.CategoryStruct.id (A ⨯ (CategoryTheory.Functor.id C).obj X)) = (CategoryTheory.exp.coev A).app X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A X Y : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<GOAL>Function.Injective CategoryTheory.CartesianClosed.curry
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A X Y : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<GOAL>Function.Injective CategoryTheory.CartesianClosed.uncurry
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>f : B ⟶ A<VAR>CategoryTheory.Exponentiable B<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id B) ((CategoryTheory.pre f).app X)) ((CategoryTheory.exp.ev B).app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (A ⟹ X))) ((CategoryTheory.exp.ev A).app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>f : B ⟶ A<VAR>CategoryTheory.Exponentiable B<VAR>X : C<GOAL>CategoryTheory.CartesianClosed.uncurry ((CategoryTheory.pre f).app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (A ⟹ X))) ((CategoryTheory.exp.ev A).app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A B X : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>f : B ⟶ A<VAR>CategoryTheory.Exponentiable B<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp.coev A).app X) ((CategoryTheory.pre f).app (A ⨯ X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp.coev B).app X) ((CategoryTheory.exp B).map (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id X)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>A : C<VAR>CategoryTheory.Exponentiable A<GOAL>CategoryTheory.pre (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (CategoryTheory.exp A)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>A₁ A₂ A₃ : C<VAR>CategoryTheory.Exponentiable A₁<VAR>CategoryTheory.Exponentiable A₂<VAR>CategoryTheory.Exponentiable A₃<VAR>f : A₁ ⟶ A₂<VAR>g : A₂ ⟶ A₃<GOAL>CategoryTheory.pre (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.pre g) (CategoryTheory.pre f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>I : C<VAR>t : CategoryTheory.Limits.IsInitial I<GOAL>(CategoryTheory.zeroMul t).inv = t.to (A ⨯ I)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>I : C<VAR>t : CategoryTheory.Limits.IsInitial I<GOAL>(CategoryTheory.zeroMul t).hom = CategoryTheory.Limits.prod.snd
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>A : C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Exponentiable A<VAR>I : C<VAR>t : CategoryTheory.Limits.IsInitial I<VAR>f : A ⟶ I<GOAL>CategoryTheory.IsIso f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>I : C<VAR>B : C<VAR>t : CategoryTheory.Limits.IsInitial I<VAR>CategoryTheory.CartesianClosed C<GOAL>CategoryTheory.Mono (t.to B)
<VAR>F : Type u_1<VAR>Field F<GOAL>IsSolvable (Polynomial.Gal 0)
<VAR>F : Type u_1<VAR>Field F<GOAL>IsSolvable (Polynomial.Gal 1)
<VAR>F : Type u_1<VAR>Field F<VAR>x : F<GOAL>IsSolvable (Polynomial.C x).Gal
<VAR>F : Type u_1<VAR>Field F<GOAL>IsSolvable Polynomial.X.Gal
<VAR>F : Type u_1<VAR>Field F<VAR>x : F<GOAL>IsSolvable (Polynomial.X - Polynomial.C x).Gal
<VAR>F : Type u_1<VAR>Field F<VAR>n : ℕ<GOAL>IsSolvable (Polynomial.X ^ n).Gal
<VAR>F : Type u_1<VAR>Field F<VAR>p q : F[X]<GOAL>IsSolvable p.Gal → IsSolvable q.Gal → IsSolvable (p * q).Gal
<VAR>F : Type u_1<VAR>Field F<VAR>s : Multiset F[X]<VAR>hs : ∀ p ∈ s, IsSolvable p.Gal<GOAL>IsSolvable s.prod.Gal
<VAR>F : Type u_1<VAR>Field F<VAR>p q : F[X]<GOAL>Fact (Polynomial.Splits (algebraMap F q.SplittingField) p) → IsSolvable q.Gal → IsSolvable p.Gal
<VAR>F : Type u_1<VAR>Field F<VAR>p q : F[X]<VAR>hpq : Polynomial.Splits (algebraMap F q.SplittingField) p<VAR>hp : IsSolvable p.Gal<VAR>hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal<GOAL>IsSolvable q.Gal
<VAR>F : Type u_1<VAR>Field F<VAR>n : ℕ<GOAL>IsSolvable (Polynomial.X ^ n - 1).Gal
<VAR>F : Type u_1<VAR>Field F<VAR>n : ℕ<VAR>a : F<VAR>h : Polynomial.Splits (RingHom.id F) (Polynomial.X ^ n - 1)<GOAL>IsSolvable (Polynomial.X ^ n - Polynomial.C a).Gal
<VAR>F : Type u_3<VAR>Field F<VAR>E : Type u_4<VAR>Field E<VAR>i : F →+* E<VAR>n : ℕ<VAR>a : F<VAR>ha : a ≠ 0<VAR>h : Polynomial.Splits i (Polynomial.X ^ n - Polynomial.C a)<GOAL>Polynomial.Splits i (Polynomial.X ^ n - 1)
<VAR>F : Type u_1<VAR>Field F<VAR>n : ℕ<VAR>x : F<GOAL>IsSolvable (Polynomial.X ^ n - Polynomial.C x).Gal
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>P : ↥(solvableByRad F E) → Prop<VAR>base : ∀ (α : F), P ((algebraMap F ↥(solvableByRad F E)) α)<VAR>add : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α + β)<VAR>neg : ∀ (α : ↥(solvableByRad F E)), P α → P (-α)<VAR>mul : ∀ (α β : ↥(solvableByRad F E)), P α → P β → P (α * β)<VAR>inv : ∀ (α : ↥(solvableByRad F E)), P α → P α⁻¹<VAR>rad : ∀ (α : ↥(solvableByRad F E)) (n : ℕ), n ≠ 0 → P (α ^ n) → P α<VAR>α : ↥(solvableByRad F E)<GOAL>P α
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : ↥(solvableByRad F E)<GOAL>IsIntegral F α
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : ↥(solvableByRad F E)<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>hα : solvableByRad.P (α ^ n)<GOAL>solvableByRad.P α
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α β γ : ↥(solvableByRad F E)<VAR>hγ : γ ∈ F⟮α, β⟯<VAR>hα : solvableByRad.P α<VAR>hβ : solvableByRad.P β<GOAL>solvableByRad.P γ
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α β : ↥(solvableByRad F E)<VAR>hβ : β ∈ F⟮α⟯<VAR>hα : solvableByRad.P α<GOAL>solvableByRad.P β
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : ↥(solvableByRad F E)<GOAL>IsSolvable (minpoly F α).Gal
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_2<VAR>Field E<VAR>Algebra F E<VAR>α : E<VAR>q : F[X]<VAR>q_irred : Irreducible q<VAR>q_aeval : (Polynomial.aeval α) q = 0<VAR>hα : IsSolvableByRad F α<GOAL>IsSolvable q.Gal
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>J : CategoryTheory.GrothendieckTopology C<VAR>A : Type u'<VAR>CategoryTheory.Category.{v', u'} A<VAR>CategoryTheory.ConcreteCategory A<VAR>CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization A<VAR>J.WEqualsLocallyBijective A<VAR>CategoryTheory.HasSheafify J A<VAR>J.HasSheafCompose (CategoryTheory.forget A)<VAR>CategoryTheory.Balanced (CategoryTheory.Sheaf J A)<VAR>F G : CategoryTheory.Sheaf J A<VAR>φ : F ⟶ G<GOAL>CategoryTheory.Sheaf.IsLocallySurjective φ ↔ CategoryTheory.Epi φ
<VAR>M : Type u_1<VAR>Monoid M<VAR>X : Type u<VAR>MulAction M X<GOAL>∀ (x : CategoryTheory.SingleObj M), (CategoryTheory.actionAsFunctor M X).obj x = X
<VAR>M : Type u_1<VAR>Monoid M<VAR>X : Type u<VAR>MulAction M X<GOAL>∀ {X_1 Y : CategoryTheory.SingleObj M} (x : X_1 ⟶ Y) (x_1 : X), (CategoryTheory.actionAsFunctor M X).map x x_1 = x • x_1
<VAR>M : Type u_1<VAR>Monoid M<VAR>X : Type u<VAR>MulAction M X<VAR>p q : CategoryTheory.ActionCategory M X<VAR>f : p ⟶ q<GOAL>(CategoryTheory.ActionCategory.π M X).map f = ↑f
<VAR>M : Type u_1<VAR>Monoid M<VAR>X : Type u<VAR>MulAction M X<VAR>p : CategoryTheory.ActionCategory M X<GOAL>(CategoryTheory.ActionCategory.π M X).obj p = CategoryTheory.SingleObj.star M
<VAR>M : Type u_1<VAR>Monoid M<VAR>X : Type u<VAR>MulAction M X<VAR>x : X<GOAL>CategoryTheory.ActionCategory.back ⟨(), x⟩ = x
<VAR>M : Type u_1<VAR>Monoid M<VAR>X : Type u<VAR>MulAction M X<VAR>x : CategoryTheory.ActionCategory M X<GOAL>⟨(), x.back⟩ = x
<VAR>M : Type u_1<VAR>Monoid M<VAR>X : Type u<VAR>MulAction M X<VAR>p q : CategoryTheory.ActionCategory M X<GOAL>(p ⟶ q) = { m // m • p.back = q.back }
<VAR>M : Type u_1<VAR>Monoid M<VAR>X : Type u<VAR>MulAction M X<VAR>x : X<VAR>f : ↥(MulAction.stabilizerSubmonoid M x)<GOAL>(CategoryTheory.ActionCategory.stabilizerIsoEnd M x) f = f
<VAR>M : Type u_1<VAR>Monoid M<VAR>X : Type u<VAR>MulAction M X<VAR>x : X<VAR>f : CategoryTheory.End ⟨(), x⟩<GOAL>(CategoryTheory.ActionCategory.stabilizerIsoEnd M x).symm f = f
<VAR>M : Type u_1<VAR>Monoid M<VAR>X : Type u<VAR>MulAction M X<VAR>x : CategoryTheory.ActionCategory M X<GOAL>↑(CategoryTheory.CategoryStruct.id x) = 1
<VAR>M : Type u_1<VAR>Monoid M<VAR>X : Type u<VAR>MulAction M X<VAR>x y z : CategoryTheory.ActionCategory M X<VAR>f : x ⟶ y<VAR>g : y ⟶ z<GOAL>↑(CategoryTheory.CategoryStruct.comp f g) = ↑g * ↑f
<VAR>X : Type u<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G X<VAR>t : X<VAR>g : G<GOAL>↑(CategoryTheory.ActionCategory.homOfPair t g) = g
<VAR>X : Type u<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G X<VAR>a' b' : CategoryTheory.ActionCategory G X<VAR>f : a' ⟶ b'<GOAL>∃ a b g, ∃ (ha : a' = ⟨(), a⟩) (hb : b' = ⟨(), b⟩) (hg : a = g⁻¹ • b), f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ActionCategory.homOfPair b g) (CategoryTheory.eqToHom ⋯))
<VAR>X : Type u<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G X<VAR>H : Type u_3<VAR>Group H<VAR>F : CategoryTheory.Functor (CategoryTheory.ActionCategory G X) (CategoryTheory.SingleObj H)<VAR>g : G<VAR>b : X<GOAL>((CategoryTheory.ActionCategory.curry F) g).left b = F.map (CategoryTheory.ActionCategory.homOfPair b g)
<VAR>X : Type u<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G X<VAR>H : Type u_3<VAR>Group H<VAR>F : CategoryTheory.Functor (CategoryTheory.ActionCategory G X) (CategoryTheory.SingleObj H)<VAR>g : G<GOAL>((CategoryTheory.ActionCategory.curry F) g).right = g
<VAR>X : Type u<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G X<VAR>H : Type u_3<VAR>Group H<VAR>F : G →* (X → H) ⋊[mulAutArrow] G<VAR>sane : ∀ (g : G), (F g).right = g<GOAL>∀ (x : CategoryTheory.ActionCategory G X), (CategoryTheory.ActionCategory.uncurry F sane).obj x = ()
<VAR>X : Type u<VAR>G : Type u_2<VAR>Group G<VAR>MulAction G X<VAR>H : Type u_3<VAR>Group H<VAR>F : G →* (X → H) ⋊[mulAutArrow] G<VAR>sane : ∀ (g : G), (F g).right = g<GOAL>∀ {x b : CategoryTheory.ActionCategory G X} (f : x ⟶ b), (CategoryTheory.ActionCategory.uncurry F sane).map f = (F ↑f).left b.back
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v, u'} D<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasFiniteProducts D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.CartesianClosed C<VAR>CategoryTheory.CartesianClosed D<VAR>CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<VAR>A B : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id (F.obj A)) ((CategoryTheory.expComparison F A).app B)) ((CategoryTheory.exp.ev (F.obj A)).app (F.obj B)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A (A ⟹ B))) (F.map ((CategoryTheory.exp.ev A).app B))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v, u'} D<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasFiniteProducts D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.CartesianClosed C<VAR>CategoryTheory.CartesianClosed D<VAR>CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<VAR>A B : C<GOAL>CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.exp.coev A).app B)) ((CategoryTheory.expComparison F A).app (A ⨯ B)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.exp.coev (F.obj A)).app (F.obj B)) ((CategoryTheory.exp (F.obj A)).map (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A B)))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v, u'} D<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasFiniteProducts D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.CartesianClosed C<VAR>CategoryTheory.CartesianClosed D<VAR>CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<VAR>A B : C<GOAL>CategoryTheory.CartesianClosed.uncurry ((CategoryTheory.expComparison F A).app B) = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.prodComparison F A (A ⟹ B))) (F.map ((CategoryTheory.exp.ev A).app B))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v, u'} D<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasFiniteProducts D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.CartesianClosed C<VAR>CategoryTheory.CartesianClosed D<VAR>CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<VAR>A A' : C<VAR>f : A' ⟶ A<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.expComparison F A) (CategoryTheory.whiskerLeft F (CategoryTheory.pre (F.map f))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerRight (CategoryTheory.pre f) F) (CategoryTheory.expComparison F A')
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v, u'} D<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasFiniteProducts D<VAR>F : CategoryTheory.Functor C D<VAR>CategoryTheory.CartesianClosed C<VAR>CategoryTheory.CartesianClosed D<VAR>CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<VAR>self : CategoryTheory.CartesianClosedFunctor F<VAR>A : C<GOAL>CategoryTheory.IsIso (CategoryTheory.expComparison F A)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v, u'} D<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasFiniteProducts D<VAR>F : CategoryTheory.Functor C D<VAR>L : CategoryTheory.Functor D C<VAR>CategoryTheory.CartesianClosed C<VAR>CategoryTheory.CartesianClosed D<VAR>CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<GOAL>(CategoryTheory.conjugateEquiv (h.comp (CategoryTheory.exp.adjunction A)) ((CategoryTheory.exp.adjunction (F.obj A)).comp h)) (CategoryTheory.frobeniusMorphism F h A) = CategoryTheory.expComparison F A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v, u'} D<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasFiniteProducts D<VAR>F : CategoryTheory.Functor C D<VAR>L : CategoryTheory.Functor D C<VAR>CategoryTheory.CartesianClosed C<VAR>CategoryTheory.CartesianClosed D<VAR>CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>i : CategoryTheory.IsIso (CategoryTheory.expComparison F A)<GOAL>CategoryTheory.IsIso (CategoryTheory.frobeniusMorphism F h A)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>D : Type u'<VAR>CategoryTheory.Category.{v, u'} D<VAR>CategoryTheory.Limits.HasFiniteProducts C<VAR>CategoryTheory.Limits.HasFiniteProducts D<VAR>F : CategoryTheory.Functor C D<VAR>L : CategoryTheory.Functor D C<VAR>CategoryTheory.CartesianClosed C<VAR>CategoryTheory.CartesianClosed D<VAR>CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>i : CategoryTheory.IsIso (CategoryTheory.frobeniusMorphism F h A)<GOAL>CategoryTheory.IsIso (CategoryTheory.expComparison F A)