Special-case Prop-valued fields in `simps`

simps does not consider whether a field of a structure is Prop-valued or not. This means the lemmas it generates don't follow the convention in three ways:

• The name use UpperCamelCase instead of lowerCamelCase. This can be solved on a case-by-case basis using initialize_simps_projection, but hopefully we can just change the default behavior.
• The lemma is stated using =, not ↔.
• The lemma is stated with too many explicit arguments.

In the following example, simps handles bar correctly but not Baz.

import Mathlib.Tactic.Simps.Basic

structure Foo where
  bar : Nat
  Baz : Prop

@[simps]
def myFoo (n : Nat) : Foo where
  bar := n
  Baz := False

#check myFoo_bar
-- myFoo_Bar (n : Nat) : (myFoo n).Bar = n
#check myFoo_Baz
-- myFoo_Baz (n : Nat) : (myFoo n).Baz = False
-- We instead want:
-- myFoo_baz {n : Nat} : (myFoo n).Baz ↔ False

Start with the Mathlib.Tactic.Simps.Basic module and the simps behavior shown in the example. Compare the generated declarations for the bar : Nat and Baz : Prop fields, and inspect initialize_simps_projection for the existing special-case behavior. Done means Prop-valued fields use lowerCamelCase names, ↔, and implicit arguments by default.