awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
let : P (f ≫ i)
⊢ P (f ≫ i)

Tactic:
let e : Y ≅ i.opensRange.toScheme := IsOpenImmersion.isoOfRangeEq i i.opensRange.ι (by simp)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
e : Y ≅ (↑(Scheme.Hom.opensRange i) : Scheme) := IsOpenImmersion.isoOfRangeEq i (Scheme.Hom.opensRange i).ι ⋯
⊢ f ≫ i = f ≫ e.hom ≫ (Scheme.Hom.opensRange i).ι

Tactic:
simp [e]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
e : Y ≅ (↑(Scheme.Hom.opensRange i) : Scheme) := IsOpenImmersion.isoOfRangeEq i (Scheme.Hom.opensRange i).ι ⋯
rw : P ((f ≫ e.hom) ≫ (Scheme.Hom.opensRange i).ι)
⊢ P (f ≫ i)

Tactic:
rw [show f ≫ i = f ≫ e.hom ≫ i.opensRange.ι by simp [e], ← Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
e : Y ≅ (↑(Scheme.Hom.opensRange i) : Scheme) := IsOpenImmersion.isoOfRangeEq i (Scheme.Hom.opensRange i).ι ⋯
rwa rwa₁ rwa₂ rwa₃ : P f
⊢ P (f ≫ e.hom)

Tactic:
rwa [P.cancel_right_of_respectsIso]

Premises used: CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
e : Y ≅ (↑(Scheme.Hom.opensRange i) : Scheme) := IsOpenImmersion.isoOfRangeEq i (Scheme.Hom.opensRange i).ι ⋯
⊢ P ((f ≫ e.hom) ≫ (Scheme.Hom.opensRange i).ι)

Tactic:
exact respects_isOpenImmersion_aux hQ _ (by rwa [P.cancel_right_of_respectsIso])

Premises used: _private.0.AlgebraicGeometry.HasRingHomProperty.respects_isOpenImmersion_aux
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ P.Respects IsOpenImmersion

Tactic:
have := respects_isOpenImmersion (P := P)
    (RingHom.locally_stableUnderCompositionWithLocalizationAwaySource hQ)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
⊢ P f ↔
    ∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))

Tactic:
⟨fun hf x ↦ ?_,
      fun hf ↦ (IsZariskiLocalAtSource.iff_exists_resLE (P := P)).mpr <| fun x ↦ ?_⟩

Premises used: Iff.mpr, Iff.intro, AlgebraicGeometry.IsZariskiLocalAtSource.iff_exists_resLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
refine_1 :
  ∀ (hf : P f) (x : ↥X),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
refine_2 :
  ∀
    (hf :
      ∀ (x : ↥X),
        ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
          (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
          Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
    (x : ↥X), ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), P (Scheme.Hom.resLE f U V e)
⊢ P f ↔
    ∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))

Tactic:
refine ⟨fun hf x ↦ ?_,
      fun hf ↦ (IsZariskiLocalAtSource.iff_exists_resLE (P := P)).mpr <| fun x ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
hf : P f
x : ↥X
refine_1 :
  ∀ (U : Opens ↥Y) (hU : U ∈ Y.affineOpens) (hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)),
    U ≤ ⊤ →
      ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
⊢ ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
    (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))

Tactic:
obtain ⟨U, hU, hfx, _⟩ := Opens.isBasis_iff_nbhd.mp Y.isBasis_affineOpens
      (Opens.mem_top <| f x)

Premises used: TopologicalSpace.Opens.mem_top, TopologicalSpace.Opens.isBasis_iff_nbhd, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Iff.mp, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
hf : P f
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
refine_1 :
  ∀ (V : Opens ↥X) (hV : V ∈ X.affineOpens) (hx : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
⊢ ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
    (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))

Tactic:
obtain ⟨V, hV, hx, e⟩ := Opens.isBasis_iff_nbhd.mp X.isBasis_affineOpens
      (show x ∈ f ⁻¹ᵁ U from hfx)

Premises used: TopologicalSpace.Opens.isBasis_iff_nbhd, Iff.mp, AlgebraicGeometry.Scheme.isBasis_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
hf : P f
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
⊢ ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))

Tactic:
simp_rw [HasRingHomProperty.iff_appLE (P := P), locally_iff_isLocalization hQi] at hf

Premises used: RingHom.locally_iff_isLocalization, AlgebraicGeometry.HasRingHomProperty.iff_appLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
refine_1 :
  ∀ (s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u))
    (hs :
      Eq (α := Ideal (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u))
        (Ideal.span (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u))) ⊤)
    (hfs :
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ]
          [inst_1 :
            Algebra (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp
              (algebraMap (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
                Sₜ)
              (CommRingCat.Hom.hom
                (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
                  (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens) e)))),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
⊢ ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
    (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))

Tactic:
obtain ⟨s, hs, hfs⟩ := hf ⟨U, hU⟩ ⟨V, hV⟩ e

Premises used: Subtype.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hs :
  Eq (α := Ideal (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u))
    (Ideal.span (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u))) ⊤
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ]
      [inst_1 :
        Algebra (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ]
      [IsLocalization.Away t Sₜ],
      Q
        (comp
          (algebraMap (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ)
          (CommRingCat.Hom.hom
            (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens) e)))
⊢ ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)

Tactic:
apply iSup_basicOpen_of_span_eq_top at hs

Premises used: AlgebraicGeometry.iSup_basicOpen_of_span_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ]
      [inst_1 :
        Algebra (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ]
      [IsLocalization.Away t Sₜ],
      Q
        (comp
          (algebraMap (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ)
          (CommRingCat.Hom.hom
            (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens) e)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
⊢ Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x

Tactic:
have : x ∈ (⨆ i ∈ s, X.basicOpen i) := hs.symm ▸ hx
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ]
      [inst_1 :
        Algebra (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ]
      [IsLocalization.Away t Sₜ],
      Q
        (comp
          (algebraMap (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ)
          (CommRingCat.Hom.hom
            (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens) e)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
this : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x
⊢ ∃ r ∈ s, x ∈ X.basicOpen r

Tactic:
simpa using this
-- Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
inst :
  HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this_1 : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    ∃ (s : Finset (↑Γ(X, (↑V : X.Opens)) : Type u)) (_ :
      Eq (α := Ideal (↑Γ(X, (↑V : X.Opens)) : Type u)) (Ideal.span (↑s : Set (↑Γ(X, (↑V : X.Opens)) : Type u))) ⊤),
      ∀ t ∈ s,
        ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ]
          [IsLocalization.Away t Sₜ],
          Q
            (comp (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) Sₜ)
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
s : Finset (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ]
      [inst_1 :
        Algebra (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ]
      [IsLocalization.Away t Sₜ],
      Q
        (comp
          (algebraMap (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)) : Type u) Sₜ)
          (CommRingCat.Hom.hom
            (Scheme.Hom.appLE f (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens) e)))
hs :
  ⨆ i ∈ (↑s : Set (↑Γ(X, (↑⟨V, hV⟩ : X.Opens)) : Type u)), X.basicOpen i =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V hV) : X.Opens)
this : Membership.mem (γ := X.Opens) (⨆ i ∈ s, X.basicOpen i) x
⊢ ∃ r ∈ s, x ∈ X.basicOpen r

Tactic:
have : ∃ r ∈ s, x ∈ X.basicOpen r := by simpa using this