awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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)
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)))
⊢ ∃ (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 ⟨Γ(Y, Y.basicOpen a.val), Γ(X, X.basicOpen (f.appTop a.val)), inferInstance,
      inferInstance, inferInstance, inferInstance, inferInstance, ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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)
⊢ 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:
(isAffineOpen_top X).isLocalization_basicOpen (f.appTop a.val)

Premises used: AlgebraicGeometry.isAffineOpen_top, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, AlgebraicGeometry.Scheme.Hom.appTop, Subtype.val, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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)
⊢ 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:
exact (isAffineOpen_top X).isLocalization_basicOpen (f.appTop a.val)

Premises used: AlgebraicGeometry.isAffineOpen_top, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, AlgebraicGeometry.Scheme.Hom.appTop, Subtype.val, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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)
⊢ IsAffine.{u} (↑(f ⁻¹ᵁ Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u))) : Scheme)

Tactic:
obtain ⟨_, hf⟩ := hf a
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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.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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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.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

Premises used: RingHom.RespectsIso.cancel_right_isIso, CommRingCat.hom_comp, AlgebraicGeometry.morphismRestrict_appTop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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))
    (CommRingCat.Hom.hom (Scheme.Hom.app f (Y.basicOpen (↑a : (↑Γ(Y, ⊤) : Type u)))))

Tactic:
rw [Scheme.Opens.ι_image_top] at hf

Premises used: AlgebraicGeometry.Scheme.Opens.ι_image_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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))
    (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 ⋯))))

Tactic:
rw [(isAffineOpen_top Y).app_basicOpen_eq_away_map _ (isAffineOpen_top X)] at hf

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.IsAffineOpen.app_basicOpen_eq_away_map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ AffineTargetMorphismProperty.IsLocal.{u} (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)

Tactic:
affineAnd_isLocal hPi.respectsIso hPi.localizationAwayPreserves hPi.ofLocalizationSpan

Premises used: RingHom.PropertyIsLocal.localizationAwayPreserves, AlgebraicGeometry.affineAnd_isLocal, RingHom.PropertyIsLocal.respectsIso, RingHom.PropertyIsLocal.ofLocalizationSpan
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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
⊢ (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).toProperty.RespectsIso

Tactic:
haveI : (affineAnd Q).toProperty.RespectsIso := affineAnd_respectsIso hQi
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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
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)
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange.{u} (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)

Tactic:
apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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
X Y S : Scheme
H :
  ∀ [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)
⊢ ∀ [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:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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
X Y S : Scheme
inst : IsAffine S
H :
  ∀ [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)
⊢ ∀ [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:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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
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)
⊢ 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:
⟨hY, hg⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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
hY : IsAffine Y
hg : (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (Q : (R →+* S) → Prop)) (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:
⟨inferInstance, hQb.pullback_fst_appTop _ hQi f _ hg⟩

Premises used: RingHom.IsStableUnderBaseChange.pullback_fst_appTop, inferInstance, AlgebraicGeometry.affineAnd, And.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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
hY : IsAffine Y
hg : (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (Q : (R →+* S) → Prop)) (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:
exact ⟨inferInstance, hQb.pullback_fst_appTop _ hQi f _ hg⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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
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))
⊢ 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))

Tactic:
simp only [targetAffineLocally, affineAnd_apply, morphismRestrict_app, CommRingCat.hom_comp,
    hQi.cancel_right_isIso]

Premises used: RingHom.RespectsIso.cancel_right_isIso, CommRingCat.hom_comp, AlgebraicGeometry.targetAffineLocally, AlgebraicGeometry.affineAnd_apply, AlgebraicGeometry.morphismRestrict_app
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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
⊢ (∀ (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:
⟨fun hf U hU ↦ ?_, fun h U ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
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
refine_1 :
  ∀
    (hf :
      ∀ (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) (hU : IsAffineOpen U), IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
refine_2 :
  ∀ (h : ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U)))
    (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.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:
refine ⟨fun hf U hU ↦ ?_, fun h U ↦ ?_⟩