# Zulip Chat Archive

## Stream: new members

### Topic: forall_exists_index

#### Vivek Rajesh Joshi (Sep 09 2023 at 06:14):

Can anyone explain to me what this theorem does (explanation of its proof is not needed), and how it is getting applied in this context?

∃ x, (∀ (i : I), x ∈ A i) ∧ f x = y iff ∀ (x : α), (∀ (i : I), x ∈ A i) ∧ f x = y

#### Kevin Buzzard (Sep 09 2023 at 06:20):

Can you post a #mwe so we can run the code on our own computer with little effort (and in particular understand the types of the terms involved in your statement)? You ask about a theorem being applied but as far as I can see you're just writing down a true/false statement, there is no proof or application

#### Kevin Buzzard (Sep 09 2023 at 06:21):

It would be like me writing `2+2=5`

and asking how it is getting applied

#### Eric Wieser (Sep 09 2023 at 06:23):

#### Kevin Buzzard (Sep 09 2023 at 06:25):

Oh I see, the clue is in the title (which is a lot less prominent on the mobile app). I still don't understand the question though, where's the application?

#### Vivek Rajesh Joshi (Sep 09 2023 at 08:00):

Kevin Buzzard said:

Oh I see, the clue is in the title (which is a lot less prominent on the mobile app). I still don't understand the question though, where's the application?

Sorry, I'll keep that in mind next time.

The line I have written is part of a proof for a theorem. The goal had the expression on the LHS, and `simp`

converted it to the expression in the RHS. After typing `simp?`

, I realised that it used the theorem `forall_exists_index`

to do this. I am unable to understand how this theorem was used here, and why the conversion makes sense.

#### Kevin Buzzard (Sep 09 2023 at 08:43):

Then post a #mwe (that's a link)

#### Vivek Rajesh Joshi (Sep 09 2023 at 09:55):

```
import Mathlib.Tactic
import Mathlib.Data.Set.Lattice
import Mathlib.Data.Set.Function
import Mathlib.Analysis.SpecialFunctions.Log.Basic
variable {α β : Type _}
variable (f : α → β)
variable (s t : Set α)
variable (u v : Set β)
open Function
open Set
variable {I : Type _} (A : I → Set α) (B : I → Set β)
example : (f '' ⋂ i, A i) ⊆ ⋂ i, f '' A i := by
intro y; simp
intro x h fxeq i
use x
exact ⟨h i, fxeq⟩
```

#### Kevin Buzzard (Sep 09 2023 at 14:15):

Yeah so `simp?`

reports that it uses `forall_exists_index`

. We can take the `simp`

call apart a bit more and see exactly what it's doing:

```
import Mathlib.Tactic
variable {α β : Type _}
variable (f : α → β)
variable (s t : Set α)
variable (u v : Set β)
open Function
open Set
variable {I : Type _} (A : I → Set α) (B : I → Set β)
#check forall_exists_index
/-
forall_exists_index.{u_1} {α : Sort u_1} {p : α → Prop} {q : (∃ x, p x) → Prop} :
(∀ (h : ∃ x, p x), q h) ↔ ∀ (x : α) (h : p x), q (_ : ∃ x, p x)
-/
example : (f '' ⋂ i, A i) ⊆ ⋂ i, f '' A i := by
intro y;
simp [-forall_exists_index] -- don't use it yet
-- ⊢ (∃ x, (∀ (i : I), x ∈ A i) ∧ f x = y) → ∀ (i : I), ∃ x, x ∈ A i ∧ f x = y
rw [forall_exists_index]
-- ⊢ ∀ (x : α), (∀ (i : I), x ∈ A i) ∧ f x = y → ∀ (i : I), ∃ x, x ∈ A i ∧ f x = y
simp
intro x h fxeq i
use x
exact ⟨h i, fxeq⟩
```

So before the application of `forall_exists_index`

the goal is (there exists x such that P x) -> Q, and after the application it's (for all x, P x -> Q), and that's what the lemma says (actually the lemma says something slightly more general but what the heck) so that's what it's doing.

#### Vivek Rajesh Joshi (Sep 09 2023 at 14:38):

I understand what `simp`

is doing, it is just rewriting the LHS of the lemma as the RHS. I just can't wrap my head around why that replacement makes sense, and what q and h are in this case.

#### Kevin Buzzard (Sep 09 2023 at 14:49):

In the application, `h`

is a proof of `(∃ x, (∀ (i : I), x ∈ A i) ∧ f x = y)`

and `q`

is the function which eats `h`

, ignores it (which is why I said that the lemma was more general than needed) and returns a proof of `∀ (i : I), ∃ x, x ∈ A i ∧ f x = y`

(a statement which doesn't depend on `h`

).

Last updated: Dec 20 2023 at 11:08 UTC