awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
⊢ P (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom)
have inr : ∀ (x : ↥(Spec Γ(X, ⊤))), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) x))
Tactic: refine this inferInstance (fun x ↦ ?_) inferInstance ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
inr : ∀ (x : ↥(Spec Γ(X, ⊤))), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) x))
⊢ P (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom)
have inr₁ : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Spec Γ(Y, ⊤) = Spec R ∧ Spec Γ(X, ⊤) = Spec S
Tactic: refine this inferInstance (fun x ↦ ?_) inferInstance ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
x : ↥(Spec Γ(X, ⊤))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) x))
have inr : Q (R := (↑(Y.presheaf.stalk (f (X.isoSpec.inv x : ↥X))) : Type u))
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f (X.isoSpec.inv x)))
Tactic: rw [Scheme.Hom.stalkMap_comp, Scheme.Hom.stalkMap_comp, CommRingCat.hom_comp,
        hQi.cancel_right_isIso, CommRingCat.hom_comp, hQi.cancel_left_isIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
⊢ ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Spec Γ(Y, ⊤) = Spec R ∧ Spec Γ(X, ⊤) = Spec S
have w : CommRingCat
Tactic: use Γ(Y, ⊤), Γ(X, ⊤)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
this :
  ∀ {Y : Scheme.{u}} (hY : IsAffine Y) {X : Scheme.{u}} {f : X ⟶ Y}
    (H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))) (hX : IsAffine X)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S), P f
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
w w₁ : CommRingCat
⊢ ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Spec Γ(Y, ⊤) = Spec R ∧ Spec Γ(X, ⊤) = Spec S
have h : Spec Γ(Y, ⊤) = Spec Γ(Y, ⊤) ∧ Spec Γ(X, ⊤) = Spec Γ(X, ⊤)
Tactic: use Γ(Y, ⊤), Γ(X, ⊤)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
Y : Scheme
hY : IsAffine Y
X : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hX : IsAffine X
hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
⊢ P f
have obtain : ∀ (R S : CommRingCat.{u}) (hY : IsAffine.{u} (Spec R)) (hX : IsAffine.{u} (Spec S)) {f : Spec S ⟶ Spec R}
  (H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))), P f
Tactic: obtain ⟨R, S, rfl, rfl⟩ := hXY
Cleared hypotheses: Y, hY, X, f, H, hX, hXY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f_1 : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
hX : IsAffine.{u} (Spec S)
f : Spec S ⟶ Spec R
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ P f
have obtain : ∀ (φ : R ⟶ S) (H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))), P (Spec.map φ)
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
hX : IsAffine.{u} (Spec S)
φ : R ⟶ S
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
⊢ P (Spec.map φ)
have rw : Q (CommRingCat.Hom.hom φ)
Tactic: rw [Spec_iff (P := P)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
hX : IsAffine.{u} (Spec S)
φ : R ⟶ S
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
⊢ Q (CommRingCat.Hom.hom φ)
have a : ∀ (J : Ideal (↑S : Type u)) (x : J.IsPrime),
  (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (Q : (R →+* S) → Prop))
    (Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) J)) (Localization.AtPrime J) _ _
    (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) J) J (CommRingCat.Hom.hom φ) sorry)
Tactic: apply hQ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P_1 : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P_1 @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
hX : IsAffine.{u} (Spec S)
φ : R ⟶ S
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
P : Ideal (↑S : Type u)
hP : P.IsPrime
⊢ Q (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) P)) (S := Localization.AtPrime P)
    (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯)
have H₁ : Q (R := (↑((Spec R).presheaf.stalk ((Spec.map φ) { asIdeal := P, isPrime := hP })) : Type u))
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) { asIdeal := P, isPrime := hP }))
Tactic: specialize H ⟨P, hP⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P_1 : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P_1 @Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine.{u} (Spec R)
hX : IsAffine.{u} (Spec S)
φ : R ⟶ S
P : Ideal (↑S : Type u)
hP : P.IsPrime
H :
  Q (R := (↑((Spec R).presheaf.stalk ((Spec.map φ) { asIdeal := P, isPrime := hP })) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) { asIdeal := P, isPrime := hP }))
⊢ Q (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) P)) (S := Localization.AtPrime P)
    (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯)
have a : ∀
  (H :
    Q (R :=
      (↑(CommRingCat.of
            (Localization.AtPrime
              (PrimeSpectrum.comap (CommRingCat.Hom.hom φ)
                  { asIdeal := P, isPrime := hP : PrimeSpectrum (↑S : Type u) }).asIdeal)) :
        Type u))
      (S :=
      (↑(CommRingCat.of (Localization.AtPrime { asIdeal := P, isPrime := hP : PrimeSpectrum (↑S : Type u) }.asIdeal)) :
        Type u))
      (CommRingCat.Hom.hom
        (CommRingCat.ofHom
          (Localization.localRingHom
            (PrimeSpectrum.comap (CommRingCat.Hom.hom φ) { asIdeal := P, isPrime := hP }).asIdeal
            { asIdeal := P, isPrime := hP }.asIdeal (CommRingCat.Hom.hom φ) sorry)))),
  Q (R := Localization.AtPrime (Ideal.comap (CommRingCat.Hom.hom φ) P)) (S := Localization.AtPrime P)
    (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) sorry)
Tactic: rwa [hQi.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso φ _)] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (h : IsAffine X ∧ IsAffine Y),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have inr : ∀ (U : Opens ↥Y) (hU : U ∈ Y.affineOpens) (hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)),
  U ≤ ⊤ → Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
Tactic: obtain ⟨U, hU, hfx, _⟩ := Opens.isBasis_iff_nbhd.mp Y.isBasis_affineOpens
      (Opens.mem_top <| f x)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (h : IsAffine X ∧ IsAffine Y),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have inr : ∀ (V : Opens ↥X) (hV : V ∈ X.affineOpens) (hx : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
  Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
Tactic: obtain ⟨V, hV, hx, e⟩ := Opens.isBasis_iff_nbhd.mp X.isBasis_affineOpens
      (show x ∈ f ⁻¹ᵁ U from hfx)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X Y : Scheme
f : X ⟶ Y
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
hf : P f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (h : IsAffine X ∧ IsAffine Y),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
h : ¬(IsAffine X ∧ IsAffine Y)
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : Membership.mem (α := ↥Y) U (f x : ↥Y)
right : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have inr : Q' (R :=
  (↑((↑U : Scheme).presheaf.stalk ((Scheme.Hom.resLE f U V e) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx))) : Type u))
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Scheme.Hom.resLE f U V e) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)))
Tactic: rw [← hQ'.arrow_mk_iso_iff (Scheme.Hom.resLEStalkMap f e ⟨x, hx⟩)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
h : IsAffine X ∧ IsAffine Y
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have hX : IsAffine X
Tactic: obtain ⟨hX, hY⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (hypothesis)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
h : IsAffine X ∧ IsAffine Y
hX : IsAffine X
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have hY : IsAffine Y
Tactic: obtain ⟨hX, hY⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
      (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
      Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
  (hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
  Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
Tactic: wlog hXY : ∃ R S, Y = Spec R ∧ X = Spec S generalizing X Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
        (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
        Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)))
    (hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
⊢ Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
have wlog : ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
  (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
  Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
Tactic: wlog hXY : ∃ R S, Y = Spec R ∧ X = Spec S generalizing X Y
Cleared hypotheses: X, Y, f, hf, x, hX, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
⊢ Q' (R := (↑((Spec Γ(Y, ⊤)).presheaf.stalk ((X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x)))
have refine_1 : P (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom)
Tactic: refine this ?_ (X.isoSpec.hom x) inferInstance inferInstance ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties (goal)
Goal:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : HasRingHomProperty P @Q
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ' : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
hQ :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    Q f →
      ∀ (J : Ideal S) (x : J.IsPrime),
        Q' (R := Localization.AtPrime (Ideal.comap f J)) (S := Localization.AtPrime J)
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)
X Y : Scheme
f : X ⟶ Y
hf : P f
x : ↥X
hX : IsAffine X
hY : IsAffine Y
this :
  ∀ {X Y : Scheme.{u}} {f : X ⟶ Y} (hf : P f) (x : ↥X) (hX : IsAffine X) (hY : IsAffine Y)
    (hXY : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S),
    Q' (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x))
hXY : ¬∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Y = Spec R ∧ X = Spec S
refine_1 : P (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom)
⊢ Q' (R := (↑((Spec Γ(Y, ⊤)).presheaf.stalk ((X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom) (X.isoSpec.hom x)))
have refine_2 : ∃ (R : CommRingCat.{u}) (S : CommRingCat.{u}), Spec Γ(Y, ⊤) = Spec R ∧ Spec Γ(X, ⊤) = Spec S
Tactic: refine this ?_ (X.isoSpec.hom x) inferInstance inferInstance ?_