fix: mkAppM to typecheck at .default transparency (#7957)

This PR ensures that `mkAppM` can be used to construct terms that are
only type-correct at at default transparency, even if we are in
`withReducible` (e.g. in simp), so that simp does not stumble over
simplifying `let` expression with simplifiable type.reliable.

Here is a reproducer of the issue this solves:
```
example (a b : Nat) (h : a = b):
  (let _ : id Bool := true; a) = (let _ : Bool := true; b) := by
  simp -zeta -zetaDelta [h]
```

This fixes #7826.

src/Lean/Meta/AppBuilder.lean

@@ -304,7 +304,7 @@ private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : Met
         | _ =>
           let x := xs[i]
           let xType ← inferType x
-          if (← isDefEq d xType) then
+          if (← withAtLeastTransparency .default (isDefEq d xType)) then
             loop b (i+1) j (args.push x) instMVars
           else
             throwAppTypeMismatch (mkAppN f args) x

tests/lean/run/issue7826.lean

@@ -0,0 +1,39 @@
+axiom SparseSet : Nat → Type
+
+def SparseSet.insert {n} (set : SparseSet n) (v : Fin n) : SparseSet n := sorry
+
+inductive Node where
+  | epsilon (next : Nat)
+
+structure NFA where
+  nodes : Array Node
+
+def NFA.get (nfa : NFA) (i : Nat) (h : i < nfa.nodes.size) : Node :=
+  nfa.nodes[i]
+
+structure Strategy' where
+  T : Type
+
+-- set_option trace.Meta.appBuilder true
+-- set_option trace.Meta.isDefEq true
+
+def εClosure (σ : Strategy') (nfa : NFA) (states : SparseSet nfa.nodes.size) (stack : List (Fin nfa.nodes.size)) :
+  -- REPRO: using `σ.T` is necessary to reproduce.
+  Option σ.T :=
+  match stack with
+  | [] => .none
+  | state :: stack' =>
+    -- REPRO: removing this `if` fixes the error.
+    if true then
+      εClosure σ nfa states stack'
+    else
+      -- REPRO: this insert is necessary to reproduce.
+      let states' := states.insert state
+      match nfa.get state state.isLt with
+      | .epsilon state' =>
+        -- REPRO: this line is also necessary to reproduce.
+        have isLt : state' < nfa.nodes.size := sorry
+        sorry
+-- REPRO: using well-founded recursion is necessary to reproduce.
+-- NOTE: the original code uses well-founded recursion to take visited states (`states`) into account.
+termination_by /-structural-/ stack

tests/lean/run/issue7826a.lean

@@ -0,0 +1,3 @@
+example (a b : Nat) (h : a = b):
+  (let _ : id Bool := true; a) = (let _ : Bool := true; b) := by
+  simp -zeta -zetaDelta [h]