awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : IsIso (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this_1 : IsAffine Y
this :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hfst : IsIso (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (this : IsAffine Y) (hY : ∃ (T : CommRingCat.{u}), Y = Spec T), isomorphisms Scheme g
hY : ¬∃ (T : CommRingCat.{u}), Y = Spec T
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))
⊢ isomorphisms Scheme (Y.isoSpec.inv ≫ g)
have H : IsIso (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.FlatDescent (goal)
Goal:
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : IsIso (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this_1 : IsAffine Y
this :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hfst : IsIso (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (this : IsAffine Y) (hY : ∃ (T : CommRingCat.{u}), Y = Spec T), isomorphisms Scheme g
hY : ¬∃ (T : CommRingCat.{u}), Y = Spec T
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))
⊢ isomorphisms Scheme (X := pullback (Spec.map φ) (Y.isoSpec.inv ≫ g)) (pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g))
have H : isomorphisms Scheme (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, (isomorphisms Scheme).cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : IsIso (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this_1 : IsAffine Y
this :
  ∀ {Y : Scheme.{u}} (g : Y ⟶ Spec R) (hfst : IsIso (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g))
    (this : IsAffine Y) (hY : ∃ (T : CommRingCat.{u}), Y = Spec T), isomorphisms Scheme g
hY : ¬∃ (T : CommRingCat.{u}), Y = Spec T
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))
H :
  isomorphisms Scheme (X := pullback (Spec.map φ) (Y.isoSpec.inv ≫ g))
    (CategoryStruct.comp (Y := pullback (Spec.map φ) g)
      (pullback.map (Spec.map φ) (Y.isoSpec.inv ≫ g) (Spec.map φ) g (𝟙 (Spec S)) Y.isoSpec.inv (𝟙 (Spec R)) ⋯ ⋯)
      (pullback.fst (Spec.map φ) g))
⊢ isomorphisms Scheme (X := pullback (Spec.map φ) (Y.isoSpec.inv ≫ g)) (pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g))
have H₁ : isomorphisms Scheme (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
Tactic: rwa [heq, (isomorphisms Scheme).cancel_left_of_respectsIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
Y : Scheme
g : Y ⟶ Spec R
hfst : IsIso (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this : IsAffine Y
hY : ∃ (T : CommRingCat.{u}), Y = Spec T
⊢ isomorphisms Scheme g
have obtain : ∀ (T : CommRingCat.{u}) (g : Spec T ⟶ Spec R)
  (hfst : IsIso (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)) (this : IsAffine.{u} (Spec T)),
  isomorphisms Scheme g
Tactic: obtain ⟨T, rfl⟩ := hY
Cleared hypotheses: Y, g, hfst, this, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
g : Spec T ⟶ Spec R
hfst : IsIso (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
this : IsAffine.{u} (Spec T)
⊢ isomorphisms Scheme g
have obtain : ∀ (ψ : R ⟶ T) (hfst : IsIso (X := pullback (Spec.map φ) (Spec.map ψ)) (pullback.fst (Spec.map φ) (Spec.map ψ))),
  isomorphisms Scheme (Spec.map ψ)
Tactic: obtain ⟨ψ, rfl⟩ := Spec.map_surjective g
Cleared hypotheses: g, hfst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
this : IsAffine.{u} (Spec T)
ψ : R ⟶ T
hfst : IsIso (X := pullback (Spec.map φ) (Spec.map ψ)) (pullback.fst (Spec.map φ) (Spec.map ψ))
⊢ isomorphisms Scheme (Spec.map ψ)
have refine_1 : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S},
  (@Surjective ⊓ @Flat) (Spec.map f) →
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (RingHom.FaithfullyFlat : (f : R →+* S) → Prop))
      (CommRingCat.Hom.hom f)
Tactic: refine of_pullback_fst_Spec_of_codescendsAlong (P := isomorphisms Scheme.{u})
      (Q' := RingHom.FaithfullyFlat) (Q := fun f ↦ Function.Bijective f) (P' := @Surjective ⊓ @Flat)
      RingHom.FaithfullyFlat.codescendsAlong_bijective ?_ ?_ h hfst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
this : IsAffine.{u} (Spec T)
ψ : R ⟶ T
hfst : IsIso (X := pullback (Spec.map φ) (Spec.map ψ)) (pullback.fst (Spec.map φ) (Spec.map ψ))
refine_1 :
  ∀ {R S : CommRingCat.{u}} {f : R ⟶ S},
    (@Surjective ⊓ @Flat) (Spec.map f) →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (RingHom.FaithfullyFlat : (f : R →+* S) → Prop))
        (CommRingCat.Hom.hom f)
⊢ isomorphisms Scheme (Spec.map ψ)
have refine_2 : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S},
  isomorphisms Scheme (Spec.map f) ↔
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
        Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S))
      (CommRingCat.Hom.hom f)
Tactic: refine of_pullback_fst_Spec_of_codescendsAlong (P := isomorphisms Scheme.{u})
      (Q' := RingHom.FaithfullyFlat) (Q := fun f ↦ Function.Bijective f) (P' := @Surjective ⊓ @Flat)
      RingHom.FaithfullyFlat.codescendsAlong_bijective ?_ ?_ h hfst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
this : IsAffine.{u} (Spec T)
ψ : R ⟶ T
hfst : IsIso (X := pullback (Spec.map φ) (Spec.map ψ)) (pullback.fst (Spec.map φ) (Spec.map ψ))
R_1 S_1 : CommRingCat
f : R_1 ⟶ S_1
hf : (@Surjective ⊓ @Flat) (Spec.map f)
⊢ (CommRingCat.Hom.hom f).FaithfullyFlat
have refine_1 : Flat (Spec.map f) ∧ Surjective (Spec.map f)
Tactic: rwa [← flat_and_surjective_SpecMap_iff, and_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
this : IsAffine.{u} (Spec T)
ψ : R ⟶ T
hfst : IsIso (X := pullback (Spec.map φ) (Spec.map ψ)) (pullback.fst (Spec.map φ) (Spec.map ψ))
R_1 S_1 : CommRingCat
f : R_1 ⟶ S_1
hf : (@Surjective ⊓ @Flat) (Spec.map f)
refine_1 : Flat (Spec.map f) ∧ Surjective (Spec.map f)
⊢ (CommRingCat.Hom.hom f).FaithfullyFlat
have refine_1₁ : Surjective (Spec.map f) ∧ Flat (Spec.map f)
Tactic: rwa [← flat_and_surjective_SpecMap_iff, and_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
h : (@Surjective ⊓ @Flat) (Spec.map φ)
T : CommRingCat
this : IsAffine.{u} (Spec T)
ψ : R ⟶ T
hfst : IsIso (X := pullback (Spec.map φ) (Spec.map ψ)) (pullback.fst (Spec.map φ) (Spec.map ψ))
refine_2 refine_2₁ :
  ∀ {R S : CommRingCat.{u}} {f : R ⟶ S},
    isomorphisms Scheme (Spec.map f) ↔
      Function.Bijective (α := (↑R : Type u)) (β := (↑S : Type u))
        (⇑(CommRingCat.Hom.hom f) : (a : (↑R : Type u)) → (↑S : Type u))
⊢ ∀ {R S : CommRingCat.{u}} {f : R ⟶ S},
    isomorphisms Scheme (Spec.map f) ↔
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦
          Function.Bijective (α := R) (β := S) (⇑f : (a : R) → S))
        (CommRingCat.Hom.hom f)
have refine_2₂ : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, True
Tactic: simp_rw [← isIso_SpecMap_iff, implies_true]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
⊢ IsOpenImmersion.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
have H : ∀ {X Y Z : Scheme.{u_1}} {f : X ⟶ Z} {g : Y ⟶ Z} [inst : HasPullback f g],
  (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f → IsOpenImmersion (X := pullback f g) (pullback.fst f g) → IsOpenImmersion g
Tactic: apply DescendsAlong.mk'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
⊢ IsOpenImmersion g
have this : UniversallyOpen g
Tactic: have : UniversallyOpen g :=
    MorphismProperty.of_pullback_fst_of_descendsAlong
      (P := @UniversallyOpen) (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (f := f)
      hf inferInstance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
x_1 : ↥(↑U : Scheme)
x : ↥Z
y : ↥Y
hy : g y = x
⊢ Eq (α := ↥(↑U : Scheme)) (g' y : ↥(↑U : Scheme)) (Subtype.mk (p := fun (x : ↥Z) ↦ x ∈ U) x ⋯ : ↥U)
have a : Eq (α := ↥Z) (U.ι (g' y : ↥(↑U : Scheme)) : ↥Z) (U.ι (Subtype.mk (p := fun (x : ↥Z) ↦ x ∈ U) x sorry) : ↥Z)
Tactic: apply U.ι.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
⊢ IsOpenImmersion g
have this₁ : Surjective g'
Tactic: have : Surjective g' := ⟨fun ⟨x, ⟨y, hy⟩⟩ ↦
    ⟨y, by apply U.ι.injective; simp [← Scheme.Hom.comp_apply, g', hy]⟩⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
⊢ IsIso (X := pullback f' g') (pullback.fst f' g')
have rw : IsOpenImmersion (X := pullback f' g') (pullback.fst f' g') ∧ Surjective (X := pullback f' g') (pullback.fst f' g')
Tactic: rw [isIso_iff_isOpenImmersion_and_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
⊢ IsOpenImmersion (X := pullback f' g') (pullback.fst f' g') ∧ Surjective (X := pullback f' g') (pullback.fst f' g')
have refine : IsOpenImmersion (X := pullback f' g') (pullback.fst f' g')
Tactic: refine ⟨?_, inferInstance⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
⊢ IsOpenImmersion (X := pullback f' g') (pullback.fst f' g')
have this₁ : IsOpenImmersion (X := pullback f (g' ≫ U.ι)) (pullback.fst f (g' ≫ U.ι))
Tactic: have : IsOpenImmersion (pullback.fst f (g' ≫ U.ι)) := by
      rwa [AlgebraicGeometry.IsOpenImmersion.lift_fac]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this : IsOpenImmersion (X := pullback f (g' ≫ U.ι)) (pullback.fst f (g' ≫ U.ι))
⊢ IsOpenImmersion (X := pullback f' g') (pullback.fst f' g' ≫ pullback.fst f U.ι)
have rw : IsOpenImmersion (X := pullback f' g') (Iso.hom (pullbackLeftPullbackSndIso f U.ι g') ≫ pullback.fst f (g' ≫ U.ι))
Tactic: rw [← pullbackLeftPullbackSndIso_hom_fst]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this : IsOpenImmersion (X := pullback f (g' ≫ U.ι)) (pullback.fst f (g' ≫ U.ι))
⊢ IsOpenImmersion (X := pullback f' g') (pullback.fst f' g')
have this₁ : IsOpenImmersion (X := pullback f' g') (pullback.fst f' g' ≫ pullback.fst f U.ι)
Tactic: have : IsOpenImmersion (pullback.fst f' g' ≫ pullback.fst f U.ι) := by
      rw [← pullbackLeftPullbackSndIso_hom_fst]
      infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this : Surjective g'
⊢ IsOpenImmersion g
have this₁ : IsIso (X := pullback f' g') (pullback.fst f' g')
Tactic: have : IsIso (pullback.fst f' g') := by
    rw [isIso_iff_isOpenImmersion_and_surjective]
    refine ⟨?_, inferInstance⟩
    have : IsOpenImmersion (pullback.fst f (g' ≫ U.ι)) := by
      rwa [AlgebraicGeometry.IsOpenImmersion.lift_fac]
    have : IsOpenImmersion (pullback.fst f' g' ≫ pullback.fst f U.ι) := by
      rw [← pullbackLeftPullbackSndIso_hom_fst]
      infer_instance
    exact .of_comp _ (pullback.fst _ _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this : IsIso (X := pullback f' g') (pullback.fst f' g')
⊢ IsIso g'
have apply : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f'
Tactic: apply MorphismProperty.of_pullback_fst_of_descendsAlong
      (P := isomorphisms Scheme) (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (f := f') ?_ this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (hypothesis)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this : IsIso (X := pullback f' g') (pullback.fst f' g')
⊢ IsOpenImmersion g
have this₁ : IsIso g'
Tactic: have : IsIso g' := by
    apply MorphismProperty.of_pullback_fst_of_descendsAlong
      (P := isomorphisms Scheme) (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (f := f') ?_ this
    exact MorphismProperty.pullback_snd _ _ hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : HasPullback f g
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hg : IsOpenImmersion (X := pullback f g) (pullback.fst f g)
this_1 : UniversallyOpen g
U : Z.Opens := { carrier := Set.range (ι := ↥Y) ⇑g, is_open' := ⋯ }
f' : pullback f U.ι ⟶ (↑U : Scheme) := pullback.snd f U.ι
g' : Y ⟶ (↑U : Scheme) := IsOpenImmersion.lift U.ι g ⋯
this_2 : Surjective g'
this_3 : IsIso (X := pullback f' g') (pullback.fst f' g')
this : IsIso g'
⊢ IsOpenImmersion g
have H : IsOpenImmersion (IsOpenImmersion.lift U.ι g sorry ≫ U.ι)
Tactic: rw [← IsOpenImmersion.lift_fac U.ι g (by simp [U])]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
⊢ P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
have refine_1 : @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat
Tactic: refine HasRingHomProperty.descendsAlong _ _ _ _ ?_ ?_ h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
refine_1 : @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat
⊢ P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
have refine_2 : ∀ {R S : CommRingCat.{u}} {f : R ⟶ S}, (@Surjective ⊓ @Flat) (Spec.map f) → (CommRingCat.Hom.hom f).FaithfullyFlat
Tactic: refine HasRingHomProperty.descendsAlong _ _ _ _ ?_ ?_ h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
⊢ @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat
have refine_1 : @Surjective ⊓ @IsLocalIso ≤ @Surjective ⊓ @Flat
Tactic: rw [inf_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
⊢ @Surjective ⊓ @IsLocalIso ≤ @Surjective ⊓ @Flat
have refine_1 : @IsLocalIso ≤ @Flat
Tactic: gcongr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
R S : CommRingCat
f : R ⟶ S
⊢ (@Surjective ⊓ @Flat) (Spec.map f) → (CommRingCat.Hom.hom f).FaithfullyFlat
have refine_2 : ∀ (hf₁ : Surjective (Spec.map f)) (hf₂ : Flat (Spec.map f)), (CommRingCat.Hom.hom f).FaithfullyFlat
Tactic: ⟨hf₁, hf₂⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
R S : CommRingCat
f : R ⟶ S
hf₁ : Surjective (Spec.map f)
hf₂ : Flat (Spec.map f)
⊢ (CommRingCat.Hom.hom f).FaithfullyFlat
have refine_2 : (CommRingCat.Hom.hom f).Flat ∧ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom f))
Tactic: rw [RingHom.FaithfullyFlat.iff_flat_and_comap_surjective]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
R S : CommRingCat
f : R ⟶ S
hf₁ : Surjective (Spec.map f)
hf₂ : Flat (Spec.map f)
⊢ (CommRingCat.Hom.hom f).Flat ∧ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom f))
have refine_2 : (CommRingCat.Hom.hom f).Flat
Tactic: refine ⟨?_, (Spec.map f).surjective⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
R S : CommRingCat
f : R ⟶ S
hf₁ : Surjective (Spec.map f)
hf₂ : Flat (Spec.map f)
⊢ (CommRingCat.Hom.hom f).Flat
have refine_2 : ∀ (hf₂ : (CommRingCat.Hom.hom f).Flat), (CommRingCat.Hom.hom f).Flat
Tactic: rwa [HasRingHomProperty.Spec_iff (P := @Flat)] at hf₂
Cleared hypotheses: hf₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
P : MorphismProperty Scheme
inst : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst_1 : IsZariskiLocalAtTarget P
⊢ P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @LocallyOfFinitePresentation)
have H : ∀ {R : CommRingCat.{u_1}} {X Y : Scheme.{u_1}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
  (@Surjective ⊓ @Flat ⊓ @LocallyOfFinitePresentation) f → P (X := pullback f g) (pullback.fst f g) → P g
Tactic: apply IsZariskiLocalAtTarget.descendsAlong