awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
hI : Ideal.IsPrime.{u_1} (α := R) (Ideal.radical (colon (M := M) ⊥ {x}))
⊢ LE.le (α := Ideal R) (annihilator.{u_1, u_2} (M := M) ⊤) (Ideal.radical (annihilator (M := M) (R ∙ x)))

Tactic:
exact (annihilator_mono le_top).trans Ideal.le_radical

Premises used: Ideal.le_radical, Submodule.annihilator_mono, le_top, LE.le.trans
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
rw :
  I.IsPrime →
    ((∃ (x : M), I = colon (M := M) ⊥ {x}) ↔
      ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M))
⊢ IsAssociatedPrime I M ↔
    I.IsPrime ∧
      ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)

Tactic:
rw [isAssociatedPrime_iff, and_congr_right_iff]

Premises used: and_congr_right_iff, isAssociatedPrime_iff
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
⊢ I.IsPrime →
    ((∃ (x : M), I = colon (M := M) ⊥ {x}) ↔
      ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M))

Tactic:
fun _ ↦ ⟨fun ⟨x, h⟩ ↦ ?_, fun ⟨f, h⟩ ↦ ⟨(f ∘ₗ mkQ I) 1, ?_⟩⟩

Premises used: _private.0.isAssociatedPrime_iff_exists_injective_linearMap.match_2, Submodule.colon, Exists, Bot.bot, LinearMap.comp, _private.0.isAssociatedPrime_iff_exists_injective_linearMap.match_1, Iff.intro, Exists.intro, Submodule.mkQ, Function.Injective, Singleton.singleton, OfNat.ofNat, Eq, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
refine_1 :
  I.IsPrime →
    (∃ (x : M), I = colon (M := M) ⊥ {x}) →
      ∀ (x : M) (h : I = colon (M := M) ⊥ {x}),
        ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
refine_2 :
  I.IsPrime →
    (∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)) →
      ∀ (f : R ⧸ I →ₗ[R] M) (h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)),
        I = colon (M := M) ⊥ (singleton (α := M) ((f ∘ₗ mkQ I : (a : R) → M) 1 : M))
⊢ I.IsPrime →
    ((∃ (x : M), I = colon (M := M) ⊥ {x}) ↔
      ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M))

Tactic:
refine fun _ ↦ ⟨fun ⟨x, h⟩ ↦ ?_, fun ⟨f, h⟩ ↦ ⟨(f ∘ₗ mkQ I) 1, ?_⟩⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
h_1 : I.IsPrime
h_2 : ∃ (x : M), I = colon (M := M) ⊥ {x}
x : M
h : I = colon (M := M) ⊥ {x}
⊢ I = ker (toSpanSingleton R M x)

Tactic:
simp [h, SetLike.ext_iff]

Premises used: SetLike.ext_iff
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
h_1 : I.IsPrime
h_2 : ∃ (x : M), I = colon (M := M) ⊥ {x}
x : M
h : I = colon (M := M) ⊥ {x}
⊢ I = ker (toSpanSingleton R M x)

Tactic:
replace h : I = ker (toSpanSingleton R M x) := by simp [h, SetLike.ext_iff]
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
h_1 : I.IsPrime
h_2 : ∃ (x : M), I = colon (M := M) ⊥ {x}
x : M
h : I = ker (toSpanSingleton R M x)
⊢ ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)

Tactic:
⟨liftQ _ _ h.le, ker_eq_bot.mp (ker_liftQ_eq_bot' _ _ h)⟩

Premises used: LinearMap.ker_eq_bot, Submodule.ker_liftQ_eq_bot', Eq.le, Exists.intro, Iff.mp, Submodule.liftQ
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
h_1 : I.IsPrime
h_2 : ∃ (x : M), I = colon (M := M) ⊥ {x}
x : M
h : I = ker (toSpanSingleton R M x)
⊢ ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)

Tactic:
exact ⟨liftQ _ _ h.le, ker_eq_bot.mp (ker_liftQ_eq_bot' _ _ h)⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
h_1 : I.IsPrime
h_2 : ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
f : R ⧸ I →ₗ[R] M
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
rw : (f ∘ₗ mkQ I).ker
| I

Tactic:
rw [← I.ker_mkQ, ← ker_comp_of_ker_eq_bot (mkQ I) (ker_eq_bot_of_injective h)]

Premises used: LinearMap.ker_eq_bot_of_injective, Submodule.mkQ, LinearMap.ker_comp_of_ker_eq_bot, Submodule.ker_mkQ
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
h_1 : I.IsPrime
h_2 : ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
f : R ⧸ I →ₗ[R] M
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
refine_2 : (f ∘ₗ mkQ I).ker = colon (M := M) ⊥ (singleton (α := M) ((f ∘ₗ mkQ I : (a : R) → M) 1 : M))
⊢ I = colon (M := M) ⊥ (singleton (α := M) ((f ∘ₗ mkQ I : (a : R) → M) 1 : M))

Tactic:
conv_lhs => rw [← I.ker_mkQ, ← ker_comp_of_ker_eq_bot (mkQ I) (ker_eq_bot_of_injective h)]

Premises used: LinearMap.ker_eq_bot_of_injective, Submodule.mkQ, LinearMap.ker_comp_of_ker_eq_bot, Submodule.ker_mkQ
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
h_1 : I.IsPrime
h_2 : ∃ (f : R ⧸ I →ₗ[R] M), Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
f : R ⧸ I →ₗ[R] M
h : Function.Injective.{u_1 + 1, u_2 + 1} (α := R ⧸ I) (β := M) (⇑f : (a : R ⧸ I) → M)
⊢ (f ∘ₗ mkQ I).ker = colon (M := M) ⊥ (singleton (α := M) ((f ∘ₗ mkQ I : (a : R) → M) 1 : M))

Tactic:
simp [SetLike.ext_iff, ← Ideal.Quotient.algebraMap_eq, Algebra.algebraMap_eq_smul_one]

Premises used: Ideal.Quotient.algebraMap_eq, SetLike.ext_iff, Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
h : IsAssociatedPrime J (R ⧸ I)
obtain : ∀ (hJ : J.IsPrime) (x : R ⧸ I) (e : J = Ideal.radical (colon (M := R ⧸ I) ⊥ {x})), J = I.radical
⊢ J = I.radical

Tactic:
obtain ⟨hJ, x, e⟩ := h
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
e : J = Ideal.radical (colon (M := R ⧸ I) ⊥ {0})
apply : J = ⊤
⊢ False

Tactic:
apply hJ.1

Premises used: Ideal.IsPrime.ne_top'
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
e : J = Ideal.radical (colon (M := R ⧸ I) ⊥ {0})
rwa : ∀ (e : J = Ideal.radical ⊤), J = ⊤
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (e : J = ⊤), J = ⊤
⊢ J = ⊤

Tactic:
rwa [colon_singleton_zero, Ideal.radical_top] at e

Premises used: Submodule.colon_singleton_zero, Ideal.radical_top
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R ⧸ I
e : J = Ideal.radical (colon (M := R ⧸ I) ⊥ {x})
⊢ x ≠ 0

Tactic:
have : x ≠ 0 := by
    rintro rfl
    apply hJ.1
    rwa [colon_singleton_zero, Ideal.radical_top] at e
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R ⧸ I
e : J = Ideal.radical (colon (M := R ⧸ I) ⊥ {x})
this : x ≠ 0
obtain :
  ∀ (x : R)
    (e :
      J =
        Ideal.radical
          (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I))))
    (this : Ne (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I)), J = I.radical
⊢ J = I.radical

Tactic:
obtain ⟨x, rfl⟩ := Ideal.Quotient.mkₐ_surjective R _ x

Premises used: Ideal.Quotient.mkₐ_surjective, rfl
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : Ne (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I)
y : R
rw :
  Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
      (HSMul.hSMul (β := R ⧸ I) y ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
rw₁ :
  Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
      (HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((algebraMap R (R ⧸ I) : (a : R) → R ⧸ I) y : R ⧸ I)
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
rw₂ :
  Membership.mem (γ := Submodule R (R ⧸ I)) ⊥
      (HMul.hMul (α := R ⧸ I) (β := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) y : R ⧸ I)
        ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I)) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
rw₃ :
  Membership.mem (α := R ⧸ I) (γ := Submodule R (R ⧸ I)) ⊥ ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
rw₄ rw₅ :
  Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I) ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
⊢ Membership.mem (γ := Ideal R)
      (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
    Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)

Tactic:
rw [mem_colon_singleton, Algebra.smul_def, Ideal.Quotient.algebraMap_eq, ← map_mul, mem_bot]

Premises used: Submodule.mem_bot, Ideal.Quotient.algebraMap_eq, map_mul, Algebra.smul_def, Submodule.mem_colon_singleton
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : Ne (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I)
⊢ ∀ {y : R},
    Membership.mem (γ := Ideal R)
        (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)

Tactic:
have h {y} : y ∈ colon ⊥ {(Ideal.Quotient.mk I) x} ↔ Ideal.Quotient.mk I (y * x) = 0 := by
    rw [mem_colon_singleton, Algebra.smul_def, Ideal.Quotient.algebraMap_eq, ← map_mul, mem_bot]
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : Ne (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I) (0 : R ⧸ I)
h :
  ∀ {y : R},
    Membership.mem (γ := Ideal R)
        (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
      Eq (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) (y * x) : R ⧸ I) (0 : R ⧸ I)
simp :
  ∀ (this : x ∉ I)
    (h :
      ∀ {y : R},
        Membership.mem (γ := Ideal R)
            (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
          y * x ∈ I),
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) =
      I.radical
⊢ J = I.radical

Tactic:
simp only [e, Ideal.Quotient.mkₐ_eq_mk, ne_eq, Ideal.Quotient.eq_zero_iff_mem] at this h ⊢

Premises used: ne_eq, Ideal.Quotient.eq_zero_iff_mem, Ideal.Quotient.mkₐ_eq_mk
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : x ∉ I
h :
  ∀ {y : R},
    Membership.mem (γ := Ideal R)
        (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
      y * x ∈ I
⊢ Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) =
    I.radical

Tactic:
le_antisymm (Ideal.radical_le_radical_iff.mpr fun y hy ↦ ?_)
    (Ideal.radical_mono fun y ↦ h.mpr ∘ I.mul_mem_right x)

Premises used: Ideal.radical_mono, Iff.mpr, Function.comp, le_antisymm, Ideal.radical_le_radical_iff, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : x ∉ I
h :
  ∀ {y : R},
    Membership.mem (γ := Ideal R)
        (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
      y * x ∈ I
refine :
  ∀ (y : R)
    (hy :
      Membership.mem (γ := Submodule R R)
        (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y),
    y ∈ I.radical
⊢ Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) =
    I.radical

Tactic:
refine le_antisymm (Ideal.radical_le_radical_iff.mpr fun y hy ↦ ?_)
    (Ideal.radical_mono fun y ↦ h.mpr ∘ I.mul_mem_right x)

Premises used: Ideal.radical_mono, Iff.mpr, Function.comp, le_antisymm, Ideal.radical_le_radical_iff, Ideal.mul_mem_right
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : x ∉ I
h :
  ∀ {y : R},
    Membership.mem (γ := Ideal R)
        (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
      y * x ∈ I
y : R
hy :
  Membership.mem (γ := Submodule R R)
    (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y
rw : y ∈ (colon I ⊤).radical
⊢ y ∈ I.radical

Tactic:
rw [← I.colon_univ, ← Set.top_eq_univ]

Premises used: Set.top_eq_univ, Submodule.colon_univ
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : x ∉ I
h :
  ∀ {y : R},
    Membership.mem (γ := Ideal R)
        (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
      y * x ∈ I
y : R
hy :
  Membership.mem (γ := Submodule R R)
    (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y
⊢ y ∈ (colon I ⊤).radical

Tactic:
(hI.mem_or_mem (h.mp hy)).resolve_left this

Premises used: Set.Mem, setOf, Or.resolve_left, Iff.mp, Submodule.IsPrimary.mem_or_mem
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I J : Ideal R
hI : I.IsPrimary
hJ : J.IsPrime
x : R
e :
  J =
    Ideal.radical (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mkₐ R I : (a : R) → R ⧸ I) x : R ⧸ I)))
this : x ∉ I
h :
  ∀ {y : R},
    Membership.mem (γ := Ideal R)
        (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y ↔
      y * x ∈ I
y : R
hy :
  Membership.mem (γ := Submodule R R)
    (colon (M := R ⧸ I) ⊥ (singleton (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) x : R ⧸ I))) y
⊢ y ∈ (colon I ⊤).radical

Tactic:
exact (hI.mem_or_mem (h.mp hy)).resolve_left this

Premises used: Or.resolve_left, Iff.mp, Submodule.IsPrimary.mem_or_mem
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
h :
  ∀ (J : Ideal R),
    Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) J ↔
      Membership.mem (γ := Set (Ideal R)) {I.radical} J
⊢ Eq (α := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) {I.radical}

Tactic:
ext J
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
J : Ideal R
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) J ↔ J = I.radical

Tactic:
⟨IsAssociatedPrime.eq_radical hI, ?_⟩

Premises used: IsAssociatedPrime.eq_radical, Iff.intro
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
J : Ideal R
h : J = I.radical → Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) J
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) J ↔ J = I.radical

Tactic:
refine ⟨IsAssociatedPrime.eq_radical hI, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
⊢ Nontrivial.{u_1} (R ⧸ I)

Tactic:
⟨(Ideal.Quotient.mk I :) 1, (Ideal.Quotient.mk I :) 0, ?_⟩

Premises used: Ideal.Quotient.mk, Nontrivial.mk, Exists.intro, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
refine : Ne (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) 1) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) 0)
⊢ Nontrivial.{u_1} (R ⧸ I)

Tactic:
refine ⟨(Ideal.Quotient.mk I :) 1, (Ideal.Quotient.mk I :) 0, ?_⟩
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
rw : ¬I = ⊤
⊢ Ne (α := R ⧸ I) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) 1) ((Ideal.Quotient.mk I : (a : R) → R ⧸ I) 0)

Tactic:
rw [Ne, Ideal.Quotient.eq, sub_zero, ← Ideal.eq_top_iff_one]

Premises used: sub_zero, Ne, Ideal.Quotient.eq, Ideal.eq_top_iff_one
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
⊢ ¬I = ⊤

Tactic:
hI.1

Premises used: And.left
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
⊢ ¬I = ⊤

Tactic:
exact hI.1

Premises used: And.left
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
⊢ Nontrivial.{u_1} (R ⧸ I)

Tactic:
haveI : Nontrivial (R ⧸ I) := by
    refine ⟨(Ideal.Quotient.mk I :) 1, (Ideal.Quotient.mk I :) 0, ?_⟩
    rw [Ne, Ideal.Quotient.eq, sub_zero, ← Ideal.eq_top_iff_one]
    exact hI.1
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
this : Nontrivial.{u_1} (R ⧸ I)
h :
  ∀ (a : Ideal R) (ha : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) a),
    Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) I.radical
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) I.radical

Tactic:
obtain ⟨a, ha⟩ := associatedPrimes.nonempty R (R ⧸ I)

Premises used: associatedPrimes.nonempty, HasQuotient.Quotient
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
this : Nontrivial.{u_1} (R ⧸ I)
a : Ideal R
ha : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) a
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) I.radical

Tactic:
ha.eq_radical hI ▸ ha

Premises used: Eq.rec, IsAssociatedPrime.eq_radical
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
inst_1 : IsNoetherianRing R
hI : I.IsPrimary
this : Nontrivial.{u_1} (R ⧸ I)
a : Ideal R
ha : Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) a
⊢ Membership.mem (γ := Set (Ideal R)) (associatedPrimes R (R ⧸ I)) I.radical

Tactic:
exact ha.eq_radical hI ▸ ha
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
⊢ (N₁.mkQ ∘ₗ N₂.subtype).ker ≤ N₁.submoduleOf N₂

Tactic:
simp [ker_comp, submoduleOf]

Premises used: LinearMap.ker_comp, Submodule.submoduleOf
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
⊢ f.ker = ⊥

Tactic:
have hf₁ : ker f = ⊥ := ker_liftQ_eq_bot _ _ _ (by simp [ker_comp, submoduleOf])
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
⊢ f.range = map N₁.mkQ N₂

Tactic:
simp [f, mapQ, range_liftQ, range_comp]

Premises used: LinearMap.range_comp, Submodule.mapQ, Submodule.range_liftQ
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
⊢ f.range = map N₁.mkQ N₂

Tactic:
have hf₂ : range f = N₂.map N₁.mkQ := by simp [f, mapQ, range_liftQ, range_comp]
-- Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
Goal:
A : Type u
inst : CommRing A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
N₁ N₂ : Submodule A M
f : ↥N₂ ⧸ N₁.submoduleOf N₂ →ₗ[A] M ⧸ N₁ := (N₁.submoduleOf N₂).mapQ N₁ N₂.subtype ⋯
hf₁ : f.ker = ⊥
hf₂ : f.range = map N₁.mkQ N₂
⊢ N₁.IsQuotientEquivQuotientPrime N₂ ↔
    ∃ (x : M),
      Ideal.IsPrime.{u} (α := A)
          (colon (M := M ⧸ N₁) ⊥ (singleton (α := M ⧸ N₁) ((N₁.mkQ : (a : M) → M ⧸ N₁) x : M ⧸ N₁))) ∧
        N₂ = N₁ ⊔ A ∙ x

Tactic:
⟨fun ⟨h, p, ⟨e⟩⟩ ↦ ?_, fun ⟨x, hx, hx'⟩ ↦ ⟨le_sup_left.trans_eq hx'.symm, ⟨_, hx⟩, ?_⟩⟩

Premises used: PrimeSpectrum.mk, Submodule.colon, LE.le.trans_eq, le_sup_left, _private.0.Submodule.isQuotientEquivQuotientPrime_iff.match_2, Exists, Bot.bot, And, _private.0.Submodule.isQuotientEquivQuotientPrime_iff.match_1, Max.max, And.intro, Submodule.IsQuotientEquivQuotientPrime, Iff.intro, Ideal.IsPrime, Exists.intro, Submodule.span, Submodule.mkQ, Singleton.singleton, Eq.symm, Eq, DFunLike.coe