case h₁
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
⊢ ((fun x => x i) '' ⋂ (k : ι), (fun x => x k) ⁻¹' v k) ⊆ v i

case h₂
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
⊢ v i ⊆ (fun x => x i) '' ⋂ (k : ι), (fun x => x k) ⁻¹' v k
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
⊢ ((fun x => x i) '' ⋂ (k : ι), (fun x => x k) ⁻¹' v k) = v i
apply Subset.antisymm
no goals
case h₁
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
⊢ ((fun x => x i) '' ⋂ (k : ι), (fun x => x k) ⁻¹' v k) ⊆ v i
simp [iInter_subset]
case h₂
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
y : α i
y_in : y ∈ v i
⊢ y ∈ (fun x => x i) '' ⋂ (k : ι), (fun x => x k) ⁻¹' v k
case h₂
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
⊢ v i ⊆ (fun x => x i) '' ⋂ (k : ι), (fun x => x k) ⁻¹' v k
intro y y_in
case h₂
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
y : α i
y_in : y ∈ v i
⊢ ∃ x, (∀ (i : ι), x i ∈ v i) ∧ x i = y
case h₂
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
y : α i
y_in : y ∈ v i
⊢ y ∈ (fun x => x i) '' ⋂ (k : ι), (fun x => x k) ⁻¹' v k
simp only [mem_image, mem_iInter, mem_preimage]
case h₂.intro
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi univ v
⊢ ∃ x, (∀ (i : ι), x i ∈ v i) ∧ x i = y
case h₂
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
hv : Set.Nonempty (pi univ v)
i : ι
y : α i
y_in : y ∈ v i
⊢ ∃ x, (∀ (i : ι), x i ∈ v i) ∧ x i = y
rcases hv with ⟨z, hz⟩
case h₂.intro
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi univ v
⊢ ∀ (i_1 : ι), update z i y i_1 ∈ v i_1
case h₂.intro
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi univ v
⊢ ∃ x, (∀ (i : ι), x i ∈ v i) ∧ x i = y
refine' ⟨Function.update z i y, _, update_same i y z⟩
case h₂.intro
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi univ v
⊢ y ∈ v i ∧ ∀ (x : ι), x ≠ i → z x ∈ v x
case h₂.intro
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi univ v
⊢ ∀ (i_1 : ι), update z i y i_1 ∈ v i_1
rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]
no goals
case h₂.intro
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi univ v
⊢ y ∈ v i ∧ ∀ (x : ι), x ≠ i → z x ∈ v x
exact ⟨y_in, fun j _ => by simpa using hz j⟩
no goals
α✝ : Type ?u.77979
β : Type ?u.77982
γ : Type ?u.77985
ι✝ : Sort ?u.77988
ι' : Sort ?u.77991
ι₂ : Sort ?u.77994
κ : ι✝ → Sort ?u.77999
κ₁ : ι✝ → Sort ?u.78004
κ₂ : ι✝ → Sort ?u.78009
κ' : ι' → Sort ?u.78014
ι : Type u_1
α : ι → Type u_2
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi univ v
j : ι
x✝ : j ≠ i
⊢ z j ∈ v j
simpa using hz j