From 5baa1627139234c73571e71aad5bf9dedb7be26a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 5 Jan 2021 12:28:47 -0800
Subject: [PATCH] chore: lean 3 behavior for `apply`

---
 src/Lean/Meta/Basic.lean        | 3 +++
 src/Lean/Meta/Tactic/Apply.lean | 2 +-
 tests/lean/run/applytransp.lean | 5 +++++
 3 files changed, 9 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/applytransp.lean

diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 2684c7b730..34a4ae7ee0 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/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
 
diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean
index 75b96d0dd9..539bb1d9aa 100644
--- a/src/Lean/Meta/Tactic/Apply.lean
+++ b/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
diff --git a/tests/lean/run/applytransp.lean b/tests/lean/run/applytransp.lean
new file mode 100644
index 0000000000..4bafb41f26
--- /dev/null
+++ b/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