awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥Y
inst_1 : IsIntegral Y
⊢ Flat (f ≫ Y.isoSpec.hom)
have refine : ∀ (i : X.affineCover.I₀), Flat (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom)
Tactic: refine (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥Y
inst_1 : IsIntegral Y
i : X.affineCover.I₀
⊢ Flat (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom)
have rw : (CommRingCat.Hom.hom (Spec.preimage (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom))).Flat
Tactic: rw [← Spec.map_preimage (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom),
    HasRingHomProperty.Spec_iff (P := @Flat)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
⊢ Topology.IsQuotientMap (X := ↥X) (Y := ↥Y) ⇑f
have rw : Topology.IsCoinducing (X := ↥X) (Y := ↥Y) ⇑f ∧ Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
Tactic: rw [Topology.isQuotientMap_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
⊢ Topology.IsCoinducing (X := ↥X) (Y := ↥Y) ⇑f ∧ Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
have refine : ∀ (s : Set ↥Y) (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)), IsOpen s
Tactic: refine ⟨.of_isOpen_preimage_iff_isOpen fun s ↦
    ⟨fun hs ↦ ?_, fun hs ↦ hs.preimage f.continuous⟩, f.surjective⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
s : Set ↥Y
hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)
⊢ IsOpen s
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y)
      (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsOpen s)
  (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsOpen s
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
s : Set ↥Y
hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y)
        (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsOpen s)
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsOpen s
⊢ IsOpen s
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y)
  (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsOpen s
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, inst, inst_1, inst_2, s, hs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
s : Set ↥Y
hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y)
    (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsOpen s
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
⊢ IsOpen s
have inr : ∀ (i : 𝒰.I₀), IsOpen (s ∩ (↑(Scheme.Hom.opensRange (𝒰.f i)) : Set ↥Y))
Tactic: rw [𝒰.isOpenCover_opensRange.isOpen_iff_inter]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
s : Set ↥Y
hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y)
    (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsOpen s
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (s ∩ (↑(Scheme.Hom.opensRange (𝒰.f i)) : Set ↥Y))
have inr : IsOpen (X := ↥Y) (Set.image (α := ↥(𝒰.X i)) (⇑(𝒰.f i)) (⇑(𝒰.f i) ⁻¹' s))
Tactic: rw [Scheme.Hom.coe_opensRange, ← Set.image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
s : Set ↥Y
hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y)
    (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsOpen s
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (X := ↥Y) (Set.image (α := ↥(𝒰.X i)) (⇑(𝒰.f i)) (⇑(𝒰.f i) ⁻¹' s))
have inr : IsOpen (X := ↥(𝒰.X i)) (⇑(𝒰.f i) ⁻¹' s)
Tactic: apply (𝒰.f i).isOpenEmbedding.isOpenMap
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
s : Set ↥Y
hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y)
    (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsOpen s
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (X := ↥(𝒰.X i)) (⇑(𝒰.f i) ⁻¹' s)
have inr : IsOpen (X := ↥(pullback (𝒰.f i) f)) (Set.preimage (β := ↥(𝒰.X i)) (⇑(pullback.fst (𝒰.f i) f)) (⇑(𝒰.f i) ⁻¹' s))
Tactic: refine this (f := pullback.fst (𝒰.f i) f) _ ?_ ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
s : Set ↥Y
hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y)
    (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsOpen s
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (X := ↥(pullback (𝒰.f i) f)) (Set.preimage (β := ↥(𝒰.X i)) (⇑(pullback.fst (𝒰.f i) f)) (⇑(𝒰.f i) ⁻¹' s))
have inr : IsOpen (X := ↥(pullback (𝒰.f i) f)) (Set.preimage (β := ↥X) (⇑(pullback.snd (𝒰.f i) f)) (⇑f ⁻¹' s))
Tactic: rw [← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, pullback.condition,
      Scheme.Hom.comp_base, TopCat.coe_comp, Set.preimage_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
s : Set ↥Y
hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ IsOpen s
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥(Spec R))
  (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)), IsOpen s
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, inst_1, inst_2, s, hs, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
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)
⊢ IsOpen s
have inr : ∀
  (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), IsOpen s
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
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)
inr :
  ∀
    (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), IsOpen s
⊢ IsOpen s
have wlog : ∀ {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
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, R, f, inst, inst_1, inst_2, s, hs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (hypothesis)
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
⊢ IsOpen s
have x : CompactSpace.{u} ↥X
Tactic: have _ : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
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 s
have inr : IsOpen (X := ↥(Spec Γ(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i, ⊤)))
  (⇑(Iso.inv (Scheme.isoSpec (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)) ≫ p ≫ f) ⁻¹' s)
Tactic: refine this (f := (∐ (fun i : 𝒰.I₀ ↦ 𝒰.X i)).isoSpec.inv ≫ p ≫ f) _ _ ?_ ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
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, ⊤)))
    (⇑(Iso.inv (Scheme.isoSpec (∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i)) ≫ p ≫ f) ⁻¹' s)
have inr : IsOpen (X := ↥(Spec Γ(∐ fun (i : 𝒰.I₀) ↦ 𝒰.X i, ⊤)))
  (Set.preimage (β := ↥X) (⇑(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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
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
⊢ IsOpen s
have obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [Flat f] [QuasiCompact f] [Surjective f]
  (hs : IsOpen (X := ↥(Spec S)) (⇑f ⁻¹' s)), IsOpen s
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, f, inst, inst_1, inst_2, hs, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
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)
⊢ IsOpen s
have obtain : ∀ (φ : R ⟶ S) [Flat (Spec.map φ)] [QuasiCompact (Spec.map φ)] [Surjective (Spec.map φ)]
  (hs : IsOpen (X := ↥(Spec S)) (⇑(Spec.map φ) ⁻¹' s)), IsOpen s
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst, inst_1, inst_2, hs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
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
have refine_1 : Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))
Tactic: refine ((PrimeSpectrum.isQuotientMap_of_generalizingMap ?_ ?_).isOpen_preimage).mp hs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
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 φ))
⊢ IsOpen s
have refine_2 : GeneralizingMap (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))
Tactic: refine ((PrimeSpectrum.isQuotientMap_of_generalizingMap ?_ ?_).isOpen_preimage).mp hs
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
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)
⊢ GeneralizingMap (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))
have refine_2 : (CommRingCat.Hom.hom φ).Flat
Tactic: apply RingHom.Flat.generalizingMap_comap
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
⊢ Epi f
have apply : Epi (Scheme.forgetToLocallyRingedSpace.map f)
Tactic: apply CategoryTheory.Functor.epi_of_epi_map (Scheme.forgetToLocallyRingedSpace)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
⊢ Epi (Scheme.forgetToLocallyRingedSpace.map f)
have apply : Epi (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f))
Tactic: apply CategoryTheory.Functor.epi_of_epi_map (LocallyRingedSpace.forgetToSheafedSpace)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : Surjective f
⊢ Epi (LocallyRingedSpace.forgetToSheafedSpace.map (Scheme.forgetToLocallyRingedSpace.map f))
have 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)
Tactic: apply SheafedSpace.epi_of_base_surjective_of_stalk_mono _ ‹Surjective f›.surj
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsAffine X
inst_1 : IsAffine Y
⊢ Flat f ∧ Surjective f ↔ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).FaithfullyFlat
have 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)))
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Flat (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ Flat (Spec.map f) ∧ Surjective (Spec.map f) ↔ (CommRingCat.Hom.hom f).FaithfullyFlat
have 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))
Tactic: rw [HasRingHomProperty.Spec_iff (P := @Flat),
    RingHom.FaithfullyFlat.iff_flat_and_comap_surjective, surjective_iff]
-- 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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
⊢ IsIso (pushoutSection H hUST hUSX hUY)
have refine : IsPullback (Scheme.Spec.map (op (Scheme.Hom.app iY UT ≫ Y.presheaf.map (homOfLE sorry).op)))
  (Scheme.Spec.map (op (Scheme.Hom.app g UX ≫ Y.presheaf.map (homOfLE sorry).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: refine (isIso_pushoutSection_iff ..).mpr (IsPullback.of_map_of_faithful Scheme.Spec ?_).unop
-- 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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
⊢ 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)))
have this : IsAffine.{u} (↑US : Scheme)
Tactic: have : IsAffine _ := hUS
-- 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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this : IsAffine.{u} (↑US : Scheme)
⊢ 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)))
have this₁ : IsAffine.{u} (↑UT : Scheme)
Tactic: have : IsAffine _ := hUT
-- 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
hUS : IsAffineOpen US
hUT : IsAffineOpen UT
hUX : IsAffineOpen UX
this_1 : IsAffine.{u} (↑US : Scheme)
this : IsAffine.{u} (↑UT : Scheme)
⊢ 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)))
have this₁ : IsAffine.{u} (↑UX : Scheme)
Tactic: have : IsAffine _ := hUX
-- 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
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)
⊢ 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)))
have hUY' : IsAffineOpen UY
Tactic: have hUY' : IsAffineOpen UY :=
    .of_isIso (Scheme.Hom.isPullback_resLE H hUST hUSX hUY).isoPullback.hom
-- 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 : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
⊢ Mono (pushoutSection H hUST hUSX hUY)
have obtain : ∀ (I : Set (↑X.affineOpens : Type u)) (hI : I.Finite) (e : UX = ⨆ i ∈ I, (↑i : X.Opens)),
  Mono (pushoutSection H hUST hUSX hUY)
Tactic: obtain ⟨I, hI, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hUX
-- 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 : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
I : Set (↑X.affineOpens : Type u)
hI : I.Finite
e : UX = ⨆ i ∈ I, (↑i : X.Opens)
⊢ Mono (pushoutSection H hUST hUSX hUY)
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 : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
I : Set (↑X.affineOpens : Type u)
hI : I.Finite
e : UX = ⨆ i ∈ I, (↑i : X.Opens)
this : Finite.{u + 1} (↑I : Type u)
⊢ ⨆ (x : (↑I : Type u)), (↑(↑x : (↑X.affineOpens : Type u)) : X.Opens) = UX
have rwa : ⨆ (i : (↑X.affineOpens : Type u)),
    ⨆ (h : i ∈ I),
      (↑(↑(Subtype.mk (p := fun (x : (↑X.affineOpens : Type u)) ↦ x ∈ I) i h) : (↑X.affineOpens : Type u)) : X.Opens) =
  UX
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 : IsAffineOpen UT
hUX : IsCompact (↑UX : Set ↥X)
I : Set (↑X.affineOpens : Type u)
hI : I.Finite
e : UX = ⨆ i ∈ I, (↑i : X.Opens)
this : Finite.{u + 1} (↑I : Type u)
rwa :
  ⨆ (i : (↑X.affineOpens : Type u)),
      ⨆ (h : i ∈ I),
        (↑(↑(Subtype.mk (p := fun (x : (↑X.affineOpens : Type u)) ↦ x ∈ I) i h) : (↑X.affineOpens : Type u)) :
          X.Opens) =
    UX
⊢ ⨆ (x : (↑I : Type u)), (↑(↑x : (↑X.affineOpens : Type u)) : X.Opens) = UX
have rwa₁ : UX =
  ⨆ (i : (↑X.affineOpens : Type u)),
    ⨆ (h : i ∈ I),
      (↑(↑(Subtype.mk (p := fun (x : (↑X.affineOpens : Type u)) ↦ x ∈ I) i h) : (↑X.affineOpens : Type u)) : X.Opens)
Tactic: rwa [iSup_subtype, eq_comm]