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
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this_1 :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
this_2 :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
    (hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y : Scheme.{u}} (f : X ⟶ Y)
    (this :
      HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
        fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    (hf : IsAffineHom f) (hY : IsAffine Y),
    (∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) →
      affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hY : ¬IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
U : (↑Y.affineOpens : Type u)
this : IsAffine.{u} (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)
⊢ IsAffineOpen (↑U : Y.Opens)

Tactic:
exact U.2

Premises used: Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
hY : IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ IsAffine X

Tactic:
have : IsAffine X := isAffine_of_isAffineHom f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this_1 :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
hY : IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
this : IsAffine X
rw : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
rw [HasRingHomProperty.iff_of_isAffine (P := affineLocally Q)]

Premises used: AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this_1 :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
hY : IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
this : IsAffine X
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
h ⊤ (isAffineOpen_top Y)

Premises used: AlgebraicGeometry.isAffineOpen_top, Set.Mem, Set.univ, setOf, Set.preimage, Top.top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this_1 :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
hY : IsAffine Y
h : ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
this : IsAffine X
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
exact h ⊤ (isAffineOpen_top Y)

Premises used: AlgebraicGeometry.isAffineOpen_top, Top.top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
h : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
U : Y.Opens
hU : IsAffineOpen U
mpr :
  ∀
    (h :
      ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)))
    (U : Y.Opens) (hU : IsAffineOpen U), Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
rw [affineLocally_iff_affineOpens_le] at h

Premises used: AlgebraicGeometry.affineLocally_iff_affineOpens_le
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
h :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
U : Y.Opens
hU : IsAffineOpen U
mpr : Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯))
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
rw [f.app_eq_appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.app_eq_appLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
h :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
U : Y.Opens
hU : IsAffineOpen U
⊢ (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (f ⁻¹ᵁ U) ⋯) : X.Opens) ≤
    f ⁻¹ᵁ (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) U hU) : Y.Opens)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty.{u} (affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hf : IsAffineHom f
h :
  ∀ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (e : (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
    Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
U : Y.Opens
hU : IsAffineOpen U
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (f ⁻¹ᵁ U) ⋯))

Tactic:
exact h ⟨U, hU⟩ ⟨f ⁻¹ᵁ U, hf.isAffine_preimage U hU⟩ (by simp)

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Subtype.mk, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.IsAffineHom.isAffine_preimage, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y),
    targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f ↔
      (@IsAffineHom ⊓ affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) =
    @IsAffineHom ⊓ affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{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 ↔
    (@IsAffineHom ⊓ affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
targetAffineLocally_affineAnd_iff_affineLocally hQ f

Premises used: AlgebraicGeometry.targetAffineLocally_affineAnd_iff_affineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RingHom.PropertyIsLocal.{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 ↔
    (@IsAffineHom ⊓ affineLocally fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
exact targetAffineLocally_affineAnd_iff_affineLocally hQ f

Premises used: AlgebraicGeometry.targetAffineLocally_affineAnd_iff_affineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q W : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQW : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → W f
X Y : Scheme
f : X ⟶ Y
h : targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
U : (↑Y.affineOpens : Type u)
⊢ affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ W (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme))
    (f ∣_ (↑U : Y.Opens))

Tactic:
⟨(h U).1, hQW (h U).2⟩

Premises used: And.right, And.left, AlgebraicGeometry.affineAnd, And.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q W : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQW : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → W f
X Y : Scheme
f : X ⟶ Y
h : targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
U : (↑Y.affineOpens : Type u)
⊢ affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ W (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme))
    (f ∣_ (↑U : Y.Opens))

Tactic:
exact ⟨(h U).1, hQW (h U).2⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
inr :
  ∀
    (this :
      ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
        {P : MorphismProperty Scheme}
        (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
        (hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y Z : Scheme.{u}}
        (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g))
    (hZ : ¬IsAffine Z), P (f ≫ g)
wlog :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme}
    (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
    (hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y Z : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
⊢ P (f ≫ g)

Tactic:
wlog hZ : IsAffine Z

Premises used: AlgebraicGeometry.IsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme}
    (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
    (hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y Z : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
hZ : ¬IsAffine Z
inr : ∀ (i : (↑Z.affineOpens : Type u)), P (X := (↑((f ≫ g) ⁻¹ᵁ (↑i : Z.Opens)) : Scheme)) ((f ≫ g) ∣_ (↑i : Z.Opens))
⊢ P (f ≫ g)

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := P) _ (iSup_affineOpens_eq_top _)]

Premises used: AlgebraicGeometry.iSup_affineOpens_eq_top, AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_iSup_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme}
    (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
    (hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y Z : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
hZ : ¬IsAffine Z
U : (↑Z.affineOpens : Type u)
inr : P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens) ≫ g ∣_ (↑U : Z.Opens))
⊢ P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) ((f ≫ g) ∣_ (↑U : Z.Opens))

Tactic:
rw [morphismRestrict_comp]

Premises used: AlgebraicGeometry.morphismRestrict_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme}
    (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
    (hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y Z : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
hZ : ¬IsAffine Z
U : (↑Z.affineOpens : Type u)
⊢ P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens) ≫ g ∣_ (↑U : Z.Opens))

Tactic:
this hA hQ _ _ (IsZariskiLocalAtTarget.restrict hf _)
        (IsZariskiLocalAtTarget.restrict hg _) U.2

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, Set.Mem, setOf, Set.preimage, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
this :
  ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop} {P : MorphismProperty Scheme}
    (hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q))
    (hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) {X Y Z : Scheme.{u}}
    (f : X ⟶ Y) (g : Y ⟶ Z) (hf : P f) (hg : P g) (hZ : IsAffine Z), P (f ≫ g)
hZ : ¬IsAffine Z
U : (↑Z.affineOpens : Type u)
⊢ P (X := (↑((f ≫ g) ⁻¹ᵁ (↑U : Z.Opens)) : Scheme)) (f ∣_ g ⁻¹ᵁ (↑U : Z.Opens) ≫ g ∣_ (↑U : Z.Opens))

Tactic:
exact this hA hQ _ _ (IsZariskiLocalAtTarget.restrict hf _)
        (IsZariskiLocalAtTarget.restrict hg _) U.2

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hg : P g
hZ : IsAffine Z
⊢ affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) g

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hg

Premises used: AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hZ : IsAffine Z
hg : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) g
⊢ IsAffine Y

Tactic:
obtain ⟨hY, hg⟩ := hg
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hZ : IsAffine Z
hg : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) g
hY : IsAffine Y
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))

Tactic:
obtain ⟨hY, hg⟩ := hg
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hZ : IsAffine Z
hY : IsAffine Y
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hf

Premises used: AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : P f
hZ : IsAffine Z
hY : IsAffine Y
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hf₁ : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))] at hf

Premises used: AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hZ : IsAffine Z
hY : IsAffine Y
hf : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
⊢ IsAffine X

Tactic:
obtain ⟨hX, hf⟩ := hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hZ : IsAffine Z
hY : IsAffine Y
hf : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hX : IsAffine X
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))

Tactic:
obtain ⟨hX, hf⟩ := hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hZ : IsAffine Z
hY : IsAffine Y
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
rw : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) (f ≫ g)
⊢ P (f ≫ g)

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := P) (Q := (affineAnd Q))]

Premises used: AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hZ : IsAffine Z
hY : IsAffine Y
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) (f ≫ g)

Tactic:
⟨hX, hQ _ _ hg hf⟩

Premises used: AlgebraicGeometry.affineAnd, And.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q_1 Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hA : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hQ : RingHom.StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hZ : IsAffine Z
hY : IsAffine Y
hg : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop g))
hX : IsAffine X
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
⊢ affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) (f ≫ g)

Tactic:
exact ⟨hX, hQ _ _ hg hf⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
h : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
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
⊢ P.IsStableUnderBaseChange

Tactic:
HasAffineProperty.isStableUnderBaseChange
    (AlgebraicGeometry.affineAnd_isStableUnderBaseChange hQi hQb)

Premises used: AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange, AlgebraicGeometry.affineAnd_isStableUnderBaseChange