case intro.intro
R : Type u
M : Type v
F : Type ?u.56157
G : Type ?u.56160
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I✝ J : Ideal R
N P : Submodule R M
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ ↑I
⊢ ↑f y ∈ I • ⊤
R : Type u
M : Type v
F : Type ?u.56157
G : Type ?u.56160
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I✝ J : Ideal R
N P : Submodule R M
I : Ideal R
f : R →ₗ[R] M
⊢ map f I ≤ I • ⊤
rintro _ ⟨y, hy, rfl⟩
case intro.intro
R : Type u
M : Type v
F : Type ?u.56157
G : Type ?u.56160
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I✝ J : Ideal R
N P : Submodule R M
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ ↑I
⊢ y • ↑f 1 ∈ I • ⊤
case intro.intro
R : Type u
M : Type v
F : Type ?u.56157
G : Type ?u.56160
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I✝ J : Ideal R
N P : Submodule R M
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ ↑I
⊢ ↑f y ∈ I • ⊤
rw [← mul_one y, ← smul_eq_mul, f.map_smul]
no goals
case intro.intro
R : Type u
M : Type v
F : Type ?u.56157
G : Type ?u.56160
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I✝ J : Ideal R
N P : Submodule R M
I : Ideal R
f : R →ₗ[R] M
y : R
hy : y ∈ ↑I
⊢ y • ↑f 1 ∈ I • ⊤
exact smul_mem_smul hy mem_top