Synthetization order error

Stream: new members

[Suryansh Shrivastava]

I was proving a topological space as T0, but I got the following error:-

cannot find synthesization order for instance FPT_T₀ with type
∀ (α : Type u) [t : TopologicalSpace α] [f : Fintype α] (p : α) [t1 : FiniteParticularPointTopology α p], T0Space α
all remaining arguments have metavariables:
@FiniteParticularPointTopology α ?p t f

the code uses a lot of inheritances, so if you guys need it to solve this error, you can mention it and I'll try to make the most compact version of it

[Patrick Massot]

Did you read Section 7.1 of #mil? It explains what this error message means.