ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>NonUnitalNonAssocCommRing A<VAR>IsCommJordan A<VAR>a b c : A<GOAL>⁅L a, L (a * a)⁆ + ⁅L a, L (b * b)⁆ + ⁅L a, L (c * c)⁆ + ⁅L a, 2 • L (a * b)⁆ + ⁅L a, 2 • L (c * a)⁆ + ⁅L a, 2 • L (b * c)⁆ + (⁅L b, L (a * a)⁆ + ⁅L b, L (b * b)⁆ + ⁅L b, L (c * c)⁆ + ⁅L b, 2 • L (a * b)⁆ + ⁅L b, 2 • L (c * a)⁆ + ⁅L b, 2 • L (b * c)⁆) + (⁅L c, L (a * a)⁆ + ⁅L c, L (b * b)⁆ + ⁅L c, L (c * c)⁆ + ⁅L c, 2 • L (a * b)⁆ + ⁅L c, 2 • L (c * a)⁆ + ⁅L c, 2 • L (b * c)⁆) = ⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆) + (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (c * a)⁆ + ⁅L c, L (c * a)⁆)) + (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) + (2 • ⁅L a, L (b * c)⁆ + 2 • ⁅L b, L (c * a)⁆ + 2 • ⁅L c, L (a * b)⁆)
<VAR>A : Type u_1<VAR>NonUnitalNonAssocCommRing A<VAR>IsCommJordan A<VAR>a b c : A<GOAL>⁅L a, L (b * b)⁆ + ⁅L b, L (a * a)⁆ + 2 • (⁅L a, L (a * b)⁆ + ⁅L b, L (a * b)⁆) + (⁅L a, L (c * c)⁆ + ⁅L c, L (a * a)⁆ + 2 • (⁅L a, L (c * a)⁆ + ⁅L c, L (c * a)⁆)) + (⁅L b, L (c * c)⁆ + ⁅L c, L (b * b)⁆ + 2 • (⁅L b, L (b * c)⁆ + ⁅L c, L (b * c)⁆)) + (2 • ⁅L a, L (b * c)⁆ + 2 • ⁅L b, L (c * a)⁆ + 2 • ⁅L c, L (a * b)⁆) = 2 • ⁅L a, L (b * c)⁆ + 2 • ⁅L b, L (c * a)⁆ + 2 • ⁅L c, L (a * b)⁆
<VAR>A : Type u_1<VAR>NonUnitalNonAssocCommRing A<VAR>IsCommJordan A<VAR>a b c : A<GOAL>2 • (⁅L a, L (b * c)⁆ + ⁅L b, L (c * a)⁆ + ⁅L c, L (a * b)⁆) = 0
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>module_M : Module R M<VAR>p q : Submodule R M<VAR>h : p = q<VAR>x : ↥p<GOAL>↑((LinearEquiv.ofEq p q h) x) = ↑x
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>module_M : Module R M<VAR>p q : Submodule R M<VAR>h : p = q<GOAL>(LinearEquiv.ofEq p q h).symm = LinearEquiv.ofEq q p ⋯
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>module_M : Module R M<VAR>p : Submodule R M<GOAL>LinearEquiv.ofEq p p ⋯ = LinearEquiv.refl R ↥p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<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>p : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>h : Submodule.map e p = q<VAR>x : ↥p<GOAL>↑((e.ofSubmodules p q h) x) = e ↑x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<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>p : Submodule R M<VAR>q : Submodule R₂ M₂<VAR>h : Submodule.map e p = q<VAR>x : ↥q<GOAL>↑((e.ofSubmodules p q h).symm x) = e.symm ↑x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>f : M ≃ₛₗ[σ₁₂] M₂<VAR>U : Submodule R₂ M₂<GOAL>↑(f.ofSubmodule' U) = LinearMap.codRestrict U ((↑f).domRestrict (Submodule.comap (↑f) U)) ⋯
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>f : M ≃ₛₗ[σ₁₂] M₂<VAR>U : Submodule R₂ M₂<VAR>x : ↥(Submodule.comap (↑f) U)<GOAL>↑((f.ofSubmodule' U) x) = f ↑x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>f : M ≃ₛₗ[σ₁₂] M₂<VAR>U : Submodule R₂ M₂<VAR>x : ↥U<GOAL>↑((f.ofSubmodule' U).symm x) = f.symm ↑x
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>h : p = ⊤<VAR>x : ↥p<GOAL>(LinearEquiv.ofTop p h) x = ↑x
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>h : p = ⊤<VAR>x : M<GOAL>↑((LinearEquiv.ofTop p h).symm x) = x
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>h : p = ⊤<VAR>x : M<GOAL>(LinearEquiv.ofTop p h).symm x = ⟨x, ⋯⟩
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<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₂<GOAL>LinearMap.range ↑e = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>F : Type u_10<VAR>EquivLike F M M₂<VAR>SemilinearEquivClass F σ₁₂ M M₂<VAR>e : F<GOAL>LinearMap.range e = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>module_M : Module R M<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₁ : R₂ →+* R<VAR>re₁₂ : RingHomInvPair σ₁₂ σ₂₁<VAR>re₂₁ : RingHomInvPair σ₂₁ σ₁₂<VAR>p : Submodule R M<VAR>Module R₂ M₂<VAR>e : ↥p ≃ₛₗ[σ₁₂] ↥⊥<GOAL>p = ⊥
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<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>h : M₂ →ₛₗ[σ₂₃] M₃<VAR>RingHomSurjective σ₂₃<VAR>RingHomSurjective σ₁₃<GOAL>LinearMap.range (h.comp ↑e) = LinearMap.range h
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<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>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₁] M<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>h : Function.LeftInverse ⇑g ⇑f<VAR>x : M<GOAL>↑((LinearEquiv.ofLeftInverse h) x) = f x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<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>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₁] M<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>h : Function.LeftInverse ⇑g ⇑f<VAR>x : ↥(LinearMap.range f)<GOAL>(LinearEquiv.ofLeftInverse h).symm x = g ↑x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<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>f : M →ₛₗ[σ₁₂] M₂<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>h : Function.Injective ⇑f<VAR>x : M<GOAL>↑((LinearEquiv.ofInjective f h) x) = f x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<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>f : M →ₛₗ[σ₁₂] M₂<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>hf : Function.Bijective ⇑f<VAR>x : M<GOAL>(LinearEquiv.ofBijective f hf) x = f x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<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>f : M →ₛₗ[σ₁₂] M₂<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>h : Function.Bijective ⇑f<VAR>x : M<GOAL>(LinearEquiv.ofBijective f h).symm (f x) = x
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>q : Submodule R ↥p<VAR>x : ↥q<GOAL>↑((p.equivSubtypeMap q) x) = (p.subtype.domRestrict q) x
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>q : Submodule R ↥p<VAR>x : ↥(Submodule.map p.subtype q)<GOAL>↑↑((p.equivSubtypeMap q).symm x) = ↑x
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>N : Type u_9<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>AddCommMonoid N<VAR>Module R N<VAR>f : M →ₗ[R] N<VAR>p : Submodule R N<VAR>hf : Function.Injective ⇑f<VAR>h : p ≤ LinearMap.range f<GOAL>∀ (a : ↥(Submodule.comap f p)), (Submodule.comap_equiv_self_of_inj_of_le hf h) a = (LinearMap.codRestrict p (f ∘ₗ (Submodule.comap f p).subtype) ⋯) a
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>A : Type u_1<VAR>SetLike A M<VAR>AddSubmonoidClass A M<VAR>SMulMemClass A R M<VAR>S' : A<GOAL>⇑(SMulMemClass.subtype S') = Subtype.val
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>x : ↥p<GOAL>p.subtype x = ↑x
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>module_M : Module R M<VAR>p : Submodule R M<GOAL>⇑p.subtype = Subtype.val
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>module_M : Module R M<VAR>p : Submodule R M<GOAL>Function.Injective ⇑p.subtype
<VAR>R : Type u<VAR>M : Type v<VAR>ι : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>x : ι → ↥p<VAR>s : Finset ι<GOAL>↑(∑ i ∈ s, x i) = ∑ i ∈ s, ↑(x i)
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>p : Submodule R M<VAR>x : ↥p<GOAL>(f.domRestrict p) x = f ↑x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>p : Submodule R₂ M₂<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>h : ∀ (c : M), f c ∈ p<VAR>x : M<GOAL>↑((LinearMap.codRestrict p f h) x) = f x
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Semiring R<VAR>Semiring R₂<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>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>g : M₂ →ₛₗ[σ₂₃] M₃<VAR>p : Submodule R₃ M₃<VAR>h : ∀ (b : M₂), g b ∈ p<GOAL>(LinearMap.codRestrict p g h).comp f = LinearMap.codRestrict p (g.comp f) ⋯
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>f : M →ₛₗ[σ₁₂] M₂<VAR>p : Submodule R₂ M₂<VAR>h : ∀ (b : M), f b ∈ p<GOAL>p.subtype.comp (LinearMap.codRestrict p f h) = f
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₁<VAR>Module R M<VAR>Module R M₁<VAR>f : M →ₗ[R] M₁<VAR>p : Submodule R M<VAR>q : Submodule R M₁<VAR>hf : ∀ x ∈ p, f x ∈ q<VAR>x : ↥p<GOAL>↑((f.restrict hf) x) = f ↑x
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₁<VAR>Module R M<VAR>Module R M₁<VAR>f : M →ₗ[R] M₁<VAR>p : Submodule R M<VAR>q : Submodule R M₁<VAR>hf : ∀ x ∈ p, f x ∈ q<VAR>x : ↥p<GOAL>(f.restrict hf) x = ⟨f ↑x, ⋯⟩
<VAR>R : Type u_10<VAR>M : Type u_11<VAR>M₁ : Type u_12<VAR>Ring R<VAR>AddCommGroup M<VAR>AddCommGroup M₁<VAR>Module R M<VAR>Module R M₁<VAR>p : Submodule R M<VAR>q : Submodule R M₁<VAR>f g : M →ₗ[R] M₁<VAR>hf : Set.MapsTo ⇑f ↑p ↑q<VAR>hg : Set.MapsTo ⇑g ↑p ↑q<VAR>hfg : Set.MapsTo ⇑(f - g) ↑p ↑q := ⋯<GOAL>f.restrict hf - g.restrict hg = (f - g).restrict hfg
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>M₂ : Type u_10<VAR>M₃ : Type u_11<VAR>AddCommMonoid M₂<VAR>AddCommMonoid M₃<VAR>Module R M₂<VAR>Module R M₃<VAR>p : Submodule R M<VAR>p₂ : Submodule R M₂<VAR>p₃ : Submodule R M₃<VAR>f : M →ₗ[R] M₂<VAR>g : M₂ →ₗ[R] M₃<VAR>hf : Set.MapsTo ⇑f ↑p ↑p₂<VAR>hg : Set.MapsTo ⇑g ↑p₂ ↑p₃<VAR>hfg : Set.MapsTo ⇑(g ∘ₗ f) ↑p ↑p₃ := ⋯<GOAL>(g ∘ₗ f).restrict hfg = g.restrict hg ∘ₗ f.restrict hf
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f g : M →ₗ[R] M<VAR>h : Commute f g<VAR>p : Submodule R M<VAR>hf : Set.MapsTo ⇑f ↑p ↑p<VAR>hg : Set.MapsTo ⇑g ↑p ↑p<GOAL>Commute (f.restrict hf) (g.restrict hg)
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₁<VAR>Module R M<VAR>Module R M₁<VAR>f : M →ₗ[R] M₁<VAR>p : Submodule R M<VAR>q : Submodule R M₁<VAR>hf : ∀ x ∈ p, f x ∈ q<GOAL>q.subtype ∘ₗ f.restrict hf = f.domRestrict p
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₁<VAR>Module R M<VAR>Module R M₁<VAR>f : M →ₗ[R] M₁<VAR>p : Submodule R M<VAR>q : Submodule R M₁<VAR>hf : ∀ x ∈ p, f x ∈ q<GOAL>f.restrict hf = LinearMap.codRestrict q (f.domRestrict p) ⋯
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₁<VAR>Module R M<VAR>Module R M₁<VAR>f : M →ₗ[R] M₁<VAR>p : Submodule R M<VAR>q : Submodule R M₁<VAR>hf : ∀ (x : M), f x ∈ q<GOAL>f.restrict ⋯ = (LinearMap.codRestrict q f hf).domRestrict p
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>ι : Type u_9<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>t : Finset ι<VAR>f : ι → M →ₛₗ[σ₁₂] M₂<VAR>b : M<GOAL>(∑ d ∈ t, f d) b = ∑ d ∈ t, (f d) b
<VAR>R : Type u_1<VAR>R₂ : Type u_3<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>σ₁₂ : R →+* R₂<VAR>ι : Type u_10<VAR>t : Finset ι<VAR>f : ι → M →ₛₗ[σ₁₂] M₂<GOAL>⇑(∑ i ∈ t, f i) = ∑ i ∈ t, ⇑(f i)
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>N : Submodule R M<VAR>g : Module.End R ↥N<VAR>G : Module.End R M<VAR>h : G ∘ₗ N.subtype = N.subtype ∘ₗ g<VAR>k : ℕ<VAR>hG : G ^ k = 0<GOAL>g ^ k = 0
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f' : M →ₗ[R] M<VAR>p : Submodule R M<VAR>n : ℕ<VAR>h : ∀ x ∈ p, f' x ∈ p<VAR>x : M<VAR>hx : x ∈ p<GOAL>(f' ^ n) x ∈ p
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>f' : M →ₗ[R] M<VAR>p : Submodule R M<VAR>n : ℕ<VAR>h : ∀ x ∈ p, f' x ∈ p<VAR>h' : ∀ x ∈ p, (f' ^ n) x ∈ p := ⋯<GOAL>f'.restrict h ^ n = (f' ^ n).restrict h'
<VAR>R : Type u_1<VAR>M : Type u_5<VAR>M₂ : Type u_7<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : M →ₗ[R] M₂<VAR>p : Submodule R M<VAR>x : ↥p<GOAL>((LinearMap.domRestrict' p) f) x = f ↑x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<VAR>h : p ≤ p'<VAR>x : ↥p<GOAL>↑((Submodule.inclusion h) x) = ↑x
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<VAR>h : p ≤ p'<VAR>x : ↥p<GOAL>(Submodule.inclusion h) x = ⟨↑x, ⋯⟩
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<VAR>h : p ≤ p'<GOAL>Function.Injective ⇑(Submodule.inclusion h)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<VAR>h : p ≤ q<GOAL>q.subtype ∘ₗ Submodule.inclusion h = p.subtype
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>↑⊥ = {0}
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⊥.toAddSubmonoid = ⊥
<VAR>R : Type u_4<VAR>M : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>⊥.toAddSubgroup = ⊥
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>x ∈ ⊥ ↔ x = 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<GOAL>p = ⊥ ↔ ∀ x ∈ p, x = 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x y : ↥⊥<GOAL>x = y
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<GOAL>p ≠ ⊥ ↔ ∃ x ∈ p, x ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>bot_lt : ⊥ < p<GOAL>∃ a, a ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>h : p ≠ ⊥<GOAL>∃ b ∈ p, b ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>∀ (x : ↥⊥), Submodule.botEquivPUnit x = PUnit.unit
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>∀ (x : PUnit.{v + 1}), Submodule.botEquivPUnit.symm x = 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Subsingleton ↥p ↔ p = ⊥
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>Subsingleton ↥p<GOAL>p = ⊥
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<GOAL>Nontrivial ↥p ↔ p ≠ ⊥
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>↑⊤ = Set.univ
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⊤.toAddSubmonoid = ⊤
<VAR>R : Type u_4<VAR>M : Type u_5<VAR>Ring R<VAR>AddCommGroup M<VAR>Module R M<GOAL>⊤.toAddSubgroup = ⊤
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>x ∈ ⊤
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<GOAL>p = ⊤ ↔ ∀ (x : M), x ∈ p
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>↑(Submodule.topEquiv.symm x) = x
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : ↥⊤<GOAL>Submodule.topEquiv x = ↑x
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Set (Submodule R M)<VAR>p : Submodule R M<GOAL>p ∈ S → sInf S ≤ p
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Set (Submodule R M)<VAR>p : Submodule R M<GOAL>(∀ q ∈ S, p ≤ q) → p ≤ sInf S
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<GOAL>↑(p ⊓ q) = ↑p ∩ ↑q
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<VAR>x : M<GOAL>x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>P : Set (Submodule R M)<GOAL>↑(sInf P) = ⋂ p ∈ P, ↑p
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>p : ι → Submodule R M<GOAL>↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_4<VAR>p : ι → Submodule R M<GOAL>↑(⨅ i, p i) = ⋂ i, ↑(p i)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Set (Submodule R M)<VAR>x : M<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_4<VAR>p : ι → Submodule R M<VAR>x : M<GOAL>x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>p : ι → Submodule R M<VAR>x : M<GOAL>x ∈ s.inf p ↔ ∀ i ∈ s, x ∈ p i
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S T : Submodule R M<VAR>x : M<GOAL>x ∈ S → x ∈ S ⊔ T
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S T : Submodule R M<VAR>x : M<GOAL>x ∈ T → x ∈ S ⊔ T
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S T : Submodule R M<VAR>s t : M<VAR>hs : s ∈ S<VAR>ht : t ∈ T<GOAL>s + t ∈ S ⊔ T
<VAR>R' : Type u_4<VAR>M' : Type u_5<VAR>Ring R'<VAR>AddCommGroup M'<VAR>Module R' M'<VAR>S T : Submodule R' M'<VAR>s t : M'<VAR>hs : s ∈ S<VAR>ht : t ∈ T<GOAL>s - t ∈ S ⊔ T
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Sort u_4<VAR>b : M<VAR>p : ι → Submodule R M<VAR>i : ι<VAR>h : b ∈ p i<GOAL>b ∈ ⨆ i, p i
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>Fintype ι<VAR>f : ι → M<VAR>p : ι → Submodule R M<VAR>h : ∀ (i : ι), f i ∈ p i<GOAL>∑ i : ι, f i ∈ ⨆ i, p i
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>f : ι → M<VAR>p : ι → Submodule R M<VAR>h : ∀ i ∈ s, f i ∈ p i<GOAL>∑ i ∈ s, f i ∈ ⨆ i ∈ s, p i
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Set (Submodule R M)<VAR>s : Submodule R M<VAR>hs : s ∈ S<VAR>x : M<GOAL>x ∈ s → x ∈ sSup S
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>s : Set (Submodule R M)<GOAL>(sSup s).toAddSubmonoid = sSup (Submodule.toAddSubmonoid '' s)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Subsingleton (Submodule R M) ↔ Subsingleton M
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Nontrivial (Submodule R M) ↔ Nontrivial M
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<GOAL>Disjoint p p' ↔ ∀ x ∈ p, x ∈ p' → x = 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<GOAL>Disjoint p p' ↔ ∀ x ∈ p, ∀ y ∈ p', x = y → x = 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<VAR>hpq : Disjoint p q<VAR>a : ↥p<VAR>ha : ↑a ∈ q<GOAL>a = 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<VAR>h : Disjoint p p'<VAR>x : ↥p<GOAL>↑x ∈ p' ↔ x = 0
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p p' : Submodule R M<VAR>h : Disjoint p p'<VAR>x : ↥p'<GOAL>↑x ∈ p ↔ x = 0
<VAR>M : Type u_3<VAR>AddCommMonoid M<GOAL>⇑AddSubmonoid.toNatSubmodule.symm = Submodule.toAddSubmonoid
<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<GOAL>↑(AddSubmonoid.toNatSubmodule S) = ↑S
<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>S : AddSubmonoid M<GOAL>(AddSubmonoid.toNatSubmodule S).toAddSubmonoid = S
<VAR>M : Type u_3<VAR>AddCommMonoid M<VAR>S : Submodule ℕ M<GOAL>AddSubmonoid.toNatSubmodule S.toAddSubmonoid = S
<VAR>M : Type u_3<VAR>AddCommGroup M<GOAL>⇑AddSubgroup.toIntSubmodule.symm = Submodule.toAddSubgroup
<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>S : AddSubgroup M<GOAL>↑(AddSubgroup.toIntSubmodule S) = ↑S
<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>S : AddSubgroup M<GOAL>(AddSubgroup.toIntSubmodule S).toAddSubgroup = S
<VAR>M : Type u_3<VAR>AddCommGroup M<VAR>S : Submodule ℤ M<GOAL>AddSubgroup.toIntSubmodule S.toAddSubgroup = S
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>Semiring R<VAR>Semiring R₂<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>F : Type u_11<VAR>FunLike F M M₂<VAR>SemilinearMapClass F τ₁₂ M M₂<VAR>RingHomSurjective τ₁₂<VAR>f : F<GOAL>↑(LinearMap.range f) = Set.range ⇑f