chore: lean 3 behavior for apply

src/Lean/Meta/Basic.lean

@@ -399,6 +399,9 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
 @[inline] def withTransparency {α} (mode : TransparencyMode) : n α → n α :=
   mapMetaM <| withConfig (fun config => { config with transparency := mode })
 
+@[inline] def withDefault {α} (x : n α) : n α :=
+  withTransparency TransparencyMode.default x
+
 @[inline] def withReducible {α} (x : n α) : n α :=
   withTransparency TransparencyMode.reducible x
 

src/Lean/Meta/Tactic/Apply.lean

@@ -16,7 +16,7 @@ namespace Lean.Meta
   (?m ...) where ?m is an unassigned metavariable.
 -/
 private def getExpectedNumArgsAux (e : Expr) : MetaM (Nat × Bool) :=
-  withReducible $ forallTelescopeReducing e fun xs body =>
+  withDefault <| forallTelescopeReducing e fun xs body =>
     pure (xs.size, body.getAppFn.isMVar)
 
 private def getExpectedNumArgs (e : Expr) : MetaM Nat := do

tests/lean/run/applytransp.lean

@@ -0,0 +1,5 @@
+theorem ex1 (h₁ : ¬ p) (h₂ : q → p) : ¬ q := by
+  intro h
+  apply h₁
+  apply h₂
+  apply h