-- Mathlib/Data/Set/Prod.lean
lemma eval_image_pi_of_not_mem [Decidable (s.pi t).Nonempty] (hi : i ∉ s) :
    eval i '' s.pi t = if (s.pi t).Nonempty then univ else ∅

Proof state:
case h.mp.intro.intro
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : i ∉ s
x : (x : ι) → α x
hx : ∀ i ∈ s, x i ∈ t i
⊢ ∃ x, ∀ i ∈ s, x i ∈ t i

Tactic:
exact ⟨x, hx⟩

Result:
no goals

Proof state:
case h.mpr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : i ∉ s
xᵢ : α i
⊢ (∃ x, ∀ i ∈ s, x i ∈ t i) → ∃ x, (∀ i ∈ s, x i ∈ t i) ∧ x i = xᵢ

Tactic:
rintro ⟨x, hx⟩

Result:
case h.mpr.intro
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : i ∉ s
xᵢ : α i
x : (i : ι) → α i
hx : ∀ i ∈ s, x i ∈ t i
⊢ ∃ x, (∀ i ∈ s, x i ∈ t i) ∧ x i = xᵢ

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : i ∉ s
⊢ eval i '' s.pi t = if (s.pi t).Nonempty then univ else ∅

Tactic:
ext xᵢ

Result:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : i ∉ s
xᵢ : α i
⊢ xᵢ ∈ eval i '' s.pi t ↔ xᵢ ∈ if (s.pi t).Nonempty then univ else ∅

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : i ∉ s
xᵢ : α i
⊢ (∃ x, (∀ i ∈ s, x i ∈ t i) ∧ x i = xᵢ) ↔ ∃ x, ∀ i ∈ s, x i ∈ t i

Tactic:
constructor

Result:
case h.mp
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : i ∉ s
xᵢ : α i
⊢ (∃ x, (∀ i ∈ s, x i ∈ t i) ∧ x i = xᵢ) → ∃ x, ∀ i ∈ s, x i ∈ t i

case h.mpr
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : i ∉ s
xᵢ : α i
⊢ (∃ x, ∀ i ∈ s, x i ∈ t i) → ∃ x, (∀ i ∈ s, x i ∈ t i) ∧ x i = xᵢ

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : i ∉ s
xᵢ : α i
⊢ xᵢ ∈ eval i '' s.pi t ↔ xᵢ ∈ if (s.pi t).Nonempty then univ else ∅

Tactic:
simp only [eval, mem_image, mem_pi, Set.Nonempty, mem_ite_empty_right, mem_univ, and_true]

Result:
case h
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : i ∉ s
xᵢ : α i
⊢ (∃ x, (∀ i ∈ s, x i ∈ t i) ∧ x i = xᵢ) ↔ ∃ x, ∀ i ∈ s, x i ∈ t i

Proof state:
case h.mpr.intro
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : i ∉ s
xᵢ : α i
x : (i : ι) → α i
hx : ∀ i ∈ s, x i ∈ t i
⊢ ∃ x, (∀ i ∈ s, x i ∈ t i) ∧ x i = xᵢ

Tactic:
refine ⟨Function.update x i xᵢ, ?_⟩

Result:
case h.mpr.intro
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : i ∉ s
xᵢ : α i
x : (i : ι) → α i
hx : ∀ i ∈ s, x i ∈ t i
⊢ (∀ i_1 ∈ s, update x i xᵢ i_1 ∈ t i_1) ∧ update x i xᵢ i = xᵢ

Proof state:
case h.mp
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : i ∉ s
xᵢ : α i
⊢ (∃ x, (∀ i ∈ s, x i ∈ t i) ∧ x i = xᵢ) → ∃ x, ∀ i ∈ s, x i ∈ t i

Tactic:
rintro ⟨x, hx, rfl⟩

Result:
case h.mp.intro.intro
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
inst✝ : Decidable (s.pi t).Nonempty
hi : i ∉ s
x : (x : ι) → α x
hx : ∀ i ∈ s, x i ∈ t i
⊢ ∃ x, ∀ i ∈ s, x i ∈ t i