ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>a : K<VAR>α : L<VAR>ha : α ^ FiniteDimensional.finrank K L = (algebraMap K L) a<VAR>hα : K⟮α⟯ = ⊤<GOAL>Irreducible (Polynomial.X ^ FiniteDimensional.finrank K L - Polynomial.C a)
<VAR>K : Type u<VAR>Field K<VAR>L : Type u_1<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>hK : (primitiveRoots (FiniteDimensional.finrank K L) K).Nonempty<VAR>a : K<VAR>α : L<VAR>ha : α ^ FiniteDimensional.finrank K L = (algebraMap K L) a<VAR>hα : K⟮α⟯ = ⊤<GOAL>Polynomial.IsSplittingField K L (Polynomial.X ^ FiniteDimensional.finrank K L - Polynomial.C a)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>FiniteDimensional K L<VAR>hK : (primitiveRoots (FiniteDimensional.finrank K L) K).Nonempty<GOAL>[IsGalois K L ∧ IsCyclic (L ≃ₐ[K] L), ∃ a, Irreducible (Polynomial.X ^ FiniteDimensional.finrank K L - Polynomial.C a) ∧ Polynomial.IsSplittingField K L (Polynomial.X ^ FiniteDimensional.finrank K L - Polynomial.C a), ∃ α, α ^ FiniteDimensional.finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤].TFAE
<VAR>C : Type u_2<VAR>CategoryTheory.Category.{u_1, u_2} C<VAR>CategoryTheory.Preadditive C<VAR>r : HomRel C<VAR>CategoryTheory.Congruence r<VAR>hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)<GOAL>(CategoryTheory.Quotient.functor r).Additive
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>Field F<VAR>Field K<VAR>Algebra F K<VAR>self : Normal F K<VAR>x : K<GOAL>Polynomial.Splits (algebraMap F K) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>Field F<VAR>Field K<VAR>Algebra F K<GOAL>Normal F K → ∀ (x : K), IsIntegral F x
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>Field F<VAR>Field K<VAR>Algebra F K<GOAL>Normal F K → ∀ (x : K), Polynomial.Splits (algebraMap F K) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>Field F<VAR>Field K<VAR>Algebra F K<GOAL>Normal F K ↔ ∀ (x : K), IsIntegral F x ∧ Polynomial.Splits (algebraMap F K) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>Field F<VAR>Field K<VAR>Algebra F K<GOAL>Normal F K → ∀ (x : K), IsIntegral F x ∧ Polynomial.Splits (algebraMap F K) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>Field F<VAR>Field K<VAR>Algebra F K<VAR>h : Normal F K<VAR>FiniteDimensional F K<GOAL>∃ p, Polynomial.IsSplittingField F K p
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>Field F<VAR>Field K<VAR>Algebra F K<VAR>E : Type u_3<VAR>Field E<VAR>Algebra F E<VAR>Algebra K E<VAR>IsScalarTower F K E<VAR>h : Normal F E<GOAL>Normal K E
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>Field F<VAR>Field K<VAR>Algebra F K<VAR>E : Type u_3<VAR>Field E<VAR>Algebra F E<VAR>Algebra K E<VAR>IsScalarTower F K E<VAR>h : Normal F E<VAR>ϕ : E →ₐ[F] K<GOAL>Function.Bijective ⇑ϕ
<VAR>F : Type u_1<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Field E'<VAR>Algebra F E'<VAR>h : Normal F E<VAR>f : E ≃ₐ[F] E'<GOAL>Normal F E'
<VAR>F : Type u_1<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>Field E'<VAR>Algebra F E'<VAR>f : E ≃ₐ[F] E'<GOAL>Normal F E ↔ Normal F E'
<VAR>F : Type u_1<VAR>E : Type u_3<VAR>Field F<VAR>Field E<VAR>Algebra F E<VAR>p : F[X]<VAR>hFEp : Polynomial.IsSplittingField F E p<GOAL>Normal F E
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>Field F<VAR>Field K<VAR>Algebra F K<VAR>L : Type u_3<VAR>Field L<VAR>Algebra F L<VAR>S : Set K<VAR>splits : ∀ x ∈ S, IsIntegral F x ∧ Polynomial.Splits (algebraMap F L) (minpoly F x)<VAR>x : K<VAR>hx : x ∈ IntermediateField.adjoin F S<GOAL>Polynomial.Splits (algebraMap F L) (minpoly F x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F L<VAR>Algebra K L<VAR>Algebra F K<VAR>IsScalarTower F K L<VAR>E : IntermediateField K L<GOAL>Normal F ↥(IntermediateField.restrictScalars F E) ↔ Normal F ↥E
<VAR>F : Type u_1<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>Field F<VAR>Field K₁<VAR>Field K₂<VAR>Algebra F K₁<VAR>Algebra F K₂<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>E : Type u_6<VAR>Field E<VAR>Algebra F E<VAR>Algebra E K₁<VAR>Algebra E K₂<VAR>IsScalarTower F E K₁<VAR>IsScalarTower F E K₂<VAR>Normal F E<VAR>x : E<GOAL>(algebraMap E K₂) ((ϕ.restrictNormal E) x) = ϕ ((algebraMap E K₁) x)
<VAR>F : Type u_1<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>Field F<VAR>Field K₁<VAR>Field K₂<VAR>Field K₃<VAR>Algebra F K₁<VAR>Algebra F K₂<VAR>Algebra F K₃<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>ψ : K₂ →ₐ[F] K₃<VAR>E : Type u_6<VAR>Field E<VAR>Algebra F E<VAR>Algebra E K₁<VAR>Algebra E K₂<VAR>Algebra E K₃<VAR>IsScalarTower F E K₁<VAR>IsScalarTower F E K₂<VAR>IsScalarTower F E K₃<VAR>Normal F E<GOAL>(ψ.restrictNormal E).comp (ϕ.restrictNormal E) = (ψ.comp ϕ).restrictNormal E
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>Field K<VAR>Field F<VAR>Algebra F K<VAR>E : IntermediateField F K<VAR>Normal F ↥E<VAR>f : ↥E →ₐ[F] K<GOAL>f.fieldRange = E
<VAR>F : Type u_1<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>Field F<VAR>Field K₁<VAR>Field K₂<VAR>Algebra F K₁<VAR>Algebra F K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>E : Type u_6<VAR>Field E<VAR>Algebra F E<VAR>Algebra E K₁<VAR>Algebra E K₂<VAR>IsScalarTower F E K₁<VAR>IsScalarTower F E K₂<VAR>Normal F E<VAR>x : E<GOAL>(algebraMap E K₂) ((χ.restrictNormal E) x) = χ ((algebraMap E K₁) x)
<VAR>F : Type u_1<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>K₃ : Type u_5<VAR>Field F<VAR>Field K₁<VAR>Field K₂<VAR>Field K₃<VAR>Algebra F K₁<VAR>Algebra F K₂<VAR>Algebra F K₃<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>ω : K₂ ≃ₐ[F] K₃<VAR>E : Type u_6<VAR>Field E<VAR>Algebra F E<VAR>Algebra E K₁<VAR>Algebra E K₂<VAR>Algebra E K₃<VAR>IsScalarTower F E K₁<VAR>IsScalarTower F E K₂<VAR>IsScalarTower F E K₃<VAR>Normal F E<GOAL>(χ.trans ω).restrictNormal E = (χ.restrictNormal E).trans (ω.restrictNormal E)
<VAR>F : Type u_1<VAR>K₁ : Type u_3<VAR>Field F<VAR>Field K₁<VAR>Algebra F K₁<VAR>E : Type u_6<VAR>Field E<VAR>Algebra F E<VAR>Algebra E K₁<VAR>IsScalarTower F E K₁<VAR>Normal F E<VAR>σ : E ≃ₐ[F] E<GOAL>(Normal.algHomEquivAut F K₁ E).symm σ = (IsScalarTower.toAlgHom F E K₁).comp ↑σ
<VAR>F : Type u_1<VAR>K₁ : Type u_3<VAR>Field F<VAR>Field K₁<VAR>Algebra F K₁<VAR>E : Type u_6<VAR>Field E<VAR>Algebra F E<VAR>Algebra E K₁<VAR>IsScalarTower F E K₁<VAR>Normal F E<VAR>σ : E →ₐ[F] K₁<GOAL>(Normal.algHomEquivAut F K₁ E) σ = σ.restrictNormal' E
<VAR>F : Type u_1<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>Field F<VAR>Field K₁<VAR>Field K₂<VAR>Algebra F K₁<VAR>Algebra F K₂<VAR>ϕ : K₁ →ₐ[F] K₂<VAR>E : Type u_6<VAR>Field E<VAR>Algebra F E<VAR>Algebra K₁ E<VAR>Algebra K₂ E<VAR>IsScalarTower F K₁ E<VAR>IsScalarTower F K₂ E<VAR>Normal F E<VAR>x : K₁<GOAL>(ϕ.liftNormal E) ((algebraMap K₁ E) x) = (algebraMap K₂ E) (ϕ x)
<VAR>F : Type u_1<VAR>K₁ : Type u_3<VAR>Field F<VAR>Field K₁<VAR>Algebra F K₁<VAR>E : Type u_6<VAR>Field E<VAR>Algebra F E<VAR>Algebra K₁ E<VAR>IsScalarTower F K₁ E<VAR>ϕ : K₁ →ₐ[F] K₁<VAR>Normal F K₁<VAR>Normal F E<GOAL>(ϕ.liftNormal E).restrictNormal K₁ = ϕ
<VAR>F : Type u_1<VAR>K₁ : Type u_3<VAR>K₂ : Type u_4<VAR>Field F<VAR>Field K₁<VAR>Field K₂<VAR>Algebra F K₁<VAR>Algebra F K₂<VAR>χ : K₁ ≃ₐ[F] K₂<VAR>E : Type u_6<VAR>Field E<VAR>Algebra F E<VAR>Algebra K₁ E<VAR>Algebra K₂ E<VAR>IsScalarTower F K₁ E<VAR>IsScalarTower F K₂ E<VAR>Normal F E<VAR>x : K₁<GOAL>(χ.liftNormal E) ((algebraMap K₁ E) x) = (algebraMap K₂ E) (χ x)
<VAR>F : Type u_1<VAR>K₁ : Type u_3<VAR>Field F<VAR>Field K₁<VAR>Algebra F K₁<VAR>E : Type u_6<VAR>Field E<VAR>Algebra F E<VAR>Algebra K₁ E<VAR>IsScalarTower F K₁ E<VAR>χ : K₁ ≃ₐ[F] K₁<VAR>Normal F K₁<VAR>Normal F E<GOAL>(χ.liftNormal E).restrictNormal K₁ = χ
<VAR>F : Type u_1<VAR>K₁ : Type u_3<VAR>Field F<VAR>Field K₁<VAR>Algebra F K₁<VAR>E : Type u_6<VAR>Field E<VAR>Algebra F E<VAR>Algebra K₁ E<VAR>IsScalarTower F K₁ E<VAR>Normal F K₁<VAR>Normal F E<GOAL>Function.Surjective ⇑(AlgEquiv.restrictNormalHom K₁)
<VAR>F : Type u_1<VAR>Field F<VAR>E : Type u_6<VAR>Field E<VAR>Algebra F E<VAR>h : Normal F E<VAR>x y : E<GOAL>minpoly F x = minpoly F y ↔ x ∈ MulAction.orbit (E ≃ₐ[F] E) y
<VAR>F : Type u_1<VAR>K₁ : Type u_3<VAR>Field F<VAR>Field K₁<VAR>Algebra F K₁<VAR>E : Type u_6<VAR>Field E<VAR>Algebra F E<VAR>Algebra K₁ E<VAR>IsScalarTower F K₁ E<VAR>Normal F K₁<VAR>h1 : IsSolvable (K₁ ≃ₐ[F] K₁)<VAR>h2 : IsSolvable (E ≃ₐ[K₁] E)<GOAL>IsSolvable (E ≃ₐ[F] E)
<VAR>K : Type u_6<VAR>L : Type u_7<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Normal K L<VAR>x y : L<VAR>hy : IsAlgebraic K y<VAR>h_ev : (Polynomial.aeval x) (minpoly K y) = 0<GOAL>∃ σ, σ x = y
<VAR>K : Type u_6<VAR>L : Type u_7<VAR>Field K<VAR>Field L<VAR>Algebra K L<VAR>Normal K L<VAR>x y : L<VAR>hy : IsAlgebraic K y<VAR>h_ev : (Polynomial.aeval x) (minpoly K y) = 0<GOAL>∃ σ, σ y = x
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>c : Set (IntermediateField.Lifts F E K)<VAR>hc : IsChain (fun x x_1 => x ≤ x_1) c<GOAL>∃ ub, ∀ a ∈ c, a ≤ ub
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>x : IntermediateField.Lifts F E K<VAR>s : E<VAR>h1 : IsIntegral (↥x.carrier) s<VAR>h2 : Polynomial.Splits x.emb.toRingHom (minpoly (↥x.carrier) s)<GOAL>∃ y, x ≤ y ∧ s ∈ y.carrier
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>x : IntermediateField.Lifts F E K<VAR>s : E<VAR>h1 : IsIntegral F s<VAR>h2 : Polynomial.Splits (algebraMap F K) (minpoly F s)<GOAL>∃ y, x ≤ y ∧ s ∈ y.carrier
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>S : Set E<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral (↥L) s ∧ Polynomial.Splits f.toRingHom (minpoly (↥L) s)<GOAL>∃ φ, φ.comp (IsScalarTower.toAlgHom F ↥L ↥(IntermediateField.adjoin (↥L) S)) = f
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>S : Set E<VAR>L : Type u_4<VAR>Field L<VAR>Algebra F L<VAR>Algebra L E<VAR>IsScalarTower F L E<VAR>f : L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral L s ∧ Polynomial.Splits f.toRingHom (minpoly L s)<GOAL>∃ φ, φ.comp (IsScalarTower.toAlgHom F L ↥(IntermediateField.adjoin L S)) = f
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>S : Set E<VAR>L : Type u_4<VAR>Field L<VAR>Algebra F L<VAR>Algebra L E<VAR>IsScalarTower F L E<VAR>f : L →ₐ[F] K<VAR>hK : ∀ s ∈ S, IsIntegral L s ∧ Polynomial.Splits f.toRingHom (minpoly L s)<VAR>hS : IntermediateField.adjoin L S = ⊤<GOAL>∃ φ, φ.comp (IsScalarTower.toAlgHom F L E) = f
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>L : Type u_4<VAR>Field L<VAR>Algebra F L<VAR>Algebra L E<VAR>IsScalarTower F L E<VAR>f : L →ₐ[F] K<VAR>hK : ∀ (s : E), IsIntegral L s ∧ Polynomial.Splits f.toRingHom (minpoly L s)<GOAL>∃ φ, φ.comp (IsScalarTower.toAlgHom F L E) = f
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hL : L ≤ IntermediateField.adjoin F S<GOAL>∃ φ, φ.comp (IntermediateField.inclusion hL) = f
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)<GOAL>Nonempty (↥(IntermediateField.adjoin F S) →ₐ[F] K)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<VAR>hS : IntermediateField.adjoin F S = ⊤<GOAL>∃ φ, φ.comp L.val = f
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)<VAR>hS : IntermediateField.adjoin F S = ⊤<GOAL>Nonempty (E →ₐ[F] K)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)<VAR>x : E<VAR>hx : x ∈ IntermediateField.adjoin F S<VAR>y : K<VAR>hy : (Polynomial.aeval y) (minpoly F x) = 0<GOAL>∃ φ, φ ⟨x, hx⟩ = y
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>S : Set E<VAR>hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)<VAR>hS : IntermediateField.adjoin F S = ⊤<VAR>x : E<VAR>y : K<VAR>hy : (Polynomial.aeval y) (minpoly F x) = 0<GOAL>∃ φ, φ x = y
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>hK' : ∀ (s : E), IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)<VAR>L : IntermediateField F E<VAR>f : ↥L →ₐ[F] K<GOAL>∃ φ, φ.comp L.val = f
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>hK' : ∀ (s : E), IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)<GOAL>Nonempty (E →ₐ[F] K)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>K : Type u_3<VAR>Field F<VAR>Field E<VAR>Field K<VAR>Algebra F E<VAR>Algebra F K<VAR>hK' : ∀ (s : E), IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)<VAR>x : E<VAR>y : K<VAR>hy : (Polynomial.aeval y) (minpoly F x) = 0<GOAL>∃ φ, φ x = y
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>Field F<VAR>Field K<VAR>Field L<VAR>Algebra F L<VAR>Algebra F K<VAR>hA : ∀ (x : K), Polynomial.Splits (algebraMap F L) (minpoly F x)<VAR>Algebra.IsAlgebraic F K<VAR>x : K<GOAL>(Set.range fun ψ => ψ x) = (minpoly F x).rootSet L
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : C<VAR>CategoryTheory.Closed A<GOAL>(CategoryTheory.ihom.adjunction A).counit = CategoryTheory.ihom.ev A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : C<VAR>CategoryTheory.Closed A<GOAL>(CategoryTheory.ihom.adjunction A).unit = CategoryTheory.ihom.coev A
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : C<VAR>CategoryTheory.Closed A<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A ((CategoryTheory.ihom A).map f)) ((CategoryTheory.ihom.ev A).app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app X) f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : C<VAR>CategoryTheory.Closed A<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ihom.coev A).app Y) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app X) ((CategoryTheory.ihom A).map (CategoryTheory.MonoidalCategory.whiskerLeft A f))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : C<VAR>CategoryTheory.Closed A<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A ((CategoryTheory.ihom.coev A).app B)) ((CategoryTheory.ihom.ev A).app (CategoryTheory.MonoidalCategory.tensorObj A B)) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj A B)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : C<VAR>CategoryTheory.Closed A<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app ((CategoryTheory.ihom A).obj B)) ((CategoryTheory.ihom A).map ((CategoryTheory.ihom.ev A).app B)) = CategoryTheory.CategoryStruct.id ((CategoryTheory.ihom A).obj B)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X Y : C<VAR>CategoryTheory.Closed A<VAR>f : CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X<GOAL>((CategoryTheory.ihom.adjunction A).homEquiv Y X) f = CategoryTheory.MonoidalClosed.curry f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X Y : C<VAR>CategoryTheory.Closed A<VAR>f : Y ⟶ (CategoryTheory.ihom A).obj X<GOAL>((CategoryTheory.ihom.adjunction A).homEquiv Y X).symm f = CategoryTheory.MonoidalClosed.uncurry f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X X' Y : C<VAR>CategoryTheory.Closed A<VAR>f : X ⟶ X'<VAR>g : CategoryTheory.MonoidalCategory.tensorObj A X' ⟶ Y<GOAL>CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A f) g) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.MonoidalClosed.curry g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X Y Y' : C<VAR>CategoryTheory.Closed A<VAR>f : CategoryTheory.MonoidalCategory.tensorObj A X ⟶ Y<VAR>g : Y ⟶ Y'<GOAL>CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry f) ((CategoryTheory.ihom A).map g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X Y Y' : C<VAR>CategoryTheory.Closed A<VAR>f : X ⟶ (CategoryTheory.ihom A).obj Y<VAR>g : Y ⟶ Y'<GOAL>CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.ihom A).map g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.uncurry f) g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X X' Y : C<VAR>CategoryTheory.Closed A<VAR>f : X ⟶ X'<VAR>g : X' ⟶ (CategoryTheory.ihom A).obj Y<GOAL>CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A f) (CategoryTheory.MonoidalClosed.uncurry g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X Y : C<VAR>CategoryTheory.Closed A<VAR>f : CategoryTheory.MonoidalCategory.tensorObj A X ⟶ Y<GOAL>CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.MonoidalClosed.curry f) = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X Y : C<VAR>CategoryTheory.Closed A<VAR>f : X ⟶ (CategoryTheory.ihom A).obj Y<GOAL>CategoryTheory.MonoidalClosed.curry (CategoryTheory.MonoidalClosed.uncurry f) = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X Y : C<VAR>CategoryTheory.Closed A<VAR>f : CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X<VAR>g : Y ⟶ (CategoryTheory.ihom A).obj X<GOAL>CategoryTheory.MonoidalClosed.curry f = g ↔ f = CategoryTheory.MonoidalClosed.uncurry g
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X Y : C<VAR>CategoryTheory.Closed A<VAR>f : CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X<VAR>g : Y ⟶ (CategoryTheory.ihom A).obj X<GOAL>g = CategoryTheory.MonoidalClosed.curry f ↔ CategoryTheory.MonoidalClosed.uncurry g = f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X Y : C<VAR>CategoryTheory.Closed A<VAR>g : Y ⟶ (CategoryTheory.ihom A).obj X<GOAL>CategoryTheory.MonoidalClosed.uncurry g = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft A g) ((CategoryTheory.ihom.ev A).app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X Y : C<VAR>CategoryTheory.Closed A<VAR>g : CategoryTheory.MonoidalCategory.tensorObj A Y ⟶ X<GOAL>CategoryTheory.MonoidalClosed.curry g = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app Y) ((CategoryTheory.ihom A).map g)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X Y : C<VAR>CategoryTheory.Closed A<GOAL>Function.Injective CategoryTheory.MonoidalClosed.curry
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X Y : C<VAR>CategoryTheory.Closed A<GOAL>Function.Injective CategoryTheory.MonoidalClosed.uncurry
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X : C<VAR>CategoryTheory.Closed A<GOAL>CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.id ((CategoryTheory.ihom A).obj X)) = (CategoryTheory.ihom.ev A).app X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A X : C<VAR>CategoryTheory.Closed A<GOAL>CategoryTheory.MonoidalClosed.curry (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj A ((CategoryTheory.Functor.id C).obj X))) = (CategoryTheory.ihom.coev A).app X
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : C<VAR>CategoryTheory.Closed A<VAR>CategoryTheory.Closed B<VAR>f : B ⟶ A<VAR>X : C<GOAL>CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft B ((CategoryTheory.MonoidalClosed.pre f).app X)) ((CategoryTheory.ihom.ev B).app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f ((CategoryTheory.ihom A).obj X)) ((CategoryTheory.ihom.ev A).app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : C<VAR>CategoryTheory.Closed A<VAR>CategoryTheory.Closed B<VAR>f : B ⟶ A<VAR>X : C<GOAL>CategoryTheory.MonoidalClosed.uncurry ((CategoryTheory.MonoidalClosed.pre f).app X) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f ((CategoryTheory.ihom A).obj X)) ((CategoryTheory.ihom.ev A).app X)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A B : C<VAR>X : C<VAR>CategoryTheory.Closed A<VAR>CategoryTheory.Closed B<VAR>f : B ⟶ A<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev A).app X) ((CategoryTheory.MonoidalClosed.pre f).app (CategoryTheory.MonoidalCategory.tensorObj A X)) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.coev B).app X) ((CategoryTheory.ihom B).map (CategoryTheory.MonoidalCategory.whiskerRight f X))
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A : C<VAR>CategoryTheory.Closed A<GOAL>CategoryTheory.MonoidalClosed.pre (CategoryTheory.CategoryStruct.id A) = CategoryTheory.CategoryStruct.id (CategoryTheory.ihom A)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>A₁ A₂ A₃ : C<VAR>CategoryTheory.Closed A₁<VAR>CategoryTheory.Closed A₂<VAR>CategoryTheory.Closed A₃<VAR>f : A₁ ⟶ A₂<VAR>g : A₂ ⟶ A₃<GOAL>CategoryTheory.MonoidalClosed.pre (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.pre g) (CategoryTheory.MonoidalClosed.pre f)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>W X Y Z : C<VAR>CategoryTheory.Closed W<VAR>CategoryTheory.Closed X<VAR>f : W ⟶ X<VAR>g : Y ⟶ Z<GOAL>CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalClosed.pre f).app Y) ((CategoryTheory.ihom W).map g) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom X).map g) ((CategoryTheory.MonoidalClosed.pre f).app Z)
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalClosed C<GOAL>∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), CategoryTheory.MonoidalClosed.internalHom.map f = CategoryTheory.MonoidalClosed.pre f.unop
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>CategoryTheory.MonoidalClosed C<VAR>X : Cᵒᵖ<GOAL>CategoryTheory.MonoidalClosed.internalHom.obj X = CategoryTheory.ihom (Opposite.unop X)