awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst : IsAffine T
t : ↥T
inst_1 : Flat f
inst_2 : IsFinite f
i : Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) ⟶ S :=
  S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl :
  Eq (α := ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
    ((pullback.fst (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) g)
        (u z) :
      ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
    (Exists.choose (p :=
        fun
          (y :
            ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))))) ↦
        Eq (α := ↥S)
          ((S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) y : ↥S)
          (g t : ↥S))
        ⋯ :
      ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
hyr :
  (pullback.snd (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) g)
      (u z : ↥(pullback i g)) =
    t
refine_1 :
  pullback (X := pullback f g) (pullback.snd f g) (u ≫ pullback.snd i g) ⟶
    pullback (Y :=
      Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))) f
      (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))
⊢ finrank f (g t) =
    IsAffine.finrank (X := pullback (X := pullback f g) (pullback.snd f g) (u ≫ pullback.snd i g))
      (pullback.snd (pullback.snd f g) (u ≫ pullback.snd i g)) z
have refine_2 : Spec R ⟶ Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))
Tactic: refine (IsAffine.finrank_of_isPullback _ _ ?_ ?_ ?_ _ _ ?_).symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst : IsAffine T
t : ↥T
inst_1 : Flat f
inst_2 : IsFinite f
i : Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) ⟶ S :=
  S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl :
  Eq (α := ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
    ((pullback.fst (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) g)
        (u z) :
      ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
    (Exists.choose (p :=
        fun
          (y :
            ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))))) ↦
        Eq (α := ↥S)
          ((S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) y : ↥S)
          (g t : ↥S))
        ⋯ :
      ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
hyr :
  (pullback.snd (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) g)
      (u z : ↥(pullback i g)) =
    t
refine_1 :
  pullback (X := pullback f g) (pullback.snd f g) (u ≫ pullback.snd i g) ⟶
    pullback (Y :=
      Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))) f
      (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))
refine_2 :
  Spec R ⟶ Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))
⊢ finrank f (g t) =
    IsAffine.finrank (X := pullback (X := pullback f g) (pullback.snd f g) (u ≫ pullback.snd i g))
      (pullback.snd (pullback.snd f g) (u ≫ pullback.snd i g)) z
have refine_3 : IsPullback (P := pullback (X := pullback f g) (pullback.snd f g) (u ≫ pullback.snd i g)) (X :=
  pullback (Y := Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))))
    f (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))))
  (pullback.map (pullback.snd f g) (u ≫ pullback.snd i g) f
    (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) (pullback.fst f g)
    (u ≫ pullback.fst i g) g sorry sorry)
  (pullback.snd (pullback.snd f g) (u ≫ pullback.snd i g))
  (pullback.snd f (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))))
  (u ≫ pullback.fst i g)
Tactic: refine (IsAffine.finrank_of_isPullback _ _ ?_ ?_ ?_ _ _ ?_).symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst : IsAffine T
t : ↥T
inst_1 : Flat f
inst_2 : IsFinite f
i : Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) ⟶ S :=
  S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl :
  Eq (α := ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
    ((pullback.fst (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) g)
        (u z) :
      ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
    (Exists.choose (p :=
        fun
          (y :
            ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))))) ↦
        Eq (α := ↥S)
          ((S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) y : ↥S)
          (g t : ↥S))
        ⋯ :
      ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
hyr :
  (pullback.snd (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) g)
      (u z : ↥(pullback i g)) =
    t
⊢ (u ≫ pullback.snd i g) ≫ g =
    (u ≫ pullback.fst i g) ≫
      S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))
have simp : u ≫ pullback.fst i g ≫ i =
  u ≫
    pullback.fst i g ≫
      S.affineCover.f
        (Exists.choose (p := fun (i : S.affineCover.I₀) ↦
          ∃ (y : ↥(S.affineCover.X i)), Eq (α := ↥S) ((S.affineCover.f i) y : ↥S) (g t : ↥S)) sorry)
Tactic: simp [← pullback.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X S T : Scheme
f : X ⟶ S
g : T ⟶ S
inst : IsAffine T
t : ↥T
inst_1 : Flat f
inst_2 : IsFinite f
i : Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) ⟶ S :=
  S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))
R : CommRingCat
u : Spec R ⟶ pullback i g
hu : IsOpenImmersion u
z : ↥(Spec R)
hyl :
  Eq (α := ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
    ((pullback.fst (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) g)
        (u z) :
      ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
    (Exists.choose (p :=
        fun
          (y :
            ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))))) ↦
        Eq (α := ↥S)
          ((S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) y : ↥S)
          (g t : ↥S))
        ⋯ :
      ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
hyr :
  (pullback.snd (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) g)
      (u z : ↥(pullback i g)) =
    t
⊢ IsAffine.finrank (X := pullback (X := pullback f g) (pullback.snd f g) (u ≫ pullback.snd i g))
      (pullback.snd (pullback.snd f g) (u ≫ pullback.snd i g)) z =
    IsAffine.finrank (X := pullback f g) (pullback.snd f g) t
have simp_rw : IsAffine.finrank (X := pullback (X := pullback f g) (pullback.snd f g) (u ≫ pullback.snd i g))
    (pullback.snd (pullback.snd f g) (u ≫ pullback.snd i g)) z =
  IsAffine.finrank (X := pullback f g) (pullback.snd f g)
    ((pullback.snd (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t))) g)
      (u z : ↥(pullback i g)))
Tactic: simp_rw [← hyr]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X S : Scheme
f : X ⟶ S
inst : IsAffine S
inst_1 : Flat f
inst_2 : IsFinite f
s : ↥S
⊢ finrank f s = IsAffine.finrank f s
have rw : finrank f ((𝟙 S) s) = IsAffine.finrank f ((𝟙 S) s)
Tactic: rw [show s = (𝟙 S : S ⟶ S) s from rfl, finrank_eq_finrank_snd_of_isAffine,
    IsAffine.finrank_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X S : Scheme
f : X ⟶ S
inst : IsAffine S
inst_1 : Flat f
inst_2 : IsFinite f
s : ↥S
rw : finrank f ((𝟙 S) s) = IsAffine.finrank f ((𝟙 S) s)
⊢ finrank f s = IsAffine.finrank f s
have rw₁ : IsAffine.finrank (X := pullback f (𝟙 S)) (pullback.snd f (𝟙 S)) s = IsAffine.finrank f ((𝟙 S) s)
Tactic: rw [show s = (𝟙 S : S ⟶ S) s from rfl, finrank_eq_finrank_snd_of_isAffine,
    IsAffine.finrank_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
X S : Scheme
f : X ⟶ S
inst : IsAffine S
inst_1 : Flat f
inst_2 : IsFinite f
s : ↥S
rw : finrank f ((𝟙 S) s) = IsAffine.finrank f ((𝟙 S) s)
rw₁ : IsAffine.finrank (X := pullback f (𝟙 S)) (pullback.snd f (𝟙 S)) s = IsAffine.finrank f ((𝟙 S) s)
⊢ finrank f s = IsAffine.finrank f s
have rw₂ : IsAffine.finrank f ((𝟙 S) s) = IsAffine.finrank f ((𝟙 S) s)
Tactic: rw [show s = (𝟙 S : S ⟶ S) s from rfl, finrank_eq_finrank_snd_of_isAffine,
    IsAffine.finrank_snd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁ : (CommRingCat.Hom.hom f).Finite
hf₂ : (CommRingCat.Hom.hom f).Flat
⊢ finrank (Spec.map f) = (CommRingCat.Hom.hom f).finrank
have hf₃ : IsFinite (Spec.map f)
Tactic: simp only [← IsFinite.SpecMap_iff, ← Flat.SpecMap_iff] at hf₁ hf₂
Cleared hypotheses: hf₁, hf₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁ : (CommRingCat.Hom.hom f).Finite
hf₂ : (CommRingCat.Hom.hom f).Flat
hf₃ : IsFinite (Spec.map f)
⊢ finrank (Spec.map f) = (CommRingCat.Hom.hom f).finrank
have hf₄ : Flat (Spec.map f)
Tactic: simp only [← IsFinite.SpecMap_iff, ← Flat.SpecMap_iff] at hf₁ hf₂
Cleared hypotheses: hf₁, hf₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁ : IsFinite (Spec.map f)
hf₂ : Flat (Spec.map f)
⊢ finrank (Spec.map f) = (CommRingCat.Hom.hom f).finrank
have hf₃ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
Tactic: have hf₁ : (Spec.map f).appTop.hom.Finite := (Spec.map f).finite_appTop
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁_1 : IsFinite (Spec.map f)
hf₂ : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
⊢ finrank (Spec.map f) = (CommRingCat.Hom.hom f).finrank
have hf₃ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
Tactic: have hf₂ : (Spec.map f).appTop.hom.Flat := (Spec.map f).flat_appTop
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁_1 : IsFinite (Spec.map f)
hf₂_1 : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
⊢ finrank (Spec.map f) = (CommRingCat.Hom.hom f).finrank
have h : ∀ (x : ↥(Spec R)), finrank (Spec.map f) x = (CommRingCat.Hom.hom f).finrank x
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁_1 : IsFinite (Spec.map f)
hf₂_1 : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x : ↥(Spec R)
⊢ finrank (Spec.map f) x = (CommRingCat.Hom.hom f).finrank x
have h : (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) = (CommRingCat.Hom.hom f).finrank x
Tactic: rw [finrank_eq_of_isAffine, IsAffine.finrank]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (hypothesis)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁_1 : IsFinite (Spec.map f)
hf₂_1 : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x : ↥(Spec R)
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) = (CommRingCat.Hom.hom f).finrank x
have this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
Tactic: have : f = (Scheme.ΓSpecIso R).inv ≫ (Spec.map f).appTop ≫ (Scheme.ΓSpecIso S).hom := by simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁_1 : IsFinite (Spec.map f)
hf₂_1 : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
| (CommRingCat.Hom.hom f).finrank x
have rw : (CommRingCat.Hom.hom ((ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom)).finrank x
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁_1 : IsFinite (Spec.map f)
hf₂_1 : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) = (CommRingCat.Hom.hom f).finrank x
have h : (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
  (CommRingCat.Hom.hom ((ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom)).finrank x
Tactic: conv_rhs => rw [this]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁_1 : IsFinite (Spec.map f)
hf₂_1 : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
    (((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).comp
          (CommRingCat.Hom.hom (ΓSpecIso R).inv)).finrank
      x
have h : (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
  ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).finrank
    ((Iso.hom (Spec R).isoSpec) x)
Tactic: rw [RingHom.finrank_comp_right_of_bijective _ _ (ConcreteCategory.bijective_of_isIso _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁_1 : IsFinite (Spec.map f)
hf₂_1 : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
h :
  (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
    ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).finrank
      ((Iso.hom (Spec R).isoSpec) x)
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
    (((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).comp
          (CommRingCat.Hom.hom (ΓSpecIso R).inv)).finrank
      x
have h₁ : ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).Finite
Tactic: rw [RingHom.finrank_comp_right_of_bijective _ _ (ConcreteCategory.bijective_of_isIso _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁_1 : IsFinite (Spec.map f)
hf₂_1 : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
h :
  (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
    ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).finrank
      ((Iso.hom (Spec R).isoSpec) x)
h₁ : ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).Finite
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
    (((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).comp
          (CommRingCat.Hom.hom (ΓSpecIso R).inv)).finrank
      x
have h₂ : ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).Flat
Tactic: rw [RingHom.finrank_comp_right_of_bijective _ _ (ConcreteCategory.bijective_of_isIso _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁_1 : IsFinite (Spec.map f)
hf₂_1 : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
h :
  (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
    ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).finrank
      ((Iso.hom (Spec R).isoSpec) x)
h₁ : ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).Finite
h₂ : ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).Flat
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
    (((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).comp
          (CommRingCat.Hom.hom (ΓSpecIso R).inv)).finrank
      x
have h₃ : PrimeSpectrum (↑Γ(Spec R, ⊤) : Type u)
Tactic: rw [RingHom.finrank_comp_right_of_bijective _ _ (ConcreteCategory.bijective_of_isIso _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁_1 : IsFinite (Spec.map f)
hf₂_1 : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
h :
  (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
    ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).finrank
      ((Iso.hom (Spec R).isoSpec) x)
h₁ : ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).Finite
h₂ : ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).Flat
h₃ : PrimeSpectrum (↑Γ(Spec R, ⊤) : Type u)
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
    (((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).comp
          (CommRingCat.Hom.hom (ΓSpecIso R).inv)).finrank
      x
have h₄ : x = PrimeSpectrum.comap (CommRingCat.Hom.hom (ΓSpecIso R).inv) ((Iso.hom (Spec R).isoSpec) x)
Tactic: rw [RingHom.finrank_comp_right_of_bijective _ _ (ConcreteCategory.bijective_of_isIso _)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁_1 : IsFinite (Spec.map f)
hf₂_1 : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
    ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).finrank
      ((Iso.hom (Spec R).isoSpec) x)
have h : (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
  (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x)
Tactic: rw [RingHom.finrank_comp_left_of_bijective _ _ (ConcreteCategory.bijective_of_isIso _) hf₁ hf₂]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁_1 : IsFinite (Spec.map f)
hf₂_1 : Flat (Spec.map f)
hf₁ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite
hf₂ : (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat
x : ↥(Spec R)
this : f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom
h :
  (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
    (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x)
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) =
    ((CommRingCat.Hom.hom (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).finrank
      ((Iso.hom (Spec R).isoSpec) x)
have h₁ : PrimeSpectrum (↑Γ(Spec R, ⊤) : Type u)
Tactic: rw [RingHom.finrank_comp_left_of_bijective _ _ (ConcreteCategory.bijective_of_isIso _) hf₁ hf₂]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Module.Flat R S
x : PrimeSpectrum R
⊢ finrank (X := Spec (CommRingCat.of S)) (Spec.map (CommRingCat.ofHom (algebraMap R S))) x = Module.rankAtStalk S x
have rw : RingHom.finrank (S := (↑(CommRingCat.of S) : Type u)) (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))) x =
  Module.rankAtStalk S x
Tactic: rw [finrank_SpecMap_eq_finrank]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Module.Flat R S
x : PrimeSpectrum R
rw :
  RingHom.finrank (S := (↑(CommRingCat.of S) : Type u)) (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))) x =
    Module.rankAtStalk S x
⊢ finrank (X := Spec (CommRingCat.of S)) (Spec.map (CommRingCat.ofHom (algebraMap R S))) x = Module.rankAtStalk S x
have hf₁ : RingHom.Finite (A := (↑(CommRingCat.of R) : Type u)) (B := (↑(CommRingCat.of S) : Type u))
  (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S)))
Tactic: rw [finrank_SpecMap_eq_finrank]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.FlatRank (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Module.Finite R S
inst_4 : Module.Flat R S
x : PrimeSpectrum R
rw :
  RingHom.finrank (S := (↑(CommRingCat.of S) : Type u)) (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))) x =
    Module.rankAtStalk S x
hf₁ :
  RingHom.Finite (A := (↑(CommRingCat.of R) : Type u)) (B := (↑(CommRingCat.of S) : Type u))
    (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S)))
⊢ finrank (X := Spec (CommRingCat.of S)) (Spec.map (CommRingCat.ofHom (algebraMap R S))) x = Module.rankAtStalk S x
have hf₂ : RingHom.Flat (R := (↑(CommRingCat.of R) : Type u)) (S := (↑(CommRingCat.of S) : Type u))
  (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S)))
Tactic: rw [finrank_SpecMap_eq_finrank]