[GOAL]
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
s : Set ι
t : (i : ι) → Set (R i)
⊢ r • pi s t ⊆ pi s (r • t)
[PROOFSTEP]
rintro x ⟨y, h, rfl⟩ i hi
[GOAL]
case intro.intro
K : Type u_1
ι : Type u_2
R : ι → Type u_3
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
[PROOFSTEP]
exact smul_mem_smul_set (h i hi)
[GOAL]
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
t : (i : ι) → Set (R i)
x : (i : ι) → R i
h : x ∈ pi univ (r • t)
⊢ x ∈ r • pi univ t
[PROOFSTEP]
refine' ⟨fun i ↦ Classical.choose (h i <| Set.mem_univ _), fun i _ ↦ _, funext fun i ↦ _⟩
[GOAL]
case refine'_1
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
t : (i : ι) → Set (R i)
x : (i : ι) → R i
h : x ∈ pi univ (r • t)
i : ι
x✝ : i ∈ univ
⊢ (fun i => Classical.choose (_ : x i ∈ (r • t) i)) i ∈ t i
[PROOFSTEP]
exact (Classical.choose_spec (h i <| Set.mem_univ i)).left
[GOAL]
case refine'_2
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
t : (i : ι) → Set (R i)
x : (i : ι) → R i
h : x ∈ pi univ (r • t)
i : ι
⊢ (fun x => r • x) (fun i => Classical.choose (_ : x i ∈ (r • t) i)) i = x i
[PROOFSTEP]
exact (Classical.choose_spec (h i <| Set.mem_univ i)).right
