awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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 : IsScalarTower R (Localization.Away f) Mₚ
r : Localization.Away f
r' : Rₚ
m : Mₚ
⊢ (r • r') • m =
    HSMul.hSMul (α := Rₚ) ((algebraMap (Localization.Away f) Rₚ : (a : Localization.Away f) → Rₚ) r : Rₚ) (r' • m)
have rw : (r • r') • m =
  HMul.hMul (α := Rₚ) ((algebraMap (Localization.Away f) Rₚ : (a : Localization.Away f) → Rₚ) r : Rₚ) r' • m
Tactic: rw [← mul_smul, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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 : IsScalarTower R (Localization.Away f) Mₚ
r : Localization.Away f
r' : Rₚ
m : Mₚ
rw :
  (r • r') • m =
    HMul.hMul (α := Rₚ) ((algebraMap (Localization.Away f) Rₚ : (a : Localization.Away f) → Rₚ) r : Rₚ) r' • m
⊢ (r • r') • m =
    HSMul.hSMul (α := Rₚ) ((algebraMap (Localization.Away f) Rₚ : (a : Localization.Away f) → Rₚ) r : Rₚ) (r' • m)
have rw₁ : (r • r') • m = (r • r') • m
Tactic: rw [← mul_smul, ← Algebra.smul_def]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (hypothesis)
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 : IsScalarTower R (Localization.Away f) Mₚ
⊢ rankAtStalk M
      (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) p
            hp'') :
        PrimeSpectrum R) =
    rankAtStalk M
      (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x
            hx) :
        PrimeSpectrum R)
have this₁ : IsScalarTower (Localization.Away f) Rₚ Mₚ
Tactic: have : IsScalarTower (Localization.Away f) Rₚ Mₚ :=
    ⟨fun r r' m ↦ show _ = algebraMap _ Rₚ r • r' • m by rw [← mul_smul, ← Algebra.smul_def]⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (hypothesis)
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))
⊢ rankAtStalk M
      (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) p
            hp'') :
        PrimeSpectrum R) =
    rankAtStalk M
      (↑(Subtype.mk (p := fun (x : PrimeSpectrum R) ↦ Membership.mem (γ := Set (PrimeSpectrum R)) (freeLocus R M) x) x
            hx) :
        PrimeSpectrum R)
have this₁ : IsLocalization p' Rₚ
Tactic: have : IsLocalization p' Rₚ :=
    IsLocalization.isLocalization_of_submonoid_le (Localization.Away f) Rₚ _ _ hp'
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Subsingleton M
⊢ Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) 0
have h : ∀ (p : PrimeSpectrum R), rankAtStalk M p = 0 p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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)
⊢ Nontrivial M
have by_contra! : ∀ (hn : Subsingleton M), False
Tactic: by_contra! hn
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
⊢ Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N)
have h : ∀ (p : PrimeSpectrum R), rankAtStalk M p = rankAtStalk N p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
Goal:
R : Type uR
M : Type uM
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Free R M
⊢ Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (↑(finrank R M) : (p : PrimeSpectrum R) → ℕ)
have h : ∀ (p : PrimeSpectrum R), rankAtStalk M p = (↑(finrank R M) : (p : PrimeSpectrum R) → ℕ) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
⊢ rankAtStalk ((i : ι) → M i) p = ∑ᶠ (i : ι), rankAtStalk.{uR, u_2} (M i) p
have intro : ∀ (val : Fintype ι), rankAtStalk ((i : ι) → M i) p = ∑ᶠ (i : ι), rankAtStalk.{uR, u_2} (M i) p
Tactic: cases nonempty_fintype ι
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (hypothesis)
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)
⊢ rankAtStalk ((i : ι) → M i) p = ∑ᶠ (i : ι), rankAtStalk.{uR, u_2} (M i) p
have this : ∀ (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
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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))
⊢ rankAtStalk ((i : ι) → M i) p = ∑ᶠ (i : ι), rankAtStalk.{uR, u_2} (M i) p
have 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))
Tactic: simp_rw [rankAtStalk, e.finrank_eq, Module.finrank_pi_fintype, finsum_eq_sum_of_fintype]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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))
⊢ rankAtStalk ((i : ι) → M i) p = ∑ᶠ (i : ι), rankAtStalk.{uR, u_2} (M i) p
have 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))
Tactic: simp_rw [rankAtStalk, e.finrank_eq, Module.finrank_pi_fintype, finsum_eq_sum_of_fintype]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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))
⊢ rankAtStalk ((i : ι) → M i) p = ∑ᶠ (i : ι), rankAtStalk.{uR, u_2} (M i) p
have 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)))
Tactic: simp_rw [rankAtStalk, e.finrank_eq, Module.finrank_pi_fintype, finsum_eq_sum_of_fintype]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
⊢ rankAtStalk M p = finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)
have rw : finrank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) =
  finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)
Tactic: rw [rankAtStalk, e.finrank_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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)
⊢ rankAtStalk M p = finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)
have rw₁ : finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M) =
  finrank (Localization.AtPrime p.asIdeal) (Localization.AtPrime p.asIdeal ⊗[R] M)
Tactic: rw [rankAtStalk, e.finrank_eq]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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 ↔ p ∉ support R M
have rw : rankAtStalk M p = 0 ↔ Subsingleton (LocalizedModule p.asIdeal.primeCompl M)
Tactic: rw [notMem_support_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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)
have refine : ∀ (h : rankAtStalk M p = 0), Subsingleton (LocalizedModule p.asIdeal.primeCompl M)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ Module.finrank_zero_of_subsingleton⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
⊢ Subsingleton (LocalizedModule p.asIdeal.primeCompl M)
have apply : Module.rank (Localization.AtPrime p.asIdeal) (LocalizedModule p.asIdeal.primeCompl M) = 0
Tactic: apply subsingleton_of_rank_zero (R := Localization.AtPrime p.asIdeal)
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
⊢ Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) 0 ↔ Subsingleton M
have refine : ∀ (h : Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) 0), Subsingleton M
Tactic: refine ⟨fun h ↦ ?_, fun _ ↦ rankAtStalk_eq_zero_of_subsingleton⟩
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
h : Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) 0
⊢ Subsingleton M
have simp_rw : ∀ (x : PrimeSpectrum R), x ∉ support R M
Tactic: simp_rw [← support_eq_empty_iff (R := R), Set.eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
h : Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) 0
p : PrimeSpectrum R
⊢ p ∉ support R M
have rw : rankAtStalk M p = 0
Tactic: rw [← rankAtStalk_eq_zero_iff_notMem_support, h, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
h : Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) 0
p : PrimeSpectrum R
rw : rankAtStalk M p = 0
⊢ p ∉ support R M
have rw₁ : Eq (α := ℕ) (0 p) 0
Tactic: rw [← rankAtStalk_eq_zero_iff_notMem_support, h, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
h : Eq.{uR + 1} (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) 0
p : PrimeSpectrum R
rw : rankAtStalk M p = 0
rw₁ : Eq (α := ℕ) (0 p) 0
⊢ p ∉ support R M
have rw₂ : Eq (α := ℕ) 0 0
Tactic: rw [← rankAtStalk_eq_zero_iff_notMem_support, h, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Spectrum.Prime.FreeLocus (goal)
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
N : Type u_1
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : Flat R N
inst_8 : Module.Finite R N
⊢ rankAtStalk (M × N) = HAdd.hAdd (α := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N)
have h : ∀ (p : PrimeSpectrum R),
  rankAtStalk (M × N) p =
    HAdd.hAdd (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) p
Tactic: ext p