From 5a5c7e908342651be88c35365892462a5f3a2f9f Mon Sep 17 00:00:00 2001
From: Marcus Rossel <marcusrossel@icloud.com>
Date: Sun, 12 May 2024 17:41:50 +0200
Subject: [PATCH] fix: typo in `Meta.unfoldProjInstWhenInstances?`

---
 src/Lean/Meta/ExprDefEq.lean | 4 ++--
 src/Lean/Meta/WHNF.lean      | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean
index 1876518f2466..9cd8b3b6c2b9 100644
--- a/src/Lean/Meta/ExprDefEq.lean
+++ b/src/Lean/Meta/ExprDefEq.lean
@@ -1904,8 +1904,8 @@ private def isDefEqUnitLike (t : Expr) (s : Expr) : MetaM Bool := do
 -/
 private def isDefEqProjInst (t : Expr) (s : Expr) : MetaM LBool := do
   if (← getTransparency) != .instances then return .undef
-  let t? ← unfoldProjInstWhenIntances? t
-  let s? ← unfoldProjInstWhenIntances? s
+  let t? ← unfoldProjInstWhenInstances? t
+  let s? ← unfoldProjInstWhenInstances? s
   if t?.isSome || s?.isSome then
     toLBoolM <| Meta.isExprDefEqAux (t?.getD t) (s?.getD s)
   else
diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean
index ee84d98b492c..ebd379279b36 100644
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -712,11 +712,11 @@ mutual
     | _ => return none
 
   /--
-    Auxiliary method for unfolding a class projection. when transparency is set to `TransparencyMode.instances`.
+    Auxiliary method for unfolding a class projection when transparency is set to `TransparencyMode.instances`.
     Recall that class instance projections are not marked with `[reducible]` because we want them to be
     in "reducible canonical form".
   -/
-  partial def unfoldProjInstWhenIntances? (e : Expr) : MetaM (Option Expr) := do
+  partial def unfoldProjInstWhenInstances? (e : Expr) : MetaM (Option Expr) := do
     if (← getTransparency) != TransparencyMode.instances then
       return none
     else
@@ -726,7 +726,7 @@ mutual
   partial def unfoldDefinition? (e : Expr) : MetaM (Option Expr) :=
     match e with
     | .app f _ =>
-      matchConstAux f.getAppFn (fun _ => unfoldProjInstWhenIntances? e) fun fInfo fLvls => do
+      matchConstAux f.getAppFn (fun _ => unfoldProjInstWhenInstances? e) fun fInfo fLvls => do
         if fInfo.levelParams.length != fLvls.length then
           return none
         else