awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
inst_3 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S_1 : CommRingCat
φ : R ⟶ S_1
h : P' (Spec.map φ)
S : CommRingCat
g : Spec S ⟶ Spec R
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
apply : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
⊢ P g

Tactic:
apply of_pullback_fst_Spec_of_codescendsAlong _ _ hQQ' H₂ _ h hf

Premises used: AlgebraicGeometry.of_pullback_fst_Spec_of_codescendsAlong
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
inst_3 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S_1 : CommRingCat
φ : R ⟶ S_1
h : P' (Spec.map φ)
S : CommRingCat
g : Spec S ⟶ Spec R
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
⊢ ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)

Tactic:
simp [HasRingHomProperty.Spec_iff (P := P)]

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
apply :
  ∀ {R S : CommRingCat.{u}} {Y : Scheme.{u}} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    P' (Spec.map φ) → P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g) → P g
⊢ P.DescendsAlong (P' ⊓ @QuasiCompact)

Tactic:
apply IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact _ _ H₁

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
⊢ IsAffine Y

Tactic:
isAffine_of_isAffineHom g

Premises used: AlgebraicGeometry.isAffine_of_isAffineHom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
convert! : IsAffineHom g
⊢ IsAffine Y

Tactic:
convert! isAffine_of_isAffineHom g
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
⊢ IsAffineHom g

Tactic:
MorphismProperty.of_pullback_fst_of_descendsAlong h <|
      AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom P inferInstance _ hf

Premises used: CategoryTheory.MorphismProperty.of_pullback_fst_of_descendsAlong, inferInstance, AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
⊢ IsAffineHom g

Tactic:
exact MorphismProperty.of_pullback_fst_of_descendsAlong h <|
      AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom P inferInstance _ hf

Premises used: CategoryTheory.MorphismProperty.of_pullback_fst_of_descendsAlong, inferInstance, AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
have : ∀ (this : IsAffine Y), P g
⊢ P g

Tactic:
have : IsAffine Y := by
    convert! isAffine_of_isAffineHom g
    exact MorphismProperty.of_pullback_fst_of_descendsAlong h <|
      AlgebraicGeometry.HasAffineProperty.affineAnd_le_isAffineHom P inferInstance _ hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this : IsAffine Y
inr :
  ∀
    (this :
      ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
        (this : IsAffine Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g)
    (hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S), P g
wlog :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (this : IsAffine Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g
⊢ P g

Tactic:
wlog hY : ∃ S, Y = Spec S generalizing Y

Premises used: AlgebraicGeometry.Spec
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this_1 : IsAffine Y
this :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (this : IsAffine Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
inr : P (Y.isoSpec.inv ≫ g)
⊢ P g

Tactic:
rw [← P.cancel_left_of_respectsIso Y.isoSpec.inv]

Premises used: AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this_1 : IsAffine Y
this :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (this : IsAffine Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
⊢ Spec.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map φ

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this_1 : IsAffine Y
this :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (this : IsAffine Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
⊢ (Y.isoSpec.inv ≫ g) ≫ 𝟙 (Spec R) = Y.isoSpec.inv ≫ g

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this_1 : IsAffine Y
this :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (this : IsAffine Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
inr :
  ∀
    (heq :
      Eq (α := pullback (Spec.map φ) (Y.isoSpec.inv ≫ g) ⟶ Spec S) (pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g))
        (CategoryStruct.comp (Y := pullback (Spec.map φ) g)
          (pullback.map (Spec.map φ) (Y.isoSpec.inv ≫ g) (Spec.map φ) g (𝟙 (Spec S)) Y.isoSpec.inv (𝟙 (Spec R)) ⋯ ⋯)
          (pullback.fst (Spec.map φ) g))),
    P (Y.isoSpec.inv ≫ g)
⊢ P (Y.isoSpec.inv ≫ g)

Tactic:
have heq : pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g) =
        pullback.map _ _ _ _ (𝟙 _) (Y.isoSpec.inv) (𝟙 _) (by simp) (by simp) ≫
          pullback.fst (Spec.map φ) g := (pullback.lift_fst _ _ _).symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this_1 : IsAffine Y
this :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (this : IsAffine Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
heq :
  Eq (α := pullback (Spec.map φ) (Y.isoSpec.inv ≫ g) ⟶ Spec S) (pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g))
    (CategoryStruct.comp (Y := pullback (Spec.map φ) g)
      (pullback.map (Spec.map φ) (Y.isoSpec.inv ≫ g) (Spec.map φ) g (𝟙 (Spec S)) Y.isoSpec.inv (𝟙 (Spec R)) ⋯ ⋯)
      (pullback.fst (Spec.map φ) g))
⊢ P (Y.isoSpec.inv ≫ g)

Tactic:
this _ ?_ inferInstance ⟨_, rfl⟩

Premises used: inferInstance, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this_1 : IsAffine Y
this :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (this : IsAffine Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
heq :
  Eq (α := pullback (Spec.map φ) (Y.isoSpec.inv ≫ g) ⟶ Spec S) (pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g))
    (CategoryStruct.comp (Y := pullback (Spec.map φ) g)
      (pullback.map (Spec.map φ) (Y.isoSpec.inv ≫ g) (Spec.map φ) g (𝟙 (Spec S)) Y.isoSpec.inv (𝟙 (Spec R)) ⋯ ⋯)
      (pullback.fst (Spec.map φ) g))
inr : P (X := pullback (Spec.map φ) (Y.isoSpec.inv ≫ g)) (pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g))
⊢ P (Y.isoSpec.inv ≫ g)

Tactic:
refine this _ ?_ inferInstance ⟨_, rfl⟩

Premises used: inferInstance, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : P' (Spec.map φ)
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this_1 : IsAffine Y
this :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (this : IsAffine Y) (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
heq :
  Eq (α := pullback (Spec.map φ) (Y.isoSpec.inv ≫ g) ⟶ Spec S) (pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g))
    (CategoryStruct.comp (Y := pullback (Spec.map φ) g)
      (pullback.map (Spec.map φ) (Y.isoSpec.inv ≫ g) (Spec.map φ) g (𝟙 (Spec S)) Y.isoSpec.inv (𝟙 (Spec R)) ⋯ ⋯)
      (pullback.fst (Spec.map φ) g))
inr :
  P (X := pullback (Spec.map φ) (Y.isoSpec.inv ≫ g))
    (CategoryStruct.comp (Y := pullback (Spec.map φ) g)
      (pullback.map (Spec.map φ) (Y.isoSpec.inv ≫ g) (Spec.map φ) g (𝟙 (Spec S)) Y.isoSpec.inv (𝟙 (Spec R)) ⋯ ⋯)
      (pullback.fst (Spec.map φ) g))
inr₁ inr₂ inr₃ inr₄ : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
⊢ P (X := pullback (Spec.map φ) (Y.isoSpec.inv ≫ g)) (pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g))

Tactic:
rwa [heq, P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
φ : R ⟶ S
h : P' (Spec.map φ)
Y : Scheme
g : Y ⟶ Spec R
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this : IsAffine Y
hY : ∃ (S : CommRingCat.{u}), Y = Spec S
obtain :
  ∀ (Y : CommRingCat.{u}) (g : Spec Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (this : IsAffine.{u} (Spec Y)), P g
⊢ P g

Tactic:
obtain ⟨Y, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_4 : CommRing S] → (R →+* S) → Prop
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
hP : HasAffineProperty P (affineAnd fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
inst_3 : MorphismProperty.DescendsAlong (@IsAffineHom) P'
hQ : RingHom.RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
R S : CommRingCat
φ : R ⟶ S
h : P' (Spec.map φ)
Y : CommRingCat
g : Spec Y ⟶ Spec R
hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this : IsAffine.{u} (Spec Y)
apply : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
⊢ P g

Tactic:
apply of_pullback_fst_Spec_of_codescendsAlong _ _ hQQ' H₂ _ h hf

Premises used: AlgebraicGeometry.of_pullback_fst_Spec_of_codescendsAlong