R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x : M
h : ∀ (a : ↑s), ↑a • x = 0
⊢ ∀ (p : Submodule R M), p ∈ torsionBy R M '' s → x ∈ p
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x : M
⊢ x ∈ torsionBySet R M s ↔ ∀ (a : ↑s), ↑a • x = 0
refine' ⟨fun h ⟨a, ha⟩ => mem_sInf.mp h _ (Set.mem_image_of_mem _ ha), fun h => mem_sInf.mpr _⟩
case intro.intro
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ : R
x : M
h : ∀ (a : ↑s), ↑a • x = 0
a : R
ha : a ∈ s
⊢ x ∈ torsionBy R M a
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
x : M
h : ∀ (a : ↑s), ↑a • x = 0
⊢ ∀ (p : Submodule R M), p ∈ torsionBy R M '' s → x ∈ p
rintro _ ⟨a, ha, rfl⟩
no goals
case intro.intro
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ : R
x : M
h : ∀ (a : ↑s), ↑a • x = 0
a : R
ha : a ∈ s
⊢ x ∈ torsionBy R M a
exact h ⟨a, ha⟩