case h
α : Type ?u.3401
G : Type ?u.3404
M : Type u_1
R : Type ?u.3410
A : Type ?u.3413
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s✝ t u : Set M
s : Submonoid M
x : M
⊢ x ∈ ↑s * ↑s ↔ x ∈ ↑s
α : Type ?u.3401
G : Type ?u.3404
M : Type u_1
R : Type ?u.3410
A : Type ?u.3413
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s✝ t u : Set M
s : Submonoid M
⊢ ↑s * ↑s = ↑s
ext x
case h
α : Type ?u.3401
G : Type ?u.3404
M : Type u_1
R : Type ?u.3410
A : Type ?u.3413
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s✝ t u : Set M
s : Submonoid M
x : M
⊢ x ∈ ↑s * ↑s → x ∈ ↑s
case h
α : Type ?u.3401
G : Type ?u.3404
M : Type u_1
R : Type ?u.3410
A : Type ?u.3413
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s✝ t u : Set M
s : Submonoid M
x : M
⊢ x ∈ ↑s * ↑s ↔ x ∈ ↑s
refine' ⟨_, fun h => ⟨x, 1, h, s.one_mem, mul_one x⟩⟩
case h.intro.intro.intro.intro
α : Type ?u.3401
G : Type ?u.3404
M : Type u_1
R : Type ?u.3410
A : Type ?u.3413
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s✝ t u : Set M
s : Submonoid M
a b : M
ha : a ∈ ↑s
hb : b ∈ ↑s
⊢ (fun x x_1 => x * x_1) a b ∈ ↑s
case h
α : Type ?u.3401
G : Type ?u.3404
M : Type u_1
R : Type ?u.3410
A : Type ?u.3413
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s✝ t u : Set M
s : Submonoid M
x : M
⊢ x ∈ ↑s * ↑s → x ∈ ↑s
rintro ⟨a, b, ha, hb, rfl⟩
no goals
case h.intro.intro.intro.intro
α : Type ?u.3401
G : Type ?u.3404
M : Type u_1
R : Type ?u.3410
A : Type ?u.3413
inst✝¹ : Monoid M
inst✝ : AddMonoid A
s✝ t u : Set M
s : Submonoid M
a b : M
ha : a ∈ ↑s
hb : b ∈ ↑s
⊢ (fun x x_1 => x * x_1) a b ∈ ↑s
exact s.mul_mem ha hb