`FG.dehomogenize_isPolytope ` in `Polyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Homogenization` its pretty involved actually
FG.dehomogenize_isPolytopeinPolyhedral.Mathlib.Geometry.Convex.ConvexSpace.Polytope.Homogenizationits pretty involved actually