allow "rcases with" tactic

server/leanserver/GameServer/FileWorker.lean

@@ -76,7 +76,8 @@ partial def findForbiddenTactics (inputCtx : Parser.InputContext) (level : GameL
       findForbiddenTactics inputCtx level arg
   | .atom info val =>
     -- ignore syntax elements that do not start with a letter
-    if 0 < val.length ∧ val.data[0]!.isAlpha then
+    -- and ignore "with" keyword
+    if 0 < val.length ∧ val.data[0]!.isAlpha ∧ val != "with" then
       if ¬ ((level.tactics.map (·.name.toString))).contains val then
         addErrorMessage info s!"You have not unlocked the tactic '{val}' yet!"
       else if level.disabledTactics.contains val

server/testgame/TestGame/Levels/Proposition/L10_And.lean

@@ -33,7 +33,7 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ (B ∧ C)) : B =>
 HiddenHint (A : Prop) (hA : A) : A =>
   "Du hast einen Beweis dafür in den *Annahmen*."
 
-NewTactics constructor assumption
+NewTactics rcases
 DisabledTactics tauto
 
 -- Statement