is_affine_open dot chaos

Stream: general

[Kevin Buzzard]

Is X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier fixed in Lean 4?

import algebraic_geometry.AffineScheme

open algebraic_geometry

#check @is_affine_open
/-
Π {X : Scheme},
  topological_space.opens ↥(X.to_LocallyRingedSpace.to_SheafedSpace.to_PresheafedSpace.carrier) → Prop
-/

[Eric Wieser]

It's fixable in lean 3 by using old-style structures