# Applying universally quantified equalities to propositions

In Lean, given an equality eq: e0 = e1, one may rewrite either e0 or e1 with the other one in a proposition P using eq ▸ P.

def f: Nat → Nat := sorry

def exampleA
(eq: x = f c)
(ex: ∃ a, a = f c)
:
∃ a, a = x
:=
eq ▸ ex

def exampleB
(eq: x = f c)
:
(∃ a, a = f c) = (∃ a, a = x)
:=
eq ▸ rfl


However, the same does not work with universally quantified equalities.

def quantifiedExampleA
(eqQuantified: ∀ c, x = f c)
(ex: ∃ c, a = f c)
:
∃ (_c: Nat), a = x
:=
-- Obviously does not work:
-- eqQuantified ▸ ex

let ⟨c, afc⟩ := ex
⟨c, eqQuantified c ▸ afc⟩

def quantifiedExampleB
(eqQuantified: ∀ c, x = f c)
:
(∃ c, a = f c) = ∃ (_c: Nat), a = x
:=
-- Again, not working :(
-- eqQuantified ▸ rfl

propext
(Iff.intro
(quantifiedExampleA eqQuantified)
(fun ex =>
let ⟨c, ax⟩ := ex
⟨c, eqQuantified c ▸ ax⟩))


As the example B shows, doing these proofs manually can get cumbersome really quickly if the existentials aren't top-level. ▸ is able to do the replacement anywhere in a proposition. Is it possible to achieve the same level of "comfort" or simplicity with universally quantified equalities as we have with ordinary equalities?

Additionally: would it be possible to support multiple quantified variables, not just one?

There are some lemmas that help dealing with these situations. For quantifiedExampleA, you can use Exists.imp, which shortens the proof to

theorem quantifiedExampleA
(eqQuantified : ∀ c, x = f c)
(ex : ∃ c, a = f c) : ∃ (_c : Nat), a = x :=
ex.imp (fun b => eqQuantified b ▸ id)


For quantifiedExampleB, there is exists_congr, which shortens the proof to

theorem quantifiedExampleB (eqQuantified : ∀ c, x = f c) :
(∃ c, a = f c) = ∃ (_c : Nat), a = x :=
propext (exists_congr (fun b => eqQuantified b ▸ Iff.rfl))


In fact, the simplifier is able to apply these lemmas for you, so you can just use simp/simpa:

theorem quantifiedExampleA
(eqQuantified : ∀ c, x = f c)
(ex : ∃ c, a = f c) : ∃ (_c : Nat), a = x := by
simpa [← eqQuantified] using ex

theorem quantifiedExampleB (eqQuantified : ∀ c, x = f c) :
(∃ c, a = f c) = ∃ (_c : Nat), a = x := by
simp [← eqQuantified]