From 8e81f03e3aae0ebfa9fa245bf125b06fa468096f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 6 May 2021 15:43:56 -0700
Subject: [PATCH] chore: adjust `stdlib` to recent changes

---
 src/Init/Data/Nat/Div.lean              | 2 +-
 src/Lean/Data/Lsp/LanguageFeatures.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/Nat/Div.lean b/src/Init/Data/Nat/Div.lean
index 81725f821d..729bdf0b41 100644
--- a/src/Init/Data/Nat/Div.lean
+++ b/src/Init/Data/Nat/Div.lean
@@ -95,7 +95,7 @@ theorem mod_lt (x : Nat) {y : Nat} : y > 0 → x % y < y := by
       exact hgt
   | ind x y h h₂ =>
     intro h₃
-    let ⟨_, h₁⟩ := h
+    have ⟨_, h₁⟩ := h
     rw [mod_eq_sub_mod h₁]
     exact h₂ h₃
 
diff --git a/src/Lean/Data/Lsp/LanguageFeatures.lean b/src/Lean/Data/Lsp/LanguageFeatures.lean
index efc12a85cc..9650660af0 100644
--- a/src/Lean/Data/Lsp/LanguageFeatures.lean
+++ b/src/Lean/Data/Lsp/LanguageFeatures.lean
@@ -166,7 +166,7 @@ partial instance : ToJson DocumentSymbol where
   toJson :=
     let rec go
       | DocumentSymbol.mk sym =>
-        have ToJson DocumentSymbol := ⟨go⟩
+        have ToJson DocumentSymbol from ⟨go⟩
         toJson sym
     go