case refine_1
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_2
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i → β i
⊢ (range fun g i => f i (g i)) ⊆ pi univ fun i => range (f i)

case refine_2
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_2
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i → β i
x : (i : ι) → β i
hx : x ∈ pi univ fun i => range (f i)
⊢ x ∈ range fun g i => f i (g i)
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_2
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i → β i
⊢ (range fun g i => f i (g i)) = pi univ fun i => range (f i)
refine Subset.antisymm ?_ fun x hx => ?_
case refine_1.intro
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_2
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
f : (i : ι) → α i → β i
x : (i : ι) → α i
i : ι
⊢ (fun g i => f i (g i)) x i ∈ (fun i => range (f i)) i
case refine_1
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_2
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i → β i
⊢ (range fun g i => f i (g i)) ⊆ pi univ fun i => range (f i)
rintro _ ⟨x, rfl⟩ i -
no goals
case refine_1.intro
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_2
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i✝ : ι
f : (i : ι) → α i → β i
x : (i : ι) → α i
i : ι
⊢ (fun g i => f i (g i)) x i ∈ (fun i => range (f i)) i
exact ⟨x i, rfl⟩
case refine_2
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_2
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i → β i
x : (i : ι) → β i
y : (i : ι) → i ∈ univ → α i
hy : ∀ (i : ι) (a : i ∈ univ), f i (y i a) = x i
⊢ x ∈ range fun g i => f i (g i)
case refine_2
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_2
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i → β i
x : (i : ι) → β i
hx : x ∈ pi univ fun i => range (f i)
⊢ x ∈ range fun g i => f i (g i)
choose y hy using hx
no goals
case refine_2
ι : Type u_1
α : ι → Type u_3
β : ι → Type u_2
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
f : (i : ι) → α i → β i
x : (i : ι) → β i
y : (i : ι) → i ∈ univ → α i
hy : ∀ (i : ι) (a : i ∈ univ), f i (y i a) = x i
⊢ x ∈ range fun g i => f i (g i)
exact ⟨fun i => y i trivial, funext fun i => hy i trivial⟩