awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this : CompactSpace.{u} ↥X
x : ↥X
r : (↑Γ(Y, ⊤) : Type u)
hr : IsAffineOpen (Y.basicOpen r)
hxr : Membership.mem (α := ↥Y) (↑(Y.basicOpen r) : Set ↥Y) (f x : ↥Y)
refine :
  IsAffineOpen
      (X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          r)) ∧
    x ∈
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          r)
⊢ ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r

Tactic:
refine ⟨f.appTop r, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this : CompactSpace.{u} ↥X
x : ↥X
r : (↑Γ(Y, ⊤) : Type u)
hr : IsAffineOpen (Y.basicOpen r)
hxr : Membership.mem (α := ↥Y) (↑(Y.basicOpen r) : Set ↥Y) (f x : ↥Y)
rw : IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r) ∧ x ∈ f ⁻¹ᵁ Y.basicOpen r
⊢ IsAffineOpen
      (X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          r)) ∧
    x ∈
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          r)

Tactic:
rw [← preimage_basicOpen_top]

Premises used: AlgebraicGeometry.Scheme.preimage_basicOpen_top
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this : CompactSpace.{u} ↥X
x : ↥X
r : (↑Γ(Y, ⊤) : Type u)
hr : IsAffineOpen (Y.basicOpen r)
hxr : Membership.mem (α := ↥Y) (↑(Y.basicOpen r) : Set ↥Y) (f x : ↥Y)
⊢ IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r) ∧ x ∈ f ⁻¹ᵁ Y.basicOpen r

Tactic:
⟨hr.preimage _, hxr⟩

Premises used: And.intro, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this : CompactSpace.{u} ↥X
x : ↥X
r : (↑Γ(Y, ⊤) : Type u)
hr : IsAffineOpen (Y.basicOpen r)
hxr : Membership.mem (α := ↥Y) (↑(Y.basicOpen r) : Set ↥Y) (f x : ↥Y)
⊢ IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r) ∧ x ∈ f ⁻¹ᵁ Y.basicOpen r

Tactic:
exact ⟨hr.preimage _, hxr⟩
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : X.IsQuasiAffine
x : ↥X
h : Membership.mem (γ := TopologicalSpace.Opens ↥X) ⊤ x
obtain :
  ∀ (r : (↑Γ(X, ⊤) : Type u)) (hr : IsAffineOpen (X.basicOpen r)) (hxr : x ∈ (↑(X.basicOpen r) : Set ↥X)),
    Membership.mem (γ := TopologicalSpace.Opens ↥X)
      (⨆ (i : { r : (↑Γ(X, ⊤) : Type u) // IsAffineOpen (X.basicOpen r) }), X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) x
⊢ Membership.mem (γ := TopologicalSpace.Opens ↥X)
    (⨆ (i : { r : (↑Γ(X, ⊤) : Type u) // IsAffineOpen (X.basicOpen r) }), X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) x

Tactic:
obtain ⟨_, ⟨_, ⟨r, hr, rfl⟩, rfl⟩, hxr, -⟩ :=
    (IsQuasiAffine.isBasis_basicOpen X).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Premises used: isOpen_univ, Set.mem_univ, AlgebraicGeometry.Scheme.IsQuasiAffine.isBasis_basicOpen, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : X.IsQuasiAffine
x : ↥X
h : Membership.mem (γ := TopologicalSpace.Opens ↥X) ⊤ x
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ (↑(X.basicOpen r) : Set ↥X)
⊢ Membership.mem (γ := TopologicalSpace.Opens ↥X)
    (⨆ (i : { r : (↑Γ(X, ⊤) : Type u) // IsAffineOpen (X.basicOpen r) }), X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) x

Tactic:
Opens.mem_iSup.mpr ⟨⟨r, hr⟩, hxr⟩

Premises used: Iff.mpr, TopologicalSpace.Opens.mem_iSup, Subtype.mk, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : X.IsQuasiAffine
x : ↥X
h : Membership.mem (γ := TopologicalSpace.Opens ↥X) ⊤ x
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ (↑(X.basicOpen r) : Set ↥X)
⊢ Membership.mem (γ := TopologicalSpace.Opens ↥X)
    (⨆ (i : { r : (↑Γ(X, ⊤) : Type u) // IsAffineOpen (X.basicOpen r) }), X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) x

Tactic:
exact Opens.mem_iSup.mpr ⟨⟨r, hr⟩, hxr⟩

Premises used: Iff.mpr, TopologicalSpace.Opens.mem_iSup, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this : CompactSpace.{u} ↥X
⊢ X.IsQuasiAffine

Tactic:
have := Scheme.IsQuasiAffine.of_isAffineHom f
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this : X.IsQuasiAffine
r : (↑Γ(Y, ⊤) : Type u)
⊢ IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)

Tactic:
have := isLocalization_basicOpen_of_qcqs isCompact_univ isQuasiSeparated_univ r
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
r : (↑Γ(Y, ⊤) : Type u)
this : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
⊢ IsLocalization.Away (R := (↑Γ(X, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop f) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
        r :
      (↑Γ(X, ⊤) : Type u))
    (↑Γ(X,
          X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              r)) :
      Type u)

Tactic:
have := isLocalization_basicOpen_of_qcqs isCompact_univ isQuasiSeparated_univ (f.appTop r)
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
r : (↑Γ(Y, ⊤) : Type u)
this_3 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this :
  IsLocalization.Away (R := (↑Γ(X, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop f) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
        r :
      (↑Γ(X, ⊤) : Type u))
    (↑Γ(X,
          X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              r)) :
      Type u)
⊢ IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
    (Hom.appLE f (Y.basicOpen r)
      (X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          r))
      ⋯)

Tactic:
CommRingCat.isPushout_of_isLocalization f.appTop.hom (f.appLE (Y.basicOpen r)
      (X.basicOpen (f.appTop r)) (Scheme.preimage_basicOpen_top ..).ge).hom ?_ (.powers r)

Premises used: Eq.ge, CommRingCat.Hom.hom, CategoryTheory.ConcreteCategory.hom, Set.Mem, Set.univ, setOf, AlgebraicGeometry.Scheme.preimage_basicOpen_top, AlgebraicGeometry.Scheme.Hom.appTop, AlgebraicGeometry.Scheme.Hom.appLE, Set.preimage, Submonoid.powers, AlgebraicGeometry.Scheme.basicOpen, DFunLike.coe, CommRingCat.isPushout_of_isLocalization
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
r : (↑Γ(Y, ⊤) : Type u)
this_3 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this :
  IsLocalization.Away (R := (↑Γ(X, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop f) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
        r :
      (↑Γ(X, ⊤) : Type u))
    (↑Γ(X,
          X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              r)) :
      Type u)
change :
  CommRingCat.Hom.hom
      (Y.presheaf.map (homOfLE ⋯).op ≫
        Hom.appLE f (Y.basicOpen r)
          (X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              r))
          ⋯) =
    CommRingCat.Hom.hom (Hom.appTop f ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ (CommRingCat.Hom.hom
          (Hom.appLE f (Y.basicOpen r)
            (X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                r))
            ⋯)).comp
      (algebraMap (↑Γ(Y, ⊤) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)) =
    RingHom.comp
      (algebraMap (↑Γ(X, ⊤) : Type u)
        (↑Γ(X,
              X.basicOpen (U := ⊤)
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (Hom.appTop f) :
                    (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                  r)) :
          Type u))
      (CommRingCat.Hom.hom (Hom.appTop f))

Tactic:
change CommRingCat.Hom.hom (Y.presheaf.map _ ≫ f.appLE _ _ _) =
      CommRingCat.Hom.hom (f.appTop ≫ X.presheaf.map _)

Premises used: CommRingCat.Hom.hom, AlgebraicGeometry.Scheme.Hom.appTop, AlgebraicGeometry.Scheme.Hom.appLE, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
r : (↑Γ(Y, ⊤) : Type u)
this_3 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this :
  IsLocalization.Away (R := (↑Γ(X, ⊤) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Hom.appTop f) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
        r :
      (↑Γ(X, ⊤) : Type u))
    (↑Γ(X,
          X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              r)) :
      Type u)
rw :
  CommRingCat.Hom.hom
      (Hom.appLE f ⊤
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯) =
    CommRingCat.Hom.hom (Hom.appTop f ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
rw₁ rw₂ :
  CommRingCat.Hom.hom (Hom.app f ⊤ ≫ X.presheaf.map (homOfLE ⋯).op) =
    CommRingCat.Hom.hom (Hom.appTop f ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
⊢ CommRingCat.Hom.hom
      (Y.presheaf.map (homOfLE ⋯).op ≫
        Hom.appLE f (Y.basicOpen r)
          (X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              r))
          ⋯) =
    CommRingCat.Hom.hom (Hom.appTop f ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))

Tactic:
rw [f.map_appLE, Scheme.Hom.appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.Scheme.Hom.map_appLE
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this : X.IsQuasiAffine
⊢ ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)

Tactic:
have (r : Γ(Y, ⊤)) :
      IsPushout f.appTop (Y.presheaf.map (homOfLE le_top).op)
        (X.presheaf.map (homOfLE le_top).op) (f.appLE (Y.basicOpen r)
          (X.basicOpen (f.appTop r)) (Scheme.preimage_basicOpen_top ..).ge) := by
    have := isLocalization_basicOpen_of_qcqs isCompact_univ isQuasiSeparated_univ r
    have := isLocalization_basicOpen_of_qcqs isCompact_univ isQuasiSeparated_univ (f.appTop r)
    refine CommRingCat.isPushout_of_isLocalization f.appTop.hom (f.appLE (Y.basicOpen r)
      (X.basicOpen (f.appTop r)) (Scheme.preimage_basicOpen_top ..).ge).hom ?_ (.powers r)
    change CommRingCat.Hom.hom (Y.presheaf.map _ ≫ f.appLE _ _ _) =
      CommRingCat.Hom.hom (f.appTop ≫ X.presheaf.map _)
    rw [f.map_appLE, Scheme.Hom.appLE]
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
⊢ IsPullback f X.toSpecΓ Y.toSpecΓ (Spec.map (Hom.appTop f))

Tactic:
isPullback_of_openCover _ _ _ _ Y.openCoverBasicOpenTop fun r ↦ ?_

Premises used: AlgebraicGeometry.Scheme.openCoverBasicOpenTop, AlgebraicGeometry.Scheme.isPullback_of_openCover
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
refine :
  ∀ (r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1),
    IsPullback (Cover.pullbackHom (P := IsOpenImmersion) Y.openCoverBasicOpenTop f r)
      ((Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ)
      (Y.openCoverBasicOpenTop.f r ≫ Y.toSpecΓ) (Spec.map (Hom.appTop f))
⊢ IsPullback f X.toSpecΓ Y.toSpecΓ (Spec.map (Hom.appTop f))

Tactic:
refine isPullback_of_openCover _ _ _ _ Y.openCoverBasicOpenTop fun r ↦ ?_

Premises used: AlgebraicGeometry.Scheme.openCoverBasicOpenTop, AlgebraicGeometry.Scheme.isPullback_of_openCover
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
rw : IsAffineOpen (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) (Hom.appTop f) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
        (↑r : (↑Γ(Y, ⊤) : Type u))))

Tactic:
rw [← Scheme.preimage_basicOpen_top]

Premises used: AlgebraicGeometry.Scheme.preimage_basicOpen_top
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
⊢ IsAffineOpen (f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))

Tactic:
r.2.preimage f

Premises used: Subtype.property, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
⊢ IsAffineOpen (f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))

Tactic:
exact r.2.preimage f

Premises used: Subtype.property, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ Scheme.Spec.map (Quiver.Hom.op (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))) ≫
      Iso.hom (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(Y, ⊤)))) =
    ⋯.isoSpec.symm.hom ≫ Y.openCoverBasicOpenTop.f r ≫ Y.toSpecΓ

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.QuasiAffine
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this_2 : X.IsQuasiAffine
this :
  ∀ (r : (↑Γ(Y, ⊤) : Type u)),
    IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
      (Hom.appLE f (Y.basicOpen r)
        (X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r))
        ⋯)
r : Y.openCoverBasicOpenTop.toPreZeroHypercover.1
e : pullback f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))).ι ≅
  Spec
    Γ(X,
      X.basicOpen (U := ⊤)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Hom.appTop f) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)))) :=
  pullbackRestrictIsoRestrict f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) ≪≫ X.isoOfEq ⋯ ≪≫ ⋯.isoSpec
⊢ Scheme.Spec.map (Hom.appTop f).op ≫ Iso.hom (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(Y, ⊤)))) =
    Iso.hom (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(X, ⊤)))) ≫ Spec.map (Hom.appTop f)

Tactic:
simp