awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
refine_2 :
  ∀ (S : P.CostructuredArrow ⊤ Scheme.Spec X),
    (fun (x : P.CostructuredArrow ⊤ Scheme.Spec X) ↦ Nonempty.{u + 1} (F.obj x ≅ R)) S →
      ∀ (e : F.obj S ≅ R),
        Scheme.Spec.map e.hom ≫
            Comma.hom
              (MorphismProperty.Comma.toComma (P := P) (Q := ⊤) (W := ⊤)
                (MorphismProperty.CostructuredArrow.mk (P := P) ⊤
                  (↑(Subtype.mk (p := fun (f : Spec (unop R) ⟶ X) ↦ P f)
                        (Spec.map e.inv.unop ≫ S.toComma (P := P) (Q := ⊤) (W := ⊤).hom) ⋯) :
                    Spec (unop R) ⟶ X)
                  ⋯)) =
          S.toComma (P := P) (Q := ⊤) (W := ⊤).hom
refine_2₁ :
  ∀ (S : P.CostructuredArrow ⊤ Scheme.Spec X),
    (fun (x : P.CostructuredArrow ⊤ Scheme.Spec X) ↦ Nonempty.{u + 1} (F.obj x ≅ R)) S →
      ∀ (e : F.obj S ≅ R), P (Spec.map e.inv.unop ≫ S.toComma (P := P) (Q := ⊤) (W := ⊤).hom)
⊢ LE.le.{u + 1} (α := ObjectProperty (P.CostructuredArrow ⊤ Scheme.Spec X))
    (fun (x : P.CostructuredArrow ⊤ Scheme.Spec X) ↦ Nonempty.{u + 1} (F.obj x ≅ R))
    (ObjectProperty.isoClosure
      (ObjectProperty.ofObj fun (f : { f : Spec (unop R) ⟶ X // P f }) ↦
        MorphismProperty.CostructuredArrow.mk (P := P) ⊤ (↑f : Spec (unop R) ⟶ X) ⋯))

Tactic:
refine fun S ⟨e⟩ ↦ ⟨_, .mk ⟨Spec.map e.inv.unop ≫ S.hom, ?_⟩,
      ⟨MorphismProperty.CostructuredArrow.isoMk e trivial trivial ?_⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
S : P.CostructuredArrow ⊤ Scheme.Spec X
h : (fun (x : P.CostructuredArrow ⊤ Scheme.Spec X) ↦ Nonempty.{u + 1} (F.obj x ≅ R)) S
e : F.obj S ≅ R
⊢ Scheme.Spec.map e.hom ≫
      Comma.hom
        (MorphismProperty.Comma.toComma (P := P) (Q := ⊤) (W := ⊤)
          (MorphismProperty.CostructuredArrow.mk (P := P) ⊤
            (↑(Subtype.mk (p := fun (f : Spec (unop R) ⟶ X) ↦ P f)
                  (Spec.map e.inv.unop ≫ S.toComma (P := P) (Q := ⊤) (W := ⊤).hom) ⋯) :
              Spec (unop R) ⟶ X)
            ⋯)) =
    S.toComma (P := P) (Q := ⊤) (W := ⊤).hom

Tactic:
simp [← Spec.map_comp_assoc, F]

Premises used: AlgebraicGeometry.Spec.map_comp_assoc
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
S : P.CostructuredArrow ⊤ Scheme.Spec X
h : (fun (x : P.CostructuredArrow ⊤ Scheme.Spec X) ↦ Nonempty.{u + 1} (F.obj x ≅ R)) S
e : F.obj S ≅ R
⊢ P (Spec.map e.inv.unop ≫ S.toComma (P := P) (Q := ⊤) (W := ⊤).hom)

Tactic:
(P.cancel_left_of_respectsIso _ _).mpr S.prop

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.Comma.prop, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X : Scheme
P : MorphismProperty Scheme
hP : P ≤ @LocallyOfFiniteType
inst : P.RespectsIso
F : P.CostructuredArrow ⊤ Scheme.Spec X ⥤ CommRingCatᵒᵖ :=
  MorphismProperty.CostructuredArrow.forget P ⊤ Scheme.Spec X ⋙ CostructuredArrow.proj Scheme.Spec X
R : CommRingCatᵒᵖ
S : P.CostructuredArrow ⊤ Scheme.Spec X
h : (fun (x : P.CostructuredArrow ⊤ Scheme.Spec X) ↦ Nonempty.{u + 1} (F.obj x ≅ R)) S
e : F.obj S ≅ R
⊢ P (Spec.map e.inv.unop ≫ S.toComma (P := P) (Q := ⊤) (W := ⊤).hom)

Tactic:
exact (P.cancel_left_of_respectsIso _ _).mpr S.prop

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.Comma.prop, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f : X ⟶ Y
h :
  ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
    Flat f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Flat) f
⊢ @Flat = affineLocally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Flat

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
h :
  (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat) ↔
    affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Flat) f
h₁ h₂ :
  (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat) ↔
    ∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat
⊢ Flat f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Flat) f

Tactic:
rw [flat_iff, affineLocally_iff_forall_isAffineOpen]

Premises used: AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, AlgebraicGeometry.flat_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
⊢ Flat f

Tactic:
HasRingHomProperty.of_isOpenImmersion
    RingHom.Flat.containsIdentities

Premises used: AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion, RingHom.Flat.containsIdentities
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ MorphismProperty.IsStableUnderComposition @Flat

Tactic:
HasRingHomProperty.stableUnderComposition RingHom.Flat.stableUnderComposition

Premises used: AlgebraicGeometry.HasRingHomProperty.stableUnderComposition, RingHom.Flat.stableUnderComposition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
R S : CommRingCat
f : R ⟶ S
⊢ Flat (Spec.map f) ↔ (CommRingCat.Hom.hom f).Flat

Tactic:
HasRingHomProperty.Spec_iff

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : Flat f
hg : Flat g
⊢ Flat (f ≫ g)

Tactic:
MorphismProperty.comp_mem _ f g hf hg

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ MorphismProperty.IsStableUnderBaseChange @Flat

Tactic:
HasRingHomProperty.isStableUnderBaseChange RingHom.Flat.isStableUnderBaseChange

Premises used: RingHom.Flat.isStableUnderBaseChange, AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst : Flat g
⊢ Flat (X := pullback f g) (pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst _ _ inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
inst : Flat f
⊢ Flat (X := pullback f g) (pullback.snd f g)

Tactic:
MorphismProperty.pullback_snd _ _ inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f_1 f : X ⟶ Y
V : Y.Opens
inst : Flat f
⊢ Flat (f ∣_ V)

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f_1 f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst : Flat f
⊢ Flat (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat
⊢ Flat f

Tactic:
HasRingHomProperty.of_stalkMap RingHom.Flat.ofLocalizationPrime H

Premises used: RingHom.Flat.ofLocalizationPrime, AlgebraicGeometry.HasRingHomProperty.of_stalkMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
x : ↥X
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat

Tactic:
HasRingHomProperty.stalkMap (P := @Flat)
    (fun f hf J hJ ↦ hf.localRingHom J (J.comap f) rfl) ‹_› x

Premises used: AlgebraicGeometry.HasRingHomProperty.stalkMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ Flat f ↔ ∀ (x : ↥X), (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).Flat

Tactic:
⟨fun _ ↦ stalkMap f, fun H ↦ of_stalkMap f H⟩

Premises used: AlgebraicGeometry.Flat.of_stalkMap, AlgebraicGeometry.Flat.stalkMap, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
X : Scheme
ι : Type v
inst : Small.{u, v} ι
Y : ι → Scheme
f : (i : ι) → Y i ⟶ X
inst_1 : ∀ (i : ι), Flat (f i)
⊢ Flat (X := ∐ Y) (Sigma.desc f)

Tactic:
IsZariskiLocalAtSource.sigmaDesc (fun _ ↦ inferInstance)

Premises used: inferInstance, AlgebraicGeometry.IsZariskiLocalAtSource.sigmaDesc
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥Y
inst_1 : IsIntegral Y
⊢ Flat f

Tactic:
(MorphismProperty.cancel_right_of_respectsIso @Flat _ Y.isoSpec.hom).mp ?_

Premises used: AlgebraicGeometry.Flat, AlgebraicGeometry.Scheme.isoSpec, Iff.mp, CategoryTheory.Iso.hom, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥Y
inst_1 : IsIntegral Y
refine : Flat (f ≫ Y.isoSpec.hom)
⊢ Flat f

Tactic:
refine (MorphismProperty.cancel_right_of_respectsIso @Flat _ Y.isoSpec.hom).mp ?_

Premises used: AlgebraicGeometry.Flat, AlgebraicGeometry.Scheme.isoSpec, Iff.mp, CategoryTheory.Iso.hom, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥Y
inst_1 : IsIntegral Y
⊢ Flat (f ≫ Y.isoSpec.hom)

Tactic:
(IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ ?_

Premises used: Iff.mpr, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥Y
inst_1 : IsIntegral Y
refine : ∀ (i : X.affineCover.I₀), Flat (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom)
⊢ Flat (f ≫ Y.isoSpec.hom)

Tactic:
refine (IsZariskiLocalAtSource.iff_of_openCover X.affineCover).mpr fun i ↦ ?_

Premises used: Iff.mpr, AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥Y
inst_1 : IsIntegral Y
i : X.affineCover.I₀
rw : (CommRingCat.Hom.hom (Spec.preimage (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom))).Flat
⊢ Flat (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom)

Tactic:
rw [← Spec.map_preimage (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom),
    HasRingHomProperty.Spec_iff (P := @Flat)]

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.HasRingHomProperty.Spec_iff, AlgebraicGeometry.Spec.map_preimage, CategoryTheory.Iso.hom, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥Y
inst_1 : IsIntegral Y
i : X.affineCover.I₀
⊢ (CommRingCat.Hom.hom (Spec.preimage (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom))).Flat

Tactic:
.of_isField (isField_of_isIntegral_of_subsingleton _) _

Premises used: RingHom.Flat.of_isField, AlgebraicGeometry.isField_of_isIntegral_of_subsingleton
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : Subsingleton.{u + 1} ↥Y
inst_1 : IsIntegral Y
i : X.affineCover.I₀
⊢ (CommRingCat.Hom.hom (Spec.preimage (X.affineCover.f i ≫ f ≫ Y.isoSpec.hom))).Flat

Tactic:
exact .of_isField (isField_of_isIntegral_of_subsingleton _) _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
rw : Topology.IsCoinducing (X := ↥X) (Y := ↥Y) ⇑f ∧ Function.Surjective (α := ↥X) (β := ↥Y) ⇑f
⊢ Topology.IsQuotientMap (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
rw [Topology.isQuotientMap_iff]

Premises used: Topology.isQuotientMap_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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

Tactic:
⟨.of_isOpen_preimage_iff_isOpen fun s ↦
    ⟨fun hs ↦ ?_, fun hs ↦ hs.preimage f.continuous⟩, f.surjective⟩

Premises used: Topology.IsCoinducing.of_isOpen_preimage_iff_isOpen, And.intro, Iff.intro, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Scheme.Hom.surjective, IsOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
refine : ∀ (s : Set ↥Y) (hs : IsOpen (X := ↥X) (⇑f ⁻¹' s)), IsOpen s
⊢ Topology.IsCoinducing (X := ↥X) (Y := ↥Y) ⇑f ∧ Function.Surjective (α := ↥X) (β := ↥Y) ⇑f

Tactic:
refine ⟨.of_isOpen_preimage_iff_isOpen fun s ↦
    ⟨fun hs ↦ ?_, fun hs ↦ hs.preimage f.continuous⟩, f.surjective⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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
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
⊢ IsOpen s

Tactic:
wlog hY : ∃ R, Y = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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
inr : ∀ (i : 𝒰.I₀), IsOpen (s ∩ (↑(Scheme.Hom.opensRange (𝒰.f i)) : Set ↥Y))
⊢ IsOpen s

Tactic:
rw [𝒰.isOpenCover_opensRange.isOpen_iff_inter]

Premises used: AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, TopologicalSpace.IsOpenCover.isOpen_iff_inter
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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₀
inr : IsOpen (X := ↥Y) (Set.image (α := ↥(𝒰.X i)) (⇑(𝒰.f i)) (⇑(𝒰.f i) ⁻¹' s))
⊢ IsOpen (s ∩ (↑(Scheme.Hom.opensRange (𝒰.f i)) : Set ↥Y))

Tactic:
rw [Scheme.Hom.coe_opensRange, ← Set.image_preimage_eq_inter_range]

Premises used: Set.image_preimage_eq_inter_range, AlgebraicGeometry.Scheme.Hom.coe_opensRange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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₀
inr : IsOpen (X := ↥(𝒰.X i)) (⇑(𝒰.f i) ⁻¹' s)
⊢ IsOpen (X := ↥Y) (Set.image (α := ↥(𝒰.X i)) (⇑(𝒰.f i)) (⇑(𝒰.f i) ⁻¹' s))

Tactic:
apply (𝒰.f i).isOpenEmbedding.isOpenMap

Premises used: CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.isOpenMap, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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)

Tactic:
this (f := pullback.fst (𝒰.f i) f) _ ?_ ⟨_, rfl⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.fst, Exists.intro, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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₀
inr : IsOpen (X := ↥(pullback (𝒰.f i) f)) (Set.preimage (β := ↥(𝒰.X i)) (⇑(pullback.fst (𝒰.f i) f)) (⇑(𝒰.f i) ⁻¹' s))
⊢ IsOpen (X := ↥(𝒰.X i)) (⇑(𝒰.f i) ⁻¹' s)

Tactic:
refine this (f := pullback.fst (𝒰.f i) f) _ ?_ ⟨_, rfl⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.fst, Exists.intro, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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₀
inr : IsOpen (X := ↥(pullback (𝒰.f i) f)) (Set.preimage (β := ↥X) (⇑(pullback.snd (𝒰.f i) f)) (⇑f ⁻¹' s))
⊢ IsOpen (X := ↥(pullback (𝒰.f i) f)) (Set.preimage (β := ↥(𝒰.X i)) (⇑(pullback.fst (𝒰.f i) f)) (⇑(𝒰.f i) ⁻¹' 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]

Premises used: Set.preimage_comp, AlgebraicGeometry.Scheme.Hom.comp_base, CategoryTheory.Limits.pullback.condition, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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) (⇑(pullback.snd (𝒰.f i) f)) (⇑f ⁻¹' s))

Tactic:
hs.preimage (Scheme.Hom.continuous _)

Premises used: AlgebraicGeometry.Scheme.Hom.continuous, IsOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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) (⇑(pullback.snd (𝒰.f i) f)) (⇑f ⁻¹' s))

Tactic:
exact hs.preimage (Scheme.Hom.continuous _)

Premises used: AlgebraicGeometry.Scheme.Hom.continuous, IsOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Flat
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
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
⊢ IsOpen s

Tactic:
obtain ⟨R, rfl⟩ := hY

Premises used: 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)
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
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
⊢ IsOpen s

Tactic:
wlog hX : ∃ S, X = Spec S
-- 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
⊢ CompactSpace.{u} ↥X

Tactic:
have _ : CompactSpace X := QuasiCompact.compactSpace_of_compactSpace f
-- 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 s

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