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