case intro.intro
R✝ : Type ?u.46750
M✝ : Type ?u.46753
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn : FG N
hin : N ≤ I • N
r : R
hr : r - 1 ∈ I
hr' : ∀ (n : M), n ∈ N → r • n = 0
⊢ ∃ r, r ∈ I ∧ ∀ (n : M), n ∈ N → r • n = n
R✝ : Type ?u.46750
M✝ : Type ?u.46753
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn : FG N
hin : N ≤ I • N
⊢ ∃ r, r ∈ I ∧ ∀ (n : M), n ∈ N → r • n = n
obtain ⟨r, hr, hr'⟩ := exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I N hn hin
no goals
case intro.intro
R✝ : Type ?u.46750
M✝ : Type ?u.46753
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn : FG N
hin : N ≤ I • N
r : R
hr : r - 1 ∈ I
hr' : ∀ (n : M), n ∈ N → r • n = 0
⊢ ∃ r, r ∈ I ∧ ∀ (n : M), n ∈ N → r • n = n
exact ⟨-(r - 1), I.neg_mem hr, fun n hn => by simpa [sub_smul] using hr' n hn⟩
no goals
R✝ : Type ?u.46750
M✝ : Type ?u.46753
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hn✝ : FG N
hin : N ≤ I • N
r : R
hr : r - 1 ∈ I
hr' : ∀ (n : M), n ∈ N → r • n = 0
n : M
hn : n ∈ N
⊢ -(r - 1) • n = n
simpa [sub_smul] using hr' n hn