Is mutual inductive type definition essential in coq core language?
It is always possible, as you noted, to translate a mutual inductive family into a non-mutual family, in much the same way as you described.
A couple of difficulties though:

If your mutual inductives are not parametrized, say you have

Inductive Foo := foo : Bar -&gt; Foo
with Bar := bar : Foo -&gt; Bar

(with some constants if you want to make the types non-empty)
Then you have 2 non-dependent types, for which induction, recursion and pattern matching are rather straightforward. But the translation you suggest involve creating a FooBar : bool -&gt; Type which now needs dependent pattern matching everywhere. It's not impossible to cope with this as well, but it makes the elaborator quite a bit more involved.

Even worse are mutual inductives with different parameters: Imagine now

Inductive Foo : nat -&gt; Type := ...
with Bar : bool -&gt; Type := ...

Now we need to define a type FooBar : forall b : bool, I b -&gt; Type where I true = nat and I false = nat. I'll let you imagine the case of multiple, possibly dependent parameters.
All these complications add up to a system that is quite complicated: I think it's a reasonable decision to add special support in the core to handle mutually inductive families, and it's the decision the Coq developers have made.
The Lean developers originally made a different decision, see here for instance.
However my understanding is that the complexities outlined above, along with the difficulty of hiding all this to the user, has made them re-think their position (I believe, but at the moment I can't find the reference of how things are in Lean 4).