awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this_1 : IsAffine.{u} (↑U : Scheme)
this : IsAffine.{u} (↑V : Scheme)
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec
have conv_rhs : Spec.map (X.presheaf.map f) ≫ hU.fromSpec =
  Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE sorry) ≫ Quiver.Hom.op (eqToHom sorry))) ≫
    Iso.inv (↑U : Scheme).isoSpec ≫ U.ι
Tactic: conv_rhs =>
    rw [fromSpec, ← X.homOfLE_ι (V := U) f.unop.le, isoSpec_inv, Category.assoc,
      ← Scheme.isoSpec_inv_naturality_assoc,
      ← Spec.map_comp_assoc, Scheme.homOfLE_appTop, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
f : op U ⟶ op V
this_1 : IsAffine.{u} (↑U : Scheme)
this : IsAffine.{u} (↑V : Scheme)
⊢ Spec.map (X.presheaf.map f) ≫ hU.fromSpec =
    Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯))) ≫
      Iso.inv (↑U : Scheme).isoSpec ≫ U.ι
have rw : Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom sorry) ≫ f)) ≫ Iso.inv (↑U : Scheme).isoSpec ≫ U.ι =
  Spec.map (X.presheaf.map (Quiver.Hom.op (homOfLE sorry) ≫ Quiver.Hom.op (eqToHom sorry))) ≫
    Iso.inv (↑U : Scheme).isoSpec ≫ U.ι
Tactic: rw [fromSpec, isoSpec_inv, Category.assoc, ← Spec.map_comp_assoc, ← Functor.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ hU.fromSpec = hV.fromSpec ≫ f
have this : IsAffine.{u} (↑U : Scheme)
Tactic: have : IsAffine U := hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine.{u} (↑U : Scheme)
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫ hU.fromSpec = hV.fromSpec ≫ f
have simp : Spec.map (Scheme.Hom.appLE f U V i) ≫
    Spec.map (Y.presheaf.map (Quiver.Hom.op (eqToHom sorry))) ≫ Iso.inv (↑U : Scheme).isoSpec ≫ U.ι =
  Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) ≫ Iso.inv (↑V : Scheme).isoSpec ≫ V.ι ≫ f
Tactic: simp only [IsAffineOpen.fromSpec, Category.assoc, isoSpec_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
V : X.Opens
U : Y.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
i : V ≤ f ⁻¹ᵁ U
this : IsAffine.{u} (↑U : Scheme)
⊢ Spec.map (Scheme.Hom.appLE f U V i) ≫
      Spec.map (Y.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫ Iso.inv (↑U : Scheme).isoSpec ≫ U.ι =
    Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ≫ Iso.inv (↑V : Scheme).isoSpec ≫ V.ι ≫ f
have simp_rw : Spec.map (Scheme.Hom.appLE f U V i) ≫
    Spec.map (Y.presheaf.map (Quiver.Hom.op (eqToHom sorry))) ≫ Iso.inv (↑U : Scheme).isoSpec ≫ U.ι =
  Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom sorry))) ≫
    Iso.inv (↑V : Scheme).isoSpec ≫ (X.homOfLE i ≫ (f ⁻¹ᵁ U).ι) ≫ f
Tactic: simp_rw [← Scheme.homOfLE_ι _ i]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
inst : IsAffine X
⊢ ⋯.fromSpec = X.isoSpec.inv
have rw : Scheme.Opens.ι ⊤ = sorry.isoSpec.hom ≫ X.isoSpec.inv
Tactic: rw [fromSpec, Iso.inv_comp_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
⊢ Scheme.Hom.app hU.fromSpec V =
    X.presheaf.map (homOfLE h).op ≫
      Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (homOfLE ⋯))
have this : U.ι ⁻¹ᵁ V = ⊤
Tactic: have : U.ι ⁻¹ᵁ V = ⊤ := eq_top_iff.mpr fun x _ ↦ h x.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ Scheme.Hom.app hU.fromSpec V =
    X.presheaf.map (homOfLE h).op ≫
      Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (homOfLE ⋯))
have rw : Eq (α := Γ(X, V) ⟶ Γ(Spec Γ(X, U), (hU.isoSpec.inv ≫ U.ι) ⁻¹ᵁ V))
  (X.presheaf.map (Quiver.Hom.op (homOfLE sorry)) ≫
    (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom sorry)) ≫
      (U.topIso.hom ≫ Iso.inv (Scheme.ΓSpecIso Γ(X, U))) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom sorry)))
  (X.presheaf.map (homOfLE h).op ≫
    Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: rw [IsAffineOpen.fromSpec, Scheme.Hom.comp_app, Scheme.Opens.ι_app, Scheme.Hom.app_eq _ this,
    ← Scheme.Hom.appTop, IsAffineOpen.isoSpec_inv_appTop]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
h : U ≤ V
this : U.ι ⁻¹ᵁ V = ⊤
⊢ Eq (α := Γ(X, V) ⟶ Γ(Spec Γ(X, U), (hU.isoSpec.inv ≫ U.ι) ⁻¹ᵁ V))
    (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫
      (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫
        (U.topIso.hom ≫ Iso.inv (Scheme.ΓSpecIso Γ(X, U))) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
    (X.presheaf.map (homOfLE h).op ≫
      Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (homOfLE ⋯)))
have simp : Eq (α := Γ(X, V) ⟶ Γ(Spec Γ(X, U), (hU.isoSpec.inv ≫ U.ι) ⁻¹ᵁ V))
  (X.presheaf.map
      (Quiver.Hom.op (homOfLE sorry) ≫
        ((Scheme.Hom.opensFunctor U.ι).map (Quiver.Hom.unop (Quiver.Hom.op (eqToHom sorry)))).op ≫
          Quiver.Hom.op (eqToHom sorry)) ≫
    Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom sorry)))
  (X.presheaf.map (homOfLE h).op ≫
    Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (homOfLE sorry)))
Tactic: simp only [Scheme.Opens.toScheme_presheaf_map, Scheme.Opens.topIso_hom,
    Category.assoc, ← X.presheaf.map_comp_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact (↑U : Set ↥X)
have h : (↑U : Set ↥X) = Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) Set.univ
Tactic: convert! @IsCompact.image _ _ _ _ Set.univ hU.fromSpec PrimeSpectrum.compactSpace.1 (by fun_prop)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ (↑U : Set ↥X) = Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) Set.univ
have h : Eq (α := Set ↥X) (Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) Set.univ)
  (Set.range (ι := ↥(Spec Γ(X, U))) ⇑hU.fromSpec)
Tactic: convert! hU.range_fromSpec.symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
U : Y.Opens
hU : IsAffineOpen U
f : X ⟶ Y
inst : IsOpenImmersion f
hU' : U ≤ Scheme.Hom.opensRange f
⊢ IsAffineOpen (f ⁻¹ᵁ U)
have rwa : IsAffineOpen (f ''ᵁ f ⁻¹ᵁ U)
Tactic: rwa [← f.isAffineOpen_iff_of_isOpenImmersion, f.image_preimage_eq_opensRange_inf,
    inf_eq_right.mpr hU']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
U : Y.Opens
hU : IsAffineOpen U
f : X ⟶ Y
inst : IsOpenImmersion f
hU' : U ≤ Scheme.Hom.opensRange f
rwa : IsAffineOpen (f ''ᵁ f ⁻¹ᵁ U)
⊢ IsAffineOpen (f ⁻¹ᵁ U)
have rwa₁ : IsAffineOpen (Scheme.Hom.opensRange f ⊓ U)
Tactic: rwa [← f.isAffineOpen_iff_of_isOpenImmersion, f.image_preimage_eq_opensRange_inf,
    inf_eq_right.mpr hU']
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ hU.fromSpec ⁻¹ᵁ U = ⊤
have simp_rw : hU.fromSpec ⁻¹ᵁ Scheme.Hom.opensRange hU.fromSpec = ⊤
Tactic: simp_rw [← hU.opensRange_fromSpec, Scheme.Hom.preimage_opensRange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.app hU.fromSpec U =
    Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯))
have rw : Scheme.Hom.app hU.fromSpec U =
  Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ Iso.hom (Scheme.ΓSpecIso Γ(X, U)) ≫ Scheme.Hom.app hU.fromSpec U
Tactic: rw [← hU.ΓSpecIso_hom_fromSpec_app, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
rw :
  Scheme.Hom.app hU.fromSpec U =
    Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ Iso.hom (Scheme.ΓSpecIso Γ(X, U)) ≫ Scheme.Hom.app hU.fromSpec U
⊢ Scheme.Hom.app hU.fromSpec U =
    Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯))
have rw₁ : Scheme.Hom.app hU.fromSpec U = Scheme.Hom.app hU.fromSpec U
Tactic: rw [← hU.ΓSpecIso_hom_fromSpec_app, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ hU.fromSpec ⁻¹ᵁ X.basicOpen f =
    (Spec Γ(X, U)).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, U)) (Iso.inv (Scheme.ΓSpecIso Γ(X, U))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), ⊤) : Type u))
        f)
have rw : Eq.{u + 1} (α := (Spec Γ(X, U)).Opens)
  ((Spec Γ(X, U)).basicOpen (U := hU.fromSpec ⁻¹ᵁ U)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier)
          (Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom sorry))) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), hU.fromSpec ⁻¹ᵁ U) : Type u))
      f))
  ((Spec Γ(X, U)).basicOpen (U := ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(X, U)) (Iso.inv (Scheme.ΓSpecIso Γ(X, U))) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), ⊤) : Type u))
      f))
Tactic: rw [Scheme.preimage_basicOpen, hU.fromSpec_app_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ hU.fromSpec ⁻¹ᵁ X.basicOpen f = PrimeSpectrum.basicOpen f
have rw : Eq.{u + 1} (α := (Spec Γ(X, U)).Opens)
  ((Spec Γ(X, U)).basicOpen (U := ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(X, U)) (Iso.inv (Scheme.ΓSpecIso Γ(X, U))) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), ⊤) : Type u))
      f))
  (PrimeSpectrum.basicOpen f)
Tactic: rw [fromSpec_preimage_basicOpen', ← basicOpen_eq_of_affine]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
rw :
  Eq.{u + 1} (α := (Spec Γ(X, U)).Opens)
    ((Spec Γ(X, U)).basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, U)) (Iso.inv (Scheme.ΓSpecIso Γ(X, U))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), ⊤) : Type u))
        f))
    (PrimeSpectrum.basicOpen f)
⊢ hU.fromSpec ⁻¹ᵁ X.basicOpen f = PrimeSpectrum.basicOpen f
have rw₁ : Eq.{u + 1} (α := (Spec Γ(X, U)).Opens)
  ((Spec Γ(X, U)).basicOpen (U := ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(X, U)) (Iso.inv (Scheme.ΓSpecIso Γ(X, U))) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), ⊤) : Type u))
      f))
  ((Spec Γ(X, U)).basicOpen (U := ⊤)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(X, U)) (Iso.inv (Scheme.ΓSpecIso Γ(X, U))) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), ⊤) : Type u))
      f))
Tactic: rw [fromSpec_preimage_basicOpen', ← basicOpen_eq_of_affine]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ hU.fromSpec ''ᵁ PrimeSpectrum.basicOpen f = X.basicOpen f
have rw : hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f = X.basicOpen f
Tactic: rw [← hU.fromSpec_preimage_basicOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f = X.basicOpen f
have h : (↑(hU.fromSpec ''ᵁ hU.fromSpec ⁻¹ᵁ X.basicOpen f) : Set ↥X) = (↑(X.basicOpen f) : Set ↥X)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ Set.image (α := ↥(Spec Γ(X, U))) (⇑hU.fromSpec) (⇑hU.fromSpec ⁻¹' (↑(X.basicOpen f) : Set ↥X)) =
    (↑(X.basicOpen f) : Set ↥X)
have h : (↑(X.basicOpen f) : Set ↥X) ⊆ (↑U : Set ↥X)
Tactic: rw [Set.image_preimage_eq_inter_range, Set.inter_eq_left, hU.range_fromSpec]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ Eq.{u + 1} (α := (Spec Γ(X, U)).Opens)
    ((Spec Γ(X, U)).basicOpen (U := hU.fromSpec ⁻¹ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app hU.fromSpec U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), hU.fromSpec ⁻¹ᵁ U) : Type u))
        f))
    (PrimeSpectrum.basicOpen f)
have rw : (Spec Γ(X, U)).basicOpen (U := hU.fromSpec ⁻¹ᵁ U)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.app hU.fromSpec U) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), hU.fromSpec ⁻¹ᵁ U) : Type u))
      f) =
  hU.fromSpec ⁻¹ᵁ X.basicOpen f
Tactic: rw [← hU.fromSpec_preimage_basicOpen, Scheme.preimage_basicOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
rw :
  (Spec Γ(X, U)).basicOpen (U := hU.fromSpec ⁻¹ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app hU.fromSpec U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), hU.fromSpec ⁻¹ᵁ U) : Type u))
        f) =
    hU.fromSpec ⁻¹ᵁ X.basicOpen f
⊢ Eq.{u + 1} (α := (Spec Γ(X, U)).Opens)
    ((Spec Γ(X, U)).basicOpen (U := hU.fromSpec ⁻¹ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app hU.fromSpec U) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), hU.fromSpec ⁻¹ᵁ U) : Type u))
        f))
    (PrimeSpectrum.basicOpen f)
have rw₁ : Eq.{u + 1} (α := (Spec Γ(X, U)).Opens)
  ((Spec Γ(X, U)).basicOpen (U := hU.fromSpec ⁻¹ᵁ U)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.app hU.fromSpec U) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), hU.fromSpec ⁻¹ᵁ U) : Type u))
      f))
  ((Spec Γ(X, U)).basicOpen (U := hU.fromSpec ⁻¹ᵁ U)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.app hU.fromSpec U) :
        (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), hU.fromSpec ⁻¹ᵁ U) : Type u))
      f))
Tactic: rw [← hU.fromSpec_preimage_basicOpen, Scheme.preimage_basicOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ IsAffineOpen (X.basicOpen f)
have rw : IsAffineOpen.{u} (X := Spec Γ(X, U)) (PrimeSpectrum.basicOpen f)
Tactic: rw [← hU.fromSpec_image_basicOpen, Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ IsAffineOpen.{u} (X := Spec Γ(X, U)) (PrimeSpectrum.basicOpen f)
have h : Spec Γ(X, U) = Spec (CommRingCat.of (↑Γ(X, U) : Type u)) →
  PrimeSpectrum.basicOpen f =
    Scheme.Hom.opensRange (X := Spec (CommRingCat.of (Localization.Away f)))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑Γ(X, U) : Type u) (Localization.Away f))))
Tactic: convert!
    isAffineOpen_opensRange
      (Spec.map (CommRingCat.ofHom <| algebraMap Γ(X, U) (Localization.Away f)))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : (↑Γ(X, ⊤) : Type u)
⊢ IsAffineOpen ((X.basicOpen r).ι ⁻¹ᵁ U)
have apply : IsAffineOpen ((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U)
Tactic: apply (X.basicOpen r).ι.isAffineOpen_iff_of_isOpenImmersion.mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
r : (↑Γ(X, ⊤) : Type u)
⊢ IsAffineOpen ((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U)
have rw : IsAffineOpen
  (X.basicOpen (U := U)
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, U)) (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, U) : Type u))
      r))
Tactic: rw [Scheme.Hom.image_preimage_eq_opensRange_inf, Scheme.Opens.opensRange_ι, inf_comm,
    ← Scheme.basicOpen_res _ _ (homOfLE le_top).op]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : (↑x : ↥X) ∈ U
⊢ ∃ (f : (↑Γ(X, U) : Type u)), X.basicOpen f ≤ V ∧ (↑x : ↥X) ∈ X.basicOpen f
have this : IsAffine.{u} (↑U : Scheme)
Tactic: have : IsAffine _ := hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : (↑x : ↥X) ∈ U
this : IsAffine.{u} (↑U : Scheme)
⊢ ∃ (f : (↑Γ(X, U) : Type u)), X.basicOpen f ≤ V ∧ (↑x : ↥X) ∈ X.basicOpen f
have obtain : ∀ (r : (↑Γ((↑U : Scheme), ⊤) : Type u))
  (h₁ : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (↑x : ↥X) h ∈ (↑((↑U : Scheme).basicOpen r) : Set ↥(↑U : Scheme)))
  (h₂ : (↑U : Scheme).basicOpen r ≤ U.ι ⁻¹ᵁ V),
  ∃ (f : (↑Γ(X, U) : Type u)), X.basicOpen f ≤ V ∧ (↑x : ↥X) ∈ X.basicOpen f
Tactic: obtain ⟨_, ⟨_, ⟨r, rfl⟩, rfl⟩, h₁, h₂ : _ ≤ U.ι ⁻¹ᵁ V⟩ :=
    (isBasis_basicOpen U).exists_subset_of_mem_open (x.2 : (⟨x, h⟩ : U) ∈ _) (U.ι ⁻¹ᵁ V).isOpen
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : (↑x : ↥X) ∈ U
this : IsAffine.{u} (↑U : Scheme)
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
h₁ : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) (↑x : ↥X) h ∈ (↑((↑U : Scheme).basicOpen r) : Set ↥(↑U : Scheme))
h₂ : (↑U : Scheme).basicOpen r ≤ U.ι ⁻¹ᵁ V
⊢ ∃ (f : (↑Γ(X, U) : Type u)), X.basicOpen f ≤ V ∧ (↑x : ↥X) ∈ X.basicOpen f
have h₃ : (↑x : ↥X) ∈ X.basicOpen r
Tactic: replace h₁ : x.1 ∈ X.basicOpen r := by simpa [U.mem_basicOpen_toScheme] using h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
x : ↥V
h : (↑x : ↥X) ∈ U
this : IsAffine.{u} (↑U : Scheme)
r : (↑Γ((↑U : Scheme), ⊤) : Type u)
h₂ : (↑U : Scheme).basicOpen r ≤ U.ι ⁻¹ᵁ V
h₁ : (↑x : ↥X) ∈ X.basicOpen r
⊢ ∃ (f : (↑Γ(X, U) : Type u)), X.basicOpen f ≤ V ∧ (↑x : ↥X) ∈ X.basicOpen f
have h₃ : X.basicOpen r ≤ V
Tactic: replace h₂ : X.basicOpen r ≤ V := by
    simpa [Scheme.image_basicOpen] using (U.ι.image_mono h₂).trans (U.ι.image_preimage_le _)
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
have basicOpenSectionsToAffine : IsLocalization (Submonoid.powers f) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)
Tactic: apply
    (IsLocalization.isLocalization_iff_of_ringEquiv (Submonoid.powers f)
      (asIso <| basicOpenSectionsToAffine hU f).commRingCatIsoToRingEquiv).mpr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
⊢ IsLocalization (Submonoid.powers f) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)
have h : (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u) =
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
            (structureSheaf (↑Γ(X, U) : Type u)))
          (op (PrimeSpectrum.basicOpen f))) :
      Type u) →
  HEq.{u + 1} (α := CommSemiring (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)) CommRing.toCommSemiring (β :=
      CommSemiring
        (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
              (ObjectProperty.FullSubcategory.obj (P :=
                Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
                (structureSheaf (↑Γ(X, U) : Type u)))
              (op (PrimeSpectrum.basicOpen f))) :
          Type u))
      CommRing.toCommSemiring →
    RingHom.toAlgebra
        ((asIso (hU.basicOpenSectionsToAffine f)).commRingCatIsoToRingEquiv.toRingHom.comp
          (algebraMap (↑Γ(X, U) : Type u) (↑Γ(X, X.basicOpen f) : Type u))) =
      StructureSheaf.openAlgebra (↑Γ(X, U) : Type u) (op (PrimeSpectrum.basicOpen f))
Tactic: convert! StructureSheaf.IsLocalization.to_basicOpen _ f using 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
e_1 :
  (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u) =
    (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
          (ObjectProperty.FullSubcategory.obj (P :=
            Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
            (structureSheaf (↑Γ(X, U) : Type u)))
          (op (PrimeSpectrum.basicOpen f))) :
      Type u)
e_2 :
  HEq.{u + 1} (α := CommSemiring (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)) CommRing.toCommSemiring (β :=
    CommSemiring
      (↑(Functor.obj (C := (Opens (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u))ᵒᵖ)
            (ObjectProperty.FullSubcategory.obj (P :=
              Presheaf.IsSheaf (Opens.grothendieckTopology (↑(PrimeSpectrum.Top (↑Γ(X, U) : Type u)) : Type u)))
              (structureSheaf (↑Γ(X, U) : Type u)))
            (op (PrimeSpectrum.basicOpen f))) :
        Type u))
    CommRing.toCommSemiring
⊢ RingHom.toAlgebra
      ((asIso (hU.basicOpenSectionsToAffine f)).commRingCatIsoToRingEquiv.toRingHom.comp
        (algebraMap (↑Γ(X, U) : Type u) (↑Γ(X, X.basicOpen f) : Type u))) =
    StructureSheaf.openAlgebra (↑Γ(X, U) : Type u) (op (PrimeSpectrum.basicOpen f))
have h : ∀ (r : (↑Γ(X, U) : Type u)),
  Eq (α := (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
    ((algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
        r :
      (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
    ((algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
        r :
      (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
Tactic: apply Algebra.algebra_ext