Existential Qauntifier in lean4

example : ∃ x : Nat, x + 1 = 4 := 
  have h : 3 + 1 = 4 := by
    calc
      3 + 1 = 2 + 1 + 1 :=  by rw [<- Nat.succ_eq_add_one 2]
       _     = 2 + (1 + 1) := by rw [Nat.add_assoc]
       _     = 2 + 2 := by rw [Nat.add_comm 1 1]
        _     = 4 := rfl
  Exists.intro 3 h

In the above we prove there exists x such that x + 1 = 4. We use the calc keyword for calculation proof. In the first step we set our hypothesis h and then move on to prove further points.

The first rewrite is [<- Nat.succ_eq_add_one 2] which substitutes Nat.succ 2 = 2 + 1. The rw tries to match Nat.succ 2 so we use it.

Next we use Nat.add_assoc (a + b + c = a + (b + c)). Next Nat.add_comm and rfl finally.

Note that rfl is powerful. If two expressions compute to the same, however complicated it treats them the same. Also rfl is at the core of Lean's kernel and not in the meta layer.

Finally, Exists.intro gives a proof of Exists p where p:α → Prop is a predicate given a witness w:α such that p w holds.

A very simple way to do this is below:

example : ∃ x : Nat, x + 1 = 4 := Exists.intro 3 rfl