awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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 φ)
have 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)))
Tactic: refine hQQ'.algebraMap_tensorProduct (R := R) (S := T) (T := S) _ (H₁ h) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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 (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)))
have 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)))
Tactic: rwa [← pullbackSpecIso_hom_fst R T S, P.cancel_left_of_respectsIso, H₂] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rwa [← pullbackSpecIso_hom_fst R T S, P.cancel_left_of_respectsIso, H₂] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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)))
⊢ 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)))
have 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)))
Tactic: rwa [← pullbackSpecIso_hom_fst R T S, P.cancel_left_of_respectsIso, H₂] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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 g
have a : P' ((T.isoSpec.inv ≫ p) ≫ f)
Tactic: apply H ((T.isoSpec.inv ≫ p) ≫ f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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)
⊢ P g
have a₁ : P (X := pullback ((T.isoSpec.inv ≫ p) ≫ f) g) (pullback.fst ((T.isoSpec.inv ≫ p) ≫ f) g)
Tactic: apply H ((T.isoSpec.inv ≫ p) ≫ f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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' ((T.isoSpec.inv ≫ p) ≫ f)
have a : P' (p ≫ f)
Tactic: rw [Category.assoc, P'.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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 ((T.isoSpec.inv ≫ p) ≫ f) g) (pullback.fst ((T.isoSpec.inv ≫ p) ≫ f) g)
have 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))
Tactic: rw [← pullbackRightPullbackFstIso_inv_fst f g (T.isoSpec.inv ≫ p),
        P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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
⊢ P.DescendsAlong (P' ⊓ @QuasiCompact)
have 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
Tactic: apply IsZariskiLocalAtTarget.descendsAlong
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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)
⊢ P g
have 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
Tactic: wlog hX : ∃ T, X = Spec T generalizing X
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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
⊢ P g
have 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
Tactic: wlog hX : ∃ T, X = Spec T generalizing X
Cleared hypotheses: X, f, hf, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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
⊢ P g
have H₂ : CompactSpace.{u} ↥X → P g
Tactic: have _ : CompactSpace X := by simpa [← quasiCompact_iff_compactSpace f] using hf.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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
⊢ P g
have H₂ : ∀ (Y_1 : Scheme.{u}) (p : Y_1 ⟶ X) (hsurj : Surjective p) (hP' : IsLocalIso p) (hY : IsAffine Y_1), P g
Tactic: obtain ⟨Y, p, hsurj, hP', hY⟩ := X.exists_hom_isAffine_of_isZariskiLocalAtSource @IsLocalIso
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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
have H₂ : (P' ⊓ @QuasiCompact) ((Y.isoSpec.inv ≫ p) ≫ f)
Tactic: refine this (f := (Y.isoSpec.inv ≫ p) ≫ f) ?_ ?_ ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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)
⊢ P g
have H₃ : P (X := pullback ((Y.isoSpec.inv ≫ p) ≫ f) g) (pullback.fst ((Y.isoSpec.inv ≫ p) ≫ f) g)
Tactic: refine this (f := (Y.isoSpec.inv ≫ p) ≫ f) ?_ ?_ ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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) ((Y.isoSpec.inv ≫ p) ≫ f)
have H₂ : (P' ⊓ @QuasiCompact) (p ≫ f)
Tactic: rw [Category.assoc, (P' ⊓ @QuasiCompact).cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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.isoSpec.inv ≫ p) ≫ f) g) (pullback.fst ((Y.isoSpec.inv ≫ p) ≫ f) g)
have 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))
Tactic: rw [← pullbackRightPullbackFstIso_inv_fst f g _, P.cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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
⊢ P g
have 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
Tactic: obtain ⟨T, rfl⟩ := hX
Cleared hypotheses: X, f, hf, h, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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)
⊢ P g
have obtain : ∀ (φ : R ⟶ T) (hf : (P' ⊓ @QuasiCompact) (Spec.map φ))
  (h : P (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)), P g
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, hf, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Descent (goal)
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'
⊢ P.DescendsAlong (P' ⊓ @QuasiCompact)
have 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
Tactic: apply IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact _ _ H₁