awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUT' : IsQuasiSeparated (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
⊢ IsIso (pushoutSection ⋯ hUSX hUST ⋯)
have obtain : ∀ (I : Set (↑T.affineOpens : Type u)) (hI : I.Finite) (e : UT = ⨆ i ∈ I, (↑i : T.Opens)),
  IsIso (pushoutSection sorry hUSX hUST sorry)
Tactic: obtain ⟨I, hI, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hUT
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUT' : IsQuasiSeparated (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set (↑T.affineOpens : Type u)
hI : I.Finite
e : UT = ⨆ i ∈ I, (↑i : T.Opens)
i : (↑I : Type u)
⊢ (↑(↑i : (↑T.affineOpens : Type u)) : T.Opens) ≤ UT
have rw : (↑(↑i : (↑T.affineOpens : Type u)) : T.Opens) ≤ ⨆ i ∈ I, (↑i : T.Opens)
Tactic: rw [e]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (hypothesis)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUT' : IsQuasiSeparated (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set (↑T.affineOpens : Type u)
hI : I.Finite
e : UT = ⨆ i ∈ I, (↑i : T.Opens)
⊢ IsIso (pushoutSection ⋯ hUSX hUST ⋯)
have hIUT : ∀ (i : (↑I : Type u)), (↑(↑i : (↑T.affineOpens : Type u)) : T.Opens) ≤ UT
Tactic: have hIUT (i : I) : i.1 ≤ UT := by rw [e]; intro i; aesop
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (hypothesis)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUT' : IsQuasiSeparated (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set (↑T.affineOpens : Type u)
hI : I.Finite
e : UT = ⨆ i ∈ I, (↑i : T.Opens)
hIUT : ∀ (i : (↑I : Type u)), (↑(↑i : (↑T.affineOpens : Type u)) : T.Opens) ≤ UT
⊢ IsIso (pushoutSection ⋯ hUSX hUST ⋯)
have this : Finite.{u + 1} (↑I : Type u)
Tactic: have := hI.to_subtype
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUT' : IsQuasiSeparated (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set (↑T.affineOpens : Type u)
hI : I.Finite
e : UT = ⨆ i ∈ I, (↑i : T.Opens)
hIUT : ∀ (i : (↑I : Type u)), (↑(↑i : (↑T.affineOpens : Type u)) : T.Opens) ≤ UT
this : Finite.{u + 1} (↑I : Type u)
⊢ ⨆ (i : (↑I : Type u)), (↑(↑i : (↑T.affineOpens : Type u)) : T.Opens) = UT
have rwa : ⨆ (i : (↑T.affineOpens : Type u)),
    ⨆ (h : i ∈ I),
      (↑(↑(Subtype.mk (p := fun (x : (↑T.affineOpens : Type u)) ↦ x ∈ I) i h) : (↑T.affineOpens : Type u)) : T.Opens) =
  UT
Tactic: rwa [iSup_subtype, eq_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
inst : Flat f
hUS : IsAffineOpen US
hUT : IsCompact (↑UT : Set ↥T)
hUT' : IsQuasiSeparated (↑UT : Set ↥T)
hUX : IsCompact (↑UX : Set ↥X)
hUX' : IsQuasiSeparated (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
I : Set (↑T.affineOpens : Type u)
hI : I.Finite
e : UT = ⨆ i ∈ I, (↑i : T.Opens)
hIUT : ∀ (i : (↑I : Type u)), (↑(↑i : (↑T.affineOpens : Type u)) : T.Opens) ≤ UT
this : Finite.{u + 1} (↑I : Type u)
rwa :
  ⨆ (i : (↑T.affineOpens : Type u)),
      ⨆ (h : i ∈ I),
        (↑(↑(Subtype.mk (p := fun (x : (↑T.affineOpens : Type u)) ↦ x ∈ I) i h) : (↑T.affineOpens : Type u)) :
          T.Opens) =
    UT
⊢ ⨆ (i : (↑I : Type u)), (↑(↑i : (↑T.affineOpens : Type u)) : T.Opens) = UT
have rwa₁ : UT =
  ⨆ (i : (↑T.affineOpens : Type u)),
    ⨆ (h : i ∈ I),
      (↑(↑(Subtype.mk (p := fun (x : (↑T.affineOpens : Type u)) ↦ x ∈ I) i h) : (↑T.affineOpens : Type u)) : T.Opens)
Tactic: rwa [iSup_subtype, eq_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
⊢ DescendsAlong (@UniversallyClosed) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
have refine_1 : @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat
Tactic: refine IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
refine_1 : @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat
⊢ DescendsAlong (@UniversallyClosed) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
have refine_2 : ∀ {R S : CommRingCat.{u_1}} {Y : Scheme.{u_1}} (φ : R ⟶ S) (g : Y ⟶ Spec R),
  (@Surjective ⊓ @Flat) (Spec.map φ) →
    UniversallyClosed (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g) → UniversallyClosed g
Tactic: refine IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
⊢ @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:
⊢ ∀ {R S : CommRingCat.{u_1}} {Y : Scheme.{u_1}} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    (@Surjective ⊓ @Flat) (Spec.map φ) →
      UniversallyClosed (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g) → UniversallyClosed g
have refine_2 : ∀ {R : CommRingCat.{u_1}} (S : CommRingCat.{u_1}) (Y : Scheme.{u_1}) (φ : R ⟶ S) (g : Y ⟶ Spec R),
  (@Surjective ⊓ @Flat) (Spec.map φ) →
    ∀ (hfst : UniversallyClosed (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)),
      Surjective (Spec.map φ) →
        Flat (Spec.map φ) →
          ∀ {T : Scheme.{u_1}} (f : T ⟶ Spec R) (x : HasPullback f g) (s : Set ↥(pullback f g)) (hs : IsClosed s),
            IsClosed (X := ↥T) (⇑(pullback.fst f g) '' s)
Tactic: refine fun {R} S Y φ g ⟨_, _⟩ hfst ↦ ⟨universally_mk' _ _ fun {T} f _ s hs ↦ ?_⟩
-- 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 : UniversallyClosed (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
left : Surjective (Spec.map φ)
right : Flat (Spec.map φ)
T : Scheme
f : T ⟶ Spec R
h_1 : HasPullback f g
s : Set ↥(pullback f g)
hs : IsClosed s
p : pullback (X := pullback (Spec.map φ) f) (Y := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) f)
    (pullback.fst (Spec.map φ) g) ⟶
  pullback (Spec.map φ) f :=
  pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
r : pullback (X := pullback (Spec.map φ) f) (Y := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) f)
    (pullback.fst (Spec.map φ) g) ⟶
  pullback f g :=
  pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
    (pullback.snd (Spec.map φ) g) (Spec.map φ) ⋯ ⋯
⊢ IsClosed (X := ↥(pullback (Spec.map φ) f))
    (Set.preimage (β := ↥T) (⇑(pullback.snd (Spec.map φ) f)) (⇑(pullback.fst f g) '' s))
have rw : IsClosed (X := ↥(pullback (Spec.map φ) f))
  (Set.image (α :=
    ↥(pullback (X := pullback (Spec.map φ) f) (Y := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) f)
        (pullback.fst (Spec.map φ) g)))
    (⇑(pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)))
    (⇑(pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
          (pullback.snd (Spec.map φ) g) (Spec.map φ) sorry sorry) ⁻¹'
      s))
Tactic: rw [← Scheme.image_preimage_eq_of_isPullback (isPullback_map_snd_snd ..)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (hypothesis)
Goal:
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : UniversallyClosed (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
left : Surjective (Spec.map φ)
right : Flat (Spec.map φ)
T : Scheme
f : T ⟶ Spec R
h_1 : HasPullback f g
s : Set ↥(pullback f g)
hs : IsClosed s
p : pullback (X := pullback (Spec.map φ) f) (Y := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) f)
    (pullback.fst (Spec.map φ) g) ⟶
  pullback (Spec.map φ) f :=
  pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
r : pullback (X := pullback (Spec.map φ) f) (Y := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) f)
    (pullback.fst (Spec.map φ) g) ⟶
  pullback f g :=
  pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
    (pullback.snd (Spec.map φ) g) (Spec.map φ) ⋯ ⋯
⊢ IsClosed (X := ↥T) (⇑(pullback.fst f g) '' s)
have this : IsClosed (X := ↥(pullback (Spec.map φ) f))
  (Set.preimage (β := ↥T) (⇑(pullback.snd (Spec.map φ) f)) (⇑(pullback.fst f g) '' s))
Tactic: have : IsClosed ((pullback.snd (Spec.map φ) f).base ⁻¹' ((pullback.fst f g).base '' s)) := by
    rw [← Scheme.image_preimage_eq_of_isPullback (isPullback_map_snd_snd ..)]
    exact p.isClosedMap _ (hs.preimage r.continuous)
-- 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 : UniversallyClosed (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
left : Surjective (Spec.map φ)
right : Flat (Spec.map φ)
T : Scheme
f : T ⟶ Spec R
h_1 : HasPullback f g
s : Set ↥(pullback f g)
hs : IsClosed s
p : pullback (X := pullback (Spec.map φ) f) (Y := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) f)
    (pullback.fst (Spec.map φ) g) ⟶
  pullback (Spec.map φ) f :=
  pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
r : pullback (X := pullback (Spec.map φ) f) (Y := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) f)
    (pullback.fst (Spec.map φ) g) ⟶
  pullback f g :=
  pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
    (pullback.snd (Spec.map φ) g) (Spec.map φ) ⋯ ⋯
this :
  IsClosed (X := ↥(pullback (Spec.map φ) f))
    (Set.preimage (β := ↥T) (⇑(pullback.snd (Spec.map φ) f)) (⇑(pullback.fst f g) '' s))
⊢ IsClosed (X := ↥T) (⇑(pullback.fst f g) '' s)
have refine_2 : ∀ (this : IsClosed (X := ↥T) (⇑(pullback.fst f g) '' s)), IsClosed (X := ↥T) (⇑(pullback.fst f g) '' s)
Tactic: rwa [(Flat.isQuotientMap_of_surjective _).isClosed_preimage] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
⊢ DescendsAlong (@UniversallyOpen) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
have refine_1 : @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat
Tactic: refine IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
refine_1 : @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat
⊢ DescendsAlong (@UniversallyOpen) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
have refine_2 : ∀ {R S : CommRingCat.{u_1}} {Y : Scheme.{u_1}} (φ : R ⟶ S) (g : Y ⟶ Spec R),
  (@Surjective ⊓ @Flat) (Spec.map φ) →
    UniversallyOpen (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g) → UniversallyOpen g
Tactic: refine IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact _ _ ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
⊢ ∀ {R S : CommRingCat.{u_1}} {Y : Scheme.{u_1}} (φ : R ⟶ S) (g : Y ⟶ Spec R),
    (@Surjective ⊓ @Flat) (Spec.map φ) →
      UniversallyOpen (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g) → UniversallyOpen g
have refine_2 : ∀ {R : CommRingCat.{u_1}} (S : CommRingCat.{u_1}) (Y : Scheme.{u_1}) (φ : R ⟶ S) (g : Y ⟶ Spec R),
  (@Surjective ⊓ @Flat) (Spec.map φ) →
    ∀ (hfst : UniversallyOpen (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)),
      Surjective (Spec.map φ) →
        Flat (Spec.map φ) →
          ∀ {T : Scheme.{u_1}} (f : T ⟶ Spec R) (x : HasPullback f g) (s : Set ↥(pullback f g)) (hs : IsOpen s),
            IsOpen (X := ↥T) (⇑(pullback.fst f g) '' s)
Tactic: refine fun {R} S Y φ g ⟨_, _⟩ hfst ↦ ⟨universally_mk' _ _ fun {T} f _ s hs ↦ ?_⟩
-- 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 : UniversallyOpen (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
left : Surjective (Spec.map φ)
right : Flat (Spec.map φ)
T : Scheme
f : T ⟶ Spec R
h_1 : HasPullback f g
s : Set ↥(pullback f g)
hs : IsOpen s
p : pullback (X := pullback (Spec.map φ) f) (Y := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) f)
    (pullback.fst (Spec.map φ) g) ⟶
  pullback (Spec.map φ) f :=
  pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
r : pullback (X := pullback (Spec.map φ) f) (Y := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) f)
    (pullback.fst (Spec.map φ) g) ⟶
  pullback f g :=
  pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
    (pullback.snd (Spec.map φ) g) (Spec.map φ) ⋯ ⋯
⊢ IsOpen (X := ↥(pullback (Spec.map φ) f))
    (Set.preimage (β := ↥T) (⇑(pullback.snd (Spec.map φ) f)) (⇑(pullback.fst f g) '' s))
have rw : IsOpen (X := ↥(pullback (Spec.map φ) f))
  (Set.image (α :=
    ↥(pullback (X := pullback (Spec.map φ) f) (Y := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) f)
        (pullback.fst (Spec.map φ) g)))
    (⇑(pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)))
    (⇑(pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
          (pullback.snd (Spec.map φ) g) (Spec.map φ) sorry sorry) ⁻¹'
      s))
Tactic: rw [← Scheme.image_preimage_eq_of_isPullback (isPullback_map_snd_snd ..)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (hypothesis)
Goal:
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : (@Surjective ⊓ @Flat) (Spec.map φ)
hfst : UniversallyOpen (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
left : Surjective (Spec.map φ)
right : Flat (Spec.map φ)
T : Scheme
f : T ⟶ Spec R
h_1 : HasPullback f g
s : Set ↥(pullback f g)
hs : IsOpen s
p : pullback (X := pullback (Spec.map φ) f) (Y := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) f)
    (pullback.fst (Spec.map φ) g) ⟶
  pullback (Spec.map φ) f :=
  pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
r : pullback (X := pullback (Spec.map φ) f) (Y := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) f)
    (pullback.fst (Spec.map φ) g) ⟶
  pullback f g :=
  pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
    (pullback.snd (Spec.map φ) g) (Spec.map φ) ⋯ ⋯
⊢ IsOpen (X := ↥T) (⇑(pullback.fst f g) '' s)
have this : IsOpen (X := ↥(pullback (Spec.map φ) f))
  (Set.preimage (β := ↥T) (⇑(pullback.snd (Spec.map φ) f)) (⇑(pullback.fst f g) '' s))
Tactic: have : IsOpen ((pullback.snd (Spec.map φ) f).base ⁻¹' ((pullback.fst f g).base '' s)) := by
    rw [← Scheme.image_preimage_eq_of_isPullback (isPullback_map_snd_snd ..)]
    exact p.isOpenMap _ (hs.preimage r.continuous)
-- 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 : UniversallyOpen (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
left : Surjective (Spec.map φ)
right : Flat (Spec.map φ)
T : Scheme
f : T ⟶ Spec R
h_1 : HasPullback f g
s : Set ↥(pullback f g)
hs : IsOpen s
p : pullback (X := pullback (Spec.map φ) f) (Y := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) f)
    (pullback.fst (Spec.map φ) g) ⟶
  pullback (Spec.map φ) f :=
  pullback.fst (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g)
r : pullback (X := pullback (Spec.map φ) f) (Y := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) f)
    (pullback.fst (Spec.map φ) g) ⟶
  pullback f g :=
  pullback.map (pullback.fst (Spec.map φ) f) (pullback.fst (Spec.map φ) g) f g (pullback.snd (Spec.map φ) f)
    (pullback.snd (Spec.map φ) g) (Spec.map φ) ⋯ ⋯
this :
  IsOpen (X := ↥(pullback (Spec.map φ) f))
    (Set.preimage (β := ↥T) (⇑(pullback.snd (Spec.map φ) f)) (⇑(pullback.fst f g) '' s))
⊢ IsOpen (X := ↥T) (⇑(pullback.fst f g) '' s)
have refine_2 : ∀ (this : IsOpen (X := ↥T) (⇑(pullback.fst f g) '' s)), IsOpen (X := ↥T) (⇑(pullback.fst f g) '' s)
Tactic: rwa [(Flat.isQuotientMap_of_surjective _).isOpen_preimage] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
⊢ DescendsAlong (@UniversallyInjective) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
have rw : (diagonal @Surjective).DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
Tactic: rw [universallyInjective_eq_diagonal]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
⊢ DescendsAlong (isomorphisms Scheme) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
have H₁ : @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat
Tactic: apply IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
H₁ : @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat
⊢ DescendsAlong (isomorphisms Scheme) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
have H : ∀ {R S : CommRingCat.{u}} {Y : Scheme.{u}} (φ : R ⟶ S) (g : Y ⟶ Spec R),
  (@Surjective ⊓ @Flat) (Spec.map φ) →
    isomorphisms Scheme (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g) → isomorphisms Scheme g
Tactic: apply IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (goal)
Goal:
⊢ @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat
have H₁ : @Surjective ⊓ @IsLocalIso ≤ @Surjective ⊓ @Flat
Tactic: rw [inf_comm]
-- 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 φ)
⊢ isomorphisms Scheme (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g) → isomorphisms Scheme g
have H : ∀ (hfst : IsIso (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)), isomorphisms Scheme g
Tactic: (hfst : IsIso _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (hypothesis)
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)
⊢ isomorphisms Scheme g
have this : IsAffine Y
Tactic: have : IsAffine Y :=
    have : UniversallyInjective g :=
      of_pullback_fst_of_descendsAlong (P := @UniversallyInjective) (f := Spec.map φ)
        (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) ⟨h, inferInstance⟩ inferInstance
    have : Surjective g :=
      of_pullback_fst_of_descendsAlong (P := @Surjective) (f := Spec.map φ)
        (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) ⟨h, inferInstance⟩ inferInstance
    have hopen' : UniversallyOpen g :=
      of_pullback_fst_of_descendsAlong (P := @UniversallyOpen) (f := Spec.map φ)
        (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) ⟨h, inferInstance⟩ inferInstance
    have : IsHomeomorph g.base := ⟨g.continuous, g.isOpenMap, g.injective, g.surjective⟩
    have : IsAffineHom g :=
      isAffineHom_of_isInducing g this.isInducing this.isClosedEmbedding.isClosed_range
    isAffine_of_isAffineHom g
-- 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 : IsAffine Y
⊢ isomorphisms Scheme g
have H : ∀
  (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), isomorphisms Scheme g
Tactic: wlog hY : ∃ T, Y = Spec T generalizing Y
-- 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 : IsAffine Y
H :
  ∀
    (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), isomorphisms Scheme g
⊢ isomorphisms Scheme g
have wlog : ∀ {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
Tactic: wlog hY : ∃ T, Y = Spec T generalizing Y
Cleared hypotheses: Y, g, hfst, this
-- 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
⊢ isomorphisms Scheme g
have H : isomorphisms Scheme (Y.isoSpec.inv ≫ g)
Tactic: rw [← (isomorphisms Scheme).cancel_left_of_respectsIso Y.isoSpec.inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatDescent (hypothesis)
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
⊢ isomorphisms Scheme (Y.isoSpec.inv ≫ g)
have 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))
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