Apply suggestions from code review

Co-authored-by: Jovan Gerbscheid <56355248+JovanGerb@users.noreply.github.com>

Author: staroperator

Mathlib/Tactic/FunProp/Mor.lean

@@ -135,9 +135,8 @@ where
       go (.app (.app c f) x) as
     | .app f a, as => go f (as.push { expr := a })
     | .forallE x t b bi, _ => do
-      let u := (← inferType t).sortLevel!
-      let v := (← withLocalDecl x bi t fun x => do
-        return (← inferType (b.instantiate1 x)).sortLevel!)
+      let u ← getLevel t
+      let v ← withLocalDecl x bi t fun x => getLevel (b.instantiate1 x)
       k (.const `_Forall [u, v]) #[{ expr := t }, { expr := .lam x t b bi }]
     | f, as => k f as.reverse
 
@@ -163,11 +162,11 @@ def getAppArgs (e : Expr) : MetaM (Array Arg) := withApp e fun _ xs => return xs
 
 /-- `mkAppN f #[a₀, ..., aₙ]` ==> `f a₀ a₁ .. aₙ` where `f` can be bundled morphism. -/
 def mkAppN (f : Expr) (xs : Array Arg) : Expr :=
-  let fn :=
+  let f :=
     if f.isConstOf `_Forall then
       Expr.mkLambdaForall f.constLevels![0]! f.constLevels![1]!
     else f
-  xs.foldl (init := fn) (fun f x =>
+  xs.foldl (init := f) (fun f x =>
     match x with
     | ⟨x, .none⟩ => (f.app x)
     | ⟨x, some coe⟩ => (coe.app f).app x)