Schemes isomorphic to affine schemes are affine

Stream: Is there code for X?

[Michał Mrugała]

I'm very surprised that the following examples are not closed by exact?. They shouldn't be difficult to prove using mem_Spec_essImage, but am I missing something obvious here? Should these be added to Mathlib?

import Mathlib.AlgebraicGeometry.AffineScheme

open AlgebraicGeometry

variable {X : Scheme}

example {Y : Scheme} [IsAffine Y] (h : X ≅ Y) : IsAffine X  := sorry --by exact?

example {R : CommRingCat} (h : X ≅ Spec R) : IsAffine X := sorry --by exact?

[Markus Himmel]

docs#AlgebraicGeometry.isAffine_of_isIso exists, it's a bit sad (but not surprising) that exact? cannot find it.

[Michał Mrugała]

Thanks, this is exactly what I needed. Do you think it's worth PRing the "morphism"-free version?