ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>φ₁ : B →ₐc[R] C<VAR>φ₂ : A →ₐc[R] B<GOAL>↑(φ₁.comp φ₂) = (↑φ₁).comp ↑φ₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ : A →ₐc[R] B<GOAL>φ.comp (BialgHom.id R A) = φ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ : A →ₐc[R] B<GOAL>(BialgHom.id R B).comp φ = φ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>Semiring C<VAR>Algebra R C<VAR>Semiring D<VAR>Algebra R D<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>CoalgebraStruct R D<VAR>φ₁ : C →ₐc[R] D<VAR>φ₂ : B →ₐc[R] C<VAR>φ₃ : A →ₐc[R] B<GOAL>(φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Semiring B<VAR>Algebra R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ : A →ₐc[R] B<VAR>R' : Type u_6<VAR>SMul R' A<VAR>SMul R' B<VAR>LinearMap.CompatibleSMul A B R' R<VAR>r : R'<VAR>x : A<GOAL>φ (r • x) = r • φ x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>CoalgebraStruct R A<GOAL>1 = BialgHom.id R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>CoalgebraStruct R A<VAR>φ₁ φ₂ : A →ₐc[R] A<GOAL>φ₁ * φ₂ = φ₁.comp φ₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>CoalgebraStruct R A<VAR>x : A<GOAL>1 x = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>CoalgebraStruct R A<VAR>φ ψ : A →ₐc[R] A<VAR>x : A<GOAL>(φ * ψ) x = φ (ψ x)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<VAR>x : A<GOAL>(Bialgebra.counitBialgHom R A) x = Coalgebra.counit x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<GOAL>↑(Bialgebra.counitBialgHom R A) = Coalgebra.counitCoalgHom R A
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>Semiring A<VAR>Bialgebra R A<VAR>f g : A →ₐc[R] R<GOAL>f = g
<VAR>R : Type u_1<VAR>CommRing R<VAR>P : Ideal R<VAR>hP : P.IsPrime<VAR>IsDedekindDomain R<VAR>x : R<VAR>x_mem : x ∈ P<VAR>hxP2 : x ∉ P ^ 2<VAR>hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q<GOAL>P = Ideal.span {x}
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommRing R<VAR>CommRing A<VAR>Algebra R A<VAR>S : Submonoid R<VAR>IsLocalization S A<VAR>I : (FractionalIdeal S A)ˣ<VAR>v : A<VAR>hv : v ∈ ↑I⁻¹<VAR>h : Submodule.comap (Algebra.linearMap R A) (↑↑I * Submodule.span R {v}) = ⊤<GOAL>(↑↑I).IsPrincipal
<VAR>R : Type u_1<VAR>CommRing R<VAR>A : Type u_2<VAR>CommRing A<VAR>Algebra R A<VAR>S : Submonoid R<VAR>IsLocalization S A<VAR>hS : S ≤ R⁰<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I I' : FractionalIdeal S A<VAR>hinv : I * I' = 1<GOAL>(↑I).IsPrincipal
<VAR>R : Type u_1<VAR>CommRing R<VAR>hf : {I | I.IsMaximal}.Finite<VAR>I : Ideal R<VAR>hI : IsUnit ↑I<GOAL>Submodule.IsPrincipal I
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>h : {I | I.IsPrime}.Finite<GOAL>IsPrincipalIdealRing R
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>Module.Free R S<VAR>Module.Finite R S<VAR>p : Ideal R<VAR>hp0 : p ≠ ⊥<VAR>p.IsPrime<VAR>Sₚ : Type u_3<VAR>CommRing Sₚ<VAR>Algebra S Sₚ<VAR>IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ<VAR>Algebra R Sₚ<VAR>IsScalarTower R S Sₚ<VAR>IsDedekindDomain Sₚ<VAR>IsDomain S<VAR>P : Ideal Sₚ<VAR>hP : P.IsPrime<VAR>hP0 : P ≠ ⊥<GOAL>P ∈ UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R Sₚ) p)
<VAR>R : Type u_1<VAR>CommRing R<VAR>IsDedekindDomain R<VAR>S : Type u_2<VAR>CommRing S<VAR>Algebra R S<VAR>Module.Free R S<VAR>Module.Finite R S<VAR>p : Ideal R<VAR>hp0 : p ≠ ⊥<VAR>p.IsPrime<VAR>Sₚ : Type u_3<VAR>CommRing Sₚ<VAR>Algebra S Sₚ<VAR>IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ<VAR>Algebra R Sₚ<VAR>IsScalarTower R S Sₚ<VAR>IsDedekindDomain Sₚ<VAR>IsDomain S<GOAL>IsPrincipalIdealRing Sₚ
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>self : RingHom.PropertyIsLocal P<GOAL>RingHom.HoldsForLocalizationAway P
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>self : RingHom.PropertyIsLocal P<GOAL>RingHom.OfLocalizationSpanTarget P
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>self : RingHom.PropertyIsLocal P<GOAL>RingHom.StableUnderComposition P
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>self : RingHom.PropertyIsLocal P<GOAL>RingHom.LocalizationPreserves P
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<GOAL>RingHom.OfLocalizationSpan P ↔ RingHom.OfLocalizationFiniteSpan P
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<GOAL>RingHom.OfLocalizationSpanTarget P ↔ RingHom.OfLocalizationFiniteSpanTarget P
<VAR>R S : Type u<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>H : RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P<VAR>hf : Function.Bijective ⇑f<GOAL>P f
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.PropertyIsLocal P<GOAL>RingHom.RespectsIso P
<VAR>R S : Type u<VAR>CommRing R<VAR>CommRing S<VAR>R' S' : Type u<VAR>CommRing R'<VAR>CommRing S'<VAR>f : R →+* S<VAR>Algebra R R'<VAR>Algebra S S'<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>H : RingHom.LocalizationPreserves P<VAR>r : R<VAR>IsLocalization.Away r R'<VAR>IsLocalization.Away (f r) S'<VAR>hf : P f<GOAL>P (IsLocalization.Away.map R' S' f r)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.PropertyIsLocal P<GOAL>RingHom.OfLocalizationSpan P
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] => P<VAR>hP' : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<VAR>R S : Type u<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>s : Set S<VAR>hs : Ideal.span s = ⊤<VAR>hT : ∀ (r : ↑s), ∃ T x x_1, ∃ (_ : IsLocalization.Away (↑r) T), P ((algebraMap S T).comp f)<GOAL>P f
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R) (hP : P.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime P)) I ≤ Ideal.map (algebraMap R (Localization.AtPrime P)) J<GOAL>I ≤ J
<VAR>R : Type u<VAR>CommRing R<VAR>I J : Ideal R<VAR>h : ∀ (P : Ideal R) (x : P.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime P)) I = Ideal.map (algebraMap R (Localization.AtPrime P)) J<GOAL>I = J
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>h : ∀ (J : Ideal R) (hJ : J.IsMaximal), Ideal.map (algebraMap R (Localization.AtPrime J)) I = ⊥<GOAL>I = ⊥
<VAR>R : Type u<VAR>CommRing R<VAR>I : Ideal R<VAR>h : ∀ (J : Ideal R) (hJ : J.IsMaximal), IsLocalization.coeSubmodule (Localization.AtPrime J) I = ⊥<GOAL>I = ⊥
<VAR>R : Type u<VAR>CommRing R<VAR>r : R<VAR>h : ∀ (J : Ideal R) (hJ : J.IsMaximal), (algebraMap R (Localization.AtPrime J)) r = 0<GOAL>r = 0
<GOAL>RingHom.LocalizationPreserves fun {R S} x x_1 f => Function.Surjective ⇑f
<GOAL>RingHom.OfLocalizationSpan fun {R S} x x_1 f => Function.Surjective ⇑f
<VAR>R S : Type u<VAR>CommRing R<VAR>CommRing S<VAR>f : R →+* S<VAR>h : Function.Surjective ⇑f<VAR>P : Ideal S<VAR>P.IsPrime<GOAL>Function.Surjective ⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯)
<GOAL>RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => Function.Surjective ⇑f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>Rₚ : Type u_3<VAR>Sₚ : Type u_4<VAR>CommSemiring R<VAR>CommRing S<VAR>CommRing Rₚ<VAR>CommRing Sₚ<VAR>Algebra R S<VAR>Algebra R Rₚ<VAR>Algebra R Sₚ<VAR>Algebra S Sₚ<VAR>Algebra Rₚ Sₚ<VAR>IsScalarTower R S Sₚ<VAR>IsScalarTower R Rₚ Sₚ<VAR>M : Submonoid R<VAR>IsLocalization M Rₚ<VAR>IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ<VAR>hRS : Module.Finite R S<GOAL>Module.Finite Rₚ Sₚ
<GOAL>RingHom.LocalizationPreserves @RingHom.Finite
<VAR>R S : Type u<VAR>CommRing R<VAR>CommRing S<VAR>R' S' : Type u<VAR>CommRing R'<VAR>CommRing S'<VAR>f : R →+* S<VAR>Algebra R R'<VAR>Algebra S S'<VAR>r : R<VAR>IsLocalization.Away r R'<VAR>IsLocalization.Away (f r) S'<VAR>hf : f.Finite<GOAL>(IsLocalization.Away.map R' S' f r).Finite
<VAR>R S : Type u<VAR>CommRing R<VAR>CommRing S<VAR>M : Submonoid R<VAR>S' : Type u<VAR>CommRing S'<VAR>Algebra S S'<VAR>Algebra R S<VAR>Algebra R S'<VAR>IsScalarTower R S S'<VAR>IsLocalization (Submonoid.map (algebraMap R S) M) S'<VAR>x : S<VAR>s : Finset S'<VAR>hx : (algebraMap S S') x ∈ Submodule.span R ↑s<GOAL>∃ m, m • x ∈ Submodule.span R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
<VAR>R : Type u<VAR>CommRing R<VAR>M : Submonoid R<VAR>R' : Type u<VAR>CommRing R'<VAR>Algebra R R'<VAR>N : Type u_1<VAR>AddCommMonoid N<VAR>Module R N<VAR>Module R' N<VAR>IsScalarTower R R' N<VAR>IsLocalization M R'<VAR>s : Set N<VAR>x : N<VAR>hx : x ∈ Submodule.span R' s<GOAL>∃ t, t • x ∈ Submodule.span R s
<VAR>R S : Type u<VAR>CommRing R<VAR>CommRing S<VAR>M : Submonoid R<VAR>R' : Type u<VAR>CommRing R'<VAR>Algebra R R'<VAR>Algebra R' S<VAR>Algebra R S<VAR>IsScalarTower R R' S<VAR>IsLocalization M R'<VAR>s : Set S<VAR>x : S<VAR>hx : x ∈ Algebra.adjoin R' s<GOAL>∃ t, t • x ∈ Algebra.adjoin R s
<GOAL>RingHom.OfLocalizationSpan @RingHom.Finite
<GOAL>RingHom.LocalizationPreserves @RingHom.FiniteType
<VAR>R S : Type u<VAR>CommRing R<VAR>CommRing S<VAR>R' S' : Type u<VAR>CommRing R'<VAR>CommRing S'<VAR>f : R →+* S<VAR>Algebra R R'<VAR>Algebra S S'<VAR>r : R<VAR>IsLocalization.Away r R'<VAR>IsLocalization.Away (f r) S'<VAR>hf : f.FiniteType<GOAL>(IsLocalization.Away.map R' S' f r).FiniteType
<VAR>R S : Type u<VAR>CommRing R<VAR>CommRing S<VAR>S' : Type u<VAR>CommRing S'<VAR>Algebra S S'<VAR>Algebra R S<VAR>Algebra R S'<VAR>IsScalarTower R S S'<VAR>M : Submonoid S<VAR>IsLocalization M S'<VAR>x : S<VAR>s : Finset S'<VAR>A : Subalgebra R S<VAR>hA₁ : ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A<VAR>hA₂ : M ≤ A.toSubmonoid<VAR>hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s<GOAL>∃ m, m • x ∈ A
<VAR>R S : Type u<VAR>CommRing R<VAR>CommRing S<VAR>M : Submonoid R<VAR>S' : Type u<VAR>CommRing S'<VAR>Algebra S S'<VAR>Algebra R S<VAR>Algebra R S'<VAR>IsScalarTower R S S'<VAR>IsLocalization (Submonoid.map (algebraMap R S) M) S'<VAR>x : S<VAR>s : Finset S'<VAR>hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s<GOAL>∃ m, m • x ∈ Algebra.adjoin R ↑(IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s)
<GOAL>RingHom.OfLocalizationSpan @RingHom.FiniteType
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>self : A →ₗc[R] B<GOAL>Coalgebra.counit ∘ₗ self.toLinearMap = Coalgebra.counit
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>self : A →ₗc[R] B<GOAL>TensorProduct.map self.toLinearMap self.toLinearMap ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ self.toLinearMap
<VAR>F : Type u_1<VAR>R : outParam (Type u_2)<VAR>A : outParam (Type u_3)<VAR>B : outParam (Type u_4)<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>FunLike F A B<VAR>self : CoalgHomClass F R A B<VAR>f : F<GOAL>TensorProduct.map ↑f ↑f ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ ↑f
<VAR>F : Type u_1<VAR>R : outParam (Type u_2)<VAR>A : outParam (Type u_3)<VAR>B : outParam (Type u_4)<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>FunLike F A B<VAR>self : CoalgHomClass F R A B<VAR>f : F<GOAL>Coalgebra.counit ∘ₗ ↑f = Coalgebra.counit
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>F : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>FunLike F A B<VAR>CoalgHomClass F R A B<VAR>f : F<VAR>x : A<GOAL>Coalgebra.counit (f x) = Coalgebra.counit x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>F : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>FunLike F A B<VAR>CoalgHomClass F R A B<VAR>f : F<VAR>x : A<GOAL>(TensorProduct.map ↑f ↑f) (Coalgebra.comul x) = Coalgebra.comul (f x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>F : Type u_6<VAR>FunLike F A B<VAR>CoalgHomClass F R A B<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A →ₗ[R] B<VAR>h : Coalgebra.counit ∘ₗ f = Coalgebra.counit<VAR>h₁ : TensorProduct.map f f ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ f<GOAL>⇑{ toLinearMap := f, counit_comp := h, map_comp_comul := h₁ } = ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A → B<VAR>h₁ : ∀ (x y : A), f (x + y) = f x + f y<VAR>h₂ : ∀ (m : R) (x : A), { toFun := f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := f, map_add' := h₁ }.toFun x<VAR>h₃ : Coalgebra.counit ∘ₗ { toFun := f, map_add' := h₁, map_smul' := h₂ } = Coalgebra.counit<VAR>h₄ : TensorProduct.map { toFun := f, map_add' := h₁, map_smul' := h₂ } { toFun := f, map_add' := h₁, map_smul' := h₂ } ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ { toFun := f, map_add' := h₁, map_smul' := h₂ }<GOAL>⇑{ toFun := f, map_add' := h₁, map_smul' := h₂, counit_comp := h₃, map_comp_comul := h₄ } = f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A →ₗ[R] B<VAR>h : Coalgebra.counit ∘ₗ f = Coalgebra.counit<VAR>h₁ : TensorProduct.map f f ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ f<GOAL>↑{ toLinearMap := f, counit_comp := h, map_comp_comul := h₁ } = f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A →ₗc[R] B<GOAL>f.toLinearMap = ↑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A →ₗc[R] B<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<GOAL>Function.Injective DFunLike.coe
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ₁ φ₂ : A →ₗc[R] B<GOAL>⇑φ₁ = ⇑φ₂ ↔ φ₁ = φ₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<GOAL>Function.Injective fun x => ↑x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<GOAL>Function.Injective AddMonoidHomClass.toAddMonoidHom
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ₁ φ₂ : A →ₗc[R] B<VAR>H : φ₁ = φ₂<VAR>x : A<GOAL>φ₁ x = φ₂ x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ : A →ₗc[R] B<VAR>x y : A<VAR>h : x = y<GOAL>φ x = φ y
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ₁ φ₂ : A →ₗc[R] B<VAR>H : ∀ (x : A), φ₁ x = φ₂ x<GOAL>φ₁ = φ₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ₁ φ₂ : A →ₗc[R] B<GOAL>φ₁ = φ₂ ↔ ∀ (x : A), φ₁ x = φ₂ x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>CoalgebraStruct R A<VAR>f g : R →ₗc[R] A<VAR>h : f 1 = g 1<GOAL>f = g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A →ₗc[R] B<VAR>h₁ : ∀ (x y : A), f (x + y) = f x + f y<VAR>h₂ : ∀ (m : R) (x : A), { toFun := ⇑f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₁ }.toFun x<VAR>h₃ : Coalgebra.counit ∘ₗ { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ } = Coalgebra.counit<VAR>h₄ : TensorProduct.map { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ } { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ } ∘ₗ Coalgebra.comul = Coalgebra.comul ∘ₗ { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }<GOAL>{ toFun := ⇑f, map_add' := h₁, map_smul' := h₂, counit_comp := h₃, map_comp_comul := h₄ } = f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A →ₗc[R] B<VAR>f' : A → B<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>f : A →ₗc[R] B<VAR>f' : A → B<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>CoalgebraStruct R A<VAR>a : A<GOAL>(CoalgHom.id R A) a = a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>CoalgebraStruct R A<GOAL>⇑(CoalgHom.id R A) = id
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>CoalgebraStruct R A<GOAL>↑(CoalgHom.id R A) = LinearMap.id
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>AddCommMonoid C<VAR>Module R C<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>φ₁ : B →ₗc[R] C<VAR>φ₂ : A →ₗc[R] B<GOAL>∀ (a : A), (φ₁.comp φ₂) a = φ₁ (φ₂ a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>AddCommMonoid C<VAR>Module R C<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>φ₁ : B →ₗc[R] C<VAR>φ₂ : A →ₗc[R] B<GOAL>⇑(φ₁.comp φ₂) = ⇑φ₁ ∘ ⇑φ₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>AddCommMonoid C<VAR>Module R C<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>φ₁ : B →ₗc[R] C<VAR>φ₂ : A →ₗc[R] B<GOAL>↑(φ₁.comp φ₂) = ↑φ₁ ∘ₗ ↑φ₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ : A →ₗc[R] B<GOAL>φ.comp (CoalgHom.id R A) = φ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ : A →ₗc[R] B<GOAL>(CoalgHom.id R B).comp φ = φ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>D : Type u_5<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>AddCommMonoid C<VAR>Module R C<VAR>AddCommMonoid D<VAR>Module R D<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>CoalgebraStruct R C<VAR>CoalgebraStruct R D<VAR>φ₁ : C →ₗc[R] D<VAR>φ₂ : B →ₗc[R] C<VAR>φ₃ : A →ₗc[R] B<GOAL>(φ₁.comp φ₂).comp φ₃ = φ₁.comp (φ₂.comp φ₃)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>AddCommMonoid B<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>φ : A →ₗc[R] B<VAR>R' : Type u_6<VAR>SMul R' A<VAR>SMul R' B<VAR>LinearMap.CompatibleSMul A B R' R<VAR>r : R'<VAR>x : A<GOAL>φ (r • x) = r • φ x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>CoalgebraStruct R A<VAR>φ₁ φ₂ : A →ₗc[R] A<GOAL>φ₁ * φ₂ = φ₁.comp φ₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>CoalgebraStruct R A<GOAL>1 = CoalgHom.id R A
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>CoalgebraStruct R A<VAR>x : A<GOAL>1 x = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>CoalgebraStruct R A<VAR>φ ψ : A →ₗc[R] A<VAR>x : A<GOAL>(φ * ψ) x = φ (ψ x)
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Coalgebra R A<VAR>x : A<GOAL>(Coalgebra.counitCoalgHom R A) x = Coalgebra.counit x
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Coalgebra R A<GOAL>↑(Coalgebra.counitCoalgHom R A) = Coalgebra.counit
<VAR>R : Type u<VAR>A : Type v<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>Module R A<VAR>Coalgebra R A<VAR>f g : A →ₗc[R] R<GOAL>f = g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<GOAL>Function.Injective CoalgEquiv.toEquiv
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e₁ e₂ : A ≃ₗc[R] B<GOAL>e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<GOAL>Function.Injective CoalgEquiv.toCoalgHom
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>CommSemiring R<VAR>AddCommMonoid A<VAR>AddCommMonoid B<VAR>Module R A<VAR>Module R B<VAR>CoalgebraStruct R A<VAR>CoalgebraStruct R B<VAR>e₁ e₂ : A ≃ₗc[R] B<GOAL>↑e₁ = ↑e₂ ↔ e₁ = e₂