diff --git a/src/Init/Control/Alternative.lean b/src/Init/Control/Alternative.lean
index 91a94fdb71..46f4de4837 100644
--- a/src/Init/Control/Alternative.lean
+++ b/src/Init/Control/Alternative.lean
@@ -10,9 +10,9 @@ universes u v
 
 class Alternative (f : Type u → Type v) extends Applicative f : Type (max (u+1) v) :=
   (failure : {α : Type u} → f α)
-  (orelse  : {α : Type u} → f α → f α → f α)
+  (orElse  : {α : Type u} → f α → f α → f α)
 
-instance (f : Type u → Type v) (α : Type u) [Alternative f] : OrElse (f α) := ⟨Alternative.orelse⟩
+instance (f : Type u → Type v) (α : Type u) [Alternative f] : OrElse (f α) := ⟨Alternative.orElse⟩
 
 variables {f : Type u → Type v} [Alternative f] {α : Type u}
 
diff --git a/src/Init/Control/Option.lean b/src/Init/Control/Option.lean
index 23089b207f..d753eede38 100644
--- a/src/Init/Control/Option.lean
+++ b/src/Init/Control/Option.lean
@@ -32,7 +32,7 @@ instance : Monad (OptionT m) := {
   bind := OptionT.bind
 }
 
-@[inline] protected def orelse (x : OptionT m α) (y : OptionT m α) : OptionT m α := id (α := m (Option α)) do
+@[inline] protected def orElse (x : OptionT m α) (y : OptionT m α) : OptionT m α := id (α := m (Option α)) do
   match (← x) with
   | some a => pure (some a)
   | _      => y
@@ -42,7 +42,7 @@ instance : Monad (OptionT m) := {
 
 instance : Alternative (OptionT m) := {
   failure := OptionT.fail,
-  orelse  := OptionT.orelse
+  orElse  := OptionT.orElse
 }
 
 @[inline] protected def lift (x : m α) : OptionT m α := id (α := m (Option α)) do
diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean
index 7e3b49891e..3594aaa182 100644
--- a/src/Init/Control/Reader.lean
+++ b/src/Init/Control/Reader.lean
@@ -40,7 +40,7 @@ instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (ReaderT ρ m) := {
   tryCatch := fun x c r => tryCatchThe ε (x r) (fun e => (c e) r)
 }
 
-@[inline] protected def orelse [Alternative m] {α : Type u} (x₁ x₂ : ReaderT ρ m α) : ReaderT ρ m α :=
+@[inline] protected def orElse [Alternative m] {α : Type u} (x₁ x₂ : ReaderT ρ m α) : ReaderT ρ m α :=
   fun s => x₁ s <|> x₂ s
 
 @[inline] protected def failure [Alternative m] {α : Type u} : ReaderT ρ m α :=
@@ -76,7 +76,7 @@ instance (ρ m) [Monad m] : MonadFunctor m (ReaderT ρ m) := ⟨fun f x r => f (
 
 instance [Alternative m] : Alternative (ReaderT ρ m) := {
   failure := ReaderT.failure,
-  orelse  := ReaderT.orelse
+  orElse  := ReaderT.orElse
 }
 
 end
diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean
index b1a5bf90f5..d965cc117b 100644
--- a/src/Init/Control/State.lean
+++ b/src/Init/Control/State.lean
@@ -52,7 +52,7 @@ instance : Monad (StateT σ m) := {
    map := StateT.map
 }
 
-@[inline] protected def orelse [Alternative m] {α : Type u} (x₁ x₂ : StateT σ m α) : StateT σ m α :=
+@[inline] protected def orElse [Alternative m] {α : Type u} (x₁ x₂ : StateT σ m α) : StateT σ m α :=
   fun s => x₁ s <|> x₂ s
 
 @[inline] protected def failure [Alternative m] {α : Type u} : StateT σ m α :=
@@ -60,7 +60,7 @@ instance : Monad (StateT σ m) := {
 
 instance [Alternative m] : Alternative (StateT σ m) := {
   failure := StateT.failure,
-  orelse  := StateT.orelse
+  orElse  := StateT.orElse
 }
 
 @[inline] protected def get : StateT σ m σ :=
diff --git a/src/Init/Data/Option/Basic.lean b/src/Init/Data/Option/Basic.lean
index 43f3958c04..a5981a61cd 100644
--- a/src/Init/Data/Option/Basic.lean
+++ b/src/Init/Data/Option/Basic.lean
@@ -62,7 +62,7 @@ instance : Monad Option := {
   | some a => p a
   | none   => false
 
-@[macroInline] protected def orelse {α : Type u} : Option α → Option α → Option α
+@[macroInline] protected def orElse {α : Type u} : Option α → Option α → Option α
   | some a, _ => some a
   | none,   b => b
 
@@ -70,7 +70,7 @@ instance : Monad Option := {
    Thus, `a <|> b` will make `Option.orelse` to behave like it was marked as `[inline]`. -/
 instance : Alternative Option := {
   failure := none,
-  orelse  := Option.orelse
+  orElse  := Option.orElse
 }
 
 @[inline] protected def lt {α : Type u} (r : α → α → Prop) : Option α → Option α → Prop
diff --git a/src/Lean/Data/SMap.lean b/src/Lean/Data/SMap.lean
index 4e10fcf606..d6eebcdf27 100644
--- a/src/Lean/Data/SMap.lean
+++ b/src/Lean/Data/SMap.lean
@@ -44,7 +44,7 @@ def empty : SMap α β := {}
 
 @[specialize] def find? : SMap α β → α → Option β
   | ⟨true, m₁, _⟩, k   => m₁.find? k
-  | ⟨false, m₁, m₂⟩, k => (m₂.find? k).orelse (m₁.find? k)
+  | ⟨false, m₁, m₂⟩, k => (m₂.find? k).orElse (m₁.find? k)
 
 @[inline] def findD (m : SMap α β) (a : α) (b₀ : β) : β :=
   (m.find? a).getD b₀
@@ -62,7 +62,7 @@ def empty : SMap α β := {}
    So, the result is correct only if we never "overwrite" `map₁` entries using `map₂`. -/
 @[specialize] def find?' : SMap α β → α → Option β
   | ⟨true, m₁, _⟩, k   => m₁.find? k
-  | ⟨false, m₁, m₂⟩, k => (m₁.find? k).orelse (m₂.find? k)
+  | ⟨false, m₁, m₂⟩, k => (m₁.find? k).orElse (m₂.find? k)
 
 /- Move from stage 1 into stage 2. -/
 def switch (m : SMap α β) : SMap α β :=
diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 0f9c0da77c..6f19b4716b 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -96,15 +96,15 @@ abbrev Delab := DelabM Syntax
 
 instance {α} : Inhabited (DelabM α) := ⟨throw $ arbitrary _⟩
 
-@[inline] protected def orelse {α} (d₁ d₂ : DelabM α) : DelabM α := do
+@[inline] protected def orElse {α} (d₁ d₂ : DelabM α) : DelabM α := do
 catchInternalId delabFailureId d₁ (fun _ => d₂)
 protected def failure {α} : DelabM α := throw $ Exception.internal delabFailureId
 instance : Alternative DelabM := {
-  orelse  := Delaborator.orelse,
+  orElse  := Delaborator.orElse,
   failure := Delaborator.failure
 }
 -- HACK: necessary since it would otherwise prefer the instance from MonadExcept
-instance {α} : OrElse (DelabM α) := ⟨Delaborator.orelse⟩
+instance {α} : OrElse (DelabM α) := ⟨Delaborator.orElse⟩
 
 -- Macro scopes in the delaborator output are ultimately ignored by the pretty printer,
 -- so give a trivial implementation.
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 74310b6dae..f62afca835 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -881,7 +881,7 @@ private def isExplicit (stx : Syntax) : Bool :=
   | _      => false
 
 private def isExplicitApp (stx : Syntax) : Bool :=
-  stx.getKind == `Lean.Parser.Term.app && isExplicit (stx.getArg 0)
+  stx.getKind == `Lean.Parser.Term.app && isExplicit stx[0]
 
 /--
   Return true if `stx` if a lambda abstraction containing a `{}` or `[]` binder annotation.
@@ -905,7 +905,8 @@ def blockImplicitLambda (stx : Syntax) : Bool :=
   Return normalized expected type if it is of the form `{a : α} → β` or `[a : α] → β` and
   `blockImplicitLambda stx` is not true, else return `none`. -/
 private def useImplicitLambda? (stx : Syntax) (expectedType? : Option Expr) : TermElabM (Option Expr) :=
-  if blockImplicitLambda stx then pure none
+  if blockImplicitLambda stx then
+    pure none
   else match expectedType? with
     | some expectedType => do
       let expectedType ← whnfForall expectedType
@@ -916,6 +917,7 @@ private def useImplicitLambda? (stx : Syntax) (expectedType? : Option Expr) : Te
 
 private def elabImplicitLambdaAux (stx : Syntax) (catchExPostpone : Bool) (expectedType : Expr) (fvars : Array Expr) : TermElabM Expr := do
   let body ← elabUsingElabFns stx expectedType catchExPostpone
+  let body ← ensureHasType expectedType body
   let r ← mkLambdaFVars fvars body
   trace[Elab.implicitForall]! r
   pure r