awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
right :
  Q (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (S :=
    (↑(CommRingCat.of
          (↑Γ(X,
                X.basicOpen (U := f ⁻¹ᵁ ⊤)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.appTop f) :
                      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                    r)) :
            Type u)) :
      Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
          (↑Γ(X,
                X.basicOpen (U := f ⁻¹ᵁ ⊤)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.appTop f) :
                      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                    r)) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) r)))
⊢ Q (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)))

Tactic:
rw [(isAffineOpen_top Y).app_basicOpen_eq_away_map f (isAffineOpen_top X),
        CommRingCat.hom_comp, hPi.cancel_right_isIso, ← Scheme.Hom.appTop]

Premises used: AlgebraicGeometry.isAffineOpen_top, RingHom.RespectsIso.cancel_right_isIso, AlgebraicGeometry.Scheme.Hom.appTop, CommRingCat.hom_comp, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
right :
  Q (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (S :=
    (↑Γ(X,
          X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              r)) :
      Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
          (↑Γ(X,
                X.basicOpen (U := ⊤)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.appTop f) :
                      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                    r)) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) r)))
⊢ Q (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (S :=
    (↑(CommRingCat.of
          (↑Γ(X,
                X.basicOpen (U := f ⁻¹ᵁ ⊤)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.appTop f) :
                      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                    r)) :
            Type u)) :
      Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
          (↑Γ(X,
                X.basicOpen (U := f ⁻¹ᵁ ⊤)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.appTop f) :
                      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                    r)) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) r)))

Tactic:
dsimp only [Opens.map_top]

Premises used: TopologicalSpace.Opens.map_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
right : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (S :=
    (↑Γ(X,
          X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              r)) :
      Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
          (↑Γ(X,
                X.basicOpen (U := ⊤)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.appTop f) :
                      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                    r)) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) r)))

Tactic:
apply hQl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
hf

Premises used: Set.Mem, Set.univ, setOf, Set.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
h_1 : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
exact hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
hs₁ :
  Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.span
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
        (↑s : Set (↑Γ(Y, ⊤) : Type u))))
    ⊤
hs₂ :
  ∀ (i : (↑Γ(X, ⊤) : Type u)),
    Membership.mem (γ := Set (↑Γ(X, ⊤) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop f)) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
          (↑s : Set (↑Γ(Y, ⊤) : Type u)))
        i →
      IsAffineOpen (X.basicOpen i)
⊢ IsAffine X

Tactic:
apply isAffine_of_isAffineOpen_basicOpen (f.appTop '' s)

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Hom.appTop, SetLike.coe, Set.image, AlgebraicGeometry.isAffine_of_isAffineOpen_basicOpen, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
⊢ Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))))
    (Ideal.map (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ⊤)

Tactic:
apply_fun Ideal.map (f.appTop).hom at hs

Premises used: CommRingCat.Hom.hom, AlgebraicGeometry.Scheme.Hom.appTop, Ideal.map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
hs :
  Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))))
    (Ideal.map (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ⊤)
hs₁ :
  ∀
    (hs :
      Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
        (Ideal.span
          ((⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) : (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
            (↑s : Set (↑Γ(Y, ⊤) : Type u))))
        (Ideal.map (R := (↑Γ(Y, ⊤) : Type u)) (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) ⊤)),
    Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
      (Ideal.span
        ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop f)) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
          (↑s : Set (↑Γ(Y, ⊤) : Type u))))
      ⊤
hs₂ hs₃ hs₄ hs₅ :
  ∀
    (hs :
      Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
        (Ideal.span
          ((⇑(CommRingCat.Hom.hom (Scheme.Hom.appTop f)) : (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
            (↑s : Set (↑Γ(Y, ⊤) : Type u))))
        ⊤),
    Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
      (Ideal.span
        ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop f)) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
          (↑s : Set (↑Γ(Y, ⊤) : Type u))))
      ⊤
⊢ Eq (α := Ideal (↑Γ(X, ⊤) : Type u))
    (Ideal.span
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appTop f)) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u)) ''
        (↑s : Set (↑Γ(Y, ⊤) : Type u))))
    ⊤

Tactic:
rwa [Ideal.map_span, Ideal.map_top] at hs

Premises used: Ideal.map_span, Ideal.map_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
r : (↑Γ(Y, ⊤) : Type u)
hr : r ∈ (↑s : Set (↑Γ(Y, ⊤) : Type u))
⊢ ∀ (r : ↥s),
    IsAffine.{u}
        (↑(X.basicOpen (U := f ⁻¹ᵁ ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                (↑r : (↑Γ(Y, ⊤) : Type u)))) :
          Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))

Tactic:
simp_rw [Scheme.preimage_basicOpen] at hf

Premises used: AlgebraicGeometry.Scheme.preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
r : (↑Γ(Y, ⊤) : Type u)
hr : r ∈ (↑s : Set (↑Γ(Y, ⊤) : Type u))
hf :
  ∀ (r : ↥s),
    IsAffine.{u}
        (↑(X.basicOpen (U := f ⁻¹ᵁ ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                (↑r : (↑Γ(Y, ⊤) : Type u)))) :
          Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
⊢ IsAffineOpen
    (X.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop f) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
        r))

Tactic:
(hf ⟨r, hr⟩).left

Premises used: Set.Mem, Set.univ, setOf, AlgebraicGeometry.IsAffineOpen, Subtype.mk, Set.preimage, And.left
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
r : (↑Γ(Y, ⊤) : Type u)
hr : r ∈ (↑s : Set (↑Γ(Y, ⊤) : Type u))
hf :
  ∀ (r : ↥s),
    IsAffine.{u}
        (↑(X.basicOpen (U := f ⁻¹ᵁ ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u))
                (↑r : (↑Γ(Y, ⊤) : Type u)))) :
          Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
⊢ IsAffineOpen
    (X.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appTop f) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
        r))

Tactic:
exact (hf ⟨r, hr⟩).left

Premises used: Subtype.mk, And.left
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
⊢ IsAffine X

Tactic:
haveI : IsAffine X := by
      apply isAffine_of_isAffineOpen_basicOpen (f.appTop '' s)
      · apply_fun Ideal.map (f.appTop).hom at hs
        rwa [Ideal.map_span, Ideal.map_top] at hs
      · rintro - ⟨r, hr, rfl⟩
        simp_rw [Scheme.preimage_basicOpen] at hf
        exact (hf ⟨r, hr⟩).left
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
this : IsAffine X
⊢ affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
⟨inferInstance, hQs.ofIsLocalization' hPi (f.appTop).hom s hs fun a ↦ ?_⟩

Premises used: CommRingCat.Hom.hom, RingHom.OfLocalizationSpan.ofIsLocalization', AlgebraicGeometry.Scheme.Hom.appTop, inferInstance, SetLike.coe, AlgebraicGeometry.affineAnd, And.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
this : IsAffine X
refine :
  ∀ (a : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)),
    ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra (↑Γ(Y, ⊤) : Type u) Rᵣ) (x_3 :
      Algebra (↑Γ(X, ⊤) : Type u) Sᵣ) (x_4 : IsLocalization.Away (↑a : (↑Γ(Y, ⊤) : Type u)) Rᵣ) (x_5 :
      IsLocalization.Away (R := (↑Γ(X, ⊤) : Type u))
        ((CommRingCat.Hom.hom (Scheme.Hom.appTop f) : (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            (↑a : (↑Γ(Y, ⊤) : Type u)) :
          (↑Γ(X, ⊤) : Type u))
        Sᵣ),
      Q (IsLocalization.Away.map Rᵣ Sᵣ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (↑a : (↑Γ(Y, ⊤) : Type u)))
⊢ affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
refine ⟨inferInstance, hQs.ofIsLocalization' hPi (f.appTop).hom s hs fun a ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
this : IsAffine X
a : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)
⊢ ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra (↑Γ(Y, ⊤) : Type u) Rᵣ) (x_3 :
    Algebra (↑Γ(X, ⊤) : Type u) Sᵣ) (x_4 : IsLocalization.Away (↑a : (↑Γ(Y, ⊤) : Type u)) Rᵣ) (x_5 :
    IsLocalization.Away (R := (↑Γ(X, ⊤) : Type u))
      ((CommRingCat.Hom.hom (Scheme.Hom.appTop f) : (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑a : (↑Γ(Y, ⊤) : Type u)) :
        (↑Γ(X, ⊤) : Type u))
      Sᵣ),
    Q (IsLocalization.Away.map Rᵣ Sᵣ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (↑a : (↑Γ(Y, ⊤) : Type u)))

Tactic:
⟨Γ(Y, Y.basicOpen a.val), Γ(X, X.basicOpen (f.appTop a.val)), inferInstance,
      inferInstance, inferInstance, inferInstance, inferInstance, ?_, ?_⟩

Premises used: CommRingCat.carrier, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Hom.appTop, inferInstance, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.Scheme.basicOpen, Exists.intro, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Subtype.val, DFunLike.coe, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace