diff --git a/src/Init/Data/String/Extra.lean b/src/Init/Data/String/Extra.lean
index b96b36fb23..89fd79abc7 100644
--- a/src/Init/Data/String/Extra.lean
+++ b/src/Init/Data/String/Extra.lean
@@ -104,8 +104,7 @@ where
 
 /--
 Decodes an array of bytes that encode a string as [UTF-8](https://en.wikipedia.org/wiki/UTF-8) into
-the corresponding string. Invalid UTF-8 characters in the byte array result in `(default : Char)`,
-or `'A'`, in the string.
+the corresponding string.
 -/
 @[extern "lean_string_from_utf8_unchecked"]
 def fromUTF8 (a : @& ByteArray) (h : validateUTF8 a) : String :=
diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 5588fcf532..5361aec984 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -1025,7 +1025,7 @@ The form
 ```
 fun_induction f
 ```
-(with no arguments to `f`) searches the goal for an unique eligible application of `f`, and uses
+(with no arguments to `f`) searches the goal for a unique eligible application of `f`, and uses
 these arguments. An application of `f` is eligible if it is saturated and the arguments that will
 become targets are free variables.
 
@@ -1058,7 +1058,7 @@ The form
 ```
 fun_cases f
 ```
-(with no arguments to `f`) searches the goal for an unique eligible application of `f`, and uses
+(with no arguments to `f`) searches the goal for a unique eligible application of `f`, and uses
 these arguments. An application of `f` is eligible if it is saturated and the arguments that will
 become targets are free variables.