ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<GOAL>(LieAlgebra.IsKilling.rootSystem H).IsCrystallographic
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>Field K<VAR>CharZero K<VAR>LieRing L<VAR>LieAlgebra K L<VAR>LieAlgebra.IsKilling K L<VAR>FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>H.IsCartanSubalgebra<VAR>LieModule.IsTriangularizable K (↥H) L<GOAL>(LieAlgebra.IsKilling.rootSystem H).IsReduced
<VAR>F : Type u_17<VAR>R : outParam (Type u_18)<VAR>S : outParam (Type u_19)<VAR>Semiring R<VAR>Semiring S<VAR>σ : outParam (R →+* S)<VAR>σ' : outParam (S →+* R)<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>M : outParam (Type u_20)<VAR>M₂ : outParam (Type u_21)<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module S M₂<VAR>EquivLike F M M₂<VAR>self : SemilinearEquivClass F σ M M₂<VAR>f : F<VAR>r : R<VAR>x : M<GOAL>f (r • x) = σ r • f x
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<GOAL>Function.Injective LinearEquiv.toEquiv
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>e₁ e₂ : M ≃ₛₗ[σ] M₂<GOAL>e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<GOAL>Function.Injective LinearEquiv.toLinearMap
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>e₁ e₂ : M ≃ₛₗ[σ] M₂<GOAL>↑e₁ = ↑e₂ ↔ e₁ = e₂
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<VAR>to_fun : M → M₂<VAR>inv_fun : M₂ → M<VAR>map_add : ∀ (x y : M), to_fun (x + y) = to_fun x + to_fun y<VAR>map_smul : ∀ (m : R) (x : M), { toFun := to_fun, map_add' := map_add }.toFun (m • x) = σ m • { toFun := to_fun, map_add' := map_add }.toFun x<VAR>left_inv : Function.LeftInverse inv_fun { toFun := to_fun, map_add' := map_add, map_smul' := map_smul }.toFun<VAR>right_inv : Function.RightInverse inv_fun { toFun := to_fun, map_add' := map_add, map_smul' := map_smul }.toFun<GOAL>⇑{ toFun := to_fun, map_add' := map_add, map_smul' := map_smul, invFun := inv_fun, left_inv := left_inv, right_inv := right_inv } = to_fun
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>RingHomInvPair σ σ'<VAR>RingHomInvPair σ' σ<GOAL>Function.Injective CoeFun.coe
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<GOAL>⇑↑e = ⇑e
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<GOAL>⇑e.toEquiv = ⇑e
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<GOAL>(↑e).toFun = ⇑e
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e e' : M ≃ₛₗ[σ] M₂<VAR>h : ∀ (x : M), e x = e' x<GOAL>e = e'
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e e' : M ≃ₛₗ[σ] M₂<GOAL>e = e' ↔ ∀ (x : M), e x = e' x
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>x x' : M<GOAL>x = x' → e x = e x'
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e e' : M ≃ₛₗ[σ] M₂<VAR>h : e = e'<VAR>x : M<GOAL>e x = e' x
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>(LinearEquiv.refl R M) x = x
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<GOAL>e.invFun = ⇑e.symm
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<GOAL>e.toEquiv.symm = ↑e.symm
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<GOAL>e.toAddEquiv = ↑e
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<GOAL>(↑e).toAddMonoidHom = e.toAddEquiv.toAddMonoidHom
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₂₁ : R₂ →+* R₁<VAR>σ₃₂ : R₃ →+* R₂<VAR>σ₃₁ : R₃ →+* R₁<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₃ : RingHomInvPair σ₂₃ σ₃₂<VAR>RingHomInvPair σ₁₃ σ₃₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>re₃₂ : RingHomInvPair σ₃₂ σ₂₃<VAR>RingHomInvPair σ₃₁ σ₁₃<VAR>e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂<VAR>e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃<VAR>c : M₁<GOAL>(e₁₂.trans e₂₃) c = e₂₃ (e₁₂ c)
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₂₁ : R₂ →+* R₁<VAR>σ₃₂ : R₃ →+* R₂<VAR>σ₃₁ : R₃ →+* R₁<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₃ : RingHomInvPair σ₂₃ σ₃₂<VAR>RingHomInvPair σ₁₃ σ₃₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>re₃₂ : RingHomInvPair σ₃₂ σ₂₃<VAR>RingHomInvPair σ₃₁ σ₁₃<VAR>e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂<VAR>e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃<GOAL>↑(e₁₂.trans e₂₃) = (↑e₂₃).comp ↑e₁₂
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>c : M₂<GOAL>e (e.symm c) = c
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>b : M<GOAL>e.symm (e b) = b
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₂₁ : R₂ →+* R₁<VAR>σ₃₂ : R₃ →+* R₂<VAR>σ₃₁ : R₃ →+* R₁<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₃ : RingHomInvPair σ₂₃ σ₃₂<VAR>RingHomInvPair σ₁₃ σ₃₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>re₃₂ : RingHomInvPair σ₃₂ σ₂₃<VAR>RingHomInvPair σ₃₁ σ₁₃<VAR>e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂<VAR>e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃<GOAL>(e₁₂.trans e₂₃).symm = e₂₃.symm.trans e₁₂.symm
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₂₁ : R₂ →+* R₁<VAR>σ₃₂ : R₃ →+* R₂<VAR>σ₃₁ : R₃ →+* R₁<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₃ : RingHomInvPair σ₂₃ σ₃₂<VAR>RingHomInvPair σ₁₃ σ₃₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>re₃₂ : RingHomInvPair σ₃₂ σ₂₃<VAR>RingHomInvPair σ₃₁ σ₁₃<VAR>e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂<VAR>e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃<VAR>c : M₃<GOAL>(e₁₂.trans e₂₃).symm c = e₁₂.symm (e₂₃.symm c)
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<GOAL>e.trans (LinearEquiv.refl S M₂) = e
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<GOAL>(LinearEquiv.refl R M).trans e = e
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>x : M₂<VAR>y : M<GOAL>e.symm x = y ↔ x = e y
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>x : M₂<VAR>y : M<GOAL>y = e.symm x ↔ e y = x
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>Semiring R₁<VAR>Semiring R₂<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂<VAR>α : Type u_18<VAR>f : M₂ → α<VAR>g : M₁ → α<GOAL>f = g ∘ ⇑e₁₂.symm ↔ f ∘ ⇑e₁₂ = g
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>Semiring R₁<VAR>Semiring R₂<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂<VAR>α : Type u_18<VAR>f : M₂ → α<VAR>g : M₁ → α<GOAL>g ∘ ⇑e₁₂.symm = f ↔ g = f ∘ ⇑e₁₂
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>Semiring R₁<VAR>Semiring R₂<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂<VAR>α : Type u_18<VAR>f : α → M₁<VAR>g : α → M₂<GOAL>f = ⇑e₁₂.symm ∘ g ↔ ⇑e₁₂ ∘ f = g
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>Semiring R₁<VAR>Semiring R₂<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂<VAR>α : Type u_18<VAR>f : α → M₁<VAR>g : α → M₂<GOAL>⇑e₁₂.symm ∘ g = f ↔ g = ⇑e₁₂ ∘ f
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂<VAR>RingHomCompTriple σ₂₁ σ₁₃ σ₂₃<VAR>f : M₂ →ₛₗ[σ₂₃] M₃<VAR>g : M₁ →ₛₗ[σ₁₃] M₃<GOAL>f = g.comp ↑e₁₂.symm ↔ f.comp ↑e₁₂ = g
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₂₁ : R₂ →+* R₁<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂<VAR>RingHomCompTriple σ₂₁ σ₁₃ σ₂₃<VAR>f : M₂ →ₛₗ[σ₂₃] M₃<VAR>g : M₁ →ₛₗ[σ₁₃] M₃<GOAL>g.comp ↑e₁₂.symm = f ↔ g = f.comp ↑e₁₂
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>σ₃₂ : R₃ →+* R₂<VAR>σ₃₁ : R₃ →+* R₁<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂<VAR>RingHomCompTriple σ₃₁ σ₁₂ σ₃₂<VAR>f : M₃ →ₛₗ[σ₃₁] M₁<VAR>g : M₃ →ₛₗ[σ₃₂] M₂<GOAL>f = (↑e₁₂.symm).comp g ↔ (↑e₁₂).comp f = g
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>Semiring R₁<VAR>Semiring R₂<VAR>Semiring R₃<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>module_M₃ : Module R₃ M₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>σ₃₂ : R₃ →+* R₂<VAR>σ₃₁ : R₃ →+* R₁<VAR>RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂<VAR>RingHomCompTriple σ₃₁ σ₁₂ σ₃₂<VAR>f : M₃ →ₛₗ[σ₃₁] M₁<VAR>g : M₃ →ₛₗ[σ₃₂] M₂<GOAL>(↑e₁₂.symm).comp g = f ↔ g = (↑e₁₂).comp f
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>(LinearEquiv.refl R M).symm = LinearEquiv.refl R M
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>Semiring R₁<VAR>Semiring R₂<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>f : M₁ ≃ₛₗ[σ₁₂] M₂<GOAL>f.trans f.symm = LinearEquiv.refl R₁ M₁
<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>M₁ : Type u_9<VAR>M₂ : Type u_10<VAR>Semiring R₁<VAR>Semiring R₂<VAR>AddCommMonoid M₁<VAR>AddCommMonoid M₂<VAR>module_M₁ : Module R₁ M₁<VAR>module_M₂ : Module R₂ M₂<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>f : M₁ ≃ₛₗ[σ₁₂] M₂<GOAL>f.symm.trans f = LinearEquiv.refl R₂ M₂
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>↑(LinearEquiv.refl R M) = LinearMap.id
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module R M₂<VAR>Module R M₃<VAR>f : M ≃ₗ[R] M₂<VAR>f' : M₂ ≃ₗ[R] M₃<GOAL>↑f' ∘ₗ ↑f = ↑(f ≪≫ₗ f')
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>f : M₂ → M<VAR>h₁ : Function.LeftInverse f (↑e).toFun<VAR>h₂ : Function.RightInverse f (↑e).toFun<GOAL>{ toLinearMap := ↑e, invFun := f, left_inv := h₁, right_inv := h₂ } = e
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>a b : M<GOAL>e (a + b) = e a + e b
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<GOAL>e 0 = 0
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>c : R<VAR>x : M<GOAL>e (c • x) = σ c • e x
<VAR>R₁ : Type u_2<VAR>N₁ : Type u_12<VAR>N₂ : Type u_13<VAR>Semiring R₁<VAR>AddCommMonoid N₁<VAR>AddCommMonoid N₂<VAR>module_N₁ : Module R₁ N₁<VAR>module_N₂ : Module R₁ N₂<VAR>e : N₁ ≃ₗ[R₁] N₂<VAR>c : R₁<VAR>x : N₁<GOAL>e (c • x) = c • e x
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>x : M<GOAL>e x = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>x : M<GOAL>e x ≠ 0 ↔ x ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<GOAL>e.symm.symm = e
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>Module R M<VAR>Module S M₂<VAR>RingHomInvPair σ' σ<VAR>RingHomInvPair σ σ'<GOAL>Function.Bijective LinearEquiv.symm
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>f : M₂ → M<VAR>h₁ : ∀ (x y : M₂), f (x + y) = f x + f y<VAR>h₂ : ∀ (m : S) (x : M₂), { toFun := f, map_add' := h₁ }.toFun (m • x) = σ' m • { toFun := f, map_add' := h₁ }.toFun x<VAR>h₃ : Function.LeftInverse ⇑e { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun<VAR>h₄ : Function.RightInverse ⇑e { toFun := f, map_add' := h₁, map_smul' := h₂ }.toFun<GOAL>{ toFun := f, map_add' := h₁, map_smul' := h₂, invFun := ⇑e, left_inv := h₃, right_inv := h₄ } = e.symm
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<VAR>f : M₂ → M<VAR>h₁ : ∀ (x y : M), e (x + y) = e x + e y<VAR>h₂ : ∀ (m : R) (x : M), { toFun := ⇑e, map_add' := h₁ }.toFun (m • x) = σ m • { toFun := ⇑e, map_add' := h₁ }.toFun x<VAR>h₃ : Function.LeftInverse f { toFun := ⇑e, map_add' := h₁, map_smul' := h₂ }.toFun<VAR>h₄ : Function.RightInverse f { toFun := ⇑e, map_add' := h₁, map_smul' := h₂ }.toFun<GOAL>{ toFun := ⇑e, map_add' := h₁, map_smul' := h₂, invFun := f, left_inv := h₃, right_inv := h₄ }.symm = let __src := LinearEquiv.symm_mk.aux e f h₁ h₂ h₃ h₄; { toFun := f, map_add' := ⋯, map_smul' := ⋯, invFun := ⇑e, left_inv := ⋯, right_inv := ⋯ }
<VAR>R : Type u_1<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>to_fun : M → M₂<VAR>inv_fun : M₂ → M<VAR>map_add : ∀ (x y : M), to_fun (x + y) = to_fun x + to_fun y<VAR>map_smul : ∀ (m : R) (x : M), { toFun := to_fun, map_add' := map_add }.toFun (m • x) = (RingHom.id R) m • { toFun := to_fun, map_add' := map_add }.toFun x<VAR>left_inv : Function.LeftInverse inv_fun { toFun := to_fun, map_add' := map_add, map_smul' := map_smul }.toFun<VAR>right_inv : Function.RightInverse inv_fun { toFun := to_fun, map_add' := map_add, map_smul' := map_smul }.toFun<GOAL>⇑{ toFun := to_fun, map_add' := map_add, map_smul' := map_smul, invFun := inv_fun, left_inv := left_inv, right_inv := right_inv }.symm = inv_fun
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<GOAL>Function.Bijective ⇑e
<VAR>R : Type u_1<VAR>S : Type u_7<VAR>M : Type u_8<VAR>M₂ : Type u_10<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>module_S_M₂ : Module S M₂<VAR>σ : R →+* S<VAR>σ' : S →+* R<VAR>re₁ : RingHomInvPair σ σ'<VAR>re₂ : RingHomInvPair σ' σ<VAR>e : M ≃ₛₗ[σ] M₂<GOAL>Function.Injective ⇑e