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
P : MorphismProperty Scheme
hA : 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
hQ : RingHom.ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X : Scheme
rw : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen (𝟙 X ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app (𝟙 X) U))
⊢ P (𝟙 X)

Tactic:
rw [eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi]

Premises used: AlgebraicGeometry.targetAffineLocally_affineAnd_iff, AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally
-- 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)
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQ : RingHom.ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen (𝟙 X ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app (𝟙 X) U))

Tactic:
⟨hU, hQ _⟩

Premises used: And.intro
-- 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)
hQi : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQ : RingHom.ContainsIdentities.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen (𝟙 X ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app (𝟙 X) U))

Tactic:
exact ⟨hU, hQ _⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
simp_rw :
  HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ↔
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
      P f ↔
        (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
          ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ↔
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
      P f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
simp_rw [isAffineHom_iff]

Premises used: AlgebraicGeometry.isAffineHom_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
⊢ HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ↔
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
      P f ↔
        (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
          ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
⟨fun h X Y f ↦ ?_, fun h ↦ ⟨affineAnd_isLocal hQi hQl hQs, ?_⟩⟩

Premises used: AlgebraicGeometry.affineAnd_isLocal, AlgebraicGeometry.HasAffineProperty.mk, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
refine_1 :
  ∀ (h : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)) (X Y : Scheme.{u})
    (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
refine_2 :
  ∀
    (h :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
        P f ↔
          (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
            ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))),
    P = targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
⊢ HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ↔
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
      P f ↔
        (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
          ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
refine ⟨fun h X Y f ↦ ?_, fun h ↦ ⟨affineAnd_isLocal hQi hQl hQs, ?_⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
h : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
refine_1 :
  (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ P f ↔
    (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
rw [eq_targetAffineLocally P, targetAffineLocally_affineAnd_iff hQi]

Premises used: AlgebraicGeometry.targetAffineLocally_affineAnd_iff, AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
h : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
lia
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
h :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
refine_2 :
  ∀ ⦃X Y : Scheme.{u}⦄ (f : X ⟶ Y),
    P f ↔ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ P = targetAffineLocally (affineAnd 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
P : MorphismProperty Scheme
hQi : 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
h :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
X Y : Scheme
f : X ⟶ Y
refine_2 :
  ((∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
⊢ P f ↔ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f

Tactic:
rw [targetAffineLocally_affineAnd_iff hQi, h f]

Premises used: AlgebraicGeometry.targetAffineLocally_affineAnd_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : 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
h :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y),
    P f ↔
      (∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
        ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))
X Y : Scheme
f : X ⟶ Y
⊢ ((∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U)) ∧
      ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsAffineOpen (f ⁻¹ᵁ U) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
aesop
-- 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)
X Y : Scheme
f : X ⟶ Y
hf : P f
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)) ⦃X Y : Scheme.{u}⦄
        (f : X ⟶ Y) (hf : P f) (hY : IsAffine Y), IsAffineHom f)
    (hY : ¬IsAffine Y), IsAffineHom f
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)) ⦃X Y : Scheme.{u}⦄
    (f : X ⟶ Y) (hf : P f) (hY : IsAffine Y), IsAffineHom f
⊢ IsAffineHom f

Tactic:
wlog hY : IsAffine Y

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)
X Y : Scheme
f : X ⟶ Y
hf : P f
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)) ⦃X Y : Scheme.{u}⦄
    (f : X ⟶ Y) (hf : P f) (hY : IsAffine Y), IsAffineHom f
hY : ¬IsAffine Y
inr : ∀ (i : (↑Y.affineOpens : Type u)), IsAffineHom (X := (↑(f ⁻¹ᵁ (↑i : Y.Opens)) : Scheme)) (f ∣_ (↑i : Y.Opens))
⊢ IsAffineHom f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsAffineHom) _ (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)
X Y : Scheme
f : X ⟶ Y
hf : P f
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)) ⦃X Y : Scheme.{u}⦄
    (f : X ⟶ Y) (hf : P f) (hY : IsAffine Y), IsAffineHom f
hY : ¬IsAffine Y
U : (↑Y.affineOpens : Type u)
⊢ IsAffineHom (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))

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

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict, 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)
X Y : Scheme
f : X ⟶ Y
hf : P f
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)) ⦃X Y : Scheme.{u}⦄
    (f : X ⟶ Y) (hf : P f) (hY : IsAffine Y), IsAffineHom f
hY : ¬IsAffine Y
U : (↑Y.affineOpens : Type u)
⊢ IsAffineHom (X := (↑(f ⁻¹ᵁ (↑U : Y.Opens)) : Scheme)) (f ∣_ (↑U : Y.Opens))

Tactic:
exact this P hA _ (IsZariskiLocalAtTarget.restrict hf _) 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)
X Y : Scheme
f : X ⟶ Y
hf : P f
hY : IsAffine Y
⊢ 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)
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
hf : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
rw : IsAffine X
⊢ IsAffineHom f

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := @IsAffineHom)]

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)
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
hf : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ IsAffine X

Tactic:
hf.1

Premises used: And.left
-- 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)
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
hf : affineAnd (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) f
⊢ IsAffine X

Tactic:
exact hf.1

Premises used: And.left
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst : HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
rw : RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ P = @IsAffineHom ⊓ P'

Tactic:
rw [HasAffineProperty.eq_targetAffineLocally (P := P),
    targetAffineLocally_affineAnd_eq_affineLocally,
    HasRingHomProperty.eq_affineLocally (P := P')]

Premises used: AlgebraicGeometry.HasRingHomProperty.eq_affineLocally, AlgebraicGeometry.targetAffineLocally_affineAnd_eq_affineLocally, AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst : HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
HasRingHomProperty.isLocal_ringHomProperty P'

Premises used: AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst : HasRingHomProperty P' fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ RingHom.PropertyIsLocal.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
exact HasRingHomProperty.isLocal_ringHomProperty P'

Premises used: AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : 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
R S : CommRingCat
f : R ⟶ S
⊢ (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso

Tactic:
have := RingHom.toMorphismProperty_respectsIso_iff.mp hQi
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : 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
R S : CommRingCat
f : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
rw : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))) ↔ Q (CommRingCat.Hom.hom f)
rw₁ : IsAffine.{u} (Spec S)
⊢ P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)

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

Premises used: and_iff_right, AlgebraicGeometry.affineAnd, AlgebraicGeometry.HasAffineProperty.iff_of_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
hP : 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
R S : CommRingCat
f : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))) ↔ Q (CommRingCat.Hom.hom f)

Tactic:
MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty Q)
    (arrowIsoΓSpecOfIsAffine f).symm

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, RingHom.toMorphismProperty, CategoryTheory.Iso.symm, AlgebraicGeometry.arrowIsoΓSpecOfIsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : 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
R S : CommRingCat
f : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ IsAffine.{u} (Spec S)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hP : 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
R S : CommRingCat
f : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q).RespectsIso
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))) ↔ Q (CommRingCat.Hom.hom f)

Tactic:
exacts [MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty Q)
    (arrowIsoΓSpecOfIsAffine f).symm, inferInstance]

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, RingHom.toMorphismProperty, CategoryTheory.Iso.symm, AlgebraicGeometry.arrowIsoΓSpecOfIsAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hP' : HasAffineProperty P' (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q')
hQQ' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → Q' f
rw :
  targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ≤
    targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q')
⊢ P ≤ P'

Tactic:
rw [HasAffineProperty.eq_targetAffineLocally (P := P),
    HasAffineProperty.eq_targetAffineLocally (P := P')]

Premises used: AlgebraicGeometry.HasAffineProperty.eq_targetAffineLocally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hP' : HasAffineProperty P' (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q')
hQQ' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → Q' f
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ≤
    targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q')

Tactic:
targetAffineLocally_affineAnd_le hQQ'

Premises used: AlgebraicGeometry.targetAffineLocally_affineAnd_le
-- Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
Goal:
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P P' : MorphismProperty Scheme
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
hP' : HasAffineProperty P' (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q')
hQQ' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → Q' f
⊢ targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q) ≤
    targetAffineLocally (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q')

Tactic:
exact targetAffineLocally_affineAnd_le hQQ'

Premises used: AlgebraicGeometry.targetAffineLocally_affineAnd_le