How much of mathlib4 can be ported to Coq using this?

[ruplet]

Hey,

I wonder if we could use the developments in this project to detect proofs in mathlib / other important Lean libraries, known proofs of which are fundamentally not transferable easily to Rocq. I know that this project requires definitional UIP, which is a big problem, but I also know that Lean itself assumes UIP. But it is, I think, easy in Lean to find out specific axioms used in proofs and maybe:
a) find theorems in Lean which have no known proof in Coq
b) translate all the remaining to Coq using this project

Do you think we could do it? If so, I would be more than eager to contribute to the project

[JasonGross]

I'm not sure how far into mathlib the importer works (it should not be too hard to check), but last I checked, it falls over in the standard library around the proof of USize.size_eq. Lean uses an optimized representation for Nat literals and has special handling for conversion involving them. Coq does not have such special handling, so any code that relies on conversion of very large Nat literals (either in the types, or in the proofs) is hard to translate.