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
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
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))
have h : Eq.{u + 1} (α := (↑Γ(X, U) : Type u) →+* (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
  (algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
  (algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
Tactic: congr 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
r : (↑Γ(X, U) : Type u)
⊢ Eq.{u + 1} (α := (↑Γ(X, U) : Type u) →+* (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
    (algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
    (algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u))
have h : CommRingCat.Hom.hom
    (X.presheaf.map (homOfLE sorry).op ≫
      Scheme.Hom.app hU.fromSpec (X.basicOpen f) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom sorry))) =
  algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)
Tactic: dsimp [CommRingCat.ofHom, RingHom.algebraMap_toAlgebra, ← CommRingCat.hom_comp,
    basicOpenSectionsToAffine]
-- 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
r : (↑Γ(X, U) : Type u)
⊢ CommRingCat.Hom.hom
      (X.presheaf.map (homOfLE ⋯).op ≫
        Scheme.Hom.app hU.fromSpec (X.basicOpen f) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) =
    algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)
have h : CommRingCat.Hom.hom
    ((Iso.inv (Scheme.ΓSpecIso Γ(X, U)) ≫ (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom sorry))) ≫
      (Spec Γ(X, U)).presheaf.map ((Opens.map hU.fromSpec.base).map (homOfLE sorry).op.unop).op ≫
        (Spec Γ(X, U)).presheaf.map (Quiver.Hom.op (eqToHom sorry))) =
  algebraMap (↑Γ(X, U) : Type u) (↑Γ(Spec Γ(X, U), PrimeSpectrum.basicOpen f) : Type u)
Tactic: rw [hU.fromSpec.naturality_assoc, hU.fromSpec_app_self]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
e : V ≤ f ⁻¹ᵁ U
r : (↑Γ(Y, U) : Type u)
this_1 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u) := ⋯
this : IsLocalization.Away (R := (↑Γ(X, V) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
        (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
      r :
    (↑Γ(X, V) : Type u))
  (↑Γ(X,
        X.basicOpen (U := V)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
              (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
            r)) :
    Type u) :=
  ⋯
⊢ Scheme.Hom.appLE f (Y.basicOpen r)
      (X.basicOpen (U := V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
            (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
          r))
      ⋯ =
    CommRingCat.ofHom
      (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))) : Type u)
        (↑(X.presheaf.1
              (op
                (X.basicOpen (U := V)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
                      (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
                    r)))) :
          Type u)
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r)
have hf : CommRingCat.Hom.hom
    (Scheme.Hom.appLE f (Y.basicOpen r)
      (X.basicOpen (U := V)
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
            (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
          r))
      sorry) =
  CommRingCat.Hom.hom
    (CommRingCat.ofHom
      (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))) : Type u)
        (↑(X.presheaf.1
              (op
                (X.basicOpen (U := V)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.appLE f U V e) :
                      (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
                    r)))) :
          Type u)
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)) r))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
          (↑Γ(X,
                X.basicOpen (U := f ⁻¹ᵁ U)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.app f U) :
                      (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                    r)) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
have this : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
Tactic: haveI := hU.isLocalization_basicOpen r
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
this : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
          (↑Γ(X,
                X.basicOpen (U := f ⁻¹ᵁ U)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.app f U) :
                      (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                    r)) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
have this₁ : IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ U) : Type u))
  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.app f U) :
        (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
      r :
    (↑Γ(X, f ⁻¹ᵁ U) : Type u))
  (↑Γ(X,
        X.basicOpen (U := f ⁻¹ᵁ U)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.app f U) :
              (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
            r)) :
    Type u)
Tactic: haveI := h.isLocalization_basicOpen (f.app U r)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
this_1 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app f U) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (↑Γ(X,
          X.basicOpen (U := f ⁻¹ᵁ U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.app f U) :
                (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
              r)) :
      Type u)
⊢ Scheme.Hom.app f (Y.basicOpen r) =
    CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
          (↑Γ(X,
                X.basicOpen (U := f ⁻¹ᵁ U)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.app f U) :
                      (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                    r)) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))
have hf : CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)) =
  CommRingCat.Hom.hom
    (CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
          (↑Γ(X,
                X.basicOpen (U := f ⁻¹ᵁ U)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.app f U) :
                      (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                    r)) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom sorry)))
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
this_1 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app f U) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (↑Γ(X,
          X.basicOpen (U := f ⁻¹ᵁ U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.app f U) :
                (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
              r)) :
      Type u)
⊢ CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)) =
    CommRingCat.Hom.hom
      (CommRingCat.ofHom
          (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
            (↑Γ(X,
                  X.basicOpen (U := f ⁻¹ᵁ U)
                    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (Scheme.Hom.app f U) :
                        (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                      r)) :
              Type u)
            (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
        X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))
have hf : Eq (α := (↑Γ(Y, U) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
  (RingHom.comp (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)))
    (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)))
  (RingHom.comp (β := (↑Γ(Y, Y.basicOpen r) : Type u))
    (CommRingCat.Hom.hom
      (CommRingCat.ofHom
          (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
            (↑Γ(X,
                  X.basicOpen (U := f ⁻¹ᵁ U)
                    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                          CommRingCat.carrier) (Scheme.Hom.app f U) :
                        (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                      r)) :
              Type u)
            (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
        X.presheaf.map (Quiver.Hom.op (eqToHom sorry))))
    (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)))
Tactic: apply IsLocalization.ringHom_ext (.powers r)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
this_1 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app f U) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (↑Γ(X,
          X.basicOpen (U := f ⁻¹ᵁ U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.app f U) :
                (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
              r)) :
      Type u)
⊢ Eq (α := (↑Γ(Y, U) : Type u) →+* (↑Γ(X, f ⁻¹ᵁ Y.basicOpen r) : Type u))
    (RingHom.comp (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen r)))
      (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)))
    (RingHom.comp (β := (↑Γ(Y, Y.basicOpen r) : Type u))
      (CommRingCat.Hom.hom
        (CommRingCat.ofHom
            (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
              (↑Γ(X,
                    X.basicOpen (U := f ⁻¹ᵁ U)
                      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u))
                            (CC := CommRingCat.carrier) (Scheme.Hom.app f U) :
                          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                        r)) :
                Type u)
              (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
          X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))))
      (algebraMap (↑Γ(Y, U) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)))
have hf : CommRingCat.Hom.hom (Y.presheaf.map (homOfLE sorry).op ≫ Scheme.Hom.app f (Y.basicOpen r)) =
  (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE sorry) ≫ Quiver.Hom.op (eqToHom sorry)))).comp
    (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Tactic: rw [IsLocalization.Away.map, CommRingCat.hom_comp, RingHom.comp_assoc, CommRingCat.hom_ofHom,
    IsLocalization.map_comp, RingHom.algebraMap_toAlgebra,
    RingHom.algebraMap_toAlgebra, ← RingHom.comp_assoc, ← CommRingCat.hom_comp,
    ← CommRingCat.hom_comp, ← X.presheaf.map_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
V : X.Opens
i : V ⟶ U
e : V = X.basicOpen f
⊢ IsLocalization.Away f (↑Γ(X, V) : Type u)
have subst : ∀ (i : X.basicOpen f ⟶ U), IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
Tactic: subst e
Cleared hypotheses: V, i, e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
g : (↑Γ(X, X.basicOpen f) : Type u)
⊢ ∃ (f' : (↑Γ(X, U) : Type u)), X.basicOpen f' = X.basicOpen g
have this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
Tactic: have := isLocalization_basicOpen hU f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
g : (↑Γ(X, X.basicOpen f) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
⊢ ∃ (f' : (↑Γ(X, U) : Type u)), X.basicOpen f' = X.basicOpen g
have obtain : ∀ (x : (↑Γ(X, U) : Type u)) (n : ℕ),
  ∃ (f' : (↑Γ(X, U) : Type u)),
    X.basicOpen f' =
      X.basicOpen
        (HSMul.hSMul (β := (↑Γ(X, X.basicOpen f) : Type u)) x
          (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
                  (a : ↥(Submonoid.powers f)) →
                    ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
                (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
                  Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n)
                  sorry)) :
            (↑Γ(X, X.basicOpen f) : Type u)))
Tactic: obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.surj'' (Submonoid.powers f) g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, U) : Type u)
n : ℕ
⊢ ∃ (f' : (↑Γ(X, U) : Type u)),
    X.basicOpen f' =
      X.basicOpen
        (HSMul.hSMul (β := (↑Γ(X, X.basicOpen f) : Type u)) x
          (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
                  (a : ↥(Submonoid.powers f)) →
                    ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
                (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
                  Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n)
                  ⋯)) :
            (↑Γ(X, X.basicOpen f) : Type u)))
have h : X.basicOpen (f * x) =
  X.basicOpen
    (HSMul.hSMul (β := (↑Γ(X, X.basicOpen f) : Type u)) x
      (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
              (a : ↥(Submonoid.powers f)) →
                ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
            (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
              Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n)
              sorry)) :
        (↑Γ(X, X.basicOpen f) : Type u)))
Tactic: use f * x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, U) : Type u)
n : ℕ
⊢ X.basicOpen (f * x) =
    X.basicOpen
      (HSMul.hSMul (β := (↑Γ(X, X.basicOpen f) : Type u)) x
        (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
                (a : ↥(Submonoid.powers f)) →
                  ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
              (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
                Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n)
                ⋯)) :
          (↑Γ(X, X.basicOpen f) : Type u)))
have h : X.basicOpen f ⊓ X.basicOpen x =
  X.basicOpen f ⊓ X.basicOpen x ⊓
    X.basicOpen (U := X.basicOpen f)
      (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
              (a : ↥(Submonoid.powers f)) →
                ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
            (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
              Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n)
              sorry)) :
        (↑Γ(X, X.basicOpen f) : Type u))
Tactic: rw [Algebra.smul_def, Scheme.basicOpen_mul, Scheme.basicOpen_mul, RingHom.algebraMap_toAlgebra,
    Scheme.basicOpen_res]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.AffineScheme (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, U) : Type u)
n : ℕ
⊢ X.basicOpen f ⊓ X.basicOpen x =
    X.basicOpen f ⊓ X.basicOpen x ⊓
      X.basicOpen (U := X.basicOpen f)
        (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
                (a : ↥(Submonoid.powers f)) →
                  ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
              (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
                Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n)
                ⋯)) :
          (↑Γ(X, X.basicOpen f) : Type u))
have h : IsUnit.{u} (M := (↑Γ(X, X.basicOpen f) : Type u))
  (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
          (a : ↥(Submonoid.powers f)) →
            ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
        (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
          Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n) sorry)) :
    (↑Γ(X, X.basicOpen f) : Type u))
Tactic: refine (inf_eq_left.mpr (inf_le_left.trans_eq (Scheme.basicOpen_of_isUnit _ ?_).symm)).symm