awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X S Y : Scheme
f : X ⟶ Y
g : Y ⟶ S
inst : IsIso f
inst_1 : Flat g
inst_2 : IsFinite g
z : ↥S
e : pullback (Y := Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
    (f ≫ g) (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) ≅
  pullback (Y := Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z))) g
    (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) :=
  Iso.trans (Y :=
    pullback (Y :=
      pullback (Y := Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
        g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
      f (pullback.fst g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z))))
    (Iso.symm
      (pullbackRightPullbackFstIso g
        (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) f))
    (asIso
      (pullback.snd f
        (pullback.fst g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))))
⊢ e.hom ≫ pullback.snd g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) =
    pullback.snd (f ≫ g) (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z))

Tactic:
simp [e]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X S Y : Scheme
f : X ⟶ Y
g : Y ⟶ S
inst : IsIso f
inst_1 : Flat g
inst_2 : IsFinite g
z : ↥S
e : pullback (Y := Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
    (f ≫ g) (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) ≅
  pullback (Y := Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z))) g
    (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) :=
  Iso.trans (Y :=
    pullback (Y :=
      pullback (Y := Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
        g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
      f (pullback.fst g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z))))
    (Iso.symm
      (pullbackRightPullbackFstIso g
        (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) f))
    (asIso
      (pullback.snd f
        (pullback.fst g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))))
⊢ e.hom ≫ pullback.snd g (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) =
    pullback.snd (f ≫ g) (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z))

Tactic:
have : e.hom ≫ pullback.snd _ _ = pullback.snd _ _ := by simp [e]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : Flat f
inst_1 : IsFinite f
y : ↥Y
obtain :
  ∀ (R : CommRingCat.{u}) (i : Spec R ⟶ Y),
    IsOpenImmersion i →
      ∀ (y' : ↥(Spec R)), finrank (X := pullback f g) (pullback.snd f g) (i y') = finrank f (g (i y' : ↥Y))
⊢ finrank (X := pullback f g) (pullback.snd f g) y = finrank f (g y)

Tactic:
obtain ⟨R, i, _, y', rfl⟩ := Y.exists_Spec_apply_eq y

Premises used: AlgebraicGeometry.Scheme.exists_Spec_apply_eq, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : Flat f
inst_1 : IsFinite f
R : CommRingCat
i : Spec R ⟶ Y
w : IsOpenImmersion i
y' : ↥(Spec R)
rw : finrank (X := pullback f g) (pullback.snd f g) (i y') = finrank f ((i ≫ g) y')
rw₁ :
  IsAffine.finrank (X := pullback (X := pullback f g) (pullback.snd f g) i) (pullback.snd (pullback.snd f g) i) y' =
    finrank f ((i ≫ g) y')
rw₂ :
  IsAffine.finrank (X := pullback (X := pullback f g) (pullback.snd f g) i) (pullback.snd (pullback.snd f g) i) y' =
    IsAffine.finrank (X := pullback f (i ≫ g)) (pullback.snd f (i ≫ g)) y'
rw₃ :
  IsAffine.finrank (X := pullback (X := pullback f g) (pullback.snd f g) i)
      (Iso.hom (pullbackLeftPullbackSndIso f g i) ≫ pullback.snd f (i ≫ g)) y' =
    IsAffine.finrank (X := pullback f (i ≫ g)) (pullback.snd f (i ≫ g)) y'
rw₄ :
  finrank (X := pullback (X := pullback f g) (pullback.snd f g) i)
      (Iso.hom (pullbackLeftPullbackSndIso f g i) ≫ pullback.snd f (i ≫ g)) y' =
    IsAffine.finrank (X := pullback f (i ≫ g)) (pullback.snd f (i ≫ g)) y'
rw₅ :
  finrank (X := pullback (X := pullback f g) (pullback.snd f g) i)
      (Iso.hom (pullbackLeftPullbackSndIso f g i) ≫ pullback.snd f (i ≫ g)) y' =
    finrank (X := pullback f (i ≫ g)) (pullback.snd f (i ≫ g)) y'
rw₆ rw₇ :
  finrank (X := pullback f (i ≫ g)) (pullback.snd f (i ≫ g)) y' =
    finrank (X := pullback f (i ≫ g)) (pullback.snd f (i ≫ g)) y'
⊢ finrank (X := pullback f g) (pullback.snd f g) (i y') = finrank f (g (i y' : ↥Y))

Tactic:
rw [← Scheme.Hom.comp_apply, finrank_eq_finrank_snd_of_isAffine,
    finrank_eq_finrank_snd_of_isAffine, ← pullbackLeftPullbackSndIso_hom_snd f g i,
    ← finrank_eq_of_isAffine, ← finrank_eq_of_isAffine, finrank_comp_left_of_isIso]

Premises used: AlgebraicGeometry.Scheme.Hom.finrank_comp_left_of_isIso, AlgebraicGeometry.Scheme.Hom.comp_apply, _private.0.AlgebraicGeometry.Scheme.Hom.finrank_eq_finrank_snd_of_isAffine, CategoryTheory.Limits.pullbackLeftPullbackSndIso_hom_snd, _private.0.AlgebraicGeometry.Scheme.Hom.finrank_eq_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst : Flat f
inst_1 : IsFinite f
y : ↥Y
rw : finrank (CategoryStruct.comp (Y := pullback f g) (Iso.hom h.isoPullback) (pullback.snd f g)) y = finrank f (g y)
rw₁ : finrank (X := pullback f g) (pullback.snd f g) y = finrank f (g y)
rw₂ rw₃ : finrank f (g y) = finrank f (g y)
⊢ finrank snd y = finrank f (g y)

Tactic:
rw [← h.isoPullback_hom_snd, finrank_comp_left_of_isIso, finrank_pullback_snd]

Premises used: AlgebraicGeometry.Scheme.Hom.finrank_comp_left_of_isIso, AlgebraicGeometry.Scheme.Hom.finrank_pullback_snd, CategoryTheory.IsPullback.isoPullback_hom_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : Flat f
inst_1 : IsFinite f
y : ↥Y
⊢ finrank (X := pullback g f) (pullback.fst g f) y = finrank f (g y)

Tactic:
finrank_of_isPullback (pullback.snd g f) _ _ _ (.flip <| .of_hasPullback _ _) y

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.Scheme.Hom.finrank_of_isPullback, CategoryTheory.IsPullback.flip, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
x : ↥X
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
        1 ≤ finrank f (f x))
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), 1 ≤ finrank f (f x)
wlog :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    1 ≤ finrank f (f x)
⊢ 1 ≤ finrank f (f x)

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
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    1 ≤ finrank f (f x)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
inr :
  ∀ (R : CommRingCat.{u}) (g : Spec R ⟶ Y) (hg : IsOpenImmersion g) (y : ↥(Spec R))
    (hy : Eq (α := ↥Y) (g y : ↥Y) (f x : ↥Y)), 1 ≤ finrank f (f x)
⊢ 1 ≤ finrank f (f x)

Tactic:
obtain ⟨R, g, hg, y, hy⟩ := Y.exists_Spec_apply_eq (f x)

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.exists_Spec_apply_eq, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    1 ≤ finrank f (f x)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : Eq (α := ↥Y) (g y : ↥Y) (f x : ↥Y)
inr : 1 ≤ finrank (X := pullback f g) (pullback.snd f g) y
⊢ 1 ≤ finrank f (f x)

Tactic:
rw [← hy, ← 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
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    1 ≤ finrank f (f x)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : Eq (α := ↥Y) (g y : ↥Y) (f x : ↥Y)
inr :
  ∀ (z : ↥(pullback f g)) (hzl : (pullback.fst f g) z = x) (hzr : (pullback.snd f g) z = y),
    1 ≤ finrank (X := pullback f g) (pullback.snd f g) y
⊢ 1 ≤ finrank (X := pullback f g) (pullback.snd f g) y

Tactic:
obtain ⟨z, hzl, hzr⟩ := Scheme.Pullback.exists_preimage_pullback (f := f) (g := g) x y hy.symm

Premises used: Eq.symm, AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    1 ≤ finrank f (f x)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : Eq (α := ↥Y) (g y : ↥Y) (f x : ↥Y)
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
inr : 1 ≤ finrank (X := pullback f g) (pullback.snd f g) ((pullback.snd f g) z)
⊢ 1 ≤ finrank (X := pullback f g) (pullback.snd f g) y

Tactic:
rw [hzr.symm]

Premises used: Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    1 ≤ finrank f (f x)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : Eq (α := ↥Y) (g y : ↥Y) (f x : ↥Y)
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
⊢ 1 ≤ finrank (X := pullback f g) (pullback.snd f g) ((pullback.snd f g) z)

Tactic:
this _ _ ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
x : ↥X
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (x : ↥X) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    1 ≤ finrank f (f x)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
R : CommRingCat
g : Spec R ⟶ Y
hg : IsOpenImmersion g
y : ↥(Spec R)
hy : Eq (α := ↥Y) (g y : ↥Y) (f x : ↥Y)
z : ↥(pullback f g)
hzl : (pullback.fst f g) z = x
hzr : (pullback.snd f g) z = y
⊢ 1 ≤ finrank (X := pullback f g) (pullback.snd f g) ((pullback.snd f g) z)

Tactic:
refine this _ _ ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
x : ↥X
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f], 1 ≤ finrank f (f x)
⊢ 1 ≤ finrank f (f x)

Tactic:
obtain ⟨R, rfl⟩ := hY

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

Tactic:
wlog hX : ∃ S, X = Spec S
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
this :
  ∀ {X : Scheme.{u}} (x : ↥X) (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), 1 ≤ finrank f (f x)
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
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
this :
  ∀ {X : Scheme.{u}} (x : ↥X) (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), 1 ≤ finrank f (f x)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h : IsAffine X
⊢ Eq (α := ↥(Spec R)) (f x : ↥(Spec R)) ((X.isoSpec.inv ≫ f) (X.isoSpec.hom x) : ↥(Spec R))

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

Tactic:
have heq : f x = (X.isoSpec.inv ≫ f) (X.isoSpec.hom x) := by simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
this :
  ∀ {X : Scheme.{u}} (x : ↥X) (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f]
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), 1 ≤ finrank f (f x)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h : IsAffine X
heq : Eq (α := ↥(Spec R)) (f x : ↥(Spec R)) ((X.isoSpec.inv ≫ f) (X.isoSpec.hom x) : ↥(Spec R))
inr : 1 ≤ finrank (X.isoSpec.inv ≫ f) ((X.isoSpec.inv ≫ f) (X.isoSpec.hom x))
⊢ 1 ≤ finrank f (f x)

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

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

Tactic:
this _ _ _ ⟨_, rfl⟩

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

Tactic:
exact this _ _ _ ⟨_, rfl⟩

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

Tactic:
obtain ⟨S, rfl⟩ := hX

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

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

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : IsFinite (Spec.map φ)
⊢ (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
x : ↥(Spec S)
φ : R ⟶ S
inst_1 : Flat (Spec.map φ)
inst_2 : IsFinite (Spec.map φ)
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
x : ↥(Spec S)
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
rw : 1 ≤ (CommRingCat.Hom.hom φ).finrank ((Spec.map φ) x)
⊢ 1 ≤ finrank (Spec.map φ) ((Spec.map φ) x)

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

Premises used: AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_eq_finrank
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
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
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)
⊢ 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
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)
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))
⊢ 1 ≤ (CommRingCat.Hom.hom φ).finrank ((Spec.map φ) x)

Tactic:
rw [← RingHom.algebraMap_toAlgebra φ.hom, RingHom.finrank_algebraMap, Nat.add_one_le_iff,
    PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap]

Premises used: CommRingCat.Hom.hom, RingHom.finrank_algebraMap, Nat.add_one_le_iff, RingHom.algebraMap_toAlgebra, PrimeSpectrum.rankAtStalk_pos_iff_mem_range_comap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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)
h :
  Eq (α := PrimeSpectrum (↑R : Type u)) (PrimeSpectrum.comap (algebraMap (↑R : Type u) (↑S : Type u)) x)
    ((Spec.map φ) x)
⊢ 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:
use x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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)
⊢ Eq (α := PrimeSpectrum (↑R : Type u)) (PrimeSpectrum.comap (algebraMap (↑R : Type u) (↑S : Type u)) x)
    ((Spec.map φ) x)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
⊢ 1 ≤ finrank f ↔ Surjective f

Tactic:
⟨fun h ↦ ?_, fun _ ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
refine_1 : ∀ (h : 1 ≤ finrank f), Surjective f
refine_2 : Surjective f → 1 ≤ finrank f
⊢ 1 ≤ finrank f ↔ Surjective f

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
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
⊢ Surjective 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
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
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)
⊢ Surjective f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @Surjective) Y.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- 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
⊢ Surjective (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) (pullback.snd f (Y.affineCover.f i))

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

Premises used: Exists.intro, rfl
-- 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
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
⊢ Surjective (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i) (pullback.snd f (Y.affineCover.f i))

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

Premises used: Exists.intro, rfl