case intro.intro.intro.intro
α : Type ?u.254804
G : Type ?u.254807
M✝ : Type ?u.254810
R : Type u_1
A : Type ?u.254816
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
i j : R
hi : i ∈ ↑M
hj : j ∈ ↑N
⊢ (fun x x_1 => x * x_1) i j ∈ ↑(M * N)
α : Type ?u.254804
G : Type ?u.254807
M✝ : Type ?u.254810
R : Type u_1
A : Type ?u.254816
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
⊢ ↑M * ↑N ⊆ ↑(M * N)
rintro _ ⟨i, j, hi, hj, rfl⟩
no goals
case intro.intro.intro.intro
α : Type ?u.254804
G : Type ?u.254807
M✝ : Type ?u.254810
R : Type u_1
A : Type ?u.254816
inst✝² : Monoid M✝
inst✝¹ : AddMonoid A
inst✝ : NonUnitalNonAssocSemiring R
M N : AddSubmonoid R
i j : R
hi : i ∈ ↑M
hj : j ∈ ↑N
⊢ (fun x x_1 => x * x_1) i j ∈ ↑(M * N)
exact mul_mem_mul hi hj