Merge some upgrades from updating to 2.24.0 from upstream/master

Author: Remyjck

src/Iris/ProofMode/Tactics/Assumption.lean

@@ -53,7 +53,7 @@ def assumptionFast {e} (hyps : Hyps bi e) : MetaM Q($e ⊢ $Q) := do
     hyps.removeG true fun _ _ b ty => try? do
       synthInstance q(FromAssumption $b $ty $Q)
     | failure
-  let (_ : Q(FromAssumption $b $ty $Q)) := inst
+  let _ : Q(FromAssumption $b $ty $Q) := inst
   have : $out =Q iprop(□?$b $ty) := ⟨⟩
   match fastPath with
   | .absorbing _ => return q(assumption (Q := $Q) $pf)

src/Iris/Std/DelabRule.lean

@@ -22,8 +22,7 @@ macro_rules
       | [(name, [])] => pure name
       | _           => throwUnsupported
 
-    let (p : TSyntaxArray `term) := p
-    if p.any (· matches `(`($$_))) then
+    if p.any fun t : TSyntax _ ↦ t matches `(`($$_)) then
       `(@[app_unexpander $(mkIdent f)]
         def unexpand : Lean.PrettyPrinter.Unexpander
           $[| $p => $s]*)