ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>x : M<GOAL>x ∈ p.toAddSubmonoid ↔ x ∈ p
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : AddSubmonoid M<VAR>x : M<VAR>h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier<GOAL>x ∈ { toAddSubmonoid := S, smul_mem' := h } ↔ x ∈ S
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : AddSubmonoid M<VAR>h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier<GOAL>↑{ toAddSubmonoid := S, smul_mem' := h } = ↑S
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<VAR>h : ∀ (c : R) {x : M}, x ∈ p.carrier → c • x ∈ p.carrier<GOAL>{ toAddSubmonoid := p.toAddSubmonoid, smul_mem' := h } = p
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S S' : AddSubmonoid M<VAR>h : ∀ (c : R) {x : M}, x ∈ S.carrier → c • x ∈ S.carrier<VAR>h' : ∀ (c : R) {x : M}, x ∈ S'.carrier → c • x ∈ S'.carrier<GOAL>{ toAddSubmonoid := S, smul_mem' := h } ≤ { toAddSubmonoid := S', smul_mem' := h' } ↔ S ≤ S'
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<VAR>h : ∀ (x : M), x ∈ p ↔ x ∈ q<GOAL>p = q
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<GOAL>p.carrier = q.carrier ↔ p = q
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Submodule R M<VAR>s : Set M<VAR>hs : s = ↑S<GOAL>↑(S.copy s hs) = s
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>S : Submodule R M<VAR>s : Set M<VAR>hs : s = ↑S<GOAL>S.copy s hs = S
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Function.Injective Submodule.toAddSubmonoid
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<GOAL>p.toAddSubmonoid = q.toAddSubmonoid ↔ p = q
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>StrictMono Submodule.toAddSubmonoid
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<GOAL>p.toAddSubmonoid ≤ q.toAddSubmonoid ↔ p ≤ q
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Monotone Submodule.toAddSubmonoid
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<GOAL>↑p.toAddSubmonoid = ↑p
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Function.Injective Submodule.toSubMulAction
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p q : Submodule R M<GOAL>p.toSubMulAction = q.toSubMulAction ↔ p = q
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>StrictMono Submodule.toSubMulAction
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>Monotone Submodule.toSubMulAction
<VAR>R : Type u<VAR>M : Type v<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>p : Submodule R M<GOAL>↑p.toSubMulAction = ↑p
<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 : M<GOAL>x ∈ p.carrier ↔ x ∈ ↑p
<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>0 ∈ p
<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 y : M<VAR>h₁ : x ∈ p<VAR>h₂ : y ∈ p<GOAL>x + y ∈ p
<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 : M<VAR>r : R<VAR>h : x ∈ p<GOAL>r • x ∈ p
<VAR>S : Type u'<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 : M<VAR>SMul S R<VAR>SMul S M<VAR>IsScalarTower S R M<VAR>r : S<VAR>h : x ∈ p<GOAL>r • x ∈ p
<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>t : Finset ι<VAR>f : ι → M<GOAL>(∀ c ∈ t, f c ∈ p) → ∑ i ∈ t, f i ∈ p
<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>t : Finset ι<VAR>f : ι → M<VAR>r : ι → R<VAR>hyp : ∀ c ∈ t, f c ∈ p<GOAL>∑ i ∈ t, r i • f i ∈ p
<VAR>G : Type u''<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 : M<VAR>Group G<VAR>MulAction G M<VAR>SMul G R<VAR>IsScalarTower G R M<VAR>g : G<GOAL>g • x ∈ p ↔ x ∈ p
<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).Nonempty
<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 : M<VAR>h : x ∈ p<GOAL>⟨x, h⟩ = 0 ↔ x = 0
<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>↑x = 0 ↔ x = 0
<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 y : ↥p<GOAL>↑(x + y) = ↑x + ↑y
<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>↑0 = 0
<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>r : R<VAR>x : ↥p<GOAL>↑(r • x) = r • ↑x
<VAR>S : Type u'<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>SMul S R<VAR>SMul S M<VAR>IsScalarTower S R M<VAR>r : S<VAR>x : ↥p<GOAL>↑(r • x) = r • ↑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<VAR>x : M<VAR>hx : x ∈ p<GOAL>↑⟨x, hx⟩ = 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<VAR>x : ↥p<GOAL>↑x ∈ p
<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>α : Type u_1<VAR>VAdd M α<VAR>g : ↥p<VAR>m : α<GOAL>g +ᵥ m = ↑g +ᵥ m
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>x : M<VAR>hx : x ∈ p<GOAL>-x ∈ p
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<VAR>p : Submodule R M<GOAL>↑p.toAddSubgroup = ↑p
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>x : M<GOAL>x ∈ p.toAddSubgroup ↔ x ∈ p
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<GOAL>Function.Injective Submodule.toAddSubgroup
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<VAR>p p' : Submodule R M<GOAL>p.toAddSubgroup = p'.toAddSubgroup ↔ p = p'
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<GOAL>StrictMono Submodule.toAddSubgroup
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<VAR>p p' : Submodule R M<GOAL>p.toAddSubgroup ≤ p'.toAddSubgroup ↔ p ≤ p'
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<GOAL>Monotone Submodule.toAddSubgroup
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>x y : M<GOAL>x ∈ p → y ∈ p → x - y ∈ p
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>x : M<GOAL>-x ∈ p ↔ x ∈ p
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>x y : M<GOAL>y ∈ p → (x + y ∈ p ↔ x ∈ p)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>x y : M<GOAL>x ∈ p → (x + y ∈ p ↔ y ∈ p)
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>x : ↥p<GOAL>↑(-x) = -↑x
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>x y : ↥p<GOAL>↑(x - y) = ↑x - ↑y
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>x y : M<VAR>hy : y ∈ p<GOAL>x - y ∈ p ↔ x ∈ p
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<VAR>p : Submodule R M<VAR>x y : M<VAR>hx : x ∈ p<GOAL>x - y ∈ p ↔ y ∈ p
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>AddCommGroup M<VAR>module_M : Module R M<VAR>p : Submodule R M<GOAL>-↑p = ↑p
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>IsDomain R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>N : Submodule R M<VAR>ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0<GOAL>x ∉ N
<VAR>R : Type u<VAR>M : Type v<VAR>Ring R<VAR>IsDomain R<VAR>AddCommGroup M<VAR>Module R M<VAR>x : M<VAR>N : Submodule R M<VAR>ortho : ∀ (c : R), ∀ y ∈ N, c • x + y = 0 → c = 0<GOAL>x ≠ 0
<VAR>S : Type u'<VAR>R : Type u<VAR>M : Type v<VAR>DivisionSemiring S<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>SMul S R<VAR>Module S M<VAR>IsScalarTower S R M<VAR>p : Submodule R M<VAR>s : S<VAR>x : M<VAR>s0 : s ≠ 0<GOAL>s • x ∈ p ↔ x ∈ p
<VAR>A : Type uA<VAR>AddCommGroup A<VAR>c c' : CharacterModule A<VAR>h : ∀ (x : A), c x = c' x<GOAL>c = c'
<VAR>R : Type uR<VAR>CommRing R<VAR>A : Type uA<VAR>AddCommGroup A<VAR>Module R A<VAR>c : CharacterModule A<VAR>r : R<VAR>a : A<GOAL>(r • c) a = c (r • a)
<VAR>R : Type uR<VAR>CommRing R<VAR>A : Type uA<VAR>AddCommGroup A<VAR>B : Type uB<VAR>AddCommGroup B<VAR>Module R A<VAR>Module R B<VAR>f : A →ₗ[R] B<VAR>L : CharacterModule B<GOAL>(CharacterModule.dual f) L = AddMonoidHom.comp L f.toAddMonoidHom
<VAR>R : Type uR<VAR>CommRing R<VAR>A : Type uA<VAR>AddCommGroup A<VAR>B : Type uB<VAR>AddCommGroup B<VAR>Module R A<VAR>Module R B<VAR>f : A →ₗ[R] B<VAR>hf : Function.Injective ⇑f<GOAL>Function.Surjective ⇑(CharacterModule.dual f)
<VAR>R : Type uR<VAR>CommRing R<VAR>A : Type uA<VAR>AddCommGroup A<VAR>B : Type uB<VAR>AddCommGroup B<VAR>Module R A<VAR>Module R B<VAR>c : A →ₗ[R] CharacterModule B<GOAL>CharacterModule.uncurry c = TensorProduct.liftAddHom c.toAddMonoidHom ⋯
<VAR>R : Type uR<VAR>CommRing R<VAR>A : Type uA<VAR>AddCommGroup A<VAR>B : Type uB<VAR>AddCommGroup B<VAR>Module R A<VAR>Module R B<VAR>c : CharacterModule (TensorProduct R A B)<GOAL>∀ (x : A), (CharacterModule.curry c) x = AddMonoidHom.comp c ↑((TensorProduct.mk R A B) x)
<VAR>R : Type uR<VAR>CommRing R<VAR>A : Type uA<VAR>AddCommGroup A<VAR>B : Type uB<VAR>AddCommGroup B<VAR>Module R A<VAR>Module R B<VAR>c : A →ₗ[R] CharacterModule B<VAR>x : (addConGen (TensorProduct.Eqv R A B)).Quotient<GOAL>(CharacterModule.homEquiv c) x = AddCon.liftOn x ⇑(FreeAddMonoid.lift fun mn => (c.toAddMonoidHom mn.1) mn.2) ⋯
<VAR>R : Type uR<VAR>CommRing R<VAR>A : Type uA<VAR>AddCommGroup A<VAR>B : Type uB<VAR>AddCommGroup B<VAR>Module R A<VAR>Module R B<VAR>a : CharacterModule (TensorProduct R A B)<GOAL>∀ (x : A) (a_1 : B), ((CharacterModule.homEquiv.symm a) x) a_1 = a (x ⊗ₜ[R] a_1)
<VAR>R : Type uR<VAR>CommRing R<VAR>A : Type uA<VAR>AddCommGroup A<VAR>A' : Type u_1<VAR>AddCommGroup A'<VAR>B : Type uB<VAR>AddCommGroup B<VAR>Module R A<VAR>Module R A'<VAR>Module R B<VAR>f : A →ₗ[R] A'<GOAL>↑CharacterModule.homEquiv.symm ∘ₗ CharacterModule.dual (LinearMap.rTensor B f) ∘ₗ ↑CharacterModule.homEquiv = LinearMap.lcomp R (CharacterModule B) f
<VAR>n : ℕ<GOAL>(CharacterModule.int.divByNat n) ↑n = 0
<VAR>A : Type uA<VAR>AddCommGroup A<VAR>a : A<GOAL>∀ (a_1 : ℤ ⧸ Ideal.span {↑(addOrderOf a)}), ↑((CharacterModule.intSpanEquivQuotAddOrderOf a).symm a_1) = ↑((LinearMap.toSpanSingleton ℤ A a).quotKerEquivRange (((LinearMap.ker (LinearMap.toSpanSingleton ℤ A a)).quotEquivOfEq (Ideal.span {↑(addOrderOf a)}) ⋯).symm a_1))
<VAR>A : Type uA<VAR>AddCommGroup A<VAR>a : A<GOAL>∀ (a_1 : ↥(Submodule.span ℤ {a})), (CharacterModule.intSpanEquivQuotAddOrderOf a) a_1 = ((LinearMap.ker (LinearMap.toSpanSingleton ℤ A a)).quotEquivOfEq (Ideal.span {↑(addOrderOf a)}) ⋯) ((LinearMap.toSpanSingleton ℤ A a).quotKerEquivRange.symm ((LinearEquiv.ofEq (Submodule.span ℤ {a}) (LinearMap.range (LinearMap.toSpanSingleton ℤ A a)) ⋯) a_1))
<VAR>A : Type uA<VAR>AddCommGroup A<VAR>a : A<GOAL>(CharacterModule.intSpanEquivQuotAddOrderOf a) ⟨a, ⋯⟩ = Submodule.Quotient.mk 1
<VAR>A : Type uA<VAR>AddCommGroup A<VAR>a : A<VAR>h : (CharacterModule.ofSpanSingleton a) ⟨a, ⋯⟩ = 0<GOAL>a = 0
<VAR>A : Type uA<VAR>AddCommGroup A<VAR>a : A<VAR>ne_zero : a ≠ 0<GOAL>∃ c, c a ≠ 0
<VAR>A : Type uA<VAR>AddCommGroup A<VAR>a : A<VAR>h : ∀ (c : CharacterModule A), c a = 0<GOAL>a = 0
<VAR>R : Type uR<VAR>CommRing R<VAR>A : Type uA<VAR>AddCommGroup A<VAR>A' : Type u_1<VAR>AddCommGroup A'<VAR>Module R A<VAR>Module R A'<VAR>f : A →ₗ[R] A'<GOAL>Function.Surjective ⇑(CharacterModule.dual f) ↔ Function.Injective ⇑f
<VAR>R : Type uR<VAR>CommRing R<VAR>A : Type uA<VAR>AddCommGroup A<VAR>A' : Type u_1<VAR>AddCommGroup A'<VAR>B : Type uB<VAR>AddCommGroup B<VAR>Module R A<VAR>Module R A'<VAR>Module R B<VAR>f : A →ₗ[R] A'<GOAL>Function.Injective ⇑(LinearMap.rTensor B f) ↔ Function.Surjective ⇑(LinearMap.lcomp R (CharacterModule B) f)
<VAR>I : Type u<VAR>f : I → Type v<VAR>α : Type u_1<VAR>(i : I) → SMul α (f i)<VAR>k : α<VAR>hk : ∀ (i : I), IsSMulRegular (f i) k<GOAL>IsSMulRegular ((i : I) → f i) k
<VAR>R : Type u_1<VAR>A : Type u_4<VAR>B : Type u_5<VAR>Monoid R<VAR>AddMonoid A<VAR>AddCommMonoid B<VAR>DistribMulAction R B<VAR>r : R<VAR>f : A →+ B<GOAL>⇑(r • f) = r • ⇑f
<VAR>R : Type u_1<VAR>A : Type u_4<VAR>B : Type u_5<VAR>Monoid R<VAR>AddMonoid A<VAR>AddCommMonoid B<VAR>DistribMulAction R B<VAR>r : R<VAR>f : A →+ B<VAR>x : A<GOAL>(r • f) x = r • f x
<VAR>R : Type u_1<VAR>A : Type u_4<VAR>Monoid R<VAR>AddCommMonoid A<VAR>DistribMulAction R A<VAR>r : R<VAR>f : AddMonoid.End A<GOAL>⇑(r • f) = r • ⇑f
<VAR>R : Type u_1<VAR>A : Type u_4<VAR>Monoid R<VAR>AddCommMonoid A<VAR>DistribMulAction R A<VAR>r : R<VAR>f : AddMonoid.End A<VAR>x : A<GOAL>(r • f) x = r • f x
<VAR>M : Type u_3<VAR>A : Type u_4<VAR>Monoid M<VAR>AddMonoid A<VAR>DistribMulAction M A<VAR>c : M<GOAL>⇑(AddMonoidHom.smulLeft c) = fun x => c • x
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⇑AddMonoidHom.smul = AddMonoidHom.smulLeft
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>m : M<VAR>n : N<VAR>p : Submodule R M<VAR>q : Submodule R N<VAR>hm : m ∈ p<VAR>hn : n ∈ q<GOAL>(f m) n ∈ Submodule.map₂ f p q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<VAR>q : Submodule R N<VAR>r : Submodule R P<GOAL>Submodule.map₂ f p q ≤ r ↔ ∀ m ∈ p, ∀ n ∈ q, (f m) n ∈ r
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>s : Set M<VAR>t : Set N<GOAL>Submodule.map₂ f (Submodule.span R s) (Submodule.span R t) = Submodule.span R (Set.image2 (fun m n => (f m) n) s t)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<GOAL>Submodule.map₂ f p ⊥ = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>q : Submodule R N<GOAL>Submodule.map₂ f ⊥ q = ⊥
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p₁ p₂ : Submodule R M<VAR>q₁ q₂ : Submodule R N<VAR>hp : p₁ ≤ p₂<VAR>hq : q₁ ≤ q₂<GOAL>Submodule.map₂ f p₁ q₁ ≤ Submodule.map₂ f p₂ q₂
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p₁ p₂ : Submodule R M<VAR>q : Submodule R N<VAR>h : p₁ ≤ p₂<GOAL>Submodule.map₂ f p₁ q ≤ Submodule.map₂ f p₂ q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<VAR>q₁ q₂ : Submodule R N<VAR>h : q₁ ≤ q₂<GOAL>Submodule.map₂ f p q₁ ≤ Submodule.map₂ f p q₂
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<VAR>q₁ q₂ : Submodule R N<GOAL>Submodule.map₂ f p (q₁ ⊔ q₂) = Submodule.map₂ f p q₁ ⊔ Submodule.map₂ f p q₂
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p₁ p₂ : Submodule R M<VAR>q : Submodule R N<GOAL>Submodule.map₂ f (p₁ ⊔ p₂) q = Submodule.map₂ f p₁ q ⊔ Submodule.map₂ f p₂ q
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<VAR>q : Submodule R N<GOAL>Set.image2 (fun m n => (f m) n) ↑p ↑q ⊆ ↑(Submodule.map₂ f p q)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<VAR>q : Submodule R N<GOAL>Submodule.map₂ f p q = Submodule.span R (Set.image2 (fun m n => (f m) n) ↑p ↑q)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>p : Submodule R M<VAR>q : Submodule R N<GOAL>Submodule.map₂ f.flip q p = Submodule.map₂ f p q
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>s : ι → Submodule R M<VAR>t : Submodule R N<GOAL>Submodule.map₂ f (⨆ i, s i) t = ⨆ i, Submodule.map₂ f (s i) t
<VAR>ι : Sort uι<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>s : Submodule R M<VAR>t : ι → Submodule R N<GOAL>Submodule.map₂ f s (⨆ i, t i) = ⨆ i, Submodule.map₂ f s (t i)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>m : M<GOAL>Submodule.map₂ f (Submodule.span R {m}) = Submodule.map (f m)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>CommSemiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid N<VAR>AddCommMonoid P<VAR>Module R M<VAR>Module R N<VAR>Module R P<VAR>f : M →ₗ[R] N →ₗ[R] P<VAR>s : Submodule R M<VAR>n : N<GOAL>Submodule.map₂ f s (Submodule.span R {n}) = Submodule.map (f.flip n) s
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : M → M₂<VAR>self : IsLinearMap R f<VAR>c : R<VAR>x : M<GOAL>f (c • x) = c • f x
<VAR>R : Type u<VAR>M : Type v<VAR>M₂ : Type w<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>f : M → M₂<VAR>self : IsLinearMap R f<VAR>x y : M<GOAL>f (x + y) = f x + f y
<VAR>R : outParam (Type u_17)<VAR>M : outParam (Type u_18)<VAR>M₂ : outParam (Type u_19)<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>F : Type u_20<VAR>FunLike F M M₂<VAR>LinearMapClass F R 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_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>F : Type u_17<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : F<VAR>FunLike F M M₃<VAR>SemilinearMapClass F σ M M₃<VAR>σ' : S →+* R<VAR>RingHomInvPair σ σ'<VAR>c : S<VAR>x : M<GOAL>c • f x = f (σ' c • x)
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>F : Type u_17<VAR>FunLike F M M₃<VAR>SemilinearMapClass F σ M M₃<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : M →ₛₗ[σ] M₃<GOAL>⇑f.toAddHom = ⇑f
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : M →ₛₗ[σ] M₃<GOAL>f.toFun = ⇑f
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f g : M →ₛₗ[σ] M₃<VAR>h : ∀ (x : M), f x = g x<GOAL>f = g
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : M →ₛₗ[σ] M₃<VAR>f' : M → M₃<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : M →ₛₗ[σ] M₃<VAR>f' : M → M₃<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : AddHom M M₃<VAR>h : ∀ (m : R) (x : M), f.toFun (m • x) = σ m • f.toFun x<GOAL>⇑{ toAddHom := f, map_smul' := h } = ⇑f
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>f : AddHom M M₃<VAR>h : ∀ (m : R) (x : M), f.toFun (m • x) = σ m • f.toFun x<GOAL>↑{ toAddHom := f, map_smul' := h } = f
<VAR>R : Type u_1<VAR>S : Type u_6<VAR>M : Type u_9<VAR>M₃ : Type u_12<VAR>Semiring R<VAR>Semiring S<VAR>AddCommMonoid M<VAR>AddCommMonoid M₃<VAR>Module R M<VAR>Module S M₃<VAR>σ : R →+* S<VAR>F : Type u_17<VAR>FunLike F M M₃<VAR>SemilinearMapClass F σ M M₃<VAR>f g : F<VAR>h : ↑f = ↑g<GOAL>f = g
<VAR>R : Type u_1<VAR>M : Type u_9<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>x : M<GOAL>LinearMap.id x = x
<VAR>R : Type u_1<VAR>M : Type u_9<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<GOAL>⇑LinearMap.id = id
<VAR>R : Type u_1<VAR>M : Type u_9<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>σ : R →+* R<VAR>RingHomId σ<VAR>x : M<GOAL>LinearMap.id' x = x
<VAR>R : Type u_1<VAR>M : Type u_9<VAR>Semiring R<VAR>AddCommMonoid M<VAR>Module R M<VAR>σ : R →+* R<VAR>RingHomId σ<GOAL>⇑LinearMap.id' = id
<VAR>R : Type u_1<VAR>M : Type u_9<VAR>M₂ : Type u_11<VAR>Semiring R<VAR>AddCommMonoid M<VAR>AddCommMonoid M₂<VAR>Module R M<VAR>Module R M₂<VAR>fₗ : M →ₗ[R] M₂<GOAL>IsLinearMap R ⇑fₗ