case refine'_1
K : Type u_1
ι : Type u_3
R : ι → Type u_2
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

case refine'_2
K : Type u_1
ι : Type u_3
R : ι → Type u_2
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
K : Type u_1
ι : Type u_3
R : ι → Type u_2
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
refine' ⟨fun i ↦ Classical.choose (h i <| Set.mem_univ _), fun i _ ↦ _, funext fun i ↦ _⟩
no goals
case refine'_1
K : Type u_1
ι : Type u_3
R : ι → Type u_2
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
exact (Classical.choose_spec (h i <| Set.mem_univ i)).left
no goals
case refine'_2
K : Type u_1
ι : Type u_3
R : ι → Type u_2
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
exact (Classical.choose_spec (h i <| Set.mem_univ i)).right