case intro.intro
F : Type ?u.213140
α : Type u_2
β : Type u_1
γ : Type ?u.213149
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
a b : α
s : Set β
x : β
hx : x ∈ s
⊢ (fun x => (a + b) • x) x ∈ a • s + b • s
F : Type ?u.213140
α : Type u_2
β : Type u_1
γ : Type ?u.213149
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
a b : α
s : Set β
⊢ (a + b) • s ⊆ a • s + b • s
rintro _ ⟨x, hx, rfl⟩
no goals
case intro.intro
F : Type ?u.213140
α : Type u_2
β : Type u_1
γ : Type ?u.213149
inst✝² : Semiring α
inst✝¹ : AddCommMonoid β
inst✝ : Module α β
a b : α
s : Set β
x : β
hx : x ∈ s
⊢ (fun x => (a + b) • x) x ∈ a • s + b • s
simpa only [add_smul] using add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hx)