case intro.intro
R : Type u_1
R₁ : Type ?u.488097
R₂ : Type u_2
R₃ : Type ?u.488103
R₄ : Type ?u.488106
S : Type ?u.488109
K : Type ?u.488112
K₂ : Type ?u.488115
M : Type u_3
M' : Type ?u.488121
M₁ : Type ?u.488124
M₂ : Type u_4
M₃ : Type ?u.488130
M₄ : Type ?u.488133
N : Type ?u.488136
N₂ : Type ?u.488139
ι : Type ?u.488142
V : Type ?u.488145
V₂ : Type ?u.488148
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₂₁ : R₂ →+* R
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
q₁ q₁' : Submodule R M'
r : R
x y : M
inst✝ : RingHomSurjective σ₁₂
F : Type ?u.488729
sc : SemilinearMapClass F σ₁₂ M M₂
f g : M →ₛₗ[σ₁₂] M₂
m : M
hm : m ∈ ↑p
⊢ ↑(f + g) m ∈ map f p ⊔ map g p
R : Type u_1
R₁ : Type ?u.488097
R₂ : Type u_2
R₃ : Type ?u.488103
R₄ : Type ?u.488106
S : Type ?u.488109
K : Type ?u.488112
K₂ : Type ?u.488115
M : Type u_3
M' : Type ?u.488121
M₁ : Type ?u.488124
M₂ : Type u_4
M₃ : Type ?u.488130
M₄ : Type ?u.488133
N : Type ?u.488136
N₂ : Type ?u.488139
ι : Type ?u.488142
V : Type ?u.488145
V₂ : Type ?u.488148
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₂₁ : R₂ →+* R
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
q₁ q₁' : Submodule R M'
r : R
x y : M
inst✝ : RingHomSurjective σ₁₂
F : Type ?u.488729
sc : SemilinearMapClass F σ₁₂ M M₂
f g : M →ₛₗ[σ₁₂] M₂
⊢ map (f + g) p ≤ map f p ⊔ map g p
rintro x ⟨m, hm, rfl⟩
no goals
case intro.intro
R : Type u_1
R₁ : Type ?u.488097
R₂ : Type u_2
R₃ : Type ?u.488103
R₄ : Type ?u.488106
S : Type ?u.488109
K : Type ?u.488112
K₂ : Type ?u.488115
M : Type u_3
M' : Type ?u.488121
M₁ : Type ?u.488124
M₂ : Type u_4
M₃ : Type ?u.488130
M₄ : Type ?u.488133
N : Type ?u.488136
N₂ : Type ?u.488139
ι : Type ?u.488142
V : Type ?u.488145
V₂ : Type ?u.488148
inst✝¹⁴ : Semiring R
inst✝¹³ : Semiring R₂
inst✝¹² : Semiring R₃
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : AddCommMonoid M₃
inst✝⁸ : AddCommMonoid M'
inst✝⁷ : Module R M
inst✝⁶ : Module R M'
inst✝⁵ : Module R₂ M₂
inst✝⁴ : Module R₃ M₃
σ₁₂ : R →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R →+* R₃
σ₂₁ : R₂ →+* R
inst✝³ : RingHomInvPair σ₁₂ σ₂₁
inst✝² : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
p p' : Submodule R M
q q' : Submodule R₂ M₂
q₁ q₁' : Submodule R M'
r : R
x y : M
inst✝ : RingHomSurjective σ₁₂
F : Type ?u.488729
sc : SemilinearMapClass F σ₁₂ M M₂
f g : M →ₛₗ[σ₁₂] M₂
m : M
hm : m ∈ ↑p
⊢ ↑(f + g) m ∈ map f p ⊔ map g p
exact add_mem_sup (mem_map_of_mem hm) (mem_map_of_mem hm)