-- Mathlib/Data/Set/Lattice.lean
theorem image_projection_prod {ι : Type*} {α : ι → Type*} {v : ∀ i : ι, Set (α i)}
    (hv : (pi univ v).Nonempty) (i : ι) :
    ((fun x : ∀ i : ι, α i => x i) '' ⋂ k, (fun x : ∀ j : ι, α j => x k) ⁻¹' v k) = v i

Proof state:
case h₁
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ (fun x => x i) '' ⋂ k, (fun x => x k) ⁻¹' v k ⊆ v i

Tactic:
simp [iInter_subset]

Result:
no goals

Proof state:
case h₂.intro
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
⊢ ∀ (i_1 : ι), update z i y i_1 ∈ v i_1

Tactic:
rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]

Result:
case h₂.intro
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
⊢ y ∈ v i ∧ ∀ (x : ι), x ≠ i → z x ∈ v x

Proof state:
case h₂
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ v i ⊆ (fun x => x i) '' ⋂ k, (fun x => x k) ⁻¹' v k

Tactic:
intro y y_in

Result:
case h₂
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
y : α i
y_in : y ∈ v i
⊢ y ∈ (fun x => x i) '' ⋂ k, (fun x => x k) ⁻¹' v k

Proof state:
case h₂.intro
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
⊢ ∃ x, (∀ (i : ι), x i ∈ v i) ∧ x i = y

Tactic:
refine ⟨Function.update z i y, ?_, update_self i y z⟩

Result:
case h₂.intro
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
⊢ ∀ (i_1 : ι), update z i y i_1 ∈ v i_1

Proof state:
case h₂
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
y : α i
y_in : y ∈ v i
⊢ ∃ x, (∀ (i : ι), x i ∈ v i) ∧ x i = y

Tactic:
rcases hv with ⟨z, hz⟩

Result:
case h₂.intro
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
⊢ ∃ x, (∀ (i : ι), x i ∈ v i) ∧ x i = y

Proof state:
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ (fun x => x i) '' ⋂ k, (fun x => x k) ⁻¹' v k = v i

Tactic:
apply Subset.antisymm

Result:
case h₁
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ (fun x => x i) '' ⋂ k, (fun x => x k) ⁻¹' v k ⊆ v i

case h₂
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
⊢ v i ⊆ (fun x => x i) '' ⋂ k, (fun x => x k) ⁻¹' v k

Proof state:
case h₂.intro
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
⊢ y ∈ v i ∧ ∀ (x : ι), x ≠ i → z x ∈ v x

Tactic:
exact ⟨y_in, fun j _ => by simpa using hz j⟩

Result:
no goals

Proof state:
case h₂
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
y : α i
y_in : y ∈ v i
⊢ y ∈ (fun x => x i) '' ⋂ k, (fun x => x k) ⁻¹' v k

Tactic:
simp only [mem_image, mem_iInter, mem_preimage]

Result:
case h₂
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
hv : (univ.pi v).Nonempty
i : ι
y : α i
y_in : y ∈ v i
⊢ ∃ x, (∀ (i : ι), x i ∈ v i) ∧ x i = y

Proof state:
ι : Type u_12
α : ι → Type u_13
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ univ.pi v
j : ι
x✝ : j ≠ i
⊢ z j ∈ v j

Tactic:
simpa using hz j

Result:
no goals