Lean and inaccessible cardinals

Question

Here it is claimed that Lean's type theory is equiconsistent with ZFC + existence of $n$ inaccessible cardinals for every natural $n$. This is a bit worrying if you just want to work with pure ZFC: how do you know if the proof in Lean didn't use the existence of inaccessible cardinals? A first thought would be checking that the proof used didn't use Type u for u bigger than $0$, but someone told me this is not enough. Can someone offer more insight into this?