awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Support
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 : I ≤ annihilator.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)
⊢ 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:
apply PrimeSpectrum.zeroLocus_anti_mono_ideal

Premises used: PrimeSpectrum.zeroLocus_anti_mono_ideal
-- Module: Mathlib.RingTheory.Support
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 : I ≤ (HSMul.hSMul (β := Submodule R M) I ⊤).colon Set.univ
⊢ I ≤ annihilator.{u_1, u_2} R (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤)

Tactic:
rw [Submodule.annihilator_quotient]

Premises used: Submodule.annihilator_quotient
-- Module: Mathlib.RingTheory.Support
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 ≤ (HSMul.hSMul (β := Submodule R M) I ⊤).colon Set.univ

Tactic:
fun x hx ↦ Submodule.mem_colon.mpr fun p hp ↦ Submodule.smul_mem_smul hx hp

Premises used: Iff.mpr, Set.Mem, Submodule.mem_colon, Submodule.smul_mem_smul
-- Module: Mathlib.RingTheory.Support
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 ≤ (HSMul.hSMul (β := Submodule R M) I ⊤).colon Set.univ

Tactic:
exact fun x hx ↦ Submodule.mem_colon.mpr fun p hp ↦ Submodule.smul_mem_smul hx hp

Premises used: Iff.mpr, Submodule.mem_colon, Submodule.smul_mem_smul
-- Module: Mathlib.RingTheory.Support
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
⊢ Nontrivial (LocalizedModule p.asIdeal.primeCompl M)

Tactic:
rw [Module.mem_support_iff] at hp₁ ⊢

Premises used: Module.mem_support_iff
-- Module: Mathlib.RingTheory.Support
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
hp₃ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
⊢ Membership.mem (γ := Set (PrimeSpectrum R)) (zeroLocus (↑I : Set R)) p

Tactic:
rw [Module.mem_support_iff] at hp₁ ⊢

Premises used: Module.mem_support_iff
-- Module: Mathlib.RingTheory.Support
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
a :
  let Mₚ' := LocalizedModule.{u_1, u_2} p.asIdeal.primeCompl (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤);
  Nontrivial Mₚ'
⊢ Nontrivial (LocalizedModule.{u_1, u_2} p.asIdeal.primeCompl (M ⧸ HSMul.hSMul (β := Submodule R M) I ⊤))

Tactic:
set Mₚ' := LocalizedModule p.asIdeal.primeCompl (M ⧸ (I • ⊤ : Submodule R M))

Premises used: LocalizedModule, HasQuotient.Quotient, HSMul.hSMul, Ideal.primeCompl, Top.top, PrimeSpectrum.asIdeal
-- Module: Mathlib.RingTheory.Support
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) ⊤) ⋯
rw : ⊤ ≠ HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤
⊢ Nontrivial Mₚ''

Tactic:
rw [Submodule.Quotient.nontrivial_iff, ne_comm]

Premises used: ne_comm, Submodule.Quotient.nontrivial_iff
-- Module: Mathlib.RingTheory.Support
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) ⊤) ⋯
h : LE.le (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) (Ideal.jacobson (annihilator Rₚ Mₚ))
⊢ ⊤ ≠ HSMul.hSMul (α := Ideal Rₚ) (β := Submodule Rₚ Mₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) ⊤

Tactic:
apply Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator

Premises used: Submodule.top_ne_ideal_smul_of_le_jacobson_annihilator
-- Module: Mathlib.RingTheory.Support
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ₚ))

Tactic:
trans ?_ (IsLocalRing.maximalIdeal_le_jacobson _)

Premises used: trans, IsLocalRing.maximalIdeal_le_jacobson
-- Module: Mathlib.RingTheory.Support
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) ⊤) ⋯
h : LE.le (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) (IsLocalRing.maximalIdeal Rₚ)
⊢ LE.le (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) (Ideal.jacobson (annihilator Rₚ Mₚ))

Tactic:
refine trans ?_ (IsLocalRing.maximalIdeal_le_jacobson _)
-- Module: Mathlib.RingTheory.Support
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) ⊤) ⋯
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)
⊢ LE.le (α := Ideal Rₚ) (Ideal.map (F := R →+* Rₚ) (algebraMap R Rₚ) I) (IsLocalRing.maximalIdeal Rₚ)

Tactic:
rw [← Localization.AtPrime.map_eq_maximalIdeal]

Premises used: Localization.AtPrime.map_eq_maximalIdeal
-- Module: Mathlib.RingTheory.Support
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.map (F := R →+* Localization.AtPrime p.asIdeal) (algebraMap R (Localization.AtPrime p.asIdeal)) p.asIdeal)

Tactic:
Ideal.map_mono hp₂

Premises used: Set.Mem, setOf, Ideal.map_mono
-- Module: Mathlib.RingTheory.Support
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.map (F := R →+* Localization.AtPrime p.asIdeal) (algebraMap R (Localization.AtPrime p.asIdeal)) p.asIdeal)

Tactic:
exact Ideal.map_mono hp₂

Premises used: Ideal.map_mono
-- Module: Mathlib.RingTheory.Support
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ₚ''

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₂
-- Module: Mathlib.RingTheory.Support
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) ⊤) ⋯
this : Nontrivial Mₚ''
⊢ Nontrivial Mₚ'

Tactic:
e.nontrivial

Premises used: Equiv.nontrivial, LinearEquiv.toAddEquiv, AddEquiv.toEquiv
-- Module: Mathlib.RingTheory.Support
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) ⊤) ⋯
this : Nontrivial Mₚ''
⊢ Nontrivial Mₚ'

Tactic:
exact e.nontrivial

Premises used: Equiv.nontrivial, LinearEquiv.toAddEquiv, AddEquiv.toEquiv
-- Module: Mathlib.RingTheory.Support
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
rw rw₁ : Eq (α := Set (PrimeSpectrum R)) (support R M ∩ zeroLocus {x}) (support R M ∩ zeroLocus {x})
⊢ Eq (α := Set (PrimeSpectrum R)) (support R M ∩ zeroLocus (↑(Ideal.span {x}) : Set R)) (support R M ∩ zeroLocus {x})

Tactic:
rw [zeroLocus_span]

Premises used: PrimeSpectrum.zeroLocus_span
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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
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 ⋯) :
        (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)
mpr :
  (∀ (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)) →
    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)
⊢ 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)

Tactic:
constructor
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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
H :
  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)
y : S
mp :
  ∀ (a : Localization.AtPrime (Ideal.comap f P))
    (ha :
      Eq (α := Localization.AtPrime P)
        (((Localization.localRingHom (Ideal.comap f P) P f ⋯ :
                RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
              (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
            a :
          Localization.AtPrime P)
        (IsLocalization.mk' (M := P.primeCompl) (Localization.AtPrime P) y 1 : Localization.AtPrime P)),
    ∃ (x : R) (r : R),
      ∃ c ∉ P,
        ((f : (a : R) → S) r : S) ∉ P ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * y = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ P,
      ((f : (a : R) → S) r : S) ∉ P ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * y = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)

Tactic:
obtain ⟨a, ha⟩ := H (IsLocalization.mk' _ y (1 : P.primeCompl))

Premises used: IsLocalization.mk', OfNat.ofNat
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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
H :
  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)
y : S
a : Localization.AtPrime (Ideal.comap f P)
ha :
  Eq (α := Localization.AtPrime P)
    (((Localization.localRingHom (Ideal.comap f P) P f ⋯ :
            RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
          (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
        a :
      Localization.AtPrime P)
    (IsLocalization.mk' (M := P.primeCompl) (Localization.AtPrime P) y 1 : Localization.AtPrime P)
mp :
  ∀ (a : R) (t : ↥(Ideal.primeCompl (Ideal.comap f P)))
    (ha :
      Eq (α := Localization.AtPrime P)
        (((Localization.localRingHom (Ideal.comap f P) P f ⋯ :
                RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
              (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
            (IsLocalization.mk' (Localization.AtPrime (Ideal.comap f P)) a t) :
          Localization.AtPrime P)
        (IsLocalization.mk' (M := P.primeCompl) (Localization.AtPrime P) y 1 : Localization.AtPrime P)),
    ∃ (x : R) (r : R),
      ∃ c ∉ P,
        ((f : (a : R) → S) r : S) ∉ P ∧
          HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * y = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)
⊢ ∃ (x : R) (r : R),
    ∃ c ∉ P,
      ((f : (a : R) → S) r : S) ∉ P ∧
        HMul.hMul (β := S) c ((f : (a : R) → S) r : S) * y = HMul.hMul (β := S) c ((f : (a : R) → S) x : S)

Tactic:
obtain ⟨a, t, rfl⟩ := IsLocalization.exists_mk'_eq (P.comap f).primeCompl a

Premises used: Ideal.comap, Ideal.primeCompl, rfl, IsLocalization.exists_mk'_eq
-- Module: Mathlib.RingTheory.SurjectiveOnStalks
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
H :
  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)
y : S
a : R
t : ↥(Ideal.primeCompl (Ideal.comap f P))
ha :
  Eq (α := Localization.AtPrime P)
    (((Localization.localRingHom (Ideal.comap f P) P f ⋯ :
            RingHom.{u_1, u_2} (Localization.AtPrime (Ideal.comap f P)) (Localization.AtPrime P)) :
          (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)
        (IsLocalization.mk' (Localization.AtPrime (Ideal.comap f P)) a t) :
      Localization.AtPrime P)
    (IsLocalization.mk' (M := P.primeCompl) (Localization.AtPrime P) y 1 : Localization.AtPrime P)
⊢ ∃ (c : ↥P.primeCompl),
    HMul.hMul (β := S) (↑c : S) ((f : (a : R) → S) a : S) =
      (↑c : S) *
        HMul.hMul (α := S)
          ((↑(Subtype.mk (p := fun (x : S) ↦ x ∈ P.primeCompl) ((f : (a : R) → S) (↑t : R)) ⋯) : S) : S) y

Tactic:
rw [Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq,
      Submonoid.coe_one, one_mul, IsLocalization.eq_iff_exists P.primeCompl] at ha

Premises used: Localization.localRingHom_mk', IsLocalization.mk'_eq_iff_eq, Submonoid.coe_one, Ideal.primeCompl, one_mul, IsLocalization.eq_iff_exists