awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
⊢ DescendsAlong (@UniversallyOpen) (@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 φ) →
      UniversallyOpen (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g) → UniversallyOpen g
⊢ DescendsAlong (@UniversallyOpen) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

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

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact
-- 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 φ) →
      UniversallyOpen (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g) → UniversallyOpen g

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

Premises used: CategoryTheory.MorphismProperty.universally_mk', AlgebraicGeometry.UniversallyOpen, IsOpenMap, AlgebraicGeometry.UniversallyOpen.mk, AlgebraicGeometry.topologically, _private.0.AlgebraicGeometry.descendsAlong_universallyClosed_surjective_inf_flat_inf_quasicompact.match_1
-- 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 : 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)
⊢ ∀ {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 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 : 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 φ) ⋯ ⋯
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 φ) ⋯ ⋯) ⁻¹'
        s))
⊢ IsOpen (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 : 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.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.isOpenMap _ (hs.preimage r.continuous)

Premises used: AlgebraicGeometry.Scheme.Hom.isOpenMap, AlgebraicGeometry.Scheme.Hom.continuous, IsOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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.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.isOpenMap _ (hs.preimage r.continuous)

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

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

Premises used: Topology.IsCoinducing.isOpen_preimage, Topology.IsQuotientMap.isCoinducing, AlgebraicGeometry.Flat.isQuotientMap_of_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
rw : (diagonal @Surjective).DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
⊢ DescendsAlong (@UniversallyInjective) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
rw [universallyInjective_eq_diagonal]

Premises used: AlgebraicGeometry.universallyInjective_eq_diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
⊢ (diagonal @Surjective).DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
H₁ : @IsLocalIso ⊓ @Surjective ≤ @Surjective ⊓ @Flat
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
⊢ DescendsAlong (isomorphisms Scheme) (@Surjective ⊓ @Flat ⊓ @QuasiCompact)

Tactic:
apply IsZariskiLocalAtTarget.descendsAlong_inf_quasiCompact

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

Tactic:
rw [inf_comm]

Premises used: inf_comm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
R S : CommRingCat
Y : Scheme
φ : R ⟶ S
g : Y ⟶ Spec R
h : (@Surjective ⊓ @Flat) (Spec.map φ)
H : ∀ (hfst : IsIso (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)), isomorphisms Scheme g
⊢ isomorphisms Scheme (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g) → isomorphisms Scheme g

Tactic:
(hfst : IsIso _)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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)
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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
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
⊢ isomorphisms Scheme g

Tactic:
wlog hY : ∃ T, Y = Spec T generalizing Y
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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
H : isomorphisms Scheme (Y.isoSpec.inv ≫ g)
⊢ isomorphisms Scheme g

Tactic:
rw [← (isomorphisms Scheme).cancel_left_of_respectsIso Y.isoSpec.inv]

Premises used: AlgebraicGeometry.Scheme, AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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
⊢ Spec.map φ ≫ 𝟙 (Spec R) = 𝟙 (Spec S) ≫ Spec.map φ

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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
⊢ (Y.isoSpec.inv ≫ g) ≫ 𝟙 (Spec R) = Y.isoSpec.inv ≫ g

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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
⊢ 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))

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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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)

Tactic:
this _ ?_ inferInstance ⟨_, rfl⟩

Premises used: inferInstance, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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 : IsIso (X := pullback (Spec.map φ) (Y.isoSpec.inv ≫ g)) (pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g))
⊢ isomorphisms Scheme (Y.isoSpec.inv ≫ g)

Tactic:
refine this _ ?_ inferInstance ⟨_, rfl⟩

Premises used: inferInstance, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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))
H₁ H₂ H₃ H₄ : isomorphisms Scheme (X := pullback (Spec.map φ) g) (pullback.fst (Spec.map φ) g)
⊢ isomorphisms Scheme (X := pullback (Spec.map φ) (Y.isoSpec.inv ≫ g)) (pullback.fst (Spec.map φ) (Y.isoSpec.inv ≫ g))

Tactic:
rwa [heq, (isomorphisms Scheme).cancel_left_of_respectsIso]

Premises used: AlgebraicGeometry.Scheme, CategoryTheory.MorphismProperty.isomorphisms, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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
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
⊢ isomorphisms Scheme g

Tactic:
obtain ⟨T, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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)
obtain :
  ∀ (ψ : R ⟶ T) (hfst : IsIso (X := pullback (Spec.map φ) (Spec.map ψ)) (pullback.fst (Spec.map φ) (Spec.map ψ))),
    isomorphisms Scheme (Spec.map ψ)
⊢ isomorphisms Scheme g

Tactic:
obtain ⟨ψ, rfl⟩ := Spec.map_surjective g

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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 ψ)

Tactic:
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

Premises used: AlgebraicGeometry.Flat, AlgebraicGeometry.Scheme, CategoryTheory.MorphismProperty.isomorphisms, AlgebraicGeometry.Surjective, AlgebraicGeometry.of_pullback_fst_Spec_of_codescendsAlong, Min.min, RingHom.FaithfullyFlat.codescendsAlong_bijective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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)
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)
⊢ isomorphisms Scheme (Spec.map ψ)

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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
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 : CommRingCat
refine_1 :
  ∀ {S : CommRingCat.{u}} {f : R_1 ⟶ 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)
⊢ ∀ {S : CommRingCat.{u}} {f : R_1 ⟶ 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:
_