ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>f : A → B<VAR>h₁ : f 1 = 1<VAR>h₂ : ∀ (x y : A), { toFun := f, map_one' := h₁ }.toFun (x * y) = { toFun := f, map_one' := h₁ }.toFun x * { toFun := f, map_one' := h₁ }.toFun y<VAR>h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0<VAR>h₄ : ∀ (x y : A), (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) = (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x + (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y<VAR>h₅ : ∀ (r : R), (↑↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) = (algebraMap R B) r<VAR>h₆ : ∀ (x : A), (↑↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ }.toRingHom).toFun (star x) = star ((↑↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ }.toRingHom).toFun x)<GOAL>⇑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_star' := h₆ } = f
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>f : A →ₐ[R] B<VAR>h : ∀ (x : A), (↑↑f.toRingHom).toFun (star x) = star ((↑↑f.toRingHom).toFun x)<GOAL>⇑{ toAlgHom := f, map_star' := h } = ⇑f
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>f : A →⋆ₐ[R] B<VAR>h₁ : f 1 = 1<VAR>h₂ : ∀ (x y : A), { toFun := ⇑f, map_one' := h₁ }.toFun (x * y) = { toFun := ⇑f, map_one' := h₁ }.toFun x * { toFun := ⇑f, map_one' := h₁ }.toFun y<VAR>h₃ : (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0<VAR>h₄ : ∀ (x y : A), (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) = (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun x + (↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂ }).toFun y<VAR>h₅ : ∀ (r : R), (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) = (algebraMap R B) r<VAR>h₆ : ∀ (x : A), (↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ }.toRingHom).toFun (star x) = star ((↑↑{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅ }.toRingHom).toFun x)<GOAL>{ toFun := ⇑f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_star' := h₆ } = f
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<GOAL>⇑(StarAlgHom.id R A) = id
<VAR>R : Type u_7<VAR>A : Type u_8<VAR>CommSemiring R<VAR>StarRing R<VAR>Semiring A<VAR>StarMul A<VAR>Algebra R A<VAR>StarModule R A<VAR>a : R<GOAL>(StarAlgHom.ofId R A) a = (algebraMap R A) a
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>C : Type u_5<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>Semiring C<VAR>Algebra R C<VAR>Star C<VAR>f : B →⋆ₐ[R] C<VAR>g : A →⋆ₐ[R] B<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>C : Type u_5<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>Semiring C<VAR>Algebra R C<VAR>Star C<VAR>f : B →⋆ₐ[R] C<VAR>g : A →⋆ₐ[R] B<VAR>a : A<GOAL>(f.comp g) a = f (g a)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>C : Type u_5<VAR>D : Type u_6<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>Semiring C<VAR>Algebra R C<VAR>Star C<VAR>Semiring D<VAR>Algebra R D<VAR>Star D<VAR>f : C →⋆ₐ[R] D<VAR>g : B →⋆ₐ[R] C<VAR>h : A →⋆ₐ[R] B<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>f : A →⋆ₐ[R] B<GOAL>(StarAlgHom.id R B).comp f = f
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>f : A →⋆ₐ[R] B<GOAL>f.comp (StarAlgHom.id R A) = f
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>CommSemiring R<VAR>Semiring A<VAR>Algebra R A<VAR>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>f : A →⋆ₐ[R] B<GOAL>⇑f.toNonUnitalStarAlgHom = ⇑f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>self : A × B<GOAL>(NonUnitalStarAlgHom.fst R A B) self = self.1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>self : A × B<GOAL>(NonUnitalStarAlgHom.snd R A B) self = self.2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R C<VAR>Star C<VAR>f : A →⋆ₙₐ[R] B<VAR>g : A →⋆ₙₐ[R] C<VAR>i : A<GOAL>(f.prod g) i = (f i, g i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R C<VAR>Star C<VAR>f : A →⋆ₙₐ[R] B<VAR>g : A →⋆ₙₐ[R] C<GOAL>⇑(f.prod g) = Pi.prod ⇑f ⇑g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R C<VAR>Star C<VAR>f : A →⋆ₙₐ[R] B<VAR>g : A →⋆ₙₐ[R] C<GOAL>(NonUnitalStarAlgHom.fst R B C).comp (f.prod g) = f
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R C<VAR>Star C<VAR>f : A →⋆ₙₐ[R] B<VAR>g : A →⋆ₙₐ[R] C<GOAL>(NonUnitalStarAlgHom.snd R B C).comp (f.prod g) = g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<GOAL>(NonUnitalStarAlgHom.fst R A B).prod (NonUnitalStarAlgHom.snd R A B) = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R C<VAR>Star C<VAR>f : (A →⋆ₙₐ[R] B) × (A →⋆ₙₐ[R] C)<GOAL>NonUnitalStarAlgHom.prodEquiv f = f.1.prod f.2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>C : Type u_4<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>DistribMulAction R C<VAR>Star C<VAR>f : A →⋆ₙₐ[R] B × C<GOAL>NonUnitalStarAlgHom.prodEquiv.symm f = ((NonUnitalStarAlgHom.fst R B C).comp f, (NonUnitalStarAlgHom.snd R B C).comp f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>StarAddMonoid A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>StarAddMonoid B<GOAL>⇑(NonUnitalStarAlgHom.inl R A B) = fun x => (x, 0)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>StarAddMonoid A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>StarAddMonoid B<VAR>x : A<GOAL>(NonUnitalStarAlgHom.inl R A B) x = (x, 0)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>StarAddMonoid A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>StarAddMonoid B<GOAL>⇑(NonUnitalStarAlgHom.inr R A B) = Prod.mk 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>StarAddMonoid A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>StarAddMonoid B<VAR>x : B<GOAL>(NonUnitalStarAlgHom.inr R A B) x = (0, x)
<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>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>self : A × B<GOAL>(StarAlgHom.fst R A B) self = self.1
<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>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>self : A × B<GOAL>(StarAlgHom.snd R A B) self = self.2
<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>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>Semiring C<VAR>Algebra R C<VAR>Star C<VAR>f : A →⋆ₐ[R] B<VAR>g : A →⋆ₐ[R] C<VAR>x : A<GOAL>(f.prod g) x = (f x, g x)
<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>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>Semiring C<VAR>Algebra R C<VAR>Star C<VAR>f : A →⋆ₐ[R] B<VAR>g : A →⋆ₐ[R] C<GOAL>⇑(f.prod g) = Pi.prod ⇑f ⇑g
<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>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>Semiring C<VAR>Algebra R C<VAR>Star C<VAR>f : A →⋆ₐ[R] B<VAR>g : A →⋆ₐ[R] C<GOAL>(StarAlgHom.fst R B C).comp (f.prod g) = f
<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>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>Semiring C<VAR>Algebra R C<VAR>Star C<VAR>f : A →⋆ₐ[R] B<VAR>g : A →⋆ₐ[R] C<GOAL>(StarAlgHom.snd R B C).comp (f.prod g) = g
<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>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<GOAL>(StarAlgHom.fst R A B).prod (StarAlgHom.snd R A B) = 1
<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>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>Semiring C<VAR>Algebra R C<VAR>Star C<VAR>f : (A →⋆ₐ[R] B) × (A →⋆ₐ[R] C)<GOAL>StarAlgHom.prodEquiv f = f.1.prod f.2
<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>Star A<VAR>Semiring B<VAR>Algebra R B<VAR>Star B<VAR>Semiring C<VAR>Algebra R C<VAR>Star C<VAR>f : A →⋆ₐ[R] B × C<GOAL>StarAlgHom.prodEquiv.symm f = ((StarAlgHom.fst R B C).comp f, (StarAlgHom.snd R B C).comp f)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>self : A ≃⋆ₐ[R] B<VAR>r : R<VAR>a : A<GOAL>self.toFun (r • a) = r • self.toFun a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>self : A ≃⋆ₐ[R] B<VAR>a : A<GOAL>self.toFun (star a) = star (self.toFun a)
<VAR>F : Type u_1<VAR>R : outParam (Type u_2)<VAR>A : outParam (Type u_3)<VAR>B : outParam (Type u_4)<VAR>Add A<VAR>Mul A<VAR>SMul R A<VAR>Star A<VAR>Add B<VAR>Mul B<VAR>SMul R B<VAR>Star B<VAR>EquivLike F A B<VAR>NonUnitalAlgEquivClass F R A B<VAR>self : StarAlgEquivClass F R A B<VAR>f : F<VAR>a : A<GOAL>f (star a) = star (f a)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆ₐ[R] B<GOAL>e.toRingEquiv = ↑e
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>f g : A ≃⋆ₐ[R] B<VAR>h : ∀ (a : A), f a = g a<GOAL>f = g
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>f g : A ≃⋆ₐ[R] B<GOAL>f = g ↔ ∀ (a : A), f a = g a
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>Add A<VAR>Mul A<VAR>SMul R A<VAR>Star A<GOAL>⇑StarAlgEquiv.refl = id
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆ₐ[R] B<GOAL>EquivLike.inv e = ⇑e.symm
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆ₐ[R] B<GOAL>e.symm.symm = e
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<GOAL>Function.Bijective StarAlgEquiv.symm
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>e : A ≃+* B<VAR>h₁ : ∀ (a : A), e.toFun (star a) = star (e.toFun a)<VAR>h₂ : ∀ (r : R) (a : A), e.toFun (r • a) = r • e.toFun a<GOAL>⇑{ toRingEquiv := e, map_star' := h₁, map_smul' := h₂ } = ⇑e
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆ₐ[R] B<VAR>e' : B → A<VAR>h₁ : Function.LeftInverse e' ⇑e<VAR>h₂ : Function.RightInverse e' ⇑e<VAR>h₃ : ∀ (x y : A), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₄ : ∀ (x y : A), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₅ : ∀ (a : A), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (star a) = star ({ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a)<VAR>h₆ : ∀ (r : R) (a : A), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (r • a) = r • { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a<GOAL>{ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅, map_smul' := h₆ } = e
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>f : A → B<VAR>f' : B → A<VAR>h₁ : Function.LeftInverse f' f<VAR>h₂ : Function.RightInverse f' f<VAR>h₃ : ∀ (x y : A), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₄ : ∀ (x y : A), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₅ : ∀ (a : A), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (star a) = star ({ toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a)<VAR>h₆ : ∀ (r : R) (a : A), { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (r • a) = r • { toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a<GOAL>{ toFun := f, invFun := f', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅, map_smul' := h₆ }.symm = let __src := StarAlgEquiv.symm_mk.aux f f' h₁ h₂ h₃ h₄ h₅ h₆; { toFun := f', invFun := f, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, map_star' := ⋯, map_smul' := ⋯ }
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>Add A<VAR>Mul A<VAR>SMul R A<VAR>Star A<GOAL>StarAlgEquiv.refl.symm = StarAlgEquiv.refl
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>f : A ≃⋆ₐ[R] B<GOAL>(↑f).symm = ↑f.symm
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆ₐ[R] B<GOAL>↑e.symm = (↑e).symm
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆ₐ[R] B<VAR>x : B<GOAL>e (e.symm x) = x
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆ₐ[R] B<VAR>x : A<GOAL>e.symm (e x) = x
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>C : Type u_5<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>Add C<VAR>Mul C<VAR>SMul R C<VAR>Star C<VAR>e₁ : A ≃⋆ₐ[R] B<VAR>e₂ : B ≃⋆ₐ[R] C<VAR>x : C<GOAL>(e₁.trans e₂).symm x = e₁.symm (e₂.symm x)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>C : Type u_5<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>Add C<VAR>Mul C<VAR>SMul R C<VAR>Star C<VAR>e₁ : A ≃⋆ₐ[R] B<VAR>e₂ : B ≃⋆ₐ[R] C<GOAL>⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>C : Type u_5<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>Add C<VAR>Mul C<VAR>SMul R C<VAR>Star C<VAR>e₁ : A ≃⋆ₐ[R] B<VAR>e₂ : B ≃⋆ₐ[R] C<VAR>x : A<GOAL>(e₁.trans e₂) x = e₂ (e₁ x)
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆ₐ[R] B<GOAL>Function.LeftInverse ⇑e.symm ⇑e
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>SMul R A<VAR>SMul R B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆ₐ[R] B<GOAL>Function.RightInverse ⇑e.symm ⇑e
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>FunLike G B A<VAR>f : F<VAR>g : G<VAR>h₁ : ∀ (x : A), g (f x) = x<VAR>h₂ : ∀ (x : B), f (g x) = x<VAR>a : B<GOAL>(StarAlgEquiv.ofStarAlgHom f g h₁ h₂).symm a = g a
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>FunLike G B A<VAR>f : F<VAR>g : G<VAR>h₁ : ∀ (x : A), g (f x) = x<VAR>h₂ : ∀ (x : B), f (g x) = x<VAR>a : A<GOAL>(StarAlgEquiv.ofStarAlgHom f g h₁ h₂) a = f a
<VAR>F : Type u_1<VAR>R : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<VAR>hf : Function.Bijective ⇑f<GOAL>⇑(StarAlgEquiv.ofBijective f hf) = ⇑f
<VAR>F : Type u_1<VAR>R : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>Monoid R<VAR>NonUnitalNonAssocSemiring A<VAR>DistribMulAction R A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>DistribMulAction R B<VAR>Star B<VAR>FunLike F A B<VAR>NonUnitalAlgHomClass F R A B<VAR>NonUnitalStarAlgHomClass F R A B<VAR>f : F<VAR>hf : Function.Bijective ⇑f<VAR>a : A<GOAL>(StarAlgEquiv.ofBijective f hf) a = f a
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>self : CategoryTheory.ExactPairing X Y<GOAL>Y ◁ CategoryTheory.ExactPairing.coevaluation' ≫ (α_ Y X Y).inv ≫ CategoryTheory.ExactPairing.evaluation' ▷ Y = (ρ_ Y).hom ≫ (λ_ Y).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>self : CategoryTheory.ExactPairing X Y<GOAL>CategoryTheory.ExactPairing.coevaluation' ▷ X ≫ (α_ X Y X).hom ≫ X ◁ CategoryTheory.ExactPairing.evaluation' = (λ_ X).hom ≫ (ρ_ X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.ExactPairing X Y<GOAL>Y ◁ η_ X Y ≫ (α_ Y X Y).inv ≫ ε_ X Y ▷ Y = (ρ_ Y).hom ≫ (λ_ Y).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.ExactPairing X Y<GOAL>η_ X Y ▷ X ≫ (α_ X Y X).hom ≫ X ◁ ε_ X Y = (λ_ X).hom ≫ (ρ_ X).inv
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.ExactPairing X Y<GOAL>Y ◁ η_ X Y ⊗≫ ε_ X Y ▷ Y = ⊗𝟙
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y : C<VAR>CategoryTheory.ExactPairing X Y<GOAL>η_ X Y ▷ X ⊗≫ X ◁ ε_ X Y = ⊗𝟙
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>CategoryTheory.HasRightDual X<GOAL>ᘁXᘁ = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>CategoryTheory.HasLeftDual X<GOAL>(ᘁX)ᘁ = X
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>CategoryTheory.HasRightDual X<GOAL>𝟙 Xᘁ = 𝟙 Xᘁ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X : C<VAR>CategoryTheory.HasLeftDual X<GOAL>(ᘁ𝟙 X) = 𝟙 ᘁX
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<VAR>CategoryTheory.HasRightDual X<VAR>CategoryTheory.HasRightDual Y<VAR>f : X ⟶ Y<VAR>g : Xᘁ ⟶ Z<GOAL>fᘁ ≫ g = (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ (f ⊗ g) ≫ (α_ Yᘁ Y Z).inv ≫ ε_ Y Yᘁ ▷ Z ≫ (λ_ Z).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<VAR>CategoryTheory.HasLeftDual X<VAR>CategoryTheory.HasLeftDual Y<VAR>f : X ⟶ Y<VAR>g : ᘁX ⟶ Z<GOAL>(ᘁf) ≫ g = (λ_ ᘁY).inv ≫ η_ (ᘁX) X ▷ ᘁY ≫ (g ⊗ f) ▷ ᘁY ≫ (α_ Z Y ᘁY).hom ≫ Z ◁ ε_ (ᘁY) Y ≫ (ρ_ Z).hom
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<VAR>CategoryTheory.HasRightDual X<VAR>CategoryTheory.HasRightDual Y<VAR>CategoryTheory.HasRightDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(f ≫ g)ᘁ = gᘁ ≫ fᘁ
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Z : C<VAR>CategoryTheory.HasLeftDual X<VAR>CategoryTheory.HasLeftDual Y<VAR>CategoryTheory.HasLeftDual Z<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<GOAL>(ᘁf ≫ g) = (ᘁg) ≫ ᘁf
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Y' Z Z' : C<VAR>CategoryTheory.ExactPairing Y Y'<VAR>f : Y' ⊗ X ⟶ Z<VAR>g : Z ⟶ Z'<GOAL>(CategoryTheory.tensorLeftHomEquiv X Y Y' Z') (f ≫ g) = (CategoryTheory.tensorLeftHomEquiv X Y Y' Z) f ≫ Y ◁ g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X X' Y Y' Z : C<VAR>CategoryTheory.ExactPairing Y Y'<VAR>f : X ⟶ X'<VAR>g : X' ⟶ Y ⊗ Z<GOAL>(CategoryTheory.tensorLeftHomEquiv X Y Y' Z).symm (f ≫ g) = Y' ◁ f ≫ (CategoryTheory.tensorLeftHomEquiv X' Y Y' Z).symm g
<VAR>C : Type u₁<VAR>CategoryTheory.Category.{v₁, u₁} C<VAR>CategoryTheory.MonoidalCategory C<VAR>X Y Y' Z Z' : C<VAR>CategoryTheory.ExactPairing Y Y'<VAR>f : X ⊗ Y ⟶ Z<VAR>g : Z ⟶ Z'<GOAL>(CategoryTheory.tensorRightHomEquiv X Y Y' Z') (f ≫ g) = (CategoryTheory.tensorRightHomEquiv X Y Y' Z) f ≫ g ▷ Y'