awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this_1 : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
this : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
e_1 : (↑(X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r) : Scheme) = (↑(X.basicOpen r) : Scheme)
⊢ X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen r
have h : X.basicOpen r = X.basicOpen r
Tactic: rw [toSpecΓ_preimage_basicOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
⊢ IsOpenImmersion ((X.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r).ι ≫ X.toSpecΓ)
have suffices : IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
Tactic: suffices IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ) by
    convert! this <;> rw [toSpecΓ_preimage_basicOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
⊢ IsOpenImmersion ((X.basicOpen r).ι ≫ X.toSpecΓ)
have rw : IsOpenImmersion (Y := Spec Γ(X, ⊤)) ((X.basicOpen r).toSpecΓ ≫ Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))))
Tactic: rw [← Opens.toSpecΓ_SpecMap_presheaf_map_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (hypothesis)
Goal:
X : Scheme
inst : CompactSpace.{u} ↥X
H : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : QuasiSeparatedSpace.{u} ↥X
x : ↥X
r : (↑Γ(X, ⊤) : Type u)
hr : IsAffineOpen (X.basicOpen r)
hxr : x ∈ X.basicOpen r
⊢ IsOpenImmersion (Y := Spec Γ(X, ⊤)) ((X.basicOpen r).toSpecΓ ≫ Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
have this₁ : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
Tactic: have := isLocalization_basicOpen_of_qcqs isCompact_univ isQuasiSeparated_univ r
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
⊢ X.IsQuasiAffine
have this : CompactSpace.{u} ↥X
Tactic: have := QuasiCompact.compactSpace_of_compactSpace f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this : CompactSpace.{u} ↥X
⊢ X.IsQuasiAffine
have refine : ∀ (x : ↥X), ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
Tactic: refine .of_forall_exists_mem_basicOpen _ fun x ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this : CompactSpace.{u} ↥X
x : ↥X
⊢ ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
have obtain : ∀ (r : (↑Γ(Y, ⊤) : Type u)) (hr : IsAffineOpen (Y.basicOpen r))
  (hxr : Membership.mem (α := ↥Y) (↑(Y.basicOpen r) : Set ↥Y) (f x : ↥Y)),
  ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
Tactic: obtain ⟨_, ⟨_, ⟨r, hr, rfl⟩, rfl⟩, hxr, -⟩ := (IsQuasiAffine.isBasis_basicOpen
    Y).exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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)
⊢ ∃ (r : (↑Γ(X, ⊤) : Type u)), IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
have 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)
Tactic: refine ⟨f.appTop r, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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
      (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)
have rw : IsAffineOpen (f ⁻¹ᵁ Y.basicOpen r) ∧ x ∈ f ⁻¹ᵁ Y.basicOpen r
Tactic: rw [← preimage_basicOpen_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : X.IsQuasiAffine
x : ↥X
h : Membership.mem (γ := TopologicalSpace.Opens ↥X) ⊤ x
⊢ Membership.mem (γ := TopologicalSpace.Opens ↥X)
    (⨆ (i : { r : (↑Γ(X, ⊤) : Type u) // IsAffineOpen (X.basicOpen r) }), X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) x
have 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
Tactic: obtain ⟨_, ⟨_, ⟨r, hr, rfl⟩, rfl⟩, hxr, -⟩ :=
    (IsQuasiAffine.isBasis_basicOpen X).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
⊢ IsPullback f X.toSpecΓ Y.toSpecΓ (Spec.map (Hom.appTop f))
have this : CompactSpace.{u} ↥X
Tactic: have := QuasiCompact.compactSpace_of_compactSpace f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this : CompactSpace.{u} ↥X
⊢ IsPullback f X.toSpecΓ Y.toSpecΓ (Spec.map (Hom.appTop f))
have this₁ : X.IsQuasiAffine
Tactic: have := Scheme.IsQuasiAffine.of_isAffineHom f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (hypothesis)
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))
      ⋯)
have this₁ : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
Tactic: have := isLocalization_basicOpen_of_qcqs isCompact_univ isQuasiSeparated_univ r
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (hypothesis)
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)
⊢ 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))
      ⋯)
have 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)
Tactic: have := isLocalization_basicOpen_of_qcqs isCompact_univ isQuasiSeparated_univ (f.appTop r)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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)
⊢ (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))
have change : CommRingCat.Hom.hom
    (Y.presheaf.map (homOfLE sorry).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))
        sorry) =
  CommRingCat.Hom.hom (Hom.appTop f ≫ X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: change CommRingCat.Hom.hom (Y.presheaf.map _ ≫ f.appLE _ _ _) =
      CommRingCat.Hom.hom (f.appTop ≫ X.presheaf.map _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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)
⊢ 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 ⋯)))
have 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))
      sorry) =
  CommRingCat.Hom.hom (Hom.appTop f ≫ X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: rw [f.map_appLE, Scheme.Hom.appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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 ⋯)))
⊢ 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 ⋯)))
have rw₁ : CommRingCat.Hom.hom (Hom.app f ⊤ ≫ X.presheaf.map (homOfLE sorry).op) =
  CommRingCat.Hom.hom (Hom.appTop f ≫ X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: rw [f.map_appLE, Scheme.Hom.appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffineHom f
inst_1 : Y.IsQuasiAffine
this_1 : CompactSpace.{u} ↥X
this : X.IsQuasiAffine
⊢ IsPullback f X.toSpecΓ Y.toSpecΓ (Spec.map (Hom.appTop f))
have this₁ : ∀ (r : (↑Γ(Y, ⊤) : Type u)),
  IsPushout (Hom.appTop f) (Y.presheaf.map (Quiver.Hom.op (homOfLE sorry))) (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))
    (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))
      sorry)
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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))
have 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))
Tactic: refine isPullback_of_openCover _ _ _ _ Y.openCoverBasicOpenTop fun r ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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
    (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))))
have rw : IsAffineOpen (f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
Tactic: rw [← Scheme.preimage_basicOpen_top]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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
⊢ 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))
have refine_1 : Scheme.Spec.map
      (Quiver.Hom.op
        (Hom.appLE f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
          (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))))
          sorry)) ≫
    sorry.isoSpec.symm.hom =
  e.symm.hom ≫ Cover.pullbackHom (P := IsOpenImmersion) Y.openCoverBasicOpenTop f r
Tactic: refine .of_iso ((this r.1).op.map Scheme.Spec) e.symm r.2.isoSpec.symm (.refl _) (.refl _)
    ?_ ?_ (by simp) (by simp)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.QuasiAffine (goal)
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
refine_1 :
  Scheme.Spec.map
        (Quiver.Hom.op
          (Hom.appLE f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
            (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))))
            ⋯)) ≫
      ⋯.isoSpec.symm.hom =
    e.symm.hom ≫ Cover.pullbackHom (P := IsOpenImmersion) Y.openCoverBasicOpenTop f r
⊢ 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))
have refine_2 : Scheme.Spec.map (Quiver.Hom.op (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)))) ≫
    Iso.hom (Iso.refl (Scheme.Spec.obj (Opposite.op Γ(X, ⊤)))) =
  e.symm.hom ≫ (Precoverage.ZeroHypercover.pullback₁ f Y.openCoverBasicOpenTop).f r ≫ X.toSpecΓ
Tactic: refine .of_iso ((this r.1).op.map Scheme.Spec) e.symm r.2.isoSpec.symm (.refl _) (.refl _)
    ?_ ?_ (by simp) (by simp)