awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
x_1 : (↑(freeLocus R M) : Type uR)
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
this_1 : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p
hp :
  Membership.mem (γ := Set (↑(freeLocus R M) : Type uR))
    (Subtype.val (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) ⁻¹'
      (↑(basicOpen f) : Set (PrimeSpectrum R)))
    (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) p hp'')
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this_2 : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this_3 : IsScalarTower R (Localization.Away f) Rₚ
this_4 : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
this_5 : IsScalarTower R (Localization.Away f) Mₚ
this : IsScalarTower (Localization.Away f) Rₚ Mₚ
l : LinearMap (R := Localization.Away f) (RingHom.id (Localization.Away f)) (LocalizedModule (Submonoid.powers f) M)
  (LocalizedModule p.asIdeal.primeCompl M) :=
  LinearMap.extendScalarsOfIsLocalization (Submonoid.powers f) (Localization.Away f)
    (IsLocalizedModule.liftOfLE (Submonoid.powers f) p.asIdeal.primeCompl hp'
      (LocalizedModule.mkLinearMap (Submonoid.powers f) M) (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M))
⊢ IsLocalization p' Rₚ

Tactic:
have : IsLocalization p' Rₚ :=
    IsLocalization.isLocalization_of_submonoid_le (Localization.Away f) Rₚ _ _ hp'
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
x_1 : (↑(freeLocus R M) : Type uR)
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
this_1 : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p
hp :
  Membership.mem (γ := Set (↑(freeLocus R M) : Type uR))
    (Subtype.val (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) ⁻¹'
      (↑(basicOpen f) : Set (PrimeSpectrum R)))
    (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) p hp'')
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this_2 : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this_3 : IsScalarTower R (Localization.Away f) Rₚ
this_4 : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
this_5 : IsScalarTower R (Localization.Away f) Mₚ
this_6 : IsScalarTower (Localization.Away f) Rₚ Mₚ
l : LinearMap (R := Localization.Away f) (RingHom.id (Localization.Away f)) (LocalizedModule (Submonoid.powers f) M)
  (LocalizedModule p.asIdeal.primeCompl M) :=
  LinearMap.extendScalarsOfIsLocalization (Submonoid.powers f) (Localization.Away f)
    (IsLocalizedModule.liftOfLE (Submonoid.powers f) p.asIdeal.primeCompl hp'
      (LocalizedModule.mkLinearMap (Submonoid.powers f) M) (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M))
this : IsLocalization p' Rₚ
⊢ IsLocalizedModule p.asIdeal.primeCompl
    ((↑R :
        {S : Type uR} →
          {M M₂ : Type (max uM uR)} →
            [inst : Semiring R] →
              [inst_4 : Semiring S] →
                [inst_5 : AddCommMonoid M] →
                  [inst_6 : AddCommMonoid M₂] →
                    [inst_7 : Module R M] →
                      [inst_8 : Module R M₂] →
                        [inst_9 : Module S M] →
                          [inst_10 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      l)

Tactic:
have : IsLocalizedModule p.asIdeal.primeCompl (l.restrictScalars R) :=
    inferInstanceAs (IsLocalizedModule p.asIdeal.primeCompl
    ((IsLocalizedModule.liftOfLE _ _ hp' (LocalizedModule.mkLinearMap (.powers f) M)
      (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M))))
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
x_1 : (↑(freeLocus R M) : Type uR)
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
this_1 : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p
hp :
  Membership.mem (γ := Set (↑(freeLocus R M) : Type uR))
    (Subtype.val (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) ⁻¹'
      (↑(basicOpen f) : Set (PrimeSpectrum R)))
    (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) p hp'')
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this_2 : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this_3 : IsScalarTower R (Localization.Away f) Rₚ
this_4 : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
this_5 : IsScalarTower R (Localization.Away f) Mₚ
this_6 : IsScalarTower (Localization.Away f) Rₚ Mₚ
l : LinearMap (R := Localization.Away f) (RingHom.id (Localization.Away f)) (LocalizedModule (Submonoid.powers f) M)
  (LocalizedModule p.asIdeal.primeCompl M) :=
  LinearMap.extendScalarsOfIsLocalization (Submonoid.powers f) (Localization.Away f)
    (IsLocalizedModule.liftOfLE (Submonoid.powers f) p.asIdeal.primeCompl hp'
      (LocalizedModule.mkLinearMap (Submonoid.powers f) M) (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M))
this_7 : IsLocalization p' Rₚ
this :
  IsLocalizedModule p.asIdeal.primeCompl
    ((↑R :
        {S : Type uR} →
          {M M₂ : Type (max uM uR)} →
            [inst : Semiring R] →
              [inst_4 : Semiring S] →
                [inst_5 : AddCommMonoid M] →
                  [inst_6 : AddCommMonoid M₂] →
                    [inst_7 : Module R M] →
                      [inst_8 : Module R M₂] →
                        [inst_9 : Module S M] →
                          [inst_10 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      l)
⊢ IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization.Away f) p.asIdeal.primeCompl) l

Tactic:
have : IsLocalizedModule (Algebra.algebraMapSubmonoid _ p.asIdeal.primeCompl) l :=
      IsLocalizedModule.of_restrictScalars p.asIdeal.primeCompl ..
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
x_1 : (↑(freeLocus R M) : Type uR)
x : PrimeSpectrum R
hx : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x
this_1 : Free (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
f : R
hf : f ∈ x.asIdeal.primeCompl
hf' : Free (Localization (Submonoid.powers f)) (LocalizedModule.Away f M)
hf'' :
  finrank (Localization (Submonoid.powers f)) (LocalizedModule.Away f M) =
    finrank (Localization.AtPrime x.asIdeal) (LocalizedModule x.asIdeal.primeCompl M)
p : PrimeSpectrum R
hp'' : Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) p
hp :
  Membership.mem (γ := Set (↑(freeLocus R M) : Type uR))
    (Subtype.val (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) ⁻¹'
      (↑(basicOpen f) : Set (PrimeSpectrum R)))
    (Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) p hp'')
p' : Submonoid (Localization (Submonoid.powers f)) :=
  Algebra.algebraMapSubmonoid (Localization (Submonoid.powers f)) p.asIdeal.primeCompl
hp' : Submonoid.powers f ≤ p.asIdeal.primeCompl
Rₚ : Type uR := Localization.AtPrime p.asIdeal
Mₚ : Type (max uR uM) := LocalizedModule p.asIdeal.primeCompl M
this_2 : Algebra (Localization.Away f) Rₚ :=
  IsLocalization.localizationAlgebraOfSubmonoidLe (Localization.Away f) Rₚ (Submonoid.powers f) p.asIdeal.primeCompl hp'
this_3 : IsScalarTower R (Localization.Away f) Rₚ
this_4 : Module (Localization.Away f) Mₚ := compHom Mₚ (algebraMap (Localization.Away f) Rₚ)
this_5 : IsScalarTower R (Localization.Away f) Mₚ
this_6 : IsScalarTower (Localization.Away f) Rₚ Mₚ
l : LinearMap (R := Localization.Away f) (RingHom.id (Localization.Away f)) (LocalizedModule (Submonoid.powers f) M)
  (LocalizedModule p.asIdeal.primeCompl M) :=
  LinearMap.extendScalarsOfIsLocalization (Submonoid.powers f) (Localization.Away f)
    (IsLocalizedModule.liftOfLE (Submonoid.powers f) p.asIdeal.primeCompl hp'
      (LocalizedModule.mkLinearMap (Submonoid.powers f) M) (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M))
this_7 : IsLocalization p' Rₚ
this_8 :
  IsLocalizedModule p.asIdeal.primeCompl
    ((↑R :
        {S : Type uR} →
          {M M₂ : Type (max uM uR)} →
            [inst : Semiring R] →
              [inst_4 : Semiring S] →
                [inst_5 : AddCommMonoid M] →
                  [inst_6 : AddCommMonoid M₂] →
                    [inst_7 : Module R M] →
                      [inst_8 : Module R M₂] →
                        [inst_9 : Module S M] →
                          [inst_10 : Module S M₂] →
                            [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      l)
this : IsLocalizedModule (Algebra.algebraMapSubmonoid (Localization.Away f) p.asIdeal.primeCompl) l
⊢ finrank Rₚ (LocalizedModule p.asIdeal.primeCompl M) =
    finrank (Localization (Submonoid.powers f)) (LocalizedModule (Submonoid.powers f) M)

Tactic:
have := Module.finrank_of_isLocalizedModule_of_free Rₚ p' l
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
inst_4 : Flat R M
e : (↑(freeLocus R M) : Type uR) ≃ₜ PrimeSpectrum R :=
  Homeomorph.trans (Homeomorph.setCongr (s := freeLocus R M) (t := Set.univ) ⋯) (Homeomorph.Set.univ (PrimeSpectrum R))
⊢ IsLocallyConstant (X := PrimeSpectrum R) (Y := ℕ)
    ((fun (x : (↑(freeLocus R M) : Type uR)) ↦ rankAtStalk M (↑x : PrimeSpectrum R)) ∘
      (⇑e.symm : (a : PrimeSpectrum R) → (↑(freeLocus R M) : Type uR)))

Tactic:
isLocallyConstant_rankAtStalk_freeLocus.comp_continuous e.symm.continuous

Premises used: Homeomorph.continuous, IsLocallyConstant.comp_continuous, Module.isLocallyConstant_rankAtStalk_freeLocus, Homeomorph.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : FinitePresentation R M
inst_4 : Flat R M
e : (↑(freeLocus R M) : Type uR) ≃ₜ PrimeSpectrum R :=
  Homeomorph.trans (Homeomorph.setCongr (s := freeLocus R M) (t := Set.univ) ⋯) (Homeomorph.Set.univ (PrimeSpectrum R))
⊢ IsLocallyConstant.{uR, 0} (X := PrimeSpectrum R) (rankAtStalk M)

Tactic:
convert! isLocallyConstant_rankAtStalk_freeLocus.comp_continuous e.symm.continuous

Premises used: Homeomorph.continuous, IsLocallyConstant.comp_continuous, Module.isLocallyConstant_rankAtStalk_freeLocus, Homeomorph.symm
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Subsingleton M
h : ∀ (p : PrimeSpectrum R), rankAtStalk M p = 0 p
⊢ Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) 0

Tactic:
ext p
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Subsingleton M
p : PrimeSpectrum R
⊢ rankAtStalk M p = 0 p

Tactic:
Module.finrank_zero_of_subsingleton

Premises used: Module.rankAtStalk, Module.finrank_zero_of_subsingleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Subsingleton M
p : PrimeSpectrum R
⊢ rankAtStalk M p = 0 p

Tactic:
exact Module.finrank_zero_of_subsingleton

Premises used: Module.finrank_zero_of_subsingleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : LT.lt.{uR} (α := (p : PrimeSpectrum R) → ℕ) 0 (rankAtStalk M)
by_contra! : ∀ (hn : Subsingleton M), False
⊢ Nontrivial M

Tactic:
by_contra! hn
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h : LT.lt.{uR} (α := (p : PrimeSpectrum R) → ℕ) 0 (rankAtStalk M)
hn : Subsingleton M
⊢ False

Tactic:
simp at h
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
h : ∀ (p : PrimeSpectrum R), rankAtStalk M p = rankAtStalk N p
⊢ Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N)

Tactic:
ext p
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
p : PrimeSpectrum R
⊢ rankAtStalk M p = rankAtStalk N p

Tactic:
IsLocalizedModule.mapEquiv p.asIdeal.primeCompl
    (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M)
    (LocalizedModule.mkLinearMap p.asIdeal.primeCompl N) _ e |>.finrank_eq

Premises used: Module.rankAtStalk, IsLocalizedModule.mapEquiv, LinearEquiv.finrank_eq, LocalizedModule.mkLinearMap, Ideal.primeCompl, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_1
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
p : PrimeSpectrum R
⊢ rankAtStalk M p = rankAtStalk N p

Tactic:
exact IsLocalizedModule.mapEquiv p.asIdeal.primeCompl
    (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M)
    (LocalizedModule.mkLinearMap p.asIdeal.primeCompl N) _ e |>.finrank_eq

Premises used: IsLocalizedModule.mapEquiv, LinearEquiv.finrank_eq, LocalizedModule.mkLinearMap, Ideal.primeCompl, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
h : ∀ (p : PrimeSpectrum R), rankAtStalk M p = (↑(finrank R M) : (p : PrimeSpectrum R) → ℕ) p
⊢ Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (↑(finrank R M) : (p : PrimeSpectrum R) → ℕ)

Tactic:
ext p
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
p : PrimeSpectrum R
⊢ rankAtStalk M p = (↑(finrank R M) : (p : PrimeSpectrum R) → ℕ) p

Tactic:
simp [rankAtStalk, finrank_of_isLocalizedModule_of_free _ p.asIdeal.primeCompl
    (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M)]

Premises used: Module.rankAtStalk, Module.finrank_of_isLocalizedModule_of_free, LocalizedModule.mkLinearMap, Ideal.primeCompl, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
inst : CommRing R
inst_1 : Nontrivial R
⊢ Eq (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk R) 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
inst : CommRing R
ι : Type u_1
inst_1 : Finite ι
M : ι → Type u_2
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{uR, u_2} R (M i)
inst_4 : ∀ (i : ι), Flat.{uR, u_2} R (M i)
inst_5 : ∀ (i : ι), Module.Finite.{uR, u_2} R (M i)
p : PrimeSpectrum R
intro : ∀ (val : Fintype ι), rankAtStalk ((i : ι) → M i) p = ∑ᶠ (i : ι), rankAtStalk.{uR, u_2} (M i) p
⊢ rankAtStalk ((i : ι) → M i) p = ∑ᶠ (i : ι), rankAtStalk.{uR, u_2} (M i) p

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
inst : CommRing R
ι : Type u_1
inst_1 : Finite ι
M : ι → Type u_2
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{uR, u_2} R (M i)
inst_4 : ∀ (i : ι), Flat.{uR, u_2} R (M i)
inst_5 : ∀ (i : ι), Module.Finite.{uR, u_2} R (M i)
p : PrimeSpectrum R
val : Fintype ι
f : ((i : ι) → M i) →ₗ[R] (i : ι) → LocalizedModule.{uR, u_2} p.asIdeal.primeCompl (M i) :=
  LinearMap.pi (φ := fun (i : ι) ↦ LocalizedModule.{uR, u_2} p.asIdeal.primeCompl (M i)) fun (i : ι) ↦
    mkLinearMap p.asIdeal.primeCompl (M i) ∘ₗ LinearMap.proj (φ := M) i
e : LocalizedModule p.asIdeal.primeCompl ((i : ι) → M i) ≃ₗ[Localization.AtPrime p.asIdeal]
  (i : ι) → LocalizedModule.{uR, u_2} p.asIdeal.primeCompl (M i) :=
  LinearEquiv.extendScalarsOfIsLocalization p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal)
    (IsLocalizedModule.linearEquiv p.asIdeal.primeCompl (mkLinearMap p.asIdeal.primeCompl ((i : ι) → M i)) f)
⊢ ∀ (i : ι), Free (Localization.AtPrime p.asIdeal) (LocalizedModule.{uR, u_2} p.asIdeal.primeCompl (M i))

Tactic:
have (i : ι) : Free (Localization.AtPrime p.asIdeal)
      (LocalizedModule p.asIdeal.primeCompl (M i)) :=
    free_of_flat_of_isLocalRing
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
inst : CommRing R
ι : Type u_1
inst_1 : Finite ι
M : ι → Type u_2
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{uR, u_2} R (M i)
inst_4 : ∀ (i : ι), Flat.{uR, u_2} R (M i)
inst_5 : ∀ (i : ι), Module.Finite.{uR, u_2} R (M i)
p : PrimeSpectrum R
val : Fintype ι
f : ((i : ι) → M i) →ₗ[R] (i : ι) → LocalizedModule.{uR, u_2} p.asIdeal.primeCompl (M i) :=
  LinearMap.pi (φ := fun (i : ι) ↦ LocalizedModule.{uR, u_2} p.asIdeal.primeCompl (M i)) fun (i : ι) ↦
    mkLinearMap p.asIdeal.primeCompl (M i) ∘ₗ LinearMap.proj (φ := M) i
e : LocalizedModule p.asIdeal.primeCompl ((i : ι) → M i) ≃ₗ[Localization.AtPrime p.asIdeal]
  (i : ι) → LocalizedModule.{uR, u_2} p.asIdeal.primeCompl (M i) :=
  LinearEquiv.extendScalarsOfIsLocalization p.asIdeal.primeCompl (Localization.AtPrime p.asIdeal)
    (IsLocalizedModule.linearEquiv p.asIdeal.primeCompl (mkLinearMap p.asIdeal.primeCompl ((i : ι) → M i)) f)
this : ∀ (i : ι), Free (Localization.AtPrime p.asIdeal) (LocalizedModule.{uR, u_2} p.asIdeal.primeCompl (M i))
intro :
  finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl ((i : ι) → M i)) =
    ∑ᶠ (i : ι), finrank (Localization.AtPrime p.asIdeal) (LocalizedModule.{uR, u_2} p.asIdeal.primeCompl (M i))
intro₁ :
  finrank (Localization.AtPrime p.asIdeal) ((i : ι) → LocalizedModule.{uR, u_2} p.asIdeal.primeCompl (M i)) =
    ∑ᶠ (i : ι), finrank (Localization.AtPrime p.asIdeal) (LocalizedModule.{uR, u_2} p.asIdeal.primeCompl (M i))
intro₂ :
  Eq (α := ℕ) (∑ i : ι, finrank (Localization.AtPrime p.asIdeal) (LocalizedModule.{uR, u_2} p.asIdeal.primeCompl (M i)))
    (∑ᶠ (i : ι), finrank (Localization.AtPrime p.asIdeal) (LocalizedModule.{uR, u_2} p.asIdeal.primeCompl (M i)))
⊢ rankAtStalk ((i : ι) → M i) p = ∑ᶠ (i : ι), rankAtStalk.{uR, u_2} (M i) p

Tactic:
simp_rw [rankAtStalk, e.finrank_eq, Module.finrank_pi_fintype, finsum_eq_sum_of_fintype]

Premises used: Module.rankAtStalk, LinearEquiv.finrank_eq, Module.finrank_pi_fintype, finsum_eq_sum_of_fintype
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : PrimeSpectrum R
e : LocalizedModule p.asIdeal.primeCompl M ≃ₗ[Localization.AtPrime p.asIdeal] Localization.AtPrime p.asIdeal ⊗[R] M :=
  equivTensorProduct p.asIdeal.primeCompl M
rw :
  finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) =
    finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)
rw₁ rw₂ :
  finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M) =
    finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)
⊢ rankAtStalk M p = finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)

Tactic:
rw [rankAtStalk, e.finrank_eq]

Premises used: Module.rankAtStalk, LinearEquiv.finrank_eq
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
p : PrimeSpectrum R
rw : rankAtStalk M p = 0 ↔ Subsingleton (LocalizedModule p.asIdeal.primeCompl M)
⊢ rankAtStalk M p = 0 ↔ p ∉ support R M

Tactic:
rw [notMem_support_iff]

Premises used: Module.notMem_support_iff
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
p : PrimeSpectrum R
⊢ rankAtStalk M p = 0 ↔ Subsingleton (LocalizedModule p.asIdeal.primeCompl M)

Tactic:
⟨fun h ↦ ?_, fun h ↦ Module.finrank_zero_of_subsingleton⟩

Premises used: Iff.intro, Module.finrank_zero_of_subsingleton
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
p : PrimeSpectrum R
refine : ∀ (h : rankAtStalk M p = 0), Subsingleton (LocalizedModule p.asIdeal.primeCompl M)
⊢ rankAtStalk M p = 0 ↔ Subsingleton (LocalizedModule p.asIdeal.primeCompl M)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Module.finrank_zero_of_subsingleton⟩
-- Module: Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Flat R M
inst_4 : Module.Finite R M
p : PrimeSpectrum R
h : rankAtStalk M p = 0
apply : Module.rank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) = 0
⊢ Subsingleton (LocalizedModule p.asIdeal.primeCompl M)

Tactic:
apply subsingleton_of_rank_zero (R := Localization.AtPrime p.asIdeal)

Premises used: Module.subsingleton_of_rank_zero