awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
⊢ 1 ≤ (CommRingCat.Hom.hom φ).finrank ((Spec.map φ) x)
have algebraizeInst₁ : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
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)
⊢ 1 ≤ (CommRingCat.Hom.hom φ).finrank ((Spec.map φ) x)
have rw : Membership.mem (α := PrimeSpectrum (↑R : Type u)) (γ := Set (PrimeSpectrum (↑R : Type u)))
  (Set.range (ι := PrimeSpectrum (↑S : Type u)) (PrimeSpectrum.comap (algebraMap (↑R : Type u) (↑S : Type u))))
  ((Spec.map φ) x : ↥(Spec R))
Tactic: rw [← RingHom.algebraMap_toAlgebra φ.hom, RingHom.finrank_algebraMap, Nat.add_one_le_iff,
    PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
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)
⊢ Membership.mem (α := PrimeSpectrum (↑R : Type u)) (γ := Set (PrimeSpectrum (↑R : Type u)))
    (Set.range (ι := PrimeSpectrum (↑S : Type u)) (PrimeSpectrum.comap (algebraMap (↑R : Type u) (↑S : Type u))))
    ((Spec.map φ) x : ↥(Spec R))
have h : Eq (α := PrimeSpectrum (↑R : Type u)) (PrimeSpectrum.comap (algebraMap (↑R : Type u) (↑S : Type u)) x) ((Spec.map φ) x)
Tactic: use x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
⊢ 1 ≤ finrank f ↔ Surjective f
have refine_1 : ∀ (h : 1 ≤ finrank f), Surjective f
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
refine_1 : ∀ (h : 1 ≤ finrank f), Surjective f
⊢ 1 ≤ finrank f ↔ Surjective f
have refine_2 : Surjective f → 1 ≤ finrank f
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
⊢ Surjective f
have refine_1 : ∀
  (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), Surjective f
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
refine_1 :
  ∀
    (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), Surjective f
⊢ Surjective f
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : 1 ≤ finrank f) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
  Surjective f
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, inst, inst_1, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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
⊢ Surjective f
have refine_1 : ∀ (i : Y.affineCover.toPreZeroHypercover.1),
  Surjective (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
Tactic: rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @Surjective) Y.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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
⊢ Surjective (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) (pullback.snd f (Y.affineCover.f i))
have refine_1 : ∀ (y : ↥(Y.affineCover.X i)),
  1 y ≤ finrank (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) (pullback.snd f (Y.affineCover.f i)) y
Tactic: refine this _ (fun y ↦ ?_) ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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 (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) (pullback.snd f (Y.affineCover.f i)) y
have refine_1 : 1 y ≤ finrank f ((Y.affineCover.f i) y)
Tactic: rw [finrank_pullback_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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
⊢ Surjective f
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : 1 ≤ finrank f), Surjective f
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, inst_1, h, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
⊢ Surjective f
have 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
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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
⊢ Surjective f
have 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
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, R, f, inst, inst_1, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
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
⊢ Surjective f
have x : IsAffine X
Tactic: have _ : IsAffine X := isAffine_of_isAffineHom f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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 f
have inr : Surjective (X.isoSpec.inv ≫ f)
Tactic: rw [← MorphismProperty.cancel_left_of_respectsIso @Surjective X.isoSpec.inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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)
have inr : ∀ (x : ↥(Spec R)), 1 x ≤ finrank (X.isoSpec.inv ≫ f) x
Tactic: refine this _ _ (fun x ↦ ?_) ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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 (X.isoSpec.inv ≫ f) x
have inr : 1 x ≤ finrank f x
Tactic: rw [finrank_comp_left_of_isIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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
⊢ Surjective f
have obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [Flat f] [IsFinite f] (h : 1 ≤ finrank f), Surjective f
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, f, inst, inst_1, h, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : 1 ≤ finrank f
⊢ Surjective f
have obtain : ∀ (φ : R ⟶ S) [Flat (Spec.map φ)] [IsFinite (Spec.map φ)] (h : 1 ≤ finrank (Spec.map φ)), Surjective (Spec.map φ)
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst, inst_1, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : IsFinite (Spec.map φ)
h : 1 ≤ finrank (Spec.map φ)
⊢ Surjective (Spec.map φ)
have surj : Function.Surjective (α := ↥(Spec S)) (β := ↥(Spec R)) ⇑(Spec.map φ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : IsFinite (Spec.map φ)
h : 1 ≤ finrank (Spec.map φ)
x : ↥(Spec R)
⊢ ∃ (a : ↥(Spec S)), (Spec.map φ) a = x
have h₁ : 1 x ≤ finrank (Spec.map φ) x
Tactic: specialize h x
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
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
⊢ ∃ (a : ↥(Spec S)), (Spec.map φ) a = x
have inst : (CommRingCat.Hom.hom φ).Flat
Tactic: simp only [IsFinite.SpecMap_iff, Flat.SpecMap_iff] at *
Cleared hypotheses: inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
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
⊢ ∃ (a : ↥(Spec S)), (Spec.map φ) a = x
have inst₁ : (CommRingCat.Hom.hom φ).Finite
Tactic: simp only [IsFinite.SpecMap_iff, Flat.SpecMap_iff] at *
Cleared hypotheses: inst_1, inst_2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
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
⊢ ∃ (a : ↥(Spec S)), (Spec.map φ) a = x
have h₁ : 1 x ≤ (CommRingCat.Hom.hom φ).finrank x
Tactic: rw [finrank_SpecMap_eq_finrank ‹_› ‹_›] at h
Cleared hypotheses: h, inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
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
⊢ ∃ (a : ↥(Spec S)), (Spec.map φ) a = x
have algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
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)
⊢ ∃ (a : ↥(Spec S)), (Spec.map φ) a = x
have algebraizeInst₁ : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : Surjective f
y : ↥Y
⊢ 1 y ≤ finrank f y
have refine_2 : ∀ (x : ↥X), 1 (f x) ≤ finrank f (f x)
Tactic: obtain ⟨x, rfl⟩ := f.surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
⊢ IsLocallyConstant (finrank f)
have 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)
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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)
⊢ IsLocallyConstant (finrank f)
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f]
  (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsLocallyConstant (finrank f)
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, inst, inst_1, inst_2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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
⊢ IsLocallyConstant (finrank f)
have inr : ∀ (x : ↥Y), ∃ (U : Set ↥Y), IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f x
Tactic: rw [IsLocallyConstant.iff_exists_open]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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
⊢ ∃ (U : Set ↥Y), IsOpen U ∧ y ∈ U ∧ ∀ x' ∈ U, finrank f x' = finrank f y
have 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)
Tactic: obtain ⟨R, g, _, x, rfl⟩ := Y.exists_Spec_apply_eq y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
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)
⊢ ∃ (U : Set ↥Y), IsOpen U ∧ Membership.mem (α := ↥Y) U (g x : ↥Y) ∧ ∀ x' ∈ U, finrank f x' = finrank f (g x)
have 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
Tactic: simp_rw [IsLocallyConstant.iff_exists_open] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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 ↥Y), IsOpen U ∧ Membership.mem (α := ↥Y) U (g x : ↥Y) ∧ ∀ x' ∈ U, finrank f x' = finrank f (g x)
have 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)
Tactic: obtain ⟨U, hU, hxU, H⟩ := this (pullback.snd f g) ⟨_, rfl⟩ x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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)
have inr : ∀ y ∈ (↑(g ''ᵁ { carrier := U, is_open' := hU : TopologicalSpace.Opens ↥(Spec R) }) : Set ↥Y),
  finrank f y = finrank f (g x)
Tactic: refine ⟨g ''ᵁ ⟨U, hU⟩, (g ''ᵁ ⟨U, hU⟩).2, ⟨x, hxU, rfl⟩, fun y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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 f (g y') = finrank f (g x)
have inr : finrank (X := pullback f g) (pullback.snd f g) y' = finrank (X := pullback f g) (pullback.snd f g) x
Tactic: rw [← finrank_pullback_snd _ g, ← finrank_pullback_snd _ g]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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
⊢ IsLocallyConstant (finrank f)
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
  IsLocallyConstant (finrank f)
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, inst_1, inst_2, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
⊢ IsLocallyConstant (finrank f)
have 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)
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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)
⊢ IsLocallyConstant (finrank f)
have 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)
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, R, f, inst, inst_1, inst_2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
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
⊢ IsLocallyConstant (finrank f)
have x : IsAffine X
Tactic: have _ : IsAffine X := isAffine_of_isAffineHom f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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 f)
have inr : IsLocallyConstant (finrank (X.isoSpec.inv ≫ f))
Tactic: rw [← finrank_comp_left_of_isIso X.isoSpec.inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
hX : ∃ (S : CommRingCat.{u}), X = Spec S
⊢ IsLocallyConstant (finrank f)
have obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
  IsLocallyConstant (finrank f)
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, f, inst, inst_1, inst_2, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
f : Spec S ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
⊢ IsLocallyConstant (finrank f)
have obtain : ∀ (φ : R ⟶ S) [Flat (Spec.map φ)] [IsFinite (Spec.map φ)] [LocallyOfFinitePresentation (Spec.map φ)],
  IsLocallyConstant (finrank (Spec.map φ))
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst, inst_1, inst_2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : IsFinite (Spec.map φ)
inst_2 : LocallyOfFinitePresentation (Spec.map φ)
⊢ IsLocallyConstant (finrank (Spec.map φ))
have inst : (CommRingCat.Hom.hom φ).Flat
Tactic: simp only [Flat.SpecMap_iff, IsFinite.SpecMap_iff, LocallyOfFinitePresentation.SpecMap_iff] at *
Cleared hypotheses: inst, inst_1, inst_2