awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
R S : CommRingCat
f : R ⟶ S
hf₁ : Surjective (Spec.map f)
hf₂ : Flat (Spec.map f)
⊢ (CommRingCat.Hom.hom f).Flat ∧ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom f))

Tactic:
⟨?_, (Spec.map f).surjective⟩

Premises used: AlgebraicGeometry.Spec.map, And.intro, AlgebraicGeometry.Scheme.Hom.surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
R S : CommRingCat
f : R ⟶ S
hf₁ : Surjective (Spec.map f)
hf₂ : Flat (Spec.map f)
refine_2 : (CommRingCat.Hom.hom f).Flat
⊢ (CommRingCat.Hom.hom f).Flat ∧ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom f))

Tactic:
refine ⟨?_, (Spec.map f).surjective⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
Q : {R S : Type u} → [inst : CommRing R] → [inst_2 : CommRing S] → (R →+* S) → Prop
inst_1 : HasRingHomProperty P fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
h :
  RingHom.CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.FaithfullyFlat
R S : CommRingCat
f : R ⟶ S
hf₁ : Surjective (Spec.map f)
hf₂ : Flat (Spec.map f)
refine_2 refine_2₁ refine_2₂ refine_2₃ : ∀ (hf₂ : (CommRingCat.Hom.hom f).Flat), (CommRingCat.Hom.hom f).Flat
⊢ (CommRingCat.Hom.hom f).Flat

Tactic:
rwa [HasRingHomProperty.Spec_iff (P := @Flat)] at hf₂

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst_1 : IsZariskiLocalAtTarget P
H :
  ∀ {R : CommRingCat.{u_1}} {X Y : Scheme.{u_1}} (f : X ⟶ Spec R) (g : Y ⟶ Spec R),
    (@Surjective ⊓ @Flat ⊓ @LocallyOfFinitePresentation) f → P (X := pullback f g) (pullback.fst f g) → P g
⊢ P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @LocallyOfFinitePresentation)

Tactic:
apply IsZariskiLocalAtTarget.descendsAlong

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.descendsAlong
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst_1 : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (X := pullback f g) (pullback.fst f g)
⊢ Subset (α := Set ↥(Spec R)) Set.univ (Set.range (ι := ↥X) ⇑f)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst_1 : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (X := pullback f g) (pullback.fst f g)
H₁ : ∀ (V : X.Opens) (hV : IsCompact V.carrier) (e : Eq (α := Set ↥(Spec R)) (⇑f '' (↑V : Set ↥X)) Set.univ), P g
⊢ P g

Tactic:
obtain ⟨V : X.Opens, hV, e⟩ := f.isOpenMap.exists_opens_image_eq_of_prespectralSpace
    f.continuous (by simp) isOpen_univ isCompact_univ

Premises used: IsOpenMap.exists_opens_image_eq_of_prespectralSpace, AlgebraicGeometry.Scheme.Hom.isOpenMap, isOpen_univ, isCompact_univ, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.Scheme.Opens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst_1 : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (X := pullback f g) (pullback.fst f g)
V : X.Opens
hV : IsCompact V.carrier
e : Eq (α := Set ↥(Spec R)) (⇑f '' (↑V : Set ↥X)) Set.univ
⊢ P g

Tactic:
MorphismProperty.of_isPullback_of_descendsAlong (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact)
    (.paste_vert (.of_hasPullback V.ι _) (.of_hasPullback f g)) ⟨⟨?_, inferInstance⟩,
      (quasiCompact_iff_compactSpace _).mpr (isCompact_iff_compactSpace.mp hV)⟩ ?_

Premises used: Iff.mpr, isCompact_iff_compactSpace, CategoryTheory.MorphismProperty.of_isPullback_of_descendsAlong, inferInstance, CategoryTheory.IsPullback.paste_vert, And.intro, CategoryTheory.IsPullback.of_hasPullback, Iff.mp, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.quasiCompact_iff_compactSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst_1 : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (X := pullback f g) (pullback.fst f g)
V : X.Opens
hV : IsCompact V.carrier
e : Eq (α := Set ↥(Spec R)) (⇑f '' (↑V : Set ↥X)) Set.univ
H₁ : Surjective (V.ι ≫ f)
H₂ : P (X := pullback (Y := pullback f g) V.ι (pullback.fst f g)) (pullback.fst V.ι (pullback.fst f g))
⊢ P g

Tactic:
refine MorphismProperty.of_isPullback_of_descendsAlong (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact)
    (.paste_vert (.of_hasPullback V.ι _) (.of_hasPullback f g)) ⟨⟨?_, inferInstance⟩,
      (quasiCompact_iff_compactSpace _).mpr (isCompact_iff_compactSpace.mp hV)⟩ ?_

Premises used: Iff.mpr, isCompact_iff_compactSpace, CategoryTheory.MorphismProperty.of_isPullback_of_descendsAlong, inferInstance, CategoryTheory.IsPullback.paste_vert, And.intro, CategoryTheory.IsPullback.of_hasPullback, Iff.mp, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.quasiCompact_iff_compactSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst_1 : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (X := pullback f g) (pullback.fst f g)
V : X.Opens
hV : IsCompact V.carrier
e : Eq (α := Set ↥(Spec R)) (⇑f '' (↑V : Set ↥X)) Set.univ
⊢ Surjective (V.ι ≫ f)

Tactic:
⟨fun x ↦ have ⟨y, hyV, e⟩ := e.ge (Set.mem_univ x); ⟨⟨y, hyV⟩, e⟩⟩

Premises used: Eq.ge, CategoryTheory.ConcreteCategory.hom, Exists, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Subtype.mk, _private.0.AlgebraicGeometry.instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget.match_1, AlgebraicGeometry.Surjective.mk, Exists.intro, CategoryTheory.CategoryStruct.comp, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Opens.ι, Eq, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst_1 : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (X := pullback f g) (pullback.fst f g)
V : X.Opens
hV : IsCompact V.carrier
e : Eq (α := Set ↥(Spec R)) (⇑f '' (↑V : Set ↥X)) Set.univ
⊢ Surjective (V.ι ≫ f)

Tactic:
exact ⟨fun x ↦ have ⟨y, hyV, e⟩ := e.ge (Set.mem_univ x); ⟨⟨y, hyV⟩, e⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst_1 : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (X := pullback f g) (pullback.fst f g)
V : X.Opens
hV : IsCompact V.carrier
e : Eq (α := Set ↥(Spec R)) (⇑f '' (↑V : Set ↥X)) Set.univ
⊢ P (X := pullback (Y := pullback f g) V.ι (pullback.fst f g)) (pullback.fst V.ι (pullback.fst f g))

Tactic:
IsZariskiLocalAtTarget.of_isPullback (.flip <| .of_hasPullback _ _) H

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
P : MorphismProperty Scheme
inst : P.DescendsAlong (@Surjective ⊓ @Flat ⊓ @QuasiCompact)
inst_1 : IsZariskiLocalAtTarget P
R : CommRingCat
X Y : Scheme
f : X ⟶ Spec R
g : Y ⟶ Spec R
h₃ : LocallyOfFinitePresentation f
h₁ : Surjective f
h₂ : Flat f
H : P (X := pullback f g) (pullback.fst f g)
V : X.Opens
hV : IsCompact V.carrier
e : Eq (α := Set ↥(Spec R)) (⇑f '' (↑V : Set ↥X)) Set.univ
⊢ P (X := pullback (Y := pullback f g) V.ι (pullback.fst f g)) (pullback.fst V.ι (pullback.fst f g))

Tactic:
exact IsZariskiLocalAtTarget.of_isPullback (.flip <| .of_hasPullback _ _) H

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Surjective f
inst_1 : Flat f
inst_2 : QuasiCompact f
⊢ (Over.pullback f).Faithful

Tactic:
MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong
    (P := @Surjective ⊓ @Flat ⊓ @QuasiCompact)
    ⟨⟨inferInstance, inferInstance⟩, inferInstance⟩

Premises used: inferInstance, And.intro, CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Surjective f
inst_1 : Flat f
inst_2 : LocallyOfFinitePresentation f
⊢ (Over.pullback f).Faithful

Tactic:
MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong
    (P := @Surjective ⊓ @Flat ⊓ @LocallyOfFinitePresentation)
    ⟨⟨inferInstance, inferInstance⟩, inferInstance⟩

Premises used: inferInstance, And.intro, CategoryTheory.MorphismProperty.faithful_overPullback_of_isomorphisms_descendAlong
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
inst_3 : Mono f
hf : (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f
hfst : isomorphisms Scheme (X := pullback f f) (pullback.fst f f)
⊢ IsIso f

Tactic:
apply MorphismProperty.of_pullback_fst_of_descendsAlong
    (P := isomorphisms Scheme.{u}) (Q := @Surjective ⊓ @Flat ⊓ @QuasiCompact) (f := f) (g := f)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
inst_3 : Mono f
⊢ (@Surjective ⊓ @Flat ⊓ @QuasiCompact) f

Tactic:
tauto
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
inst_3 : Mono f
⊢ isomorphisms Scheme (X := pullback f f) (pullback.fst f f)

Tactic:
inferInstanceAs <| IsIso (pullback.fst f f)

Premises used: _private.0.AlgebraicGeometry.Flat.isIso_of_surjective_of_mono._proof_1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : QuasiCompact f
inst_2 : Surjective f
inst_3 : Mono f
⊢ isomorphisms Scheme (X := pullback f f) (pullback.fst f f)

Tactic:
exact inferInstanceAs <| IsIso (pullback.fst f f)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
        IsOpenImmersion f)
    (hf : ¬Surjective f), IsOpenImmersion f
wlog :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
⊢ IsOpenImmersion f

Tactic:
wlog hf : Surjective f

Premises used: AlgebraicGeometry.Surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
⊢ IsOpenImmersion U.ι

Tactic:
have hU : IsOpenImmersion U.ι := U.instIsOpenImmersionι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
⊢ Subset (α := Set ↥Y) (Set.range (ι := ↥X) ⇑f) (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)

Tactic:
simp [U]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
⊢ f = f' ≫ U.ι

Tactic:
simp [f']
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
⊢ f = f' ≫ U.ι

Tactic:
have heq : f = f' ≫ U.ι := by simp [f']
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
rwa rwa₁ rwa₂ rwa₃ : Flat f
⊢ Flat (f' ≫ U.ι)

Tactic:
rwa [← heq]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
⊢ Flat f'

Tactic:
have hflat : Flat f' :=
      of_postcomp (W := @Flat) f' U.ι hU (by rwa [← heq])
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
rwa rwa₁ rwa₂ rwa₃ : LocallyOfFinitePresentation f
⊢ LocallyOfFinitePresentation (f' ≫ U.ι)

Tactic:
rwa [← heq]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
⊢ LocallyOfFinitePresentation f'

Tactic:
have hfinpres : LocallyOfFinitePresentation f' :=
      of_postcomp (W := @LocallyOfFinitePresentation) f' U.ι hU (by rwa [← heq])
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
hfinpres : LocallyOfFinitePresentation f'
⊢ Mono f'

Tactic:
have hmono : Mono f' := mono_of_mono_fac heq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
hfinpres : LocallyOfFinitePresentation f'
hmono : Mono f'
inr : IsOpenImmersion (f' ≫ U.ι)
⊢ IsOpenImmersion f

Tactic:
rw [heq]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
hfinpres : LocallyOfFinitePresentation f'
hmono : Mono f'
x_1 : ↥(↑U : Scheme)
x : ↥Y
y : ↥X
hy : f y = x
a : Eq (α := ↥Y) (U.ι (f' y : ↥(↑U : Scheme)) : ↥Y) (U.ι (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) x ⋯) : ↥Y)
⊢ Eq (α := ↥(↑U : Scheme)) (f' y : ↥(↑U : Scheme)) (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) x ⋯ : ↥U)

Tactic:
apply U.ι.injective

Premises used: AlgebraicGeometry.Scheme.Hom.injective, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
hfinpres : LocallyOfFinitePresentation f'
hmono : Mono f'
x_1 : ↥(↑U : Scheme)
x : ↥Y
y : ↥X
hy : f y = x
⊢ Eq (α := ↥Y) (U.ι (f' y : ↥(↑U : Scheme)) : ↥Y) (U.ι (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) x ⋯) : ↥Y)

Tactic:
simp [← Scheme.Hom.comp_apply, f', hy]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
hfinpres : LocallyOfFinitePresentation f'
hmono : Mono f'
⊢ IsOpenImmersion f'

Tactic:
have := this f' ⟨fun ⟨x, ⟨y, hy⟩⟩ ↦
      ⟨y, by apply U.ι.injective; simp [← Scheme.Hom.comp_apply, f', hy]⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
this_1 :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [LocallyOfFinitePresentation f] [Mono f] (hf : Surjective f),
    IsOpenImmersion f
hf : ¬Surjective f
U : Y.Opens := { carrier := Set.range (ι := ↥X) ⇑f, is_open' := ⋯ }
hU : IsOpenImmersion U.ι
f' : X ⟶ (↑U : Scheme) := lift U.ι f ⋯
heq : f = f' ≫ U.ι
hflat : Flat f'
hfinpres : LocallyOfFinitePresentation f'
hmono : Mono f'
this : IsOpenImmersion f'
⊢ IsOpenImmersion (f' ≫ U.ι)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
hf : Surjective f
⊢ IsHomeomorph (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
have hhomeo : IsHomeomorph f.base := ⟨f.continuous, f.isOpenMap, f.injective, f.surjective⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
hf : Surjective f
hhomeo : IsHomeomorph (X := ↥X) (Y := ↥Y) ⇑f
⊢ QuasiCompact f

Tactic:
have : QuasiCompact f := ⟨fun U hU hc ↦ hhomeo.homeomorph.isCompact_preimage.mpr hc⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
hf : Surjective f
hhomeo : IsHomeomorph (X := ↥X) (Y := ↥Y) ⇑f
this : QuasiCompact f
⊢ IsIso f

Tactic:
have := Flat.isIso_of_surjective_of_mono f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
hf : Surjective f
hhomeo : IsHomeomorph (X := ↥X) (Y := ↥Y) ⇑f
this_1 : QuasiCompact f
this : IsIso f
⊢ IsOpenImmersion f

Tactic:
.of_isIso f

Premises used: AlgebraicGeometry.IsOpenImmersion.of_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatMono
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : LocallyOfFinitePresentation f
inst_2 : Mono f
hf : Surjective f
hhomeo : IsHomeomorph (X := ↥X) (Y := ↥Y) ⇑f
this_1 : QuasiCompact f
this : IsIso f
⊢ IsOpenImmersion f

Tactic:
exact .of_isIso f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X S Y T : Scheme
f : X ⟶ S
inst : IsAffine S
inst_1 : IsAffine T
f' : Y ⟶ T
g' : Y ⟶ X
g : T ⟶ S
h : IsPullback g' f' f g
inst_2 : Flat f
inst_3 : IsFinite f
s : ↥S
t : ↥T
hs : g t = s
subst : finrank f' t = finrank f (g t)
⊢ finrank f' t = finrank f s

Tactic:
subst hs
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X S Y T : Scheme
f : X ⟶ S
inst : IsAffine S
inst_1 : IsAffine T
f' : Y ⟶ T
g' : Y ⟶ X
g : T ⟶ S
h : IsPullback g' f' f g
inst_2 : Flat f
inst_3 : IsFinite f
t : ↥T
⊢ IsAffine X

Tactic:
have : IsAffine X := isAffine_of_isAffineHom f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X S Y T : Scheme
f : X ⟶ S
inst : IsAffine S
inst_1 : IsAffine T
f' : Y ⟶ T
g' : Y ⟶ X
g : T ⟶ S
h : IsPullback g' f' f g
inst_2 : Flat f
inst_3 : IsFinite f
t : ↥T
this : IsAffine X
⊢ IsPushout (Scheme.Hom.appTop f) (Scheme.Hom.appTop g) (Scheme.Hom.appTop g') (Scheme.Hom.appTop f')

Tactic:
have : IsPushout f.appTop g.appTop g'.appTop f'.appTop := isPushout_appTop_of_isPullback h