case intro.intro
K : Type u_1
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → SMul K (R i)
r : K
s : Set ι
t : (i : ι) → Set (R i)
y : (i : ι) → R i
h : y ∈ pi s t
i : ι
hi : i ∈ s
⊢ (fun x => r • x) y i ∈ (r • t) i
K : Type u_1
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → SMul K (R i)
r : K
s : Set ι
t : (i : ι) → Set (R i)
⊢ r • pi s t ⊆ pi s (r • t)
rintro x ⟨y, h, rfl⟩ i hi
no goals
case intro.intro
K : Type u_1
ι : Type u_3
R : ι → Type u_2
inst✝ : (i : ι) → SMul K (R i)
r : K
s : Set ι
t : (i : ι) → Set (R i)
y : (i : ι) → R i
h : y ∈ pi s t
i : ι
hi : i ∈ s
⊢ (fun x => r • x) y i ∈ (r • t) i
exact smul_mem_smul_set (h i hi)