awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
respectsIso : (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).toProperty.RespectsIso
to_basicOpen :
  ∀ {X Y : Scheme.{u}} [inst : IsAffine Y] (f : X ⟶ Y) (r : (↑Γ(Y, ⊤) : Type u)),
    sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X := (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme))
        (f ∣_ Y.basicOpen r)
⊢ AffineTargetMorphismProperty.IsLocal.{u} (sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P)
have of_basicOpenCover : ∀ {X Y : Scheme.{u}} [inst : IsAffine Y] (f : X ⟶ Y) (s : Finset (↑Γ(Y, ⊤) : Type u)),
  Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤ →
    (∀ (r : ↥s),
        sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X :=
          (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme)) (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))) →
      sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
⊢ sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X := (↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme))
    (f ∣_ Y.basicOpen r)
have to_basicOpen : ∀ (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r),
  P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑V : X.Opens) e))
Tactic: rw [sourceAffineLocally_morphismRestrict]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
⊢ X.basicOpen (U := (↑U : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens))) (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
        r) =
    (↑U : X.Opens)
have simp : X.basicOpen (U := (↑U : X.Opens))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, (↑U : X.Opens))) (X.presheaf.map (Quiver.Hom.op (homOfLE sorry))) :
        (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          r :
        (↑Γ(X, ⊤) : Type u))) =
  (↑U : X.Opens)
Tactic: simp only [Scheme.Hom.appLE, Opens.map_top, CommRingCat.comp_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
⊢ X.basicOpen (U := (↑U : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            r :
          (↑Γ(X, ⊤) : Type u))) =
    (↑U : X.Opens)
have rw : (↑U : X.Opens) ⊓
    X.basicOpen (U := ⊤)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
        r) =
  (↑U : X.Opens)
Tactic: rw [Scheme.basicOpen_res]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑U : X.Opens) hU))
have to_basicOpen : ∀
  (this :
    X.basicOpen (U := (↑U : X.Opens))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens))) (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
          r) =
      (↑U : X.Opens)),
  P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑U : X.Opens) hU))
Tactic: have : X.basicOpen (f.appLE ⊤ U (by simp) r) = U := by
      simp only [Scheme.Hom.appLE, Opens.map_top, CommRingCat.comp_apply]
      rw [Scheme.basicOpen_res]
      simpa using hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
this :
  X.basicOpen (U := (↑U : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens))) (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
        r) =
    (↑U : X.Opens)
⊢ P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (↑U : X.Opens) hU))
have to_basicOpen : P (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (S :=
  (↑Γ(X,
        X.basicOpen (U := (↑U : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
            r)) :
    Type u))
  (CommRingCat.Hom.hom
    (CommRingCat.ofHom
      (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))) : Type u) (P := (↑Γ(X, (↑U : X.Opens)) : Type u))
        (↑(X.presheaf.1
              (op
                (X.basicOpen (U := (↑U : X.Opens))
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                        (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry) :
                      (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
                    r)))) :
          Type u)
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry)) r)))
Tactic: rw [← f.appLE_congr (by simp [Scheme.Hom.appLE]) rfl this (fun f => P f.hom),
      IsAffineOpen.appLE_eq_away_map f (isAffineOpen_top Y) U.2 _ r]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u)
H : sourceAffineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
U : (↑X.affineOpens : Type u)
hU : (↑U : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen r
this :
  X.basicOpen (U := (↑U : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens))) (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
          (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
        r) =
    (↑U : X.Opens)
⊢ P (R := (↑Γ(Y, Y.basicOpen r) : Type u)) (S :=
    (↑Γ(X,
          X.basicOpen (U := (↑U : X.Opens))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                  (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
              r)) :
      Type u))
    (IsLocalization.Away.map (↑(Y.presheaf.1 (op (Y.basicOpen r))) : Type u) (P := (↑Γ(X, (↑U : X.Opens)) : Type u))
      (↑(X.presheaf.1
            (op
              (X.basicOpen (U := (↑U : X.Opens))
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (X := Γ(Y, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                      (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
                    (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
                  r)))) :
        Type u)
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯)) r)
have to_basicOpen : P (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry))
Tactic: apply +allowSynthFailures h₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hs' :
  ∀ (r : ↥s),
    sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X :=
      (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme)) (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
U : (↑X.affineOpens : Type u)
⊢ P (R := (↑Γ(Y, ⊤) : Type u)) (S := (↑Γ(X, (↑U : X.Opens)) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯))
have of_basicOpenCover : ∀ (r : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)),
  (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _
    (Localization.Away (M := (↑Γ(X, (↑U : X.Opens)) : Type u))
      ((CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)) :
        (↑Γ(X, (↑U : X.Opens)) : Type u)))
    _ _ (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) sorry)) (↑r : (↑Γ(Y, ⊤) : Type u)))
Tactic: apply h₃ _ _ hs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₂ : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
h₃ : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hs' :
  ∀ (r : ↥s),
    sourceAffineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ P (X :=
      (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme)) (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))
U : (↑X.affineOpens : Type u)
r : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)
⊢ P (S :=
    Localization.Away (M := (↑Γ(X, (↑U : X.Opens)) : Type u))
      ((CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯) :
            (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
          (↑r : (↑Γ(Y, ⊤) : Type u)) :
        (↑Γ(X, (↑U : X.Opens)) : Type u)))
    (Localization.awayMap (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ (↑U : X.Opens) ⋯)) (↑r : (↑Γ(Y, ⊤) : Type u)))
have hs'₁ : ∀ (r : ↥s) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))),
  P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) (↑V : X.Opens) e))
Tactic: simp_rw [sourceAffineLocally_morphismRestrict] at hs'
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : (↑Y.affineOpens : Type u)
V₁ V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ (↑V₁ : X.Opens)
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) (↑U₁ : Y.Opens) (f x : ↥Y)
⊢ ∃ (r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)) (s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)) (_ : x ∈ X.basicOpen s) (e :
    X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r), P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))
have obtain : ∀ (r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)) (r' : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u))
  (hBrr' : Y.basicOpen r = Y.basicOpen r') (hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) (f x : ↥Y)),
  ∃ (r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)) (s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)) (_ : x ∈ X.basicOpen s) (e :
    X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r), P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))
Tactic: obtain ⟨r, r', hBrr', hBfx⟩ := exists_basicOpen_le_affine_inter U₁.2 U₂.2 (f x)
    ⟨hfx₁, e₂ hx₂⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : (↑Y.affineOpens : Type u)
V₁ V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ (↑V₁ : X.Opens)
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) (↑U₁ : Y.Opens) (f x : ↥Y)
r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)
r' : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) (f x : ↥Y)
⊢ ∃ (r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)) (s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)) (_ : x ∈ X.basicOpen s) (e :
    X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r), P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))
have ha : IsAffineOpen
  (X.basicOpen (U := (↑V₂ : X.Opens))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
        (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
      r'))
Tactic: have ha : IsAffineOpen (X.basicOpen (f.appLE U₂ V₂ e₂ r')) := V₂.2.basicOpen _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : (↑Y.affineOpens : Type u)
V₁ V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ (↑V₁ : X.Opens)
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) (↑U₁ : Y.Opens) (f x : ↥Y)
r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)
r' : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) (f x : ↥Y)
ha :
  IsAffineOpen
    (X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r'))
⊢ ∃ (r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)) (s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)) (_ : x ∈ X.basicOpen s) (e :
    X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r), P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))
have hxa : x ∈
  X.basicOpen (U := (↑V₂ : X.Opens))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
        (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
      r')
Tactic: have hxa : x ∈ X.basicOpen (f.appLE U₂ V₂ e₂ r') := by
    simpa [Scheme.Hom.appLE, ← Scheme.preimage_basicOpen] using And.intro hx₂ (hBrr' ▸ hBfx)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hPa : StableUnderCompositionWithLocalizationAwayTarget.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
x : ↥X
U₁ U₂ : (↑Y.affineOpens : Type u)
V₁ V₂ : (↑X.affineOpens : Type u)
hx₁ : x ∈ (↑V₁ : X.Opens)
hx₂ : x ∈ (↑V₂ : X.Opens)
e₂ : (↑V₂ : X.Opens) ≤ f ⁻¹ᵁ (↑U₂ : Y.Opens)
h₂ : P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂))
hfx₁ : Membership.mem (α := ↥Y) (↑U₁ : Y.Opens) (f x : ↥Y)
r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)
r' : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)
hBrr' : Y.basicOpen r = Y.basicOpen r'
hBfx : Membership.mem (α := ↥Y) (Y.basicOpen r) (f x : ↥Y)
ha :
  IsAffineOpen
    (X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r'))
hxa :
  x ∈
    X.basicOpen (U := (↑V₂ : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
          (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
        r')
⊢ ∃ (r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)) (s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)) (_ : x ∈ X.basicOpen s) (e :
    X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r), P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))
have obtain : ∀ (s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u))
  (s' :
    (↑Γ(X,
          X.basicOpen (U := (↑V₂ : X.Opens))
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appLE f (↑U₂ : Y.Opens) (↑V₂ : X.Opens) e₂) :
                (a : (↑Γ(Y, (↑U₂ : Y.Opens)) : Type u)) → (↑Γ(X, (↑V₂ : X.Opens)) : Type u))
              r')) :
      Type u))
  (hBss' : X.basicOpen s = X.basicOpen s') (hBx : x ∈ X.basicOpen s),
  ∃ (r : (↑Γ(Y, (↑U₁ : Y.Opens)) : Type u)) (s : (↑Γ(X, (↑V₁ : X.Opens)) : Type u)) (_ : x ∈ X.basicOpen s) (e :
    X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r), P (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e))
Tactic: obtain ⟨s, s', hBss', hBx⟩ := exists_basicOpen_le_affine_inter V₁.2 ha x ⟨hx₁, hxa⟩