ι : Type u_1
α : ι → Type u_3
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
β : ι → Type u_2
m : (i : ι) → α i → β i
⊢ ∀ (x : Set ((i : ι) → β i)),
    (∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ x) →
      ∀ (i : ι), ∃ t₁, t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' x
ι : Type u_1
α : ι → Type u_3
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
β : ι → Type u_2
m : (i : ι) → α i → β i
⊢ map (fun k i => m i (k i)) (Filter.coprodᵢ f) ≤ Filter.coprodᵢ fun i => map (m i) (f i)
simp only [le_def, mem_map, mem_coprodᵢ_iff]
ι : Type u_1
α : ι → Type u_3
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
β : ι → Type u_2
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
⊢ ∃ t₁, t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' s
ι : Type u_1
α : ι → Type u_3
f f₁ f₂ : (i : ι) → Filter (α i)
s : (i : ι) → Set (α i)
β : ι → Type u_2
m : (i : ι) → α i → β i
⊢ ∀ (x : Set ((i : ι) → β i)),
    (∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ x) →
      ∀ (i : ι), ∃ t₁, t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' x
intro s h i
case intro.intro
ι : Type u_1
α : ι → Type u_3
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
β : ι → Type u_2
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
t : Set (β i)
H : m i ⁻¹' t ∈ f i
hH : eval i ⁻¹' t ⊆ s
⊢ ∃ t₁, t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' s
ι : Type u_1
α : ι → Type u_3
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
β : ι → Type u_2
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
⊢ ∃ t₁, t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' s
obtain ⟨t, H, hH⟩ := h i
no goals
case intro.intro
ι : Type u_1
α : ι → Type u_3
f f₁ f₂ : (i : ι) → Filter (α i)
s✝ : (i : ι) → Set (α i)
β : ι → Type u_2
m : (i : ι) → α i → β i
s : Set ((i : ι) → β i)
h : ∀ (i : ι), ∃ t₁, m i ⁻¹' t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ s
i : ι
t : Set (β i)
H : m i ⁻¹' t ∈ f i
hH : eval i ⁻¹' t ⊆ s
⊢ ∃ t₁, t₁ ∈ f i ∧ eval i ⁻¹' t₁ ⊆ (fun k i => m i (k i)) ⁻¹' s
exact ⟨{ x : α i | m i x ∈ t }, H, fun x hx => hH hx⟩