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_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)
⊢ P g
have 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
Tactic: wlog hY : ∃ S, Y = Spec S generalizing Y
-- 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'
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
⊢ P g
have 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
Tactic: wlog hY : ∃ S, Y = Spec S generalizing Y
Cleared hypotheses: Y, g, 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_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
⊢ P g
have inr : ∀ (i : Y.affineCover.I₀), P (Y.affineCover.f i ≫ g)
Tactic: rw [IsZariskiLocalAtSource.iff_of_openCover (P := P) Y.affineCover]
-- 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'
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₀
⊢ P (Y.affineCover.f i ≫ g)
have 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))
          sorry sorry)
        (pullback.fst (Spec.map φ) 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
-- 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'
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
⊢ P g
have 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
Tactic: obtain ⟨S, rfl⟩ := hY
Cleared hypotheses: Y, g, hf, hY
-- 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'
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)
⊢ P g
have apply : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
Tactic: apply of_pullback_fst_Spec_of_codescendsAlong _ _ hQQ' H₂ _ h 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_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'
⊢ 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₁
-- 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)
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
have convert! : IsAffineHom g
Tactic: convert! isAffine_of_isAffineHom g
-- 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)
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)
⊢ P g
have have : ∀ (this : IsAffine Y), 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
-- 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)
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
⊢ P g
have 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
Tactic: wlog hY : ∃ S, Y = Spec S generalizing Y
-- 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)
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
⊢ P g
have 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
Tactic: wlog hY : ∃ S, Y = Spec S generalizing Y
Cleared hypotheses: Y, g, hf, this
-- 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)
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
⊢ P g
have inr : P (Y.isoSpec.inv ≫ g)
Tactic: rw [← P.cancel_left_of_respectsIso Y.isoSpec.inv]
-- 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)
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
⊢ P (Y.isoSpec.inv ≫ g)
have 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)) sorry sorry)
        (pullback.fst (Spec.map φ) 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
-- 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)
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)
have inr : P (X := pullback (Spec.map φ) (Y.isoSpec.inv ≫ g)) (pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g))
Tactic: refine this _ ?_ inferInstance ⟨_, rfl⟩
-- 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)
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 (X := pullback (Spec.map φ) (Y.isoSpec.inv ≫ g)) (pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g))
have 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)) sorry sorry)
    (pullback.fst (Spec.map φ) g))
Tactic: rwa [heq, P.cancel_left_of_respectsIso]
-- 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)
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
⊢ P g
have 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
Tactic: obtain ⟨Y, rfl⟩ := hY
Cleared hypotheses: Y, g, hf, this, hY
-- 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)
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)
⊢ P g
have apply : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, P (Spec.map f) ↔ Q (CommRingCat.Hom.hom f)
Tactic: apply of_pullback_fst_Spec_of_codescendsAlong _ _ hQQ' H₂ _ h hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ @Etale = affineLocally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale
have h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
  Etale f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale) f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
⊢ Etale f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale) f
have h : (∀ {U : Y.Opens},
    IsAffineOpen U →
      ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Etale) ↔
  affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale) f
Tactic: rw [etale_iff, affineLocally_iff_forall_isAffineOpen]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Etale (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
h :
  (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Etale) ↔
    affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale) f
⊢ Etale f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Etale) f
have h₁ : (∀ {U : Y.Opens},
    IsAffineOpen U →
      ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Etale) ↔
  ∀ {U : Y.Opens},
    IsAffineOpen U →
      ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Etale
Tactic: rw [etale_iff, affineLocally_iff_forall_isAffineOpen]