feat: make Theorem an Inhabited instance (#12324)

This PR adds a default `Inhabited` instance to `Theorem` type.

The need to do so came up in #12296 , as `Theorem` is one of the entries
of the structure which is the key entry of `SimpleScopedEnvExtension`.

src/Lean/Meta/Sym/Simp/Theorems.lean

@@ -24,6 +24,7 @@ structure Theorem where
   pattern : Pattern
   /-- Right-hand side of the equation. -/
   rhs     : Expr
+  deriving Inhabited
 
 instance : BEq Theorem where
   beq thm₁ thm₂ := thm₁.expr == thm₂.expr