awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Support (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
p : Ideal R
inst_4 : p.IsPrime
inst_5 : Subsingleton (LocalizedModule p.primeCompl M)
this :
  Membership.mem (γ := Set (PrimeSpectrum R)) (Module.support R M)ᶜ { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)
have this₁ : ∃ (i : R) (_ : i ∈ (↑(Module.annihilator R M) : Set R)),
  Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {i})ᶜ { asIdeal := p, isPrime := sorry : PrimeSpectrum R }
Tactic: rw [Module.support_eq_zeroLocus, ← Set.biUnion_of_singleton (Module.annihilator R M : Set R),
    PrimeSpectrum.zeroLocus_iUnion₂, Set.compl_iInter₂, Set.mem_iUnion₂] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
p : Ideal R
inst_4 : p.IsPrime
inst_5 : Subsingleton (LocalizedModule p.primeCompl M)
this :
  ∃ (i : R) (_ : i ∈ (↑(Module.annihilator R M) : Set R)),
    Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {i})ᶜ { asIdeal := p, isPrime := ⋯ : PrimeSpectrum R }
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)
have obtain : ∀ (f : R) (hf : f ∈ (↑(Module.annihilator R M) : Set R))
  (hf' : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus {f})ᶜ { asIdeal := p, isPrime := sorry : PrimeSpectrum R }),
  ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)
Tactic: obtain ⟨f, hf, hf'⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Support (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
M' : Type u_5
inst_4 : AddCommMonoid M'
inst_5 : Module R M'
l : M →ₗ[R] M'
p : Ideal R
inst_6 : p.IsPrime
inst_7 : IsLocalizedModule p.primeCompl l
inst_8 : Subsingleton M'
e : LocalizedModule p.primeCompl M ≃ₗ[R] M' := iso p.primeCompl l
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)
have this : Subsingleton (LocalizedModule p.primeCompl M)
Tactic: have : Subsingleton (LocalizedModule p.primeCompl M) := e.subsingleton
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
⊢ Eq (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
    (support R M ∩ zeroLocus (↑I : Set R))
have a : Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
  (support R M ∩ zeroLocus (↑I : Set R))
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
a :
  Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
    (support R M ∩ zeroLocus (↑I : Set R))
⊢ Eq (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
    (support R M ∩ zeroLocus (↑I : Set R))
have a₁ : Subset (α := Set (PrimeSpectrum R)) (support R M ∩ zeroLocus (↑I : Set R))
  (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
Tactic: apply subset_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
⊢ Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
    (support R M ∩ zeroLocus (↑I : Set R))
have a : Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)) (support R M)
Tactic: refine Set.subset_inter ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
a : Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)) (support R M)
⊢ Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
    (support R M ∩ zeroLocus (↑I : Set R))
have a₁ : Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
  (zeroLocus (↑I : Set R))
Tactic: refine Set.subset_inter ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
⊢ Subset (α := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))
    (zeroLocus (↑I : Set R))
have a : Subset (α := Set (PrimeSpectrum R))
  (zeroLocus (↑(annihilator.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)) : Set R)) (zeroLocus (↑I : Set R))
Tactic: rw [support_eq_zeroLocus]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
⊢ Subset (α := Set (PrimeSpectrum R))
    (zeroLocus (↑(annihilator.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)) : Set R))
    (zeroLocus (↑I : Set R))
have a : I ≤ annihilator.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
Tactic: apply PrimeSpectrum.zeroLocus_anti_mono_ideal
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
⊢ I ≤ annihilator.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
have a : I ≤ (HSMul.hSMul (β := Submodule R M) I ⊤).colon Set.univ
Tactic: rw [Submodule.annihilator_quotient]
-- Lean 4 proof step from Mathlib.RingTheory.Support (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Membership.mem (γ := Set (PrimeSpectrum R)) (support R M) p
hp₂ : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) p
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (support.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)) p
have hp₃ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
Tactic: rw [Module.mem_support_iff] at hp₁ ⊢
Cleared hypotheses: hp₁, hp₂
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) p
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule.{u_1, u_2} p.asIdeal.primeCompl (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
Mₚ'' : Type (max u_1 u_2) :=
  Mₚ ⧸ HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
⊢ Submodule.localized p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤) =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
have rw : Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
    (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) (HSMul.hSMul (β := Submodule R M) I ⊤) =
  HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
Tactic: rw [Submodule.localized,
        Submodule.localized'_smul, Ideal.localized'_eq_map, Submodule.localized'_top]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) p
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule.{u_1, u_2} p.asIdeal.primeCompl (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
Mₚ'' : Type (max u_1 u_2) :=
  Mₚ ⧸ HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
rw :
  Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
      (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) (HSMul.hSMul (β := Submodule R M) I ⊤) =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
⊢ Submodule.localized p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤) =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
have rw₁ : HSMul.hSMul (α := Submodule (Localization (M := R) p.asIdeal.primeCompl) (Localization (M := R) p.asIdeal.primeCompl))
    (β := Submodule (Localization (M := R) p.asIdeal.primeCompl) (LocalizedModule p.asIdeal.primeCompl M))
    (Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
      (Algebra.linearMap R (Localization (M := R) p.asIdeal.primeCompl)) I)
    (Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
      (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) ⊤) =
  HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
Tactic: rw [Submodule.localized,
        Submodule.localized'_smul, Ideal.localized'_eq_map, Submodule.localized'_top]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) p
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule.{u_1, u_2} p.asIdeal.primeCompl (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
Mₚ'' : Type (max u_1 u_2) :=
  Mₚ ⧸ HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
rw :
  Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
      (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) (HSMul.hSMul (β := Submodule R M) I ⊤) =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
rw₁ :
  HSMul.hSMul (α := Submodule (Localization (M := R) p.asIdeal.primeCompl) (Localization (M := R) p.asIdeal.primeCompl))
      (β := Submodule (Localization (M := R) p.asIdeal.primeCompl) (LocalizedModule p.asIdeal.primeCompl M))
      (Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
        (Algebra.linearMap R (Localization (M := R) p.asIdeal.primeCompl)) I)
      (Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
        (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) ⊤) =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
⊢ Submodule.localized p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤) =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
have rw₂ : HSMul.hSMul (α := Submodule (Localization (M := R) p.asIdeal.primeCompl) (Localization (M := R) p.asIdeal.primeCompl))
    (β := Submodule (Localization (M := R) p.asIdeal.primeCompl) (LocalizedModule p.asIdeal.primeCompl M))
    (Ideal.map (F := R →+* Localization (M := R) p.asIdeal.primeCompl)
      (algebraMap R (Localization (M := R) p.asIdeal.primeCompl)) I)
    (Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
      (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) ⊤) =
  HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
Tactic: rw [Submodule.localized,
        Submodule.localized'_smul, Ideal.localized'_eq_map, Submodule.localized'_top]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) p
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule.{u_1, u_2} p.asIdeal.primeCompl (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
Mₚ'' : Type (max u_1 u_2) :=
  Mₚ ⧸ HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
rw :
  Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
      (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) (HSMul.hSMul (β := Submodule R M) I ⊤) =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
rw₁ :
  HSMul.hSMul (α := Submodule (Localization (M := R) p.asIdeal.primeCompl) (Localization (M := R) p.asIdeal.primeCompl))
      (β := Submodule (Localization (M := R) p.asIdeal.primeCompl) (LocalizedModule p.asIdeal.primeCompl M))
      (Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
        (Algebra.linearMap R (Localization (M := R) p.asIdeal.primeCompl)) I)
      (Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
        (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) ⊤) =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
rw₂ :
  HSMul.hSMul (α := Submodule (Localization (M := R) p.asIdeal.primeCompl) (Localization (M := R) p.asIdeal.primeCompl))
      (β := Submodule (Localization (M := R) p.asIdeal.primeCompl) (LocalizedModule p.asIdeal.primeCompl M))
      (Ideal.map (F := R →+* Localization (M := R) p.asIdeal.primeCompl)
        (algebraMap R (Localization (M := R) p.asIdeal.primeCompl)) I)
      (Submodule.localized' (Localization (M := R) p.asIdeal.primeCompl) p.asIdeal.primeCompl
        (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) ⊤) =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
⊢ Submodule.localized p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤) =
    HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
have rw₃ : HSMul.hSMul (α := Submodule (Localization (M := R) p.asIdeal.primeCompl) (Localization (M := R) p.asIdeal.primeCompl))
    (β := Submodule (Localization (M := R) p.asIdeal.primeCompl) (LocalizedModule p.asIdeal.primeCompl M))
    (Ideal.map (F := R →+* Localization (M := R) p.asIdeal.primeCompl)
      (algebraMap R (Localization (M := R) p.asIdeal.primeCompl)) I)
    ⊤ =
  HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
Tactic: rw [Submodule.localized,
        Submodule.localized'_smul, Ideal.localized'_eq_map, Submodule.localized'_top]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) p
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule.{u_1, u_2} p.asIdeal.primeCompl (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
Mₚ'' : Type (max u_1 u_2) :=
  Mₚ ⧸ HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
e : Mₚ' ≃ₗ[Rₚ] Mₚ'' :=
  (localizedQuotientEquiv p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤)).symm ≪≫ₗ
    (Submodule.localized p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤)).quotEquivOfEq
      (HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤) ⋯
⊢ Nontrivial Mₚ''
have rw : ⊤ ≠ HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
Tactic: rw [Submodule.Quotient.nontrivial_iff, ne_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) p
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule.{u_1, u_2} p.asIdeal.primeCompl (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
Mₚ'' : Type (max u_1 u_2) :=
  Mₚ ⧸ HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
e : Mₚ' ≃ₗ[Rₚ] Mₚ'' :=
  (localizedQuotientEquiv p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤)).symm ≪≫ₗ
    (Submodule.localized p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤)).quotEquivOfEq
      (HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤) ⋯
⊢ ⊤ ≠ HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
have h : LE.le (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) (Ideal.jacobson (annihilator Rₚ Mₚ))
Tactic: apply Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) p
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule.{u_1, u_2} p.asIdeal.primeCompl (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
Mₚ'' : Type (max u_1 u_2) :=
  Mₚ ⧸ HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
e : Mₚ' ≃ₗ[Rₚ] Mₚ'' :=
  (localizedQuotientEquiv p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤)).symm ≪≫ₗ
    (Submodule.localized p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤)).quotEquivOfEq
      (HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤) ⋯
⊢ LE.le (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) (Ideal.jacobson (annihilator Rₚ Mₚ))
have h : LE.le (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) (IsLocalRing.maximalIdeal Rₚ)
Tactic: refine trans ?_ (IsLocalRing.maximalIdeal_le_jacobson _)
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) p
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule.{u_1, u_2} p.asIdeal.primeCompl (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
Mₚ'' : Type (max u_1 u_2) :=
  Mₚ ⧸ HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
e : Mₚ' ≃ₗ[Rₚ] Mₚ'' :=
  (localizedQuotientEquiv p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤)).symm ≪≫ₗ
    (Submodule.localized p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤)).quotEquivOfEq
      (HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤) ⋯
⊢ LE.le (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) (IsLocalRing.maximalIdeal Rₚ)
have h : LE.le (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I)
  (Ideal.map (F := R →+* Localization.AtPrime p.asIdeal) (algebraMap R (Localization.AtPrime p.asIdeal)) p.asIdeal)
Tactic: rw [← Localization.AtPrime.map_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Support (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) p
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule.{u_1, u_2} p.asIdeal.primeCompl (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
Mₚ'' : Type (max u_1 u_2) :=
  Mₚ ⧸ HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
e : Mₚ' ≃ₗ[Rₚ] Mₚ'' :=
  (localizedQuotientEquiv p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤)).symm ≪≫ₗ
    (Submodule.localized p.asIdeal.primeCompl (HSMul.hSMul (β := Submodule R M) I ⊤)).quotEquivOfEq
      (HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤) ⋯
⊢ Nontrivial Mₚ'
have this : Nontrivial Mₚ''
Tactic: have : Nontrivial Mₚ'' := by
      rw [Submodule.Quotient.nontrivial_iff, ne_comm]
      apply Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator
      refine trans ?_ (IsLocalRing.maximalIdeal_le_jacobson _)
      rw [← Localization.AtPrime.map_eq_maximalIdeal]
      exact Ideal.map_mono hp₂
-- Lean 4 proof step from Mathlib.RingTheory.Support (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
x : R
⊢ Eq (α := Set (PrimeSpectrum R)) (support R M ∩ zeroLocus (↑(Ideal.span {x}) : Set R)) (support R M ∩ zeroLocus {x})
have rw : Eq (α := Set (PrimeSpectrum R)) (support R M ∩ zeroLocus {x}) (support R M ∩ zeroLocus {x})
Tactic: rw [zeroLocus_span]
-- Lean 4 proof step from Mathlib.RingTheory.SurjectiveOnStalks (goal)
Goal:
R : Type u_1
inst : CommRing R
S : Type u_2
inst_1 : CommRing S
f : R →+* S
P : Ideal S
inst_2 : P.IsPrime
⊢ Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f P)) (β := Localization.AtPrime P)
      (⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) :
        (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P) ↔
    ∀ (s : S),
      ∃ (x : R) (r : R),
        ∃ c ∉ P,
          ((f : (a : R) → S) r : S) ∉ P ∧
            HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
have mp : Function.Surjective.{u_1 + 1, u_2 + 1} (α := Localization.AtPrime (Ideal.comap f P)) (β := Localization.AtPrime P)
    (⇑(Localization.localRingHom (Ideal.comap f P) P f sorry) :
      (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P) →
  ∀ (s : S),
    ∃ (x : R) (r : R),
      ∃ c ∉ P,
        ((f : (a : R) → S) r : S) ∉ P ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * s = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
Tactic: constructor