awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
⊢ affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
have this : IsAffine X
Tactic: haveI : IsAffine X := by
      apply isAffine_of_isAffineOpen_basicOpen (f.appTop '' s)
      · apply_fun Ideal.map (f.appTop).hom at hs
        rwa [Ideal.map_span, Ideal.map_top] at hs
      · rintro - ⟨r, hr, rfl⟩
        simp_rw [Scheme.preimage_basicOpen] at hf
        exact (hf ⟨r, hr⟩).left
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
this : IsAffine X
⊢ affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
have refine : ∀ (a : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)),
  ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra (↑Γ(Y, ⊤) : Type u) Rᵣ) (x_3 :
    Algebra (↑Γ(X, ⊤) : Type u) Sᵣ) (x_4 : IsLocalization.Away (↑a : (↑Γ(Y, ⊤) : Type u)) Rᵣ) (x_5 :
    IsLocalization.Away (R := (↑Γ(X, ⊤) : Type u))
      ((CommRingCat.Hom.hom (Scheme.Hom.appTop f) : (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑a : (↑Γ(Y, ⊤) : Type u)) :
        (↑Γ(X, ⊤) : Type u))
      Sᵣ),
    Q (IsLocalization.Away.map Rᵣ Sᵣ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (↑a : (↑Γ(Y, ⊤) : Type u)))
Tactic: refine ⟨inferInstance, hQs.ofIsLocalization' hPi (f.appTop).hom s hs fun a ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
this : IsAffine X
a : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)
⊢ ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra (↑Γ(Y, ⊤) : Type u) Rᵣ) (x_3 :
    Algebra (↑Γ(X, ⊤) : Type u) Sᵣ) (x_4 : IsLocalization.Away (↑a : (↑Γ(Y, ⊤) : Type u)) Rᵣ) (x_5 :
    IsLocalization.Away (R := (↑Γ(X, ⊤) : Type u))
      ((CommRingCat.Hom.hom (Scheme.Hom.appTop f) : (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑a : (↑Γ(Y, ⊤) : Type u)) :
        (↑Γ(X, ⊤) : Type u))
      Sᵣ),
    Q (IsLocalization.Away.map Rᵣ Sᵣ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (↑a : (↑Γ(Y, ⊤) : Type u)))
have refine_1 : IsLocalization.Away (R := (↑Γ(X, ⊤) : Type u))
  ((CommRingCat.Hom.hom (Scheme.Hom.appTop f) : (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
      (↑a : (↑Γ(Y, ⊤) : Type u)) :
    (↑Γ(X, ⊤) : Type u))
  (↑Γ(X,
        X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            (↑a : (↑Γ(Y, ⊤) : Type u)))) :
    Type u)
Tactic: refine ⟨Γ(Y, Y.basicOpen a.val), Γ(X, X.basicOpen (f.appTop a.val)), inferInstance,
      inferInstance, inferInstance, inferInstance, inferInstance, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
this : IsAffine X
a : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)
refine_1 :
  IsLocalization.Away (R := (↑Γ(X, ⊤) : Type u))
    ((CommRingCat.Hom.hom (Scheme.Hom.appTop f) : (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
        (↑a : (↑Γ(Y, ⊤) : Type u)) :
      (↑Γ(X, ⊤) : Type u))
    (↑Γ(X,
          X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              (↑a : (↑Γ(Y, ⊤) : Type u)))) :
      Type u)
⊢ ∃ (Rᵣ : Type u) (Sᵣ : Type u) (x : CommRing Rᵣ) (x_1 : CommRing Sᵣ) (x_2 : Algebra (↑Γ(Y, ⊤) : Type u) Rᵣ) (x_3 :
    Algebra (↑Γ(X, ⊤) : Type u) Sᵣ) (x_4 : IsLocalization.Away (↑a : (↑Γ(Y, ⊤) : Type u)) Rᵣ) (x_5 :
    IsLocalization.Away (R := (↑Γ(X, ⊤) : Type u))
      ((CommRingCat.Hom.hom (Scheme.Hom.appTop f) : (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
          (↑a : (↑Γ(Y, ⊤) : Type u)) :
        (↑Γ(X, ⊤) : Type u))
      Sᵣ),
    Q (IsLocalization.Away.map Rᵣ Sᵣ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (↑a : (↑Γ(Y, ⊤) : Type u)))
have refine_2 : Q (R := (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)) (S :=
  (↑Γ(X,
        X.basicOpen (U := ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Scheme.Hom.appTop f) :
              (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
            (↑a : (↑Γ(Y, ⊤) : Type u)))) :
    Type u))
  (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)
    (↑Γ(X,
          X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              (↑a : (↑Γ(Y, ⊤) : Type u)))) :
      Type u)
    (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (↑a : (↑Γ(Y, ⊤) : Type u)))
Tactic: refine ⟨Γ(Y, Y.basicOpen a.val), Γ(X, X.basicOpen (f.appTop a.val)), inferInstance,
      inferInstance, inferInstance, inferInstance, inferInstance, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
this : IsAffine X
a : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)
⊢ Q (R := (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)) (S :=
    (↑Γ(X,
          X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              (↑a : (↑Γ(Y, ⊤) : Type u)))) :
      Type u))
    (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)
      (↑Γ(X,
            X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Scheme.Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑a : (↑Γ(Y, ⊤) : Type u)))) :
        Type u)
      (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (↑a : (↑Γ(Y, ⊤) : Type u)))
have left : IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Scheme)
Tactic: obtain ⟨_, hf⟩ := hf a
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
this : IsAffine X
a : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)
left : IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Scheme)
⊢ Q (R := (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)) (S :=
    (↑Γ(X,
          X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              (↑a : (↑Γ(Y, ⊤) : Type u)))) :
      Type u))
    (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)
      (↑Γ(X,
            X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Scheme.Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑a : (↑Γ(Y, ⊤) : Type u)))) :
        Type u)
      (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (↑a : (↑Γ(Y, ⊤) : Type u)))
have hf₁ : Q (R := (↑Γ((↑(Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
  (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u)))))
Tactic: obtain ⟨_, hf⟩ := hf a
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf_1 :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
this : IsAffine X
a : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)
left : IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Scheme)
hf :
  Q (R := (↑Γ((↑(Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u)))))
⊢ Q (R := (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)) (S :=
    (↑Γ(X,
          X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              (↑a : (↑Γ(Y, ⊤) : Type u)))) :
      Type u))
    (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)
      (↑Γ(X,
            X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Scheme.Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑a : (↑Γ(Y, ⊤) : Type u)))) :
        Type u)
      (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (↑a : (↑Γ(Y, ⊤) : Type u)))
have hf₁ : Q (R := (↑Γ((↑(Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
  (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))).ι ''ᵁ ⊤)))
Tactic: rw [morphismRestrict_appTop, CommRingCat.hom_comp, hPi.cancel_right_isIso] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf_1 :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
this : IsAffine X
a : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)
left : IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Scheme)
hf_2 :
  Q (R := (↑Γ((↑(Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))).ι ''ᵁ ⊤)))
hf :
  Q (R := (↑Γ(Y, (Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))).ι ''ᵁ ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))).ι ''ᵁ ⊤)))
⊢ Q (R := (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)) (S :=
    (↑Γ(X,
          X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              (↑a : (↑Γ(Y, ⊤) : Type u)))) :
      Type u))
    (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)
      (↑Γ(X,
            X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Scheme.Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑a : (↑Γ(Y, ⊤) : Type u)))) :
        Type u)
      (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (↑a : (↑Γ(Y, ⊤) : Type u)))
have hf₁ : Q (R := (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u))
  (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u)))))
Tactic: rw [Scheme.Opens.ι_image_top] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
h : IsAffine Y
f : X ⟶ Y
s : Finset (↑Γ(Y, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u))) ⊤
hf_1 :
  ∀ (r : ↥s),
    IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme) ∧
      Q (R := (↑Γ((↑(Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u)))))
this : IsAffine X
a : (↑(↑s : Set (↑Γ(Y, ⊤) : Type u)) : Type u)
left : IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Scheme)
hf_2 :
  Q (R := (↑Γ((↑(Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Scheme), ⊤) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app f ((Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))).ι ''ᵁ ⊤)))
hf :
  Q (R := (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u))
    (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u)))))
⊢ Q (R := (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)) (S :=
    (↑Γ(X,
          X.basicOpen (U := ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.appTop f) :
                (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
              (↑a : (↑Γ(Y, ⊤) : Type u)))) :
      Type u))
    (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)
      (↑Γ(X,
            X.basicOpen (U := ⊤)
              ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                    CommRingCat.carrier) (Scheme.Hom.appTop f) :
                  (a : (↑Γ(Y, ⊤) : Type u)) → (↑Γ(X, ⊤) : Type u))
                (↑a : (↑Γ(Y, ⊤) : Type u)))) :
        Type u)
      (CommRingCat.Hom.hom (Scheme.Hom.appTop f)) (↑a : (↑Γ(Y, ⊤) : Type u)))
have hf₁ : Q (R := (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u))
  (CommRingCat.Hom.hom
    (CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Type u)
          (↑Γ(X,
                X.basicOpen (U := f ⁻¹ᵁ ⊤)
                  ((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, f ⁻¹ᵁ ⊤) : Type u))
                    (↑a : (↑Γ(Y, ⊤) : Type u)))) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.app f ⊤)) (↑a : (↑Γ(Y, ⊤) : Type u))) ≫
      X.presheaf.map (Quiver.Hom.op (eqToHom sorry))))
Tactic: rw [(isAffineOpen_top Y).app_basicOpen_eq_away_map _ (isAffineOpen_top X)] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (hypothesis)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQb : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange.{u} (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
have this : (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
Tactic: haveI : (affineAnd Q).toProperty.RespectsIso := affineAnd_respectsIso hQi
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQb : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange.{u} (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
have H : ∀ ⦃X Y S : Scheme.{u}⦄ [inst : IsAffine S] [inst_1 : IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
  affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) g →
    affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := Limits.pullback f g) (Limits.pullback.fst f g)
Tactic: apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQb : RingHom.IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
this : (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
⊢ affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) g →
    affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := Limits.pullback f g) (Limits.pullback.fst f g)
have H : ∀ (hY : IsAffine Y) (hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))),
  affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q (X := Limits.pullback f g) (Limits.pullback.fst f g)
Tactic: ⟨hY, hg⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.AffineAnd (goal)
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
have simp : (∀ (U : (↑Y.affineOpens : Type u)),
    IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme) ∧
      Q (R := (↑Γ((↑(↑U : Y.Opens) : Scheme), ⊤) : Type u))
        (CommRingCat.Hom.hom (Scheme.Hom.app f ((↑U : Y.Opens).ι ''ᵁ ⊤)))) ↔
  ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
Tactic: simp only [targetAffineLocally, affineAnd_apply, morphismRestrict_app, CommRingCat.hom_comp,
    hQi.cancel_right_isIso]