Comparing have with let bindings in Lean4

Here is how have operates

Internally, have h : p := s; t becomes the term (fun (h : p) => t) s. Put differently, s proves p, while t proves the intended conclusion under the assumption h : p, and lambda abstraction followed by application joins them together.

Here is how let operates

The let construct provides more powerful abbreviation, so some expressions let a := t1; t2 have no equivalent (fun a => t2) t1. For practice, work out why the definition called keepType below passes type checking while loseType does not.

def keepType := let chosen := Nat; fun item : chosen => item + 4
/-
  def loseType := (fun chosen => fun item : chosen => item + 4) Nat
-/

The distinction is that let retains a definition, whereas have discards it.

For instance, this example accepts let, but substituting have fails in Lean 4.

example : {item : Nat // item = 0} := let item := 0 ; ⟨item, rfl⟩

Typically, proofs use have, while other things use let. Within Lean3's tactic mode, dsimp [x] lets you unfold let x := ..., but I don't know the corresponding approach in Lean4.

Consider this example with a practical use:

def divisibleByTwo (number : Nat) : Prop :=
  ∃ factor : Nat, number = factor * 2

theorem doubled_half (number : Nat) : divisibleByTwo (number / 2 * 2) :=
  let half := number / 2
  have : number / 2 * 2 = half * 2 := rfl
  Exists.intro half this

theorem doubled_failure (number : Nat) : divisibleByTwo (number / 2 * 2) :=
  have half := number / 2
  have : number / 2 * 2 = half * 2 := rfl -- error: type mismatch
  Exists.intro half this

The initial proof works, whereas the other one fails at its rfl expression. The reason is that let substitutes the definition number / 2 for all later uses of half. After have, however, the compiler retains only that half has type Nat and discards its definition, leaving rfl unable to identify number / 2 * 2 with an arbitrary half / 2.

Consequently, we normally introduce intermediate propositions or lemmas with have, since the type system needs evidence for the particular proposition without needing the proof's actual procedure. By contrast, let introduces variables when later parts of the proof need their definitions.