no goals
R✝ : Type ?u.404363
A✝ : Type ?u.404366
B : Type ?u.404369
M✝ : Type ?u.404372
N : Type ?u.404375
inst✝¹¹ : Semiring R✝
inst✝¹⁰ : AddCommMonoid M✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R✝ N
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
s : Finset A
hs : Submodule.span R ↑s = ⊤
t : Finset M
ht : Submodule.span A ↑t = ⊤
⊢ Submodule.span R (image2 (fun x x_1 => x • x_1) ↑s ↑t) = ⊤
erw [Set.image2_smul, Submodule.span_smul_of_span_eq_top hs (↑t : Set M), ht,
  Submodule.restrictScalars_top]