awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥(Spec R))
    (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)) (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsOpen s
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
inr :
  IsOpen (X := ↥(Spec Γ(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i, ⊤)))
    (⇑(Iso.inv (Scheme.isoSpec (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)) ≫ p ≫ f) ⁻¹' s)
⊢ IsOpen s

Tactic:
refine this (f := (∐ (fun i : 𝒰.I₀ ↦ 𝒰.X i)).isoSpec.inv ≫ p ≫ f) _ _ ?_ ⟨_, rfl⟩

Premises used: AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.PreZeroHypercover.X, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.sigmaObj, CategoryTheory.Iso.inv, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥(Spec R))
    (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)) (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsOpen s
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
inr :
  IsOpen (X := ↥(Spec Γ(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i, ⊤)))
    (Set.preimage (β := ↥X) (⇑(Iso.inv (Scheme.isoSpec (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)) ≫ p)) (⇑f ⁻¹' s))
⊢ IsOpen (X := ↥(Spec Γ(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i, ⊤)))
    (⇑(Iso.inv (Scheme.isoSpec (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)) ≫ p ≫ f) ⁻¹' s)

Tactic:
rw [← Category.assoc, Scheme.Hom.comp_base, TopCat.coe_comp, Set.preimage_comp]

Premises used: CategoryTheory.Category.assoc, Set.preimage_comp, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥(Spec R))
    (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)) (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsOpen s
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
⊢ IsOpen (X := ↥(Spec Γ(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i, ⊤)))
    (Set.preimage (β := ↥X) (⇑(Iso.inv (Scheme.isoSpec (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)) ≫ p)) (⇑f ⁻¹' s))

Tactic:
hs.preimage (_ ≫ p).continuous

Premises used: CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.Hom.continuous, IsOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥(Spec R))
    (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)) (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsOpen s
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
p : (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i) ⟶ X := Sigma.desc fun (i : 𝒰.I₀) ↦ 𝒰.f i
⊢ IsOpen (X := ↥(Spec Γ(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i, ⊤)))
    (Set.preimage (β := ↥X) (⇑(Iso.inv (Scheme.isoSpec (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)) ≫ p)) (⇑f ⁻¹' s))

Tactic:
exact hs.preimage (_ ≫ p).continuous

Premises used: CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.Hom.continuous, IsOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
s : Set ↥(Spec R)
hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain :
  ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f]
    (hs : IsOpen (X := ↥(Spec S)) (⇑f ⁻¹' s)), IsOpen s
⊢ IsOpen s

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
f : Spec S ⟶ Spec R
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
hs : IsOpen (X := ↥(Spec S)) (⇑f ⁻¹' s)
obtain :
  ∀ (φ : R ⟶ S) [Flat (Spec.map φ)] [QuasiCompact (Spec.map φ)] [Surjective (Spec.map φ)]
    (hs : IsOpen (X := ↥(Spec S)) (⇑(Spec.map φ) ⁻¹' s)), IsOpen s
⊢ IsOpen s

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : QuasiCompact (Spec.map φ)
inst_2 : Surjective (Spec.map φ)
hs : IsOpen (X := ↥(Spec S)) (⇑(Spec.map φ) ⁻¹' s)
⊢ IsOpen s

Tactic:
((PrimeSpectrum.isQuotientMap_of_generalizingMap ?_ ?_).isOpen_preimage).mp hs

Premises used: PrimeSpectrum.isQuotientMap_of_generalizingMap, Topology.IsCoinducing.isOpen_preimage, Topology.IsQuotientMap.isCoinducing, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : QuasiCompact (Spec.map φ)
inst_2 : Surjective (Spec.map φ)
hs : IsOpen (X := ↥(Spec S)) (⇑(Spec.map φ) ⁻¹' s)
refine_1 : Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))
refine_2 : GeneralizingMap (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))
⊢ IsOpen s

Tactic:
refine ((PrimeSpectrum.isQuotientMap_of_generalizingMap ?_ ?_).isOpen_preimage).mp hs

Premises used: PrimeSpectrum.isQuotientMap_of_generalizingMap, Topology.IsCoinducing.isOpen_preimage, Topology.IsQuotientMap.isCoinducing, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : QuasiCompact (Spec.map φ)
inst_2 : Surjective (Spec.map φ)
hs : IsOpen (X := ↥(Spec S)) (⇑(Spec.map φ) ⁻¹' s)
⊢ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))

Tactic:
(surjective_iff (Spec.map φ)).mp inferInstance

Premises used: AlgebraicGeometry.Spec.map, inferInstance, AlgebraicGeometry.surjective_iff, Iff.mp, PrimeSpectrum.comap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : QuasiCompact (Spec.map φ)
inst_2 : Surjective (Spec.map φ)
hs : IsOpen (X := ↥(Spec S)) (⇑(Spec.map φ) ⁻¹' s)
⊢ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))

Tactic:
exact (surjective_iff (Spec.map φ)).mp inferInstance

Premises used: AlgebraicGeometry.Spec.map, inferInstance, AlgebraicGeometry.surjective_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : QuasiCompact (Spec.map φ)
inst_2 : Surjective (Spec.map φ)
hs : IsOpen (X := ↥(Spec S)) (⇑(Spec.map φ) ⁻¹' s)
refine_2 : (CommRingCat.Hom.hom φ).Flat
⊢ GeneralizingMap (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))

Tactic:
apply RingHom.Flat.generalizingMap_comap

Premises used: RingHom.Flat.generalizingMap_comap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
R : CommRingCat
s : Set ↥(Spec R)
S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : QuasiCompact (Spec.map φ)
inst_2 : Surjective (Spec.map φ)
hs : IsOpen (X := ↥(Spec S)) (⇑(Spec.map φ) ⁻¹' s)
refine_2 refine_2₁ refine_2₂ refine_2₃ : Flat (Spec.map φ)
⊢ (CommRingCat.Hom.hom φ).Flat

Tactic:
rwa [← HasRingHomProperty.Spec_iff (P := @Flat)]

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
apply : Epi (Scheme.forgetToLocallyRingedSpace.map f)
⊢ Epi f

Tactic:
apply CategoryTheory.Functor.epi_of_epi_map (Scheme.forgetToLocallyRingedSpace)

Premises used: CategoryTheory.Functor.epi_of_epi_map, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
apply : Epi (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f))
⊢ Epi (Scheme.forgetToLocallyRingedSpace.map f)

Tactic:
apply CategoryTheory.Functor.epi_of_epi_map (LocallyRingedSpace.forgetToSheafedSpace)

Premises used: AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
apply :
  ∀
    (x :
      (↑(↑(LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj X)).toPresheafedSpace :
            TopCat) :
        Type u)),
    Mono (X :=
      (LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj Y)).presheaf.stalk
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f)).hom.base :
            (a :
                (↑(↑(LocallyRingedSpace.forgetToSheafedSpace.obj
                            (Scheme.forgetToLocallyRingedSpace.obj X)).toPresheafedSpace :
                      TopCat) :
                  Type u)) →
              (↑(↑(LocallyRingedSpace.forgetToSheafedSpace.obj
                          (Scheme.forgetToLocallyRingedSpace.obj Y)).toPresheafedSpace :
                    TopCat) :
                Type u))
          x))
      (PresheafedSpace.Hom.stalkMap
        (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f)).hom x)
⊢ Epi (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f))

Tactic:
apply SheafedSpace.epi_of_base_surjective_of_stalk_mono _ ‹Surjective f›.surj

Premises used: AlgebraicGeometry.SheafedSpace.epi_of_base_surjective_of_stalk_mono
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
x :
  (↑(↑(LocallyRingedSpace.forgetToSheafedSpace.obj (Scheme.forgetToLocallyRingedSpace.obj X)).toPresheafedSpace :
        TopCat) :
    Type u)
algInst : Algebra (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).toAlgebra
⊢ Module.FaithfullyFlat.{u, u} (↑(Y.presheaf.stalk (f x)) : Type u) (↑(X.presheaf.stalk x) : Type u)

Tactic:
have : Module.FaithfullyFlat (Y.presheaf.stalk (f x)) (X.presheaf.stalk x) :=
    @Module.FaithfullyFlat.of_flat_of_isLocalHom _ _ _ _ _ _ _
      (Flat.stalkMap f x) (f.toLRSHom.prop x)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine X
inst_1 : IsAffine Y
rw :
  Flat (Spec.map (Scheme.Hom.appTop f)) ∧
      Function.Surjective (α := ↥(Spec Γ(X, ⊤))) (β := ↥(Spec Γ(Y, ⊤))) ⇑(Spec.map (Scheme.Hom.appTop f)) ↔
    Flat (Spec.map (Scheme.Hom.appTop f)) ∧
      Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom (Scheme.Hom.appTop f)))
⊢ Flat f ∧ Surjective f ↔ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).FaithfullyFlat

Tactic:
rw [RingHom.FaithfullyFlat.iff_flat_and_comap_surjective,
    MorphismProperty.arrow_mk_iso_iff @Surjective (arrowIsoSpecΓOfIsAffine f),
    MorphismProperty.arrow_mk_iso_iff @Flat (arrowIsoSpecΓOfIsAffine f),
    ← HasRingHomProperty.Spec_iff (P := @Flat), surjective_iff]

Premises used: AlgebraicGeometry.Flat, AlgebraicGeometry.arrowIsoSpecΓOfIsAffine, AlgebraicGeometry.surjective_iff, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, AlgebraicGeometry.HasRingHomProperty.Spec_iff, RingHom.FaithfullyFlat.iff_flat_and_comap_surjective, AlgebraicGeometry.Surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine X
inst_1 : IsAffine Y
⊢ Flat (Spec.map (Scheme.Hom.appTop f)) ∧
      Function.Surjective (α := ↥(Spec Γ(X, ⊤))) (β := ↥(Spec Γ(Y, ⊤))) ⇑(Spec.map (Scheme.Hom.appTop f)) ↔
    Flat (Spec.map (Scheme.Hom.appTop f)) ∧
      Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom (Scheme.Hom.appTop f)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine X
inst_1 : IsAffine Y
inst_2 : Flat f
⊢ (CommRingCat.Hom.hom (appTop f)).Flat

Tactic:
HasRingHomProperty.appTop (P := @Flat) _ inferInstance

Premises used: AlgebraicGeometry.Flat, inferInstance, AlgebraicGeometry.HasRingHomProperty.appTop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
R S : CommRingCat
f : R ⟶ S
rw :
  (CommRingCat.Hom.hom f).Flat ∧ Function.Surjective (α := ↥(Spec S)) (β := ↥(Spec R)) ⇑(Spec.map f) ↔
    (CommRingCat.Hom.hom f).Flat ∧ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom f))
⊢ Flat (Spec.map f) ∧ Surjective (Spec.map f) ↔ (CommRingCat.Hom.hom f).FaithfullyFlat

Tactic:
rw [HasRingHomProperty.Spec_iff (P := @Flat),
    RingHom.FaithfullyFlat.iff_flat_and_comap_surjective, surjective_iff]

Premises used: AlgebraicGeometry.surjective_iff, AlgebraicGeometry.HasRingHomProperty.Spec_iff, RingHom.FaithfullyFlat.iff_flat_and_comap_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ (CommRingCat.Hom.hom f).Flat ∧ Function.Surjective (α := ↥(Spec S)) (β := ↥(Spec R)) ⇑(Spec.map f) ↔
    (CommRingCat.Hom.hom f).Flat ∧ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom f))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
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
⊢ UY ≤ g ⁻¹ᵁ UX

Tactic:
simp [*]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
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
⊢ UY ≤ iY ⁻¹ᵁ UT

Tactic:
simp [*]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
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
⊢ Scheme.Hom.appLE iX US UX hUSX ≫ Scheme.Hom.appLE g UX UY ⋯ =
    Scheme.Hom.appLE f US UT hUST ≫ Scheme.Hom.appLE iY UT UY ⋯

Tactic:
simp only [Scheme.Hom.appLE_comp_appLE, H.w]

Premises used: CategoryTheory.IsPullback.toCommSq, CategoryTheory.CommSq.w, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE
-- 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
h : IsIso (pushoutSection H hUST hUSX hUY)
⊢ Scheme.Hom.appLE iX US UX hUSX ≫ Iso.hom (Iso.refl Γ(X, UX)) =
    Iso.hom (Iso.refl Γ(S, US)) ≫ Scheme.Hom.appLE iX US UX hUSX

Tactic:
simp
-- 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
h : IsIso (pushoutSection H hUST hUSX hUY)
⊢ Scheme.Hom.appLE f US UT hUST ≫ Iso.hom (Iso.refl Γ(T, UT)) =
    Iso.hom (Iso.refl Γ(S, US)) ≫ Scheme.Hom.appLE f US UT hUST

Tactic:
simp
-- 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
h : IsIso (pushoutSection H hUST hUSX hUY)
⊢ pushout.inl (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) ≫
      (asIso (pushoutSection H hUST hUSX hUY)).hom =
    Iso.hom (Iso.refl Γ(X, UX)) ≫ Scheme.Hom.appLE g UX UY ⋯

Tactic:
simp
-- 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
h : IsIso (pushoutSection H hUST hUSX hUY)
⊢ pushout.inr (Scheme.Hom.appLE iX US UX hUSX) (Scheme.Hom.appLE f US UT hUST) ≫
      (asIso (pushoutSection H hUST hUSX hUY)).hom =
    Iso.hom (Iso.refl Γ(T, UT)) ≫ Scheme.Hom.appLE iY UT UY ⋯

Tactic:
simp
-- 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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
(isIso_pushoutSection_iff ..).mpr (IsPullback.of_map_of_faithful Scheme.Spec ?_).unop

Premises used: Iff.mpr, CategoryTheory.IsPullback.of_map_of_faithful, AlgebraicGeometry.Scheme.Spec, AlgebraicGeometry.isIso_pushoutSection_iff, CategoryTheory.IsPullback.unop
-- 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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
refine :
  IsPullback (Scheme.Spec.map (op (Scheme.Hom.app iY UT ≫ Y.presheaf.map (homOfLE ⋯).op)))
    (Scheme.Spec.map (op (Scheme.Hom.app g UX ≫ Y.presheaf.map (homOfLE ⋯).op)))
    (Scheme.Spec.map (op (Scheme.Hom.app f US ≫ T.presheaf.map (homOfLE hUST).op)))
    (Scheme.Spec.map (op (Scheme.Hom.app iX US ≫ X.presheaf.map (homOfLE hUSX).op)))
⊢ IsIso (pushoutSection H hUST hUSX hUY)

Tactic:
refine (isIso_pushoutSection_iff ..).mpr (IsPullback.of_map_of_faithful Scheme.Spec ?_).unop

Premises used: Iff.mpr, CategoryTheory.IsPullback.of_map_of_faithful, AlgebraicGeometry.Scheme.Spec, AlgebraicGeometry.isIso_pushoutSection_iff, CategoryTheory.IsPullback.unop
-- 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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
⊢ IsAffine.{u} (↑US : Scheme)

Tactic:
have : IsAffine _ := hUS
-- 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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this : IsAffine.{u} (↑US : Scheme)
⊢ IsAffine.{u} (↑UT : Scheme)

Tactic:
have : IsAffine _ := hUT
-- 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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this_1 : IsAffine.{u} (↑US : Scheme)
this : IsAffine.{u} (↑UT : Scheme)
⊢ IsAffine.{u} (↑UX : Scheme)

Tactic:
have : IsAffine _ := hUX
-- 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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this_1 : IsAffine.{u} (↑US : Scheme)
this_2 : IsAffine.{u} (↑UT : Scheme)
this : IsAffine.{u} (↑UX : Scheme)
⊢ IsAffineOpen UY

Tactic:
have hUY' : IsAffineOpen UY :=
    .of_isIso (Scheme.Hom.isPullback_resLE H hUST hUSX hUY).isoPullback.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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this_1 : IsAffine.{u} (↑US : Scheme)
this_2 : IsAffine.{u} (↑UT : Scheme)
this : IsAffine.{u} (↑UX : Scheme)
hUY' : IsAffineOpen UY
⊢ Scheme.Hom.resLE iY UT UY ⋯ ≫ hUT.isoSpec.hom =
    hUY'.isoSpec.hom ≫ Scheme.Spec.map (op (Scheme.Hom.app iY UT ≫ Y.presheaf.map (homOfLE ⋯).op))

Tactic:
simp
-- 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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this_1 : IsAffine.{u} (↑US : Scheme)
this_2 : IsAffine.{u} (↑UT : Scheme)
this : IsAffine.{u} (↑UX : Scheme)
hUY' : IsAffineOpen UY
⊢ Scheme.Hom.resLE g UX UY ⋯ ≫ hUX.isoSpec.hom =
    hUY'.isoSpec.hom ≫ Scheme.Spec.map (op (Scheme.Hom.app g UX ≫ Y.presheaf.map (homOfLE ⋯).op))

Tactic:
simp
-- 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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this_1 : IsAffine.{u} (↑US : Scheme)
this_2 : IsAffine.{u} (↑UT : Scheme)
this : IsAffine.{u} (↑UX : Scheme)
hUY' : IsAffineOpen UY
⊢ Scheme.Hom.resLE f US UT hUST ≫ hUS.isoSpec.hom =
    hUT.isoSpec.hom ≫ Scheme.Spec.map (op (Scheme.Hom.app f US ≫ T.presheaf.map (homOfLE hUST).op))

Tactic:
simp
-- 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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this_1 : IsAffine.{u} (↑US : Scheme)
this_2 : IsAffine.{u} (↑UT : Scheme)
this : IsAffine.{u} (↑UX : Scheme)
hUY' : IsAffineOpen UY
⊢ Scheme.Hom.resLE iX US UX hUSX ≫ hUS.isoSpec.hom =
    hUX.isoSpec.hom ≫ Scheme.Spec.map (op (Scheme.Hom.app iX US ≫ X.presheaf.map (homOfLE hUSX).op))

Tactic:
simp
-- 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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this_1 : IsAffine.{u} (↑US : Scheme)
this_2 : IsAffine.{u} (↑UT : Scheme)
this : IsAffine.{u} (↑UX : Scheme)
hUY' : IsAffineOpen UY
⊢ IsPullback (Scheme.Spec.map (op (Scheme.Hom.app iY UT ≫ Y.presheaf.map (homOfLE ⋯).op)))
    (Scheme.Spec.map (op (Scheme.Hom.app g UX ≫ Y.presheaf.map (homOfLE ⋯).op)))
    (Scheme.Spec.map (op (Scheme.Hom.app f US ≫ T.presheaf.map (homOfLE hUST).op)))
    (Scheme.Spec.map (op (Scheme.Hom.app iX US ≫ X.presheaf.map (homOfLE hUSX).op)))

Tactic:
exact .of_iso (Scheme.Hom.isPullback_resLE H hUST hUSX hUY).flip hUY'.isoSpec hUT.isoSpec
    hUX.isoSpec hUS.isoSpec (by simp) (by simp) (by simp) (by simp)