awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst_3 : IsZariskiLocalAtTarget P
H :
  ∀ {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
R : CommRingCat
X Y_1 : Scheme
f : X ⟶ Spec R
g : Y_1 ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) (hf : (P' ⊓ @QuasiCompact) f) (h : P (X := pullback f g) (pullback.fst f g))
    (hX : ∃ (T : CommRingCat.{u}), X = Spec T), P g
hX : ¬∃ (T : CommRingCat.{u}), X = Spec T
h_1 : CompactSpace.{u} ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
⊢ P g

Tactic:
this (f := (Y.isoSpec.inv ≫ p) ≫ f) ?_ ?_ ⟨_, rfl⟩

Premises used: AlgebraicGeometry.Scheme.isoSpec, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst_3 : IsZariskiLocalAtTarget P
H :
  ∀ {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
R : CommRingCat
X Y_1 : Scheme
f : X ⟶ Spec R
g : Y_1 ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) (hf : (P' ⊓ @QuasiCompact) f) (h : P (X := pullback f g) (pullback.fst f g))
    (hX : ∃ (T : CommRingCat.{u}), X = Spec T), P g
hX : ¬∃ (T : CommRingCat.{u}), X = Spec T
h_1 : CompactSpace.{u} ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
H₂ : (P' ⊓ @QuasiCompact) ((Y.isoSpec.inv ≫ p) ≫ f)
H₃ : P (X := pullback ((Y.isoSpec.inv ≫ p) ≫ f) g) (pullback.fst ((Y.isoSpec.inv ≫ p) ≫ f) g)
⊢ P g

Tactic:
refine this (f := (Y.isoSpec.inv ≫ p) ≫ f) ?_ ?_ ⟨_, rfl⟩

Premises used: AlgebraicGeometry.Scheme.isoSpec, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst_3 : IsZariskiLocalAtTarget P
H :
  ∀ {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
R : CommRingCat
X Y_1 : Scheme
f : X ⟶ Spec R
g : Y_1 ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) (hf : (P' ⊓ @QuasiCompact) f) (h : P (X := pullback f g) (pullback.fst f g))
    (hX : ∃ (T : CommRingCat.{u}), X = Spec T), P g
hX : ¬∃ (T : CommRingCat.{u}), X = Spec T
h_1 : CompactSpace.{u} ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
H₂ : (P' ⊓ @QuasiCompact) (p ≫ f)
⊢ (P' ⊓ @QuasiCompact) ((Y.isoSpec.inv ≫ p) ≫ f)

Tactic:
rw [Category.assoc, (P' ⊓ @QuasiCompact).cancel_left_of_respectsIso]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.QuasiCompact, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, Min.min
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst_3 : IsZariskiLocalAtTarget P
H :
  ∀ {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
R : CommRingCat
X Y_1 : Scheme
f : X ⟶ Spec R
g : Y_1 ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) (hf : (P' ⊓ @QuasiCompact) f) (h : P (X := pullback f g) (pullback.fst f g))
    (hX : ∃ (T : CommRingCat.{u}), X = Spec T), P g
hX : ¬∃ (T : CommRingCat.{u}), X = Spec T
h_1 : CompactSpace.{u} ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
⊢ (P' ⊓ @QuasiCompact) (p ≫ f)

Tactic:
⟨P'.comp_mem _ _ (H₁ _ ⟨hP', hsurj⟩) hf.1, inferInstance⟩

Premises used: inferInstance, CategoryTheory.MorphismProperty.comp_mem, And.left, And.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst_3 : IsZariskiLocalAtTarget P
H :
  ∀ {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
R : CommRingCat
X Y_1 : Scheme
f : X ⟶ Spec R
g : Y_1 ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) (hf : (P' ⊓ @QuasiCompact) f) (h : P (X := pullback f g) (pullback.fst f g))
    (hX : ∃ (T : CommRingCat.{u}), X = Spec T), P g
hX : ¬∃ (T : CommRingCat.{u}), X = Spec T
h_1 : CompactSpace.{u} ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
⊢ (P' ⊓ @QuasiCompact) (p ≫ f)

Tactic:
exact ⟨P'.comp_mem _ _ (H₁ _ ⟨hP', hsurj⟩) hf.1, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst_3 : IsZariskiLocalAtTarget P
H :
  ∀ {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
R : CommRingCat
X Y_1 : Scheme
f : X ⟶ Spec R
g : Y_1 ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) (hf : (P' ⊓ @QuasiCompact) f) (h : P (X := pullback f g) (pullback.fst f g))
    (hX : ∃ (T : CommRingCat.{u}), X = Spec T), P g
hX : ¬∃ (T : CommRingCat.{u}), X = Spec T
h_1 : CompactSpace.{u} ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
H₂ :
  P (X := pullback (Y := pullback f g) (Y.isoSpec.inv ≫ p) (pullback.fst f g))
    (pullback.fst (Y.isoSpec.inv ≫ p) (pullback.fst f g))
⊢ P (X := pullback ((Y.isoSpec.inv ≫ p) ≫ f) g) (pullback.fst ((Y.isoSpec.inv ≫ p) ≫ f) g)

Tactic:
rw [← pullbackRightPullbackFstIso_inv_fst f g _, P.cancel_left_of_respectsIso]

Premises used: CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst_3 : IsZariskiLocalAtTarget P
H :
  ∀ {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
R : CommRingCat
X Y_1 : Scheme
f : X ⟶ Spec R
g : Y_1 ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) (hf : (P' ⊓ @QuasiCompact) f) (h : P (X := pullback f g) (pullback.fst f g))
    (hX : ∃ (T : CommRingCat.{u}), X = Spec T), P g
hX : ¬∃ (T : CommRingCat.{u}), X = Spec T
h_1 : CompactSpace.{u} ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
⊢ P (X := pullback (Y := pullback f g) (Y.isoSpec.inv ≫ p) (pullback.fst f g))
    (pullback.fst (Y.isoSpec.inv ≫ p) (pullback.fst f g))

Tactic:
P.pullback_fst _ _ h

Premises used: CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst_3 : IsZariskiLocalAtTarget P
H :
  ∀ {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
R : CommRingCat
X Y_1 : Scheme
f : X ⟶ Spec R
g : Y_1 ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) (hf : (P' ⊓ @QuasiCompact) f) (h : P (X := pullback f g) (pullback.fst f g))
    (hX : ∃ (T : CommRingCat.{u}), X = Spec T), P g
hX : ¬∃ (T : CommRingCat.{u}), X = Spec T
h_1 : CompactSpace.{u} ↥X
Y : Scheme
p : Y ⟶ X
hsurj : Surjective p
hP' : IsLocalIso p
hY : IsAffine Y
⊢ P (X := pullback (Y := pullback f g) (Y.isoSpec.inv ≫ p) (pullback.fst f g))
    (pullback.fst (Y.isoSpec.inv ≫ p) (pullback.fst f g))

Tactic:
exact P.pullback_fst _ _ h

Premises used: CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst_3 : IsZariskiLocalAtTarget P
H :
  ∀ {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
R : CommRingCat
Y : Scheme
g : Y ⟶ Spec R
X : Scheme
f : X ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (X := pullback f g) (pullback.fst f g)
hX : ∃ (T : CommRingCat.{u}), X = Spec T
obtain :
  ∀ (T : CommRingCat.{u}) (f : Spec T ⟶ Spec R) (hf : (P' ⊓ @QuasiCompact) f)
    (h : P (X := pullback f g) (pullback.fst f g)), P g
⊢ P g

Tactic:
obtain ⟨T, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst_3 : IsZariskiLocalAtTarget P
H :
  ∀ {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
R : CommRingCat
Y : Scheme
g : Y ⟶ Spec R
T : CommRingCat
f : Spec T ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (X := pullback f g) (pullback.fst f g)
obtain :
  ∀ (φ : R ⟶ T) (hf : (P' ⊓ @QuasiCompact) (Spec.map φ))
    (h : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)), P g
⊢ P g

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst_3 : IsZariskiLocalAtTarget P
H :
  ∀ {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
R : CommRingCat
Y : Scheme
g : Y ⟶ Spec R
T : CommRingCat
φ : R ⟶ T
hf : (P' ⊓ @QuasiCompact) (Spec.map φ)
h : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
⊢ P g

Tactic:
H φ g hf.1 h

Premises used: And.left
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.IsStableUnderBaseChange
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H₁ : @IsLocalIso ⊓ @Surjective ≤ P'
inst_3 : IsZariskiLocalAtTarget P
H :
  ∀ {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
R : CommRingCat
Y : Scheme
g : Y ⟶ Spec R
T : CommRingCat
φ : R ⟶ T
hf : (P' ⊓ @QuasiCompact) (Spec.map φ)
h : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
⊢ P g

Tactic:
exact H φ g hf.1 h

Premises used: And.left
-- 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'
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)
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 : 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)
inr :
  ∀
    (this :
      ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
        (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))
    (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)
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 : 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 :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
inr : ∀ (i : Y.affineCover.I₀), P (Y.affineCover.f i ≫ g)
⊢ P g

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) Y.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- 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 : 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 :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
i : Y.affineCover.I₀
⊢ 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)
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 : 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 :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
i : Y.affineCover.I₀
⊢ (Y.affineCover.f i ≫ g) ≫ 𝟙 (Spec R) = Y.affineCover.f i ≫ 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)
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 : 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 :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
i : Y.affineCover.I₀
inr :
  ∀
    (heq :
      Eq (α := pullback (Spec.map φ) (Y.affineCover.f i ≫ g) ⟶ Spec S)
        (pullback.fst (Spec.map φ) (Y.affineCover.f i ≫ g))
        (CategoryStruct.comp (Y := pullback (Spec.map φ) g)
          (pullback.map (Spec.map φ) (Y.affineCover.f i ≫ g) (Spec.map φ) g (𝟙 (Spec S)) (Y.affineCover.f i)
            (𝟙 (Spec R)) ⋯ ⋯)
          (pullback.fst (Spec.map φ) g))),
    P (Y.affineCover.f i ≫ g)
⊢ P (Y.affineCover.f i ≫ g)

Tactic:
have heq : pullback.fst (Spec.map φ) (Y.affineCover.f i ≫ g) =
        pullback.map _ _ _ _ (𝟙 _) (Y.affineCover.f i) (𝟙 _) (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)
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 : 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 :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
i : Y.affineCover.I₀
heq :
  Eq (α := pullback (Spec.map φ) (Y.affineCover.f i ≫ g) ⟶ Spec S) (pullback.fst (Spec.map φ) (Y.affineCover.f i ≫ g))
    (CategoryStruct.comp (Y := pullback (Spec.map φ) g)
      (pullback.map (Spec.map φ) (Y.affineCover.f i ≫ g) (Spec.map φ) g (𝟙 (Spec S)) (Y.affineCover.f i) (𝟙 (Spec R)) ⋯
        ⋯)
      (pullback.fst (Spec.map φ) g))
⊢ P (Y.affineCover.f i ≫ g)

Tactic:
this _ (heq ▸ AlgebraicGeometry.IsZariskiLocalAtSource.comp hf _) ⟨_, rfl⟩

Premises used: Eq.rec, Exists.intro, Eq.symm, AlgebraicGeometry.IsZariskiLocalAtSource.comp, 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)
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 : 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 :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), P g
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
i : Y.affineCover.I₀
heq :
  Eq (α := pullback (Spec.map φ) (Y.affineCover.f i ≫ g) ⟶ Spec S) (pullback.fst (Spec.map φ) (Y.affineCover.f i ≫ g))
    (CategoryStruct.comp (Y := pullback (Spec.map φ) g)
      (pullback.map (Spec.map φ) (Y.affineCover.f i ≫ g) (Spec.map φ) g (𝟙 (Spec S)) (Y.affineCover.f i) (𝟙 (Spec R)) ⋯
        ⋯)
      (pullback.fst (Spec.map φ) g))
⊢ P (Y.affineCover.f i ≫ g)

Tactic:
exact this _ (heq ▸ AlgebraicGeometry.IsZariskiLocalAtSource.comp hf _) ⟨_, rfl⟩

Premises used: 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)
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 : 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)
hY : ∃ (S : CommRingCat.{u}), Y = Spec S
obtain :
  ∀ (S_1 : CommRingCat.{u}) (g : Spec S_1 ⟶ Spec R)
    (hf : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)), P g
⊢ P g

Tactic:
obtain ⟨S, rfl⟩ := hY

Premises used: rfl