case intro.intro.intro.intro
α : Type ?u.68
G : Type ?u.71
M : Type u_1
R : Type ?u.77
A : Type ?u.80
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s t u : Set M
S : Submonoid M
hs : s ⊆ ↑S
ht : t ⊆ ↑S
p q : M
hp : p ∈ s
hq : q ∈ t
⊢ (fun x x_1 => x * x_1) p q ∈ ↑S
α : Type ?u.68
G : Type ?u.71
M : Type u_1
R : Type ?u.77
A : Type ?u.80
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s t u : Set M
S : Submonoid M
hs : s ⊆ ↑S
ht : t ⊆ ↑S
⊢ s * t ⊆ ↑S
rintro _ ⟨p, q, hp, hq, rfl⟩
no goals
case intro.intro.intro.intro
α : Type ?u.68
G : Type ?u.71
M : Type u_1
R : Type ?u.77
A : Type ?u.80
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s t u : Set M
S : Submonoid M
hs : s ⊆ ↑S
ht : t ⊆ ↑S
p q : M
hp : p ∈ s
hq : q ∈ t
⊢ (fun x x_1 => x * x_1) p q ∈ ↑S
exact Submonoid.mul_mem _ (hs hp) (ht hq)