awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
inst_2 : LocallyOfFinitePresentation f
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain :
  ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [Flat f] [IsFinite f] [LocallyOfFinitePresentation f],
    IsLocallyConstant (finrank f)
⊢ IsLocallyConstant (finrank f)

Tactic:
obtain ⟨S, rfl⟩ := hX

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

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

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : IsFinite (Spec.map φ)
inst_2 : LocallyOfFinitePresentation (Spec.map φ)
⊢ (CommRingCat.Hom.hom φ).Flat

Tactic:
simp only [Flat.SpecMap_iff, IsFinite.SpecMap_iff, LocallyOfFinitePresentation.SpecMap_iff] at *

Premises used: AlgebraicGeometry.IsFinite.SpecMap_iff, AlgebraicGeometry.LocallyOfFinitePresentation.SpecMap_iff, AlgebraicGeometry.Flat.SpecMap_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
inst_1 : Flat (Spec.map φ)
inst_2 : IsFinite (Spec.map φ)
inst_3 : LocallyOfFinitePresentation (Spec.map φ)
inst : (CommRingCat.Hom.hom φ).Flat
⊢ (CommRingCat.Hom.hom φ).Finite

Tactic:
simp only [Flat.SpecMap_iff, IsFinite.SpecMap_iff, LocallyOfFinitePresentation.SpecMap_iff] at *

Premises used: AlgebraicGeometry.IsFinite.SpecMap_iff, AlgebraicGeometry.LocallyOfFinitePresentation.SpecMap_iff, AlgebraicGeometry.Flat.SpecMap_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
inst_1 : Flat (Spec.map φ)
inst_2 : IsFinite (Spec.map φ)
inst_3 : LocallyOfFinitePresentation (Spec.map φ)
inst : (CommRingCat.Hom.hom φ).Flat
inst₁ : (CommRingCat.Hom.hom φ).Finite
⊢ (CommRingCat.Hom.hom φ).FinitePresentation

Tactic:
simp only [Flat.SpecMap_iff, IsFinite.SpecMap_iff, LocallyOfFinitePresentation.SpecMap_iff] at *

Premises used: AlgebraicGeometry.IsFinite.SpecMap_iff, AlgebraicGeometry.LocallyOfFinitePresentation.SpecMap_iff, AlgebraicGeometry.Flat.SpecMap_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
inst_2 : (CommRingCat.Hom.hom φ).FinitePresentation
rw : IsLocallyConstant (CommRingCat.Hom.hom φ).finrank
⊢ IsLocallyConstant (finrank (Spec.map φ))

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

Premises used: AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_eq_finrank
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
inst_2 : (CommRingCat.Hom.hom φ).FinitePresentation
⊢ 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
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
inst_2 : (CommRingCat.Hom.hom φ).FinitePresentation
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
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
inst_2 : (CommRingCat.Hom.hom φ).FinitePresentation
algebraizeInst : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst₁ : Module.Finite.{u, u} (↑R : Type u) (↑S : Type u)
⊢ Algebra.FinitePresentation.{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
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
inst_2 : (CommRingCat.Hom.hom φ).FinitePresentation
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)
algebraizeInst_2 : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
⊢ ∀ (R S : Type u) [inst : CommRing R] [inst_3 : CommRing S] [inst_4 : Algebra R S] [Module.Finite R S]
    [Algebra.FinitePresentation R S], Module.FinitePresentation R S

Tactic:
have := Module.FinitePresentation.of_finite_of_finitePresentation
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
inst_2 : (CommRingCat.Hom.hom φ).FinitePresentation
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)
algebraizeInst_2 : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
this :
  ∀ (R S : Type u) [inst : CommRing R] [inst_3 : CommRing S] [inst_4 : Algebra R S] [Module.Finite R S]
    [Algebra.FinitePresentation R S], Module.FinitePresentation R S
⊢ IsLocallyConstant (CommRingCat.Hom.hom φ).finrank

Tactic:
Module.isLocallyConstant_rankAtStalk

Premises used: Module.isLocallyConstant_rankAtStalk, RingHom.finrank
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).Flat
inst_1 : (CommRingCat.Hom.hom φ).Finite
inst_2 : (CommRingCat.Hom.hom φ).FinitePresentation
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)
algebraizeInst_2 : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
this :
  ∀ (R S : Type u) [inst : CommRing R] [inst_3 : CommRing S] [inst_4 : Algebra R S] [Module.Finite R S]
    [Algebra.FinitePresentation R S], Module.FinitePresentation R S
⊢ IsLocallyConstant (CommRingCat.Hom.hom φ).finrank

Tactic:
exact Module.isLocallyConstant_rankAtStalk

Premises used: Module.isLocallyConstant_rankAtStalk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
h : ∀ (y : ↥Y), finrank f y = 1 y
⊢ finrank f = 1

Tactic:
ext y
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
y : ↥Y
h : ∀ (R : CommRingCat.{u}) (g : Spec R ⟶ Y), IsOpenImmersion g → ∀ (y : ↥(Spec R)), finrank f (g y) = 1 (g y)
⊢ finrank f y = 1 y

Tactic:
obtain ⟨R, g, _, 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 : Scheme
f : X ⟶ Y
inst : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
y : ↥(Spec R)
⊢ Nontrivial.{u} (↑R : Type u)

Tactic:
have : Nontrivial R := y.nontrivial
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial.{u} (↑R : Type u)
h : Module.rankAtStalk (↑R : Type u) y = 1
h₁ : (CommRingCat.Hom.hom (𝟙 R)).Finite
h₂ : (CommRingCat.Hom.hom (𝟙 R)).Flat
⊢ finrank f (g y) = 1 (g y)

Tactic:
rw [← finrank_pullback_snd, ← Category.comp_id (pullback.snd f g), finrank_comp_left_of_isIso,
    ← Spec.map_id, finrank_SpecMap_eq_finrank, CommRingCat.hom_id, Pi.one_apply,
    ← Algebra.algebraMap_self, RingHom.finrank_algebraMap]

Premises used: Algebra.algebraMap_self, CategoryTheory.Limits.pullback.snd, Pi.one_apply, RingHom.finrank_algebraMap, AlgebraicGeometry.Spec.map_id, AlgebraicGeometry.Scheme.Hom.finrank_comp_left_of_isIso, CategoryTheory.Category.comp_id, AlgebraicGeometry.Scheme.Hom.finrank_pullback_snd, CommRingCat.hom_id, AlgebraicGeometry.Scheme.Hom.finrank_SpecMap_eq_finrank
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial.{u} (↑R : Type u)
⊢ Module.rankAtStalk (↑R : Type u) y = 1

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial.{u} (↑R : Type u)
⊢ (CommRingCat.Hom.hom (𝟙 R)).Finite

Tactic:
RingHom.Finite.id R

Premises used: CommRingCat.carrier, RingHom.Finite.id
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial.{u} (↑R : Type u)
⊢ (CommRingCat.Hom.hom (𝟙 R)).Finite

Tactic:
exact RingHom.Finite.id R

Premises used: CommRingCat.carrier, RingHom.Finite.id
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial.{u} (↑R : Type u)
⊢ (CommRingCat.Hom.hom (𝟙 R)).Flat

Tactic:
RingHom.Flat.id ↑R

Premises used: CommRingCat.carrier, RingHom.Flat.id
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
R : CommRingCat
g : Spec R ⟶ Y
w : IsOpenImmersion g
y : ↥(Spec R)
this : Nontrivial.{u} (↑R : Type u)
⊢ (CommRingCat.Hom.hom (𝟙 R)).Flat

Tactic:
exact RingHom.Flat.id ↑R

Premises used: CommRingCat.carrier, RingHom.Flat.id
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
⊢ IsIso f ↔ finrank f = 1

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

Premises used: AlgebraicGeometry.Scheme.Hom.finrank_eq_one_of_isIso, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
refine : ∀ (h : finrank f = 1), IsIso f
⊢ IsIso f ↔ finrank f = 1

Tactic:
refine ⟨fun h ↦ finrank_eq_one_of_isIso f, fun h ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1)
        (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsIso f)
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsIso f
wlog :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIso f
⊢ IsIso 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 : finrank f = 1
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIso f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
inr :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    MorphismProperty.isomorphisms Scheme (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)
⊢ IsIso f

Tactic:
rw [← MorphismProperty.isomorphisms.iff,
      IsZariskiLocalAtTarget.iff_of_openCover (P := .isomorphisms Scheme) Y.affineCover]

Premises used: CategoryTheory.MorphismProperty.isomorphisms.iff, 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 : finrank f = 1
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIso f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ MorphismProperty.isomorphisms Scheme (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i))

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
h : finrank f = 1
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIso f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
inr : finrank (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) = 1
⊢ MorphismProperty.isomorphisms Scheme (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i))

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
h : finrank f = 1
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIso f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
inr :
  ∀ (y : ↥(Y.affineCover.X i)),
    finrank (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) y = 1 y
⊢ finrank (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) = 1

Tactic:
ext y
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [Flat f] [IsFinite f] (h : finrank f = 1) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsIso f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
inr : finrank f ((Y.affineCover.f i) y) = 1 y
inr₁ : Eq (α := ℕ) (1 ((Y.affineCover.f i) y)) (1 y)
inr₂ : Eq (α := ℕ) 1 (1 y)
inr₃ inr₄ : Eq (α := ℕ) 1 1
⊢ finrank (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) y = 1 y

Tactic:
rw [finrank_pullback_snd, h, Pi.one_apply, Pi.one_apply]

Premises used: Pi.one_apply, 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
h : finrank f = 1
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : finrank f = 1), IsIso f
⊢ IsIso f

Tactic:
obtain ⟨R, rfl⟩ := hY

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

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

Tactic:
rw [← isIso_comp_left_iff X.isoSpec.inv]

Premises used: AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.isIso_comp_left_iff, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : finrank f = 1)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIso f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h_1 : IsAffine X
⊢ IsIso (X.isoSpec.inv ≫ f)

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

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

Tactic:
refine this _ _ ?_ ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
this :
  ∀ {X : Scheme.{u}} (R : CommRingCat.{u}) (f : X ⟶ Spec R) [Flat f] [IsFinite f] (h : finrank f = 1)
    (hX : ∃ (S : CommRingCat.{u}), X = Spec S), IsIso f
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
h_1 : IsAffine X
inr : finrank f = 1
inr₁ inr₂ : Eq.{u + 1} (α := (s : ↥(Spec R)) → ℕ) 1 1
⊢ finrank (X.isoSpec.inv ≫ f) = 1

Tactic:
rw [finrank_comp_left_of_isIso, h]

Premises used: AlgebraicGeometry.Scheme.Hom.finrank_comp_left_of_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : Flat f
inst_1 : IsFinite f
h : finrank f = 1
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Spec R) [Flat f] [IsFinite f] (h : finrank f = 1), IsIso f
⊢ IsIso f

Tactic:
obtain ⟨S, rfl⟩ := hX

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

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

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
inst : Flat (Spec.map φ)
inst_1 : IsFinite (Spec.map φ)
h : finrank (Spec.map φ) = 1
⊢ (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
φ : R ⟶ S
inst_1 : Flat (Spec.map φ)
inst_2 : IsFinite (Spec.map φ)
h : finrank (Spec.map φ) = 1
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
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
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
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
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
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
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 :
  Function.Bijective (α := (↑R : Type u)) (β := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑R : Type u)) → (↑S : Type u))
⊢ IsIso φ

Tactic:
rw [ConcreteCategory.isIso_iff_bijective]

Premises used: CategoryTheory.ConcreteCategory.isIso_iff_bijective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
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)
a : Eq.{u + 1} (α := (p : PrimeSpectrum (↑R : Type u)) → ℕ) (Module.rankAtStalk (↑S : Type u)) 1
⊢ Function.Bijective (α := (↑R : Type u)) (β := (↑S : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑R : Type u)) → (↑S : Type u))

Tactic:
apply Module.algebraMap_bijective_of_rankAtStalk

Premises used: Module.algebraMap_bijective_of_rankAtStalk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
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)
a a₁ a₂ a₃ :
  ∀ (h : (CommRingCat.Hom.hom φ).finrank = 1),
    (CommRingCat.Hom.hom φ).Flat →
      (CommRingCat.Hom.hom φ).Finite →
        let algInst := (CommRingCat.Hom.hom φ).toAlgebra;
        Module.Flat.{u, u} (↑R : Type u) (↑S : Type u) →
          Module.Finite.{u, u} (↑R : Type u) (↑S : Type u) →
            Eq.{u + 1} (α := (p : PrimeSpectrum (↑R : Type u)) → ℕ) (Module.rankAtStalk (↑S : Type u)) 1
⊢ Eq.{u + 1} (α := (p : PrimeSpectrum (↑R : Type u)) → ℕ) (Module.rankAtStalk (↑S : Type u)) 1

Tactic:
rwa [finrank_SpecMap_eq_finrank ‹_› ‹_›] at h

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

Tactic:
have : IsIso φ := by
    rw [ConcreteCategory.isIso_iff_bijective]
    apply Module.algebraMap_bijective_of_rankAtStalk
    rwa [finrank_SpecMap_eq_finrank ‹_› ‹_›] at h
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FlatRank
Goal:
R S : CommRingCat
φ : R ⟶ S
h : finrank (Spec.map φ) = 1
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)
this : IsIso φ
⊢ IsIso (Spec.map φ)

Tactic:
infer_instance