feat(Tactic/SimpIntro): add support for introducing non-propositions (#24372)

This PR improves the `simp_intro` tactic so that it can be used when there are non-propositions. Non-propositions are not added to the simp set. This lets `simp_intro` be used in situations that previously needed manual `intro` and `simp`.

For example, the following one can be solved like this

```lean
example (r : Nat → Prop) : (∀ x, x > 0 → r x) → ∀ y z, y = 0 → z > y → r z := by
  simp
  intro hr
  try simp at hr -- does nothing
  try simp [hr] -- does nothing
  intro y z
  try simp [hr] -- does nothing
  intro hy
  try simp [hr] at hy -- does nothing
  simp [hr, hy]
  intro hyz
  try simp [hr, hy] at hyz
  simp [hr, hy, hyz] -- accomplish the goal successfully
```

while the previous `simp_intro` cannot introduce `y` and `z` here.

```lean
example (r : Nat → Prop) : (∀ x, x > 0 → r x) → ∀ y z, y = 0 → z > y → r z := by
  /- the previous `simp_intro` fails with message:
     invalid 'simp', proposition expected
       Nat  -/
  simp_intro ..   -- or `simp_intro hr y`

example (r : Nat → Prop) : (∀ x, x > 0 → r x) → ∀ y z, y = 0 → z > y → r z := by
  -- unsolved
  simp_intro hr
```

Now with this PR, the tactic is successful:
```lean
example (r : Nat → Prop) : (∀ x, x > 0 → r x) → ∀ y z, y = 0 → z > y → r z := by
  simp_intro ..   -- or `simp_intro hr y z hy hz`
```

Author: Hagb

Mathlib/Tactic/SimpIntro.lean

@@ -30,8 +30,13 @@ partial def simpIntroCore (g : MVarId) (ctx : Simp.Context) (simprocs : Simp.Sim
   let n := if var.isIdent then var.getId else `_
   let withFVar := fun (fvar, g) ↦ g.withContext do
     Term.addLocalVarInfo var (mkFVar fvar)
-    let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar fvar) (.fvar fvar)
-    simpIntroCore g (ctx.setSimpTheorems simpTheorems) simprocs discharge? more ids'
+    let ctx : Simp.Context ←
+      if (← Meta.isProp <| ← fvar.getType) then
+        let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar fvar) (.fvar fvar)
+        pure <| ctx.setSimpTheorems simpTheorems
+      else
+        pure ctx
+    simpIntroCore g ctx simprocs discharge? more ids'
   match t with
   | .letE .. => withFVar (← g.intro n)
   | .forallE (body := body) .. =>

MathlibTest/simp_intro.lean

@@ -14,3 +14,9 @@ example (h : y = z) : x + 0 = y → x = z := by
   simp_intro .. [h]
 
 example (h : y = z) : x + 0 = y → x = z := by simp_intro _; exact h
+
+example : ∀ (r : Nat → Prop), (∀ x, x > 0 → r x) → ∀ y z, y = 0 → z > y → r z := by
+  simp_intro ..
+
+example : ∀ (r : Nat → Prop), (∀ x, x > 0 → r x) → ∀ y z, y = 0 → z > y → r z := by
+  simp_intro r hr y z hy hz