awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
this :
  ∀ {X Y Z : Scheme.{u}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)) (hZ : ∃ (R : CommRingCat.{u}), Z = Spec R), P g
hZ : ¬∃ (R : CommRingCat.{u}), Z = Spec R
i : Z.affineCover.toPreZeroHypercover.1
ι : Z.affineCover.X i ⟶ Z := Z.affineCover.f i
e : pullback (X := pullback f ι) (Y := pullback g ι) (pullback.snd f ι) (pullback.snd g ι) ≅
  pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι) :=
  pullbackLeftPullbackSndIso f ι (pullback.snd g ι) ≪≫
    Iso.trans (Y := pullback (Y := pullback g ι) f (pullback.fst g ι ≫ g)) (pullback.congrHom ⋯ ⋯)
      (Iso.trans (Y := pullback (X := pullback f g) (pullback.snd f g ≫ g) ι) (Iso.symm (pullbackAssoc f g g ι))
        (pullback.congrHom ⋯ ⋯ ≪≫ Iso.symm (pullbackRightPullbackFstIso f ι (pullback.fst f g))))
heq : e.hom ≫ pullback.snd (pullback.fst f g) (pullback.fst f ι) = pullback.fst (pullback.snd f ι) (pullback.snd g ι)
⊢ P (X := pullback (X := pullback f g) (Y := pullback f ι) (pullback.fst f g) (pullback.fst f ι))
    (pullback.snd (pullback.fst f g) (pullback.fst f ι))

Tactic:
exact AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback (iY := pullback.fst f ι)
        (CategoryTheory.IsPullback.of_hasPullback _ _) hf

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
hZ : ∃ (R : CommRingCat.{u}), Z = Spec R
obtain :
  ∀ (R : CommRingCat.{u}) {f : X ⟶ Spec R} {g : Y ⟶ Spec R} [inst : HasPullback f g] (h : P' f)
    (hf : P (X := pullback f g) (pullback.fst f g)), P g
⊢ P g

Tactic:
obtain ⟨R, rfl⟩ := hZ

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y : Scheme
R : CommRingCat
f : X ⟶ Spec R
g : Y ⟶ Spec R
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
⊢ P g

Tactic:
H f g h hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : IsZariskiLocalAtTarget P
inst_1 : P'.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y : Scheme
R : CommRingCat
f : X ⟶ Spec R
g : Y ⟶ Spec R
inst_2 : HasPullback f g
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
⊢ P g

Tactic:
exact H f g h hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : P.RespectsIso
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
f : Spec T ⟶ Spec R
g : Spec S ⟶ Spec R
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
obtain : ∀ (φ : R ⟶ S) (hf : P (X := pullback f (Spec.map φ)) (pullback.fst f (Spec.map φ))), P (Spec.map φ)
⊢ P g

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

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : P.RespectsIso
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
f : Spec T ⟶ Spec R
h : P' f
φ : R ⟶ S
hf : P (X := pullback f (Spec.map φ)) (pullback.fst f (Spec.map φ))
obtain :
  ∀ (ψ : R ⟶ T) (h : P' (Spec.map ψ))
    (hf : P (X := pullback (Spec.map ψ) (Spec.map φ)) (pullback.fst (Spec.map ψ) (Spec.map φ))), P (Spec.map φ)
⊢ P (Spec.map φ)

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

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : P.RespectsIso
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
φ : R ⟶ S
ψ : R ⟶ T
h : P' (Spec.map ψ)
hf : P (X := pullback (Spec.map ψ) (Spec.map φ)) (pullback.fst (Spec.map ψ) (Spec.map φ))
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑T : Type u) := (CommRingCat.Hom.hom ψ).toAlgebra
replace :
  ∀
    (hf :
      P (X :=
        pullback (X := Spec (CommRingCat.of (↑T : Type u))) (Y := Spec (CommRingCat.of (↑S : Type u))) (Z :=
          Spec (CommRingCat.of (↑R : Type u))) (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
          (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
        (pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
          (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))),
    P (Spec.map φ)
⊢ P (Spec.map φ)

Tactic:
replace hf : P (pullback.fst (Spec.map <| CommRingCat.ofHom <| algebraMap R T)
    (Spec.map <| CommRingCat.ofHom <| algebraMap R S)) := hf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : P.RespectsIso
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
φ : R ⟶ S
ψ : R ⟶ T
h : P' (Spec.map ψ)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑T : Type u) := (CommRingCat.Hom.hom ψ).toAlgebra
hf :
  P (X :=
    pullback (X := Spec (CommRingCat.of (↑T : Type u))) (Y := Spec (CommRingCat.of (↑S : Type u))) (Z :=
      Spec (CommRingCat.of (↑R : Type u))) (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
    (pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
rw : Q (CommRingCat.Hom.hom φ)
⊢ P (Spec.map φ)

Tactic:
rw [H₂]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : P.RespectsIso
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
φ : R ⟶ S
ψ : R ⟶ T
h : P' (Spec.map ψ)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑T : Type u) := (CommRingCat.Hom.hom ψ).toAlgebra
hf :
  P (X :=
    pullback (X := Spec (CommRingCat.of (↑T : Type u))) (Y := Spec (CommRingCat.of (↑S : Type u))) (Z :=
      Spec (CommRingCat.of (↑R : Type u))) (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
    (pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
⊢ Q (CommRingCat.Hom.hom φ)

Tactic:
hQQ'.algebraMap_tensorProduct (R := R) (S := T) (T := S) _ (H₁ h) ?_

Premises used: CommRingCat.carrier, RingHom.CodescendsAlong.algebraMap_tensorProduct
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : P.RespectsIso
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
φ : R ⟶ S
ψ : R ⟶ T
h : P' (Spec.map ψ)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑T : Type u) := (CommRingCat.Hom.hom ψ).toAlgebra
hf :
  P (X :=
    pullback (X := Spec (CommRingCat.of (↑T : Type u))) (Y := Spec (CommRingCat.of (↑S : Type u))) (Z :=
      Spec (CommRingCat.of (↑R : Type u))) (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
    (pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
refine :
  Q (R := (↑T : Type u)) (S := (↑T : Type u) ⊗[(↑R : Type u)] (↑S : Type u))
    (algebraMap (↑T : Type u) ((↑T : Type u) ⊗[(↑R : Type u)] (↑S : Type u)))
⊢ Q (CommRingCat.Hom.hom φ)

Tactic:
refine hQQ'.algebraMap_tensorProduct (R := R) (S := T) (T := S) _ (H₁ h) ?_

Premises used: CommRingCat.carrier, RingHom.CodescendsAlong.algebraMap_tensorProduct
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst : P.RespectsIso
hQQ' :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q'
H₁ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P' (Spec.map f) → Q' (CommRingCat.Hom.hom f)
H₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
R S T : CommRingCat
φ : R ⟶ S
ψ : R ⟶ T
h : P' (Spec.map ψ)
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑T : Type u) := (CommRingCat.Hom.hom ψ).toAlgebra
hf :
  P (X :=
    pullback (X := Spec (CommRingCat.of (↑T : Type u))) (Y := Spec (CommRingCat.of (↑S : Type u))) (Z :=
      Spec (CommRingCat.of (↑R : Type u))) (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
    (pullback.fst (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
rwa :
  ∀
    (hf :
      P (X :=
        pullback (X := Spec (CommRingCat.of (↑T : Type u))) (Y := Spec (CommRingCat.of (↑S : Type u))) (Z :=
          Spec (CommRingCat.of (↑R : Type u))) (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
          (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))))
        (Y := Spec (CommRingCat.of (↑T : Type u)))
        (Iso.hom (pullbackSpecIso (↑R : Type u) (↑T : Type u) (↑S : Type u)) ≫
          Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom))),
    Q (R := (↑T : Type u)) (S := (↑T : Type u) ⊗[(↑R : Type u)] (↑S : Type u))
      (algebraMap (↑T : Type u) ((↑T : Type u) ⊗[(↑R : Type u)] (↑S : Type u)))
rwa₁ :
  ∀
    (hf :
      P (X := Spec (CommRingCat.of ((↑T : Type u) ⊗[(↑R : Type u)] (↑S : Type u)))) (Y :=
        Spec (CommRingCat.of (↑T : Type u))) (Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom))),
    Q (R := (↑T : Type u)) (S := (↑T : Type u) ⊗[(↑R : Type u)] (↑S : Type u))
      (algebraMap (↑T : Type u) ((↑T : Type u) ⊗[(↑R : Type u)] (↑S : Type u)))
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀
    (hf :
      Q (R := (↑(CommRingCat.of (↑T : Type u)) : Type u)) (S :=
        (↑(CommRingCat.of ((↑T : Type u) ⊗[(↑R : Type u)] (↑S : Type u))) : Type u))
        (CommRingCat.Hom.hom (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom))),
    Q (R := (↑T : Type u)) (S := (↑T : Type u) ⊗[(↑R : Type u)] (↑S : Type u))
      (algebraMap (↑T : Type u) ((↑T : Type u) ⊗[(↑R : Type u)] (↑S : Type u)))
⊢ Q (R := (↑T : Type u)) (S := (↑T : Type u) ⊗[(↑R : Type u)] (↑S : Type u))
    (algebraMap (↑T : Type u) ((↑T : Type u) ⊗[(↑R : Type u)] (↑S : Type u)))

Tactic:
rwa [← pullbackSpecIso_hom_fst R T S, P.cancel_left_of_respectsIso, H₂] at hf

Premises used: CommRingCat.carrier, AlgebraicGeometry.pullbackSpecIso_hom_fst, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.RespectsIso
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {S X : Scheme.{u}} (f : Spec R ⟶ S) (g : X ⟶ S),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z T : Scheme
inst_3 : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
a : P' ((T.isoSpec.inv ≫ p) ≫ f)
a₁ : P (X := pullback ((T.isoSpec.inv ≫ p) ≫ f) g) (pullback.fst ((T.isoSpec.inv ≫ p) ≫ f) g)
⊢ P g

Tactic:
apply H ((T.isoSpec.inv ≫ p) ≫ f)

Premises used: AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.RespectsIso
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {S X : Scheme.{u}} (f : Spec R ⟶ S) (g : X ⟶ S),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z T : Scheme
inst_3 : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
a : P' (p ≫ f)
⊢ P' ((T.isoSpec.inv ≫ p) ≫ f)

Tactic:
rw [Category.assoc, P'.cancel_left_of_respectsIso]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.RespectsIso
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {S X : Scheme.{u}} (f : Spec R ⟶ S) (g : X ⟶ S),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z T : Scheme
inst_3 : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
⊢ P' (p ≫ f)

Tactic:
P'.comp_mem _ _ hp h

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.RespectsIso
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {S X : Scheme.{u}} (f : Spec R ⟶ S) (g : X ⟶ S),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z T : Scheme
inst_3 : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
⊢ P' (p ≫ f)

Tactic:
exact P'.comp_mem _ _ hp h

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.RespectsIso
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {S X : Scheme.{u}} (f : Spec R ⟶ S) (g : X ⟶ S),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z T : Scheme
inst_3 : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
a :
  P (X := pullback (Y := pullback f g) (T.isoSpec.inv ≫ p) (pullback.fst f g))
    (pullback.fst (T.isoSpec.inv ≫ p) (pullback.fst f g))
⊢ P (X := pullback ((T.isoSpec.inv ≫ p) ≫ f) g) (pullback.fst ((T.isoSpec.inv ≫ p) ≫ f) g)

Tactic:
rw [← pullbackRightPullbackFstIso_inv_fst f g (T.isoSpec.inv ≫ p),
        P.cancel_left_of_respectsIso]

Premises used: AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.RespectsIso
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {S X : Scheme.{u}} (f : Spec R ⟶ S) (g : X ⟶ S),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z T : Scheme
inst_3 : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
⊢ P (X := pullback (Y := pullback f g) (T.isoSpec.inv ≫ p) (pullback.fst f g))
    (pullback.fst (T.isoSpec.inv ≫ p) (pullback.fst f g))

Tactic:
P.pullback_fst _ _ hf

Premises used: CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Descent
Goal:
P P' : MorphismProperty Scheme
inst : P'.RespectsIso
inst_1 : P'.IsStableUnderComposition
inst_2 : P.IsStableUnderBaseChange
H :
  ∀ {R : CommRingCat.{u}} {S X : Scheme.{u}} (f : Spec R ⟶ S) (g : X ⟶ S),
    P' f → P (X := pullback f g) (pullback.fst f g) → P g
X Y Z T : Scheme
inst_3 : IsAffine T
p : T ⟶ X
hp : P' p
f : X ⟶ Z
g : Y ⟶ Z
h : P' f
hf : P (X := pullback f g) (pullback.fst f g)
⊢ P (X := pullback (Y := pullback f g) (T.isoSpec.inv ≫ p) (pullback.fst f g))
    (pullback.fst (T.isoSpec.inv ≫ p) (pullback.fst f g))

Tactic:
exact P.pullback_fst _ _ hf

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
H₂ :
  ∀ {R : CommRingCat.{u}} {X Y : Scheme.{u}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    (P' ⊓ @QuasiCompact) f → P (X := pullback f g) (pullback.fst f g) → P g
⊢ P.DescendsAlong (P' ⊓ @QuasiCompact)

Tactic:
apply IsZariskiLocalAtTarget.descendsAlong

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong
-- 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 : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
hf : (P' ⊓ @QuasiCompact) f
h : P (X := pullback f g) (pullback.fst f g)
H₂ :
  ∀
    (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), P g
wlog :
  ∀ {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
⊢ P g

Tactic:
wlog hX : ∃ T, X = Spec T generalizing X
-- 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 : Scheme
f : X ⟶ Spec R
g : Y ⟶ 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
⊢ CompactSpace.{u} ↥X

Tactic:
simpa [← quasiCompact_iff_compactSpace f] using hf.2

Premises used: And.right, AlgebraicGeometry.quasiCompact_iff_compactSpace
-- 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 : Scheme
f : X ⟶ Spec R
g : Y ⟶ 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₂ : CompactSpace.{u} ↥X → P g
⊢ P g

Tactic:
have _ : CompactSpace X := by simpa [← quasiCompact_iff_compactSpace f] using hf.2
-- 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 : Scheme
f : X ⟶ Spec R
g : Y ⟶ 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
H₂ : ∀ (Y_1 : Scheme.{u}) (p : Y_1 ⟶ X) (hsurj : Surjective p) (hP' : IsLocalIso p) (hY : IsAffine Y_1), P g
⊢ P g

Tactic:
obtain ⟨Y, p, hsurj, hP', hY⟩ := X.exists_hom_isAffine_of_isZariskiLocalAtSource @IsLocalIso

Premises used: AlgebraicGeometry.IsLocalIso, AlgebraicGeometry.Scheme.exists_hom_isAffine_of_isZariskiLocalAtSource