feat: Thunk is inhabited (#12469)

This PR adds the `Inhabited` instance for `Thunk`.

We need this in batteries to call `PersistentEnvExtension.getState` on a
state that is wrapped in a `Thunk`, see
https://github.com/leanprover-community/batteries/pull/1667/changes.

src/Init/Core.lean

@@ -172,6 +172,8 @@ instance thunkCoe : CoeTail α (Thunk α) where
   -- Since coercions are expanded eagerly, `a` is evaluated lazily.
   coe a := ⟨fun _ => a⟩
 
+instance [Inhabited α] : Inhabited (Thunk α) := ⟨.pure default⟩
+
 /-- A variation on `Eq.ndrec` with the equality argument first. -/
 abbrev Eq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {motive : α → Sort u1} {b : α} (h : a = b) (m : motive a) : motive b :=
   Eq.ndrec m h