chore(AlgebraicGeometry): use Cover.idx instead of Exists.choose in Cover.ulift (#31236)

This makes it have better `simps` lemmas.

Author: chrisflav

Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean

@@ -231,7 +231,7 @@ def AffineCover.cover {X : Scheme.{u}} (𝒰 : X.AffineCover P) :
 @[simps!]
 def Cover.ulift (𝒰 : Cover.{v} (precoverage P) X) : Cover.{u} (precoverage P) X where
   I₀ := X
-  X x := 𝒰.X (𝒰.exists_eq x).choose
+  X x := 𝒰.X (𝒰.idx x)
   f x := 𝒰.f _
   mem₀ := by
     rw [presieve₀_mem_precoverage_iff]

Mathlib/AlgebraicGeometry/Gluing.lean

@@ -732,7 +732,7 @@ def isColimitForgetToLocallyRingedSpace :
         reassoc_of% GlueData.ι_isoLocallyRingedSpace_inv,
         ← cancel_epi (Hom.isoOpensRange (F.map _)).hom.toLRSHom]
       simp only [Opens.iSupOpenCover, Cover.ulift, V, ← Hom.comp_toLRSHom_assoc,
-        Cover.ι_fromGlued_assoc, homOfLE_ι, Hom.isoOpensRange_hom_ι]
+        Cover.ι_fromGlued_assoc, homOfLE_ι, Hom.isoOpensRange_hom_ι, Cover.idx]
       generalize_proofs _ _ h
       rw [homOfLE_tAux F ↓i ↓j h.choose.2.1 h.choose.2.2, Iso.hom_inv_id_assoc]
       exact (s.w h.choose.2.1).trans (s.w h.choose.2.2).symm)