awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
hUX : IsCompact (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
this : Mono (pushoutSection ⋯ hUSX hUST ⋯)
⊢ Mono (pushoutSection ⋯ hUSX hUST ⋯)

Tactic:
this
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
hUX : IsCompact (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
this : Mono (pushoutSection ⋯ hUSX hUST ⋯)
h :
  Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
      pushoutSection H hUST hUSX hUY =
    pushoutSection ⋯ hUSX hUST ⋯
⊢ Mono (X := pushout (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX))
    (Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
      pushoutSection H hUST hUSX hUY)

Tactic:
convert! this
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
hUX : IsCompact (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
suffices : Mono (pushoutSection ⋯ hUSX hUST ⋯)
⊢ Mono (pushoutSection H hUST hUSX hUY)

Tactic:
suffices Mono (pushoutSection H.flip hUSX hUST (hUY.trans (inf_comm _ _))) by
    rw [← mono_comp_iff_of_isIso (pushoutSymmetry _ _).hom]; convert! this; cat_disch
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
hUX : IsCompact (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
⊢ Mono (pushoutSection ⋯ hUSX hUST ⋯)

Tactic:
mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat _ _ _ _ hUS hUX hUT hiX

Premises used: AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
hUX : IsCompact (↑UX : Set ↥X)
hiX : (CommRingCat.Hom.hom (Scheme.Hom.appLE iX US UX hUSX)).Flat
⊢ Mono (pushoutSection ⋯ hUSX hUST ⋯)

Tactic:
exact mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat _ _ _ _ hUS hUX hUT hiX

Premises used: AlgebraicGeometry.mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
rw :
  IsIso (X := pushout (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX))
    (Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
      pushoutSection H hUST hUSX hUY)
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
rw [← isIso_comp_left_iff (pushoutSymmetry _ _).hom]

Premises used: CategoryTheory.isIso_comp_left_iff, CategoryTheory.Limits.pushoutSymmetry, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ IsIso (pushoutSection ⋯ hUSX hUST ⋯)

Tactic:
this
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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
this : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
h :
  Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
      pushoutSection H hUST hUSX hUY =
    pushoutSection ⋯ hUSX hUST ⋯
⊢ IsIso (X := pushout (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX))
    (Iso.hom (pushoutSymmetry (Scheme.Hom.appLE f US UT hUST) (Scheme.Hom.appLE iX US UX hUSX)) ≫
      pushoutSection H hUST hUSX hUY)

Tactic:
convert! this
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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
suffices : IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
suffices IsIso (pushoutSection H.flip hUSX hUST (hUY.trans (inf_comm _ _))) by
    rw [← isIso_comp_left_iff (pushoutSymmetry _ _).hom]; convert! this; cat_disch
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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
obtain :
  ∀ (I : Set (↑T.affineOpens : Type u)) (hI : I.Finite) (e : UT = ⨆ i ∈ I, (↑i : T.Opens)),
    IsIso (pushoutSection ⋯ hUSX hUST ⋯)
⊢ IsIso (pushoutSection ⋯ hUSX hUST ⋯)

Tactic:
obtain ⟨I, hI, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hUT

Premises used: Iff.mp, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
rw : (↑(↑i : (↑T.affineOpens : Type u)) : T.Opens) ≤ ⨆ i ∈ I, (↑i : T.Opens)
⊢ (↑(↑i : (↑T.affineOpens : Type u)) : T.Opens) ≤ UT

Tactic:
rw [e]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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_1 : (↑I : Type u)
i : ↥T
⊢ i ∈ (↑(↑i_1 : (↑T.affineOpens : Type u)) : T.Opens) → Membership.mem (γ := Opens ↥T) (⨆ i ∈ I, (↑i : T.Opens)) i

Tactic:
aesop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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

Tactic:
have hIUT (i : I) : i.1 ≤ UT := by rw [e]; intro i; aesop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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
⊢ Finite.{u + 1} (↑I : Type u)

Tactic:
have := hI.to_subtype
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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
rwa₁ rwa₂ rwa₃ 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)
⊢ ⨆ (i : (↑I : Type u)), (↑(↑i : (↑T.affineOpens : Type u)) : T.Opens) = UT

Tactic:
rwa [iSup_subtype, eq_comm]

Premises used: iSup_subtype, eq_comm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)
⊢ IsIso (pushoutSection ⋯ hUSX hUST ⋯)

Tactic:
exact isIso_pushoutSection_of_iSup_eq _ _ _ _ (fun i : I ↦ i) (by rwa [iSup_subtype, eq_comm])
    (fun i ↦ isIso_pushoutSection_of_isQuasiSeparated_of_flat_left _ _ _ _ hUS i.1.2 hUX hUX')
    (fun i j ↦ mono_pushoutSection_of_isCompact_of_flat_left_of_ringHomFlat _ _ _ _ hUS hUX
    (hUT' _ _ (hIUT _) i.1.1.2 i.1.2.isCompact (hIUT _) j.1.1.2 j.1.2.isCompact) hiX) hiX
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
⊢ @Surjective ⊓ (@Surjective ⊓ @Flat ⊓ @QuasiCompact) = @Surjective ⊓ @Flat ⊓ @QuasiCompact

Tactic:
grind
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
⊢ DescendsAlong (@UniversallyClosed) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact _ _ ?_ ?_

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
refine_1 : @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat
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
⊢ DescendsAlong (@UniversallyClosed) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
refine IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact _ _ ?_ ?_

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
refine_1 : @Surjective ⊓ @IsLocalIso ≤ @Surjective ⊓ @Flat
⊢ @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat

Tactic:
rw [inf_comm]

Premises used: inf_comm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
⊢ @Surjective ⊓ @IsLocalIso ≤ @Surjective ⊓ @Flat

Tactic:
inf_le_inf le_rfl (IsLocalIso.le_of_isZariskiLocalAtSource _)

Premises used: le_rfl, inf_le_inf, AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
⊢ @Surjective ⊓ @IsLocalIso ≤ @Surjective ⊓ @Flat

Tactic:
exact inf_le_inf le_rfl (IsLocalIso.le_of_isZariskiLocalAtSource _)

Premises used: le_rfl, inf_le_inf, AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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

Tactic:
fun {R} S Y φ g ⟨_, _⟩ hfst ↦ ⟨universally_mk' _ _ fun {T} f _ s hs ↦ ?_⟩

Premises used: CategoryTheory.MorphismProperty.universally_mk', IsClosedMap, AlgebraicGeometry.topologically, AlgebraicGeometry.UniversallyClosed, _private.0.AlgebraicGeometry.descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact.match_1, AlgebraicGeometry.UniversallyClosed.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
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)
⊢ ∀ {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 fun {R} S Y φ g ⟨_, _⟩ hfst ↦ ⟨universally_mk' _ _ fun {T} f _ s hs ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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 φ) ⋯ ⋯
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 φ) ⋯ ⋯) ⁻¹'
        s))
⊢ IsClosed (X := ↥(pullback (Spec.map φ) f))
    (Set.preimage (β := ↥T) (⇑(pullback.snd (Spec.map φ) f)) (⇑(pullback.fst f g) '' s))

Tactic:
rw [← Scheme.image_preimage_eq_of_isPullback (isPullback_map_snd_snd ..)]

Premises used: CategoryTheory.Limits.isPullback_map_snd_snd, AlgebraicGeometry.Scheme.image_preimage_eq_of_isPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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.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 φ) ⋯ ⋯) ⁻¹'
        s))

Tactic:
p.isClosedMap _ (hs.preimage r.continuous)

Premises used: AlgebraicGeometry.Scheme.Hom.isClosedMap, AlgebraicGeometry.Scheme.Hom.continuous, IsClosed.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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.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 φ) ⋯ ⋯) ⁻¹'
        s))

Tactic:
exact p.isClosedMap _ (hs.preimage r.continuous)

Premises used: AlgebraicGeometry.Scheme.Hom.isClosedMap, AlgebraicGeometry.Scheme.Hom.continuous, IsClosed.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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))

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)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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))
refine_2 refine_2₁ refine_2₂ refine_2₃ :
  ∀ (this : IsClosed (X := ↥T) (⇑(pullback.fst f g) '' s)), 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

Premises used: Topology.IsCoinducing.isClosed_preimage, Topology.IsQuotientMap.isCoinducing, AlgebraicGeometry.Flat.isQuotientMap_of_surjective