awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
⊢ Eq (α := ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
    ((u ≫ pullback.fst i g) 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)))))

Tactic:
hyl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
⊢ Eq (α := ↥(Spec (S.affineOpenCover.X (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))))
    ((u ≫ pullback.fst i g) 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)))))

Tactic:
exact hyl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
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)))
⊢ 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

Tactic:
simp_rw [← hyr]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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)
      ((pullback.snd (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))
          g)
        (u z : ↥(pullback i g)))

Tactic:
IsAffine.finrank_snd (pullback.snd f g) (u ≫ pullback.snd _ _) z

Premises used: Set.Mem, _private.0.AlgebraicGeometry.IsAffine.finrank_snd, CategoryTheory.Limits.pullback.snd, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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)
      ((pullback.snd (S.affineOpenCover.f (P := IsOpenImmersion) (S.affineOpenCover.idx (P := IsOpenImmersion) (g t)))
          g)
        (u z : ↥(pullback i g)))

Tactic:
exact IsAffine.finrank_snd (pullback.snd f g) (u ≫ pullback.snd _ _) z

Premises used: _private.0.AlgebraicGeometry.IsAffine.finrank_snd, CategoryTheory.Limits.pullback.snd, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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)
rw₂ rw₃ : IsAffine.finrank f ((𝟙 S) s) = IsAffine.finrank f ((𝟙 S) s)
⊢ finrank f s = IsAffine.finrank f s

Tactic:
rw [show s = (𝟙 S : S ⟶ S) s from rfl, finrank_eq_finrank_snd_of_isAffine,
    IsAffine.finrank_snd]

Premises used: _private.0.AlgebraicGeometry.IsAffine.finrank_snd, _private.0.AlgebraicGeometry.Scheme.Hom.finrank_eq_finrank_snd_of_isAffine, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁ : (CommRingCat.Hom.hom f).Finite
hf₂ : (CommRingCat.Hom.hom f).Flat
⊢ IsFinite (Spec.map f)

Tactic:
simp only [← IsFinite.SpecMap_iff, ← Flat.SpecMap_iff] at hf₁ hf₂

Premises used: AlgebraicGeometry.IsFinite.SpecMap_iff, AlgebraicGeometry.Flat.SpecMap_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁ : (CommRingCat.Hom.hom f).Finite
hf₂ : (CommRingCat.Hom.hom f).Flat
hf₃ : IsFinite (Spec.map f)
⊢ Flat (Spec.map f)

Tactic:
simp only [← IsFinite.SpecMap_iff, ← Flat.SpecMap_iff] at hf₁ hf₂

Premises used: AlgebraicGeometry.IsFinite.SpecMap_iff, AlgebraicGeometry.Flat.SpecMap_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
f : R ⟶ S
hf₁ : IsFinite (Spec.map f)
hf₂ : Flat (Spec.map f)
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).Finite

Tactic:
have hf₁ : (Spec.map f).appTop.hom.Finite := (Spec.map f).finite_appTop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).Flat

Tactic:
have hf₂ : (Spec.map f).appTop.hom.Flat := (Spec.map f).flat_appTop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
h : ∀ (x : ↥(Spec R)), finrank (Spec.map f) x = (CommRingCat.Hom.hom f).finrank x
⊢ finrank (Spec.map f) = (CommRingCat.Hom.hom f).finrank

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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)
h :
  (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) = (CommRingCat.Hom.hom f).finrank x
⊢ finrank (Spec.map f) x = (CommRingCat.Hom.hom f).finrank x

Tactic:
rw [finrank_eq_of_isAffine, IsAffine.finrank]

Premises used: _private.0.AlgebraicGeometry.IsAffine.finrank, _private.0.AlgebraicGeometry.Scheme.Hom.finrank_eq_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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)
⊢ f = (ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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)
⊢ 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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
rw : (CommRingCat.Hom.hom ((ΓSpecIso R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom)).finrank x
| (CommRingCat.Hom.hom f).finrank x

Tactic:
rw [this]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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 R).inv ≫ appTop (Spec.map f) ≫ (ΓSpecIso S).hom)).finrank x
⊢ (CommRingCat.Hom.hom (appTop (Spec.map f))).finrank ((Iso.hom (Spec R).isoSpec) x) = (CommRingCat.Hom.hom f).finrank x

Tactic:
conv_rhs => rw [this]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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)
h₄ : x = PrimeSpectrum.comap (CommRingCat.Hom.hom (ΓSpecIso R).inv) ((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

Tactic:
rw [RingHom.finrank_comp_right_of_bijective _ _ (ConcreteCategory.bijective_of_isIso _)]

Premises used: RingHom.finrank_comp_right_of_bijective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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)
h₁ : PrimeSpectrum (↑Γ(Spec R, ⊤) : Type u)
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)
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)))).finrank
      ((Iso.hom (Spec R).isoSpec) x)

Tactic:
rw [RingHom.finrank_comp_left_of_bijective _ _ (ConcreteCategory.bijective_of_isIso _) hf₁ hf₂]

Premises used: RingHom.finrank_comp_left_of_bijective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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 (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).Finite

Tactic:
.comp (.of_surjective _ (ConcreteCategory.bijective_of_isIso _).surjective) hf₁

Premises used: RingHom.Finite.comp, RingHom.Finite.of_surjective, Function.Bijective.surjective, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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 (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).Finite

Tactic:
exact .comp (.of_surjective _ (ConcreteCategory.bijective_of_isIso _).surjective) hf₁
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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 (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).Flat

Tactic:
.comp hf₂ (.of_bijective (ConcreteCategory.bijective_of_isIso _))

Premises used: RingHom.Flat.comp, RingHom.Flat.of_bijective, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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 (ΓSpecIso S).hom).comp (CommRingCat.Hom.hom (appTop (Spec.map f)))).Flat

Tactic:
exact .comp hf₂ (.of_bijective (ConcreteCategory.bijective_of_isIso _))
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
⊢ x = PrimeSpectrum.comap (CommRingCat.Hom.hom (ΓSpecIso R).inv) ((Iso.hom (Spec R).isoSpec) x)

Tactic:
simp [isoSpec_Spec_hom, SpecMap_ΓSpecIso_hom, ← AlgebraicGeometry.Spec.map_apply,
      ← Scheme.Hom.comp_apply, toSpecΓ_SpecMap_ΓSpecIso_inv]

Premises used: AlgebraicGeometry.SpecMap_ΓSpecIso_hom, AlgebraicGeometry.Scheme.isoSpec_Spec_hom, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Spec.map_apply, AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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)))
hf₂ :
  RingHom.Flat (R := (↑(CommRingCat.of R) : Type u)) (S := (↑(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

Tactic:
rw [finrank_SpecMap_eq_finrank]

Premises used: AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_eq_finrank
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
⊢ RingHom.finrank (S := (↑(CommRingCat.of S) : Type u)) (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S))) x =
    Module.rankAtStalk S x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
⊢ RingHom.Finite (A := (↑(CommRingCat.of R) : Type u)) (B := (↑(CommRingCat.of S) : Type u))
    (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S)))

Tactic:
simpa [RingHom.finite_algebraMap]

Premises used: RingHom.finite_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
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
⊢ RingHom.Flat (R := (↑(CommRingCat.of R) : Type u)) (S := (↑(CommRingCat.of S) : Type u))
    (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap R S)))

Tactic:
simpa [RingHom.flat_algebraMap_iff]

Premises used: RingHom.flat_algebraMap_iff
-- 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
h : ∀ (z : ↥S), finrank (f ≫ g) z = finrank g z
⊢ finrank (f ≫ g) = finrank g

Tactic:
ext z