fix: wildcard generalize only generalizes visible theorems

`generalize ... at *` sometimes will try to modify the recursive hypothesis
corresponding to the current theorem being defined, which may not be the
expected behaviour.  It should only try to `generalize` hypotheses that it can
actually modify and are visible, not implementation details. Otherwise this
means that there are discrepancies between `generalize ... at *` and `generalize
... at H`, even though `H` is the only hypothesis in the context.

This commit uses `getLocalHyps` instead of `getFVarIds` to get the current valid
`FVarIds` in the context.  This uses `isImplementationDetail` to filter out
`FVarIds` that are implementation details in the context and are not visible to
the user and should not be manipulated by `generalize`.

Closes 4845

src/Lean/Elab/Tactic/Generalize.lean

@@ -30,7 +30,7 @@ open Meta
       args := args.push { hName?, expr, xName? := arg[3].getId : GeneralizeArg }
     let hyps ← match expandOptLocation stx[2] with
     | .targets hyps _ => getFVarIds hyps
-    | .wildcard => pure (← getLCtx).getFVarIds
+    | .wildcard => pure ((← getLocalHyps).map (·.fvarId!))
     let mvarId ← getMainGoal
     mvarId.withContext do
       let (_, newVars, mvarId) ← mvarId.generalizeHyp args hyps

tests/lean/4845.lean

@@ -0,0 +1,12 @@
+/-!
+  Generalize should not try to abstract the variable from hypotheses that are
+  implementation details. -/
+
+/-!
+  In this case, generalize tries to revert the lemma being defined to generalize
+  the 0 in it. -/
+
+example : 0 = 0 → True := by
+  intro H; generalize _H : 0 = z at *
+  trace_state
+  constructor

tests/lean/4845.lean.expected.out

@@ -0,0 +1,4 @@
+z : Nat
+_H : 0 = z
+H : z = z
+⊢ True