fix: use default transparency for mkAppOptM in propagateCtorHomo

`propagateCtorHomo` constructs injectivity proofs via `mkAppOptM`, which
unifies implicit arguments at the current transparency. For indexed
inductive types like `Vector`, the implicit size argument may require
default transparency to unify (e.g., `({ toList := [] }.mapFinIdx f).size`
with `0`). Without this, `mkAppOptM` throws `throwAppTypeMismatch`.

Previously, `isDefEqBounded` in the canonicalizer masked this by eagerly
unifying such arguments during canonicalization. This fix addresses the
root cause, enabling the removal of `isDefEqBounded`.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

src/Lean/Meta/Tactic/Grind/Ctor.lean

@@ -51,7 +51,7 @@ private def propagateCtorHomo (α : Expr) (a b : Expr) : GoalM Unit := do
     There is no guarantee that `inferType (← mkEqProof a b)` is structurally equal to `a = b`.
     -/
     let mask := mask.set! (n-1) (some (← mkExpectedTypeHint (← mkEqProof a b) (← mkEq a b)))
-    let injLemma ← mkAppOptM injDeclName mask
+    let injLemma ← withDefault <| mkAppOptM injDeclName mask
     let injLemmaType ← inferType injLemma
     let gen := max (← getGeneration a) (← getGeneration b)
     propagateInjEqs injLemmaType injLemma gen