awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : 1 ≤ finrank f) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    Surjective f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
refine_1 : 1 y ≤ finrank f ((Y.affineCover.f i) y)
⊢ 1 y ≤ finrank (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) (pullback.snd f (Y.affineCover.f i)) y

Tactic:
rw [finrank_pullback_snd]

Premises used: AlgebraicGeometry.Scheme.Hom.finrank_pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : 1 ≤ finrank f) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    Surjective f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ 1 y ≤ finrank f ((Y.affineCover.f i) y)

Tactic:
h _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : 1 ≤ finrank f) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    Surjective f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ 1 y ≤ finrank f ((Y.affineCover.f i) y)

Tactic:
exact h _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : 1 ≤ finrank f), Surjective f
⊢ Surjective f

Tactic:
obtain ⟨R, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : 1 ≤ finrank f)
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S), Surjective f)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), Surjective f
wlog :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : 1 ≤ finrank f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), Surjective f
⊢ Surjective f

Tactic:
wlog hX : ∃ S, X = Spec S
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : 1 ≤ finrank f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), Surjective f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ IsAffine X

Tactic:
have _ : IsAffine X := isAffine_of_isAffineHom f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : 1 ≤ finrank f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), Surjective f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h_1 : IsAffine X
inr : Surjective (X.isoSpec.inv ≫ f)
⊢ Surjective f

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso @Surjective X.isoSpec.inv]

Premises used: AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.Surjective, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : 1 ≤ finrank f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), Surjective f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h_1 : IsAffine X
⊢ Surjective (X.isoSpec.inv ≫ f)

Tactic:
this _ _ (fun x ↦ ?_) ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : 1 ≤ finrank f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), Surjective f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h_1 : IsAffine X
inr : ∀ (x : ↥(Spec R)), 1 x ≤ finrank (X.isoSpec.inv ≫ f) x
⊢ Surjective (X.isoSpec.inv ≫ f)

Tactic:
refine this _ _ (fun x ↦ ?_) ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : 1 ≤ finrank f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), Surjective f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h_1 : IsAffine X
x : ↥(Spec R)
inr : 1 x ≤ finrank f x
⊢ 1 x ≤ finrank (X.isoSpec.inv ≫ f) x

Tactic:
rw [finrank_comp_left_of_isIso]

Premises used: AlgebraicGeometry.Scheme.Hom.finrank_comp_left_of_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : 1 ≤ finrank f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), Surjective f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h_1 : IsAffine X
x : ↥(Spec R)
⊢ 1 x ≤ finrank f x

Tactic:
h x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : 1 ≤ finrank f)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), Surjective f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h_1 : IsAffine X
x : ↥(Spec R)
⊢ 1 x ≤ finrank f x

Tactic:
exact h x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [Flat f] [IsFinite f] (h : 1 ≤ finrank f), Surjective f
⊢ Surjective f

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
obtain :
  ∀ (φ : R ⟶ S) [Flat (Spec.map φ)] [IsFinite (Spec.map φ)] (h : 1 ≤ finrank (Spec.map φ)), Surjective (Spec.map φ)
⊢ Surjective f

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

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : IsFinite (Spec.map φ)
h : 1 ≤ finrank (Spec.map φ)
surj : Function.Surjective (α := ↥(Spec S)) (β := ↥(Spec R)) ⇑(Spec.map φ)
⊢ Surjective (Spec.map φ)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : IsFinite (Spec.map φ)
h : 1 ≤ finrank (Spec.map φ)
x : ↥(Spec R)
⊢ 1 x ≤ finrank (Spec.map φ) x

Tactic:
specialize h x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : IsFinite (Spec.map φ)
x : ↥(Spec R)
h : 1 x ≤ finrank (Spec.map φ) x
⊢ (CommRingCat.Hom.hom φ).Flat

Tactic:
simp only [IsFinite.SpecMap_iff, Flat.SpecMap_iff] at *

Premises used: AlgebraicGeometry.IsFinite.SpecMap_iff, AlgebraicGeometry.Flat.SpecMap_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
inst_1 : Flat (Spec.map φ)
inst_2 : IsFinite (Spec.map φ)
x : ↥(Spec R)
h : 1 x ≤ finrank (Spec.map φ) x
inst : (CommRingCat.Hom.hom φ).Flat
⊢ (CommRingCat.Hom.hom φ).Finite

Tactic:
simp only [IsFinite.SpecMap_iff, Flat.SpecMap_iff] at *

Premises used: AlgebraicGeometry.IsFinite.SpecMap_iff, AlgebraicGeometry.Flat.SpecMap_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
x : ↥(Spec R)
h : 1 x ≤ finrank (Spec.map φ) x
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
⊢ 1 x ≤ (CommRingCat.Hom.hom φ).finrank x

Tactic:
rw [finrank_SpecMap_eq_finrank ‹_› ‹_›] at h

Premises used: AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_eq_finrank
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
x : ↥(Spec R)
h : 1 x ≤ finrank (Spec.map φ) x
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
h₁ : 1 x ≤ (CommRingCat.Hom.hom φ).finrank x
⊢ (CommRingCat.Hom.hom φ).Flat

Tactic:
rw [finrank_SpecMap_eq_finrank ‹_› ‹_›] at h

Premises used: AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_eq_finrank
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
x : ↥(Spec R)
h : 1 x ≤ finrank (Spec.map φ) x
inst_1 : (CommRingCat.Hom.hom φ).Flat
inst_2 : (CommRingCat.Hom.hom φ).Finite
h₁ : 1 x ≤ (CommRingCat.Hom.hom φ).finrank x
inst : (CommRingCat.Hom.hom φ).Flat
⊢ (CommRingCat.Hom.hom φ).Finite

Tactic:
rw [finrank_SpecMap_eq_finrank ‹_› ‹_›] at h

Premises used: AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_eq_finrank
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
x : ↥(Spec R)
h : 1 x ≤ (CommRingCat.Hom.hom φ).finrank x
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
⊢ Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)

Tactic:
algebraize [φ.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
x : ↥(Spec R)
h : 1 x ≤ (CommRingCat.Hom.hom φ).finrank x
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
⊢ Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)

Tactic:
algebraize [φ.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
x : ↥(Spec R)
h : 1 x ≤ (CommRingCat.Hom.hom φ).finrank x
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ ∃ (a : ↥(Spec S)), (Spec.map φ) a = x

Tactic:
(PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap _).mp h

Premises used: Set.Mem, setOf, Iff.mp, Set.range, PrimeSpectrum.comap, PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
x : ↥(Spec R)
h : 1 x ≤ (CommRingCat.Hom.hom φ).finrank x
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ ∃ (a : ↥(Spec S)), (Spec.map φ) a = x

Tactic:
exact (PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap _).mp h

Premises used: Iff.mp, PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : Surjective f
y : ↥Y
refine_2 : ∀ (x : ↥X), 1 (f x) ≤ finrank f (f x)
⊢ 1 y ≤ finrank f y

Tactic:
obtain ⟨x, rfl⟩ := f.surjective y

Premises used: AlgebraicGeometry.Scheme.Hom.surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : Surjective f
x : ↥X
⊢ 1 (f x) ≤ finrank f (f x)

Tactic:
one_le_finrank_map f x

Premises used: AlgebraicGeometry.Scheme.Hom.one_le_finrank_map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : Surjective f
x : ↥X
⊢ 1 (f x) ≤ finrank f (f x)

Tactic:
exact one_le_finrank_map f x

Premises used: AlgebraicGeometry.Scheme.Hom.one_le_finrank_map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
        (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsLocallyConstant (finrank f))
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsLocallyConstant (finrank f)
wlog :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsLocallyConstant (finrank f)
⊢ IsLocallyConstant (finrank f)

Tactic:
wlog hY : ∃ R, Y = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsLocallyConstant (finrank f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
inr : ∀ (x : ↥Y), ∃ (U : Set ↥Y), IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x
⊢ IsLocallyConstant (finrank f)

Tactic:
rw [IsLocallyConstant.iff_exists_open]

Premises used: IsLocallyConstant.iff_exists_open
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsLocallyConstant (finrank f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
y : ↥Y
inr :
  ∀ (R : CommRingCat.{u}) (g : Spec R ⟶ Y),
    IsOpenImmersion g →
      ∀ (x : ↥(Spec R)),
        ∃ (U : Set ↥Y), IsOpen U ∧ Membership.mem (α := ↥Y) U (g x : ↥Y) ∧ ∀ x' ∈ U, finrank f x' = finrank f (g x)
⊢ ∃ (U : Set ↥Y), IsOpen U ∧ y ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f y

Tactic:
obtain ⟨R, g, _, x, rfl⟩ := Y.exists_Spec_apply_eq y

Premises used: AlgebraicGeometry.Scheme.exists_Spec_apply_eq, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsLocallyConstant (finrank f)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
x : ↥(Spec R)
⊢ ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R) (x : ↥Y),
    ∃ (U : Set ↥Y), IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x

Tactic:
simp_rw [IsLocallyConstant.iff_exists_open] at this

Premises used: IsLocallyConstant.iff_exists_open
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
x : ↥(Spec R)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R) (x : ↥Y),
    ∃ (U : Set ↥Y), IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x
inr :
  ∀ (U : Set ↥(Spec R)) (hU : IsOpen U) (hxU : x ∈ U)
    (H :
      ∀ x' ∈ U, finrank (X := pullback f g) (pullback.snd f g) x' = finrank (X := pullback f g) (pullback.snd f g) x),
    ∃ (U : Set ↥Y), IsOpen U ∧ Membership.mem (α := ↥Y) U (g x : ↥Y) ∧ ∀ x' ∈ U, finrank f x' = finrank f (g x)
⊢ ∃ (U : Set ↥Y), IsOpen U ∧ Membership.mem (α := ↥Y) U (g x : ↥Y) ∧ ∀ x' ∈ U, finrank f x' = finrank f (g x)

Tactic:
obtain ⟨U, hU, hxU, H⟩ := this (pullback.snd f g) ⟨_, rfl⟩ x

Premises used: CategoryTheory.Limits.pullback.snd, Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
x : ↥(Spec R)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R) (x : ↥Y),
    ∃ (U : Set ↥Y), IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x
U : Set ↥(Spec R)
hU : IsOpen U
hxU : x ∈ U
H : ∀ x' ∈ U, finrank (X := pullback f g) (pullback.snd f g) x' = finrank (X := pullback f g) (pullback.snd f g) x
⊢ ∃ (U : Set ↥Y), IsOpen U ∧ Membership.mem (α := ↥Y) U (g x : ↥Y) ∧ ∀ x' ∈ U, finrank f x' = finrank f (g x)

Tactic:
⟨g ''ᵁ ⟨U, hU⟩, (g ''ᵁ ⟨U, hU⟩).2, ⟨x, hxU, rfl⟩, fun y ↦ ?_⟩

Premises used: AlgebraicGeometry.Scheme.Hom.opensFunctor, SetLike.coe, TopologicalSpace.Opens.mk, And.intro, Exists.intro, TopologicalSpace.Opens.is_open', CategoryTheory.Functor.obj, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
x : ↥(Spec R)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R) (x : ↥Y),
    ∃ (U : Set ↥Y), IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x
U : Set ↥(Spec R)
hU : IsOpen U
hxU : x ∈ U
H : ∀ x' ∈ U, finrank (X := pullback f g) (pullback.snd f g) x' = finrank (X := pullback f g) (pullback.snd f g) x
inr :
  ∀ y ∈ (↑(g ''ᵁ { carrier := U, is_open' := hU : TopologicalSpace.Opens ↥(Spec R) }) : Set ↥Y),
    finrank f y = finrank f (g x)
⊢ ∃ (U : Set ↥Y), IsOpen U ∧ Membership.mem (α := ↥Y) U (g x : ↥Y) ∧ ∀ x' ∈ U, finrank f x' = finrank f (g x)

Tactic:
refine ⟨g ''ᵁ ⟨U, hU⟩, (g ''ᵁ ⟨U, hU⟩).2, ⟨x, hxU, rfl⟩, fun y ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
x : ↥(Spec R)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R) (x : ↥Y),
    ∃ (U : Set ↥Y), IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x
U : Set ↥(Spec R)
hU : IsOpen U
hxU : x ∈ U
H : ∀ x' ∈ U, finrank (X := pullback f g) (pullback.snd f g) x' = finrank (X := pullback f g) (pullback.snd f g) x
y' : ↥(Spec R)
hyU : y' ∈ U
inr : finrank (X := pullback f g) (pullback.snd f g) y' = finrank (X := pullback f g) (pullback.snd f g) x
⊢ finrank f (g y') = finrank f (g x)

Tactic:
rw [← finrank_pullback_snd _ g, ← finrank_pullback_snd _ g]

Premises used: AlgebraicGeometry.Scheme.Hom.finrank_pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
x : ↥(Spec R)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R) (x : ↥Y),
    ∃ (U : Set ↥Y), IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x
U : Set ↥(Spec R)
hU : IsOpen U
hxU : x ∈ U
H : ∀ x' ∈ U, finrank (X := pullback f g) (pullback.snd f g) x' = finrank (X := pullback f g) (pullback.snd f g) x
y' : ↥(Spec R)
hyU : y' ∈ U
⊢ finrank (X := pullback f g) (pullback.snd f g) y' = finrank (X := pullback f g) (pullback.snd f g) x

Tactic:
H y' hyU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
x : ↥(Spec R)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R) (x : ↥Y),
    ∃ (U : Set ↥Y), IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x
U : Set ↥(Spec R)
hU : IsOpen U
hxU : x ∈ U
H : ∀ x' ∈ U, finrank (X := pullback f g) (pullback.snd f g) x' = finrank (X := pullback f g) (pullback.snd f g) x
y' : ↥(Spec R)
hyU : y' ∈ U
⊢ finrank (X := pullback f g) (pullback.snd f g) y' = finrank (X := pullback f g) (pullback.snd f g) x

Tactic:
exact H y' hyU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
obtain :
  ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
    IsLocallyConstant (finrank f)
⊢ IsLocallyConstant (finrank f)

Tactic:
obtain ⟨R, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
        (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsLocallyConstant (finrank f))
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), IsLocallyConstant (finrank f)
wlog :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsLocallyConstant (finrank f)
⊢ IsLocallyConstant (finrank f)

Tactic:
wlog hX : ∃ S, X = Spec S
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsLocallyConstant (finrank f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ IsAffine X

Tactic:
have _ : IsAffine X := isAffine_of_isAffineHom f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsLocallyConstant (finrank f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h : IsAffine X
inr : IsLocallyConstant (finrank (X.isoSpec.inv ≫ f))
⊢ IsLocallyConstant (finrank f)

Tactic:
rw [← finrank_comp_left_of_isIso X.isoSpec.inv]

Premises used: AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.Scheme.Hom.finrank_comp_left_of_isIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsLocallyConstant (finrank f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h : IsAffine X
⊢ IsLocallyConstant (finrank (X.isoSpec.inv ≫ f))

Tactic:
this _ _ ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsLocallyConstant (finrank f)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h : IsAffine X
⊢ IsLocallyConstant (finrank (X.isoSpec.inv ≫ f))

Tactic:
exact this _ _ ⟨_, rfl⟩

Premises used: Exists.intro, rfl