awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X S Y : Scheme
f : X ⟶ Y
g : Y ⟶ S
inst : IsIso f
inst_1 : Flat g
inst_2 : IsFinite g
⊢ finrank (f ≫ g) = finrank g
have h : ∀ (z : ↥S), finrank (f ≫ g) z = finrank g z
Tactic: ext z
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
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)))))
⊢ finrank (f ≫ g) z = finrank g z
have this : 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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)))))
this :
  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))
⊢ finrank (f ≫ g) z = finrank g z
have h : IsAffine.finrank (X :=
    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.snd (f ≫ g) (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))
    (Exists.choose (p :=
      fun (y : ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)))) ↦
      (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) z)) y = z) sorry) =
  finrank g z
Tactic: rw [finrank, finrank, ← this, IsAffine.finrank_comp_left_of_isIso]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : Flat f
inst_1 : IsFinite f
y : ↥Y
⊢ finrank (X := pullback f g) (pullback.snd f g) y = finrank f (g y)
have 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))
Tactic: obtain ⟨R, i, _, y', rfl⟩ := Y.exists_Spec_apply_eq y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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)
⊢ finrank (X := pullback f g) (pullback.snd f g) (i y') = finrank f (g (i y' : ↥Y))
have rw : finrank (X := pullback f g) (pullback.snd f g) (i y') = finrank f ((i ≫ g) 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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')
⊢ finrank (X := pullback f g) (pullback.snd f g) (i y') = finrank f (g (i y' : ↥Y))
have 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')
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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')
⊢ finrank (X := pullback f g) (pullback.snd f g) (i y') = finrank f (g (i y' : ↥Y))
have 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'
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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'
⊢ finrank (X := pullback f g) (pullback.snd f g) (i y') = finrank f (g (i y' : ↥Y))
have 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'
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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'
⊢ finrank (X := pullback f g) (pullback.snd f g) (i y') = finrank f (g (i y' : ↥Y))
have 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'
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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'
⊢ finrank (X := pullback f g) (pullback.snd f g) (i y') = finrank f (g (i y' : ↥Y))
have 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'
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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'
⊢ finrank (X := pullback f g) (pullback.snd f g) (i y') = finrank f (g (i y' : ↥Y))
have 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'
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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
⊢ finrank snd y = finrank f (g y)
have rw : finrank (CategoryStruct.comp (Y := pullback f g) (Iso.hom h.isoPullback) (pullback.snd f g)) y = finrank f (g y)
Tactic: rw [← h.isoPullback_hom_snd, finrank_comp_left_of_isIso, finrank_pullback_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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)
⊢ finrank snd y = finrank f (g y)
have rw₁ : finrank (X := pullback f g) (pullback.snd f g) y = finrank f (g y)
Tactic: rw [← h.isoPullback_hom_snd, finrank_comp_left_of_isIso, finrank_pullback_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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)
⊢ finrank snd y = finrank f (g y)
have rw₂ : finrank f (g y) = finrank f (g y)
Tactic: rw [← h.isoPullback_hom_snd, finrank_comp_left_of_isIso, 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
x : ↥X
⊢ 1 ≤ finrank f (f x)
have 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)
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
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)
⊢ 1 ≤ finrank f (f x)
have 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)
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, inst, inst_1, 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
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
⊢ 1 ≤ finrank f (f x)
have 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)
Tactic: obtain ⟨R, g, hg, y, hy⟩ := Y.exists_Spec_apply_eq (f 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
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)
⊢ 1 ≤ finrank f (f x)
have inr : 1 ≤ finrank (X := pullback f g) (pullback.snd f g) y
Tactic: rw [← hy, ← 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
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)
⊢ 1 ≤ finrank (X := pullback f g) (pullback.snd f g) y
have 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
Tactic: obtain ⟨z, hzl, hzr⟩ := Scheme.Pullback.exists_preimage_pullback (f := f) (g := g) x y hy.symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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) y
have inr : 1 ≤ finrank (X := pullback f g) (pullback.snd f g) ((pullback.snd f g) z)
Tactic: rw [hzr.symm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
x : ↥X
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ 1 ≤ finrank f (f x)
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f], 1 ≤ finrank f (f x)
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, inst_1, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X : Scheme
x : ↥X
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
⊢ 1 ≤ finrank f (f x)
have 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)
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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)
⊢ 1 ≤ finrank f (f x)
have 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)
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, x, R, f, inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
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
⊢ 1 ≤ finrank f (f x)
have x₁ : IsAffine X
Tactic: have _ : IsAffine X := isAffine_of_isAffineHom f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
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
⊢ 1 ≤ finrank f (f x)
have heq : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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 f (f x)
have inr : 1 ≤ finrank (X.isoSpec.inv ≫ f) ((X.isoSpec.inv ≫ f) (X.isoSpec.hom x))
Tactic: rw [← finrank_comp_left_of_isIso X.isoSpec.inv, heq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
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
⊢ 1 ≤ finrank f (f x)
have obtain : ∀ (S : CommRingCat.{u}) (x : ↥(Spec S)) (f : Spec S ⟶ Spec R) [Flat f] [IsFinite f], 1 ≤ finrank f (f x)
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, x, f, inst, inst_1, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
x : ↥(Spec S)
f : Spec S ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
⊢ 1 ≤ finrank f (f x)
have obtain : ∀ (φ : R ⟶ S) [Flat (Spec.map φ)] [IsFinite (Spec.map φ)], 1 ≤ finrank (Spec.map φ) ((Spec.map φ) x)
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : IsFinite (Spec.map φ)
⊢ 1 ≤ finrank (Spec.map φ) ((Spec.map φ) 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
x : ↥(Spec S)
φ : R ⟶ S
inst_1 : Flat (Spec.map φ)
inst_2 : IsFinite (Spec.map φ)
inst : (CommRingCat.Hom.hom φ).Flat
⊢ 1 ≤ finrank (Spec.map φ) ((Spec.map φ) 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 (goal)
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
⊢ 1 ≤ finrank (Spec.map φ) ((Spec.map φ) x)
have rw : 1 ≤ (CommRingCat.Hom.hom φ).finrank ((Spec.map φ) x)
Tactic: rw [finrank_SpecMap_eq_finrank ‹_› ‹_›]
-- 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
⊢ 1 ≤ (CommRingCat.Hom.hom φ).finrank ((Spec.map φ) x)
have algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
Tactic: algebraize [φ.hom]