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
hx : x ∈ torsionBySet R M s
⊢ x ∈ torsionBySet R M ↑(Ideal.span s)
R : Type u_2
M : Type u_1
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a : R
⊢ torsionBySet R M s = torsionBySet R M ↑(Ideal.span s)
refine le_antisymm (fun x hx => ?_) (torsionBySet_le_torsionBySet_of_subset subset_span)
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
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ ∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0
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
hx : x ∈ torsionBySet R M s
⊢ x ∈ torsionBySet R M ↑(Ideal.span s)
rw [mem_torsionBySet_iff] at hx ⊢
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
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ Ideal.span s ≤ Ideal.torsionOf R M x
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
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ ∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0
suffices Ideal.span s ≤ Ideal.torsionOf R M x by
  rintro ⟨a, ha⟩
  exact this ha
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
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ s ⊆ ↑(Ideal.torsionOf R M x)
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
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ Ideal.span s ≤ Ideal.torsionOf R M x
rw [Ideal.span_le]
no goals
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
hx : ∀ (a : ↑s), ↑a • x = 0
⊢ s ⊆ ↑(Ideal.torsionOf R M x)
exact fun a ha => hx ⟨a, ha⟩
case mk
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
hx : ∀ (a : ↑s), ↑a • x = 0
this : Ideal.span s ≤ Ideal.torsionOf R M x
a : R
ha : a ∈ ↑(Ideal.span s)
⊢ ↑{ val := a, property := ha } • x = 0
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
hx : ∀ (a : ↑s), ↑a • x = 0
this : Ideal.span s ≤ Ideal.torsionOf R M x
⊢ ∀ (a : ↑↑(Ideal.span s)), ↑a • x = 0
rintro ⟨a, ha⟩
no goals
case mk
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
hx : ∀ (a : ↑s), ↑a • x = 0
this : Ideal.span s ≤ Ideal.torsionOf R M x
a : R
ha : a ∈ ↑(Ideal.span s)
⊢ ↑{ val := a, property := ha } • x = 0
exact this ha