R : Type u_3
inst✝¹⁶ : CommSemiring R
R' : Type ?u.489165
inst✝¹⁵ : Monoid R'
R'' : Type ?u.489171
inst✝¹⁴ : Semiring R''
M : Type u_1
N : Type u_2
P : Type ?u.489183
Q : Type ?u.489186
S : Type ?u.489189
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : DistribMulAction R' M
inst✝² : Module R'' M
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
⊢ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} ≤ Submodule.span R (Set.image2 (fun m n => ↑(↑(mk R M N) m) n) ↑⊤ ↑⊤)
R : Type u_3
inst✝¹⁶ : CommSemiring R
R' : Type ?u.489165
inst✝¹⁵ : Monoid R'
R'' : Type ?u.489171
inst✝¹⁴ : Semiring R''
M : Type u_1
N : Type u_2
P : Type ?u.489183
Q : Type ?u.489186
S : Type ?u.489189
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : DistribMulAction R' M
inst✝² : Module R'' M
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
⊢ Submodule.map₂ (mk R M N) ⊤ ⊤ = ⊤
rw [← top_le_iff, ← span_tmul_eq_top, Submodule.map₂_eq_span_image2]
no goals
R : Type u_3
inst✝¹⁶ : CommSemiring R
R' : Type ?u.489165
inst✝¹⁵ : Monoid R'
R'' : Type ?u.489171
inst✝¹⁴ : Semiring R''
M : Type u_1
N : Type u_2
P : Type ?u.489183
Q : Type ?u.489186
S : Type ?u.489189
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : DistribMulAction R' M
inst✝² : Module R'' M
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
⊢ Submodule.span R {t | ∃ m n, m ⊗ₜ[R] n = t} ≤ Submodule.span R (Set.image2 (fun m n => ↑(↑(mk R M N) m) n) ↑⊤ ↑⊤)
exact Submodule.span_mono fun _ ⟨m, n, h⟩ => ⟨m, n, trivial, trivial, h⟩