R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ a b : R
dvd : a ∣ b
⊢ torsionBySet R M ↑(span R {a}) ≤ torsionBySet R M {b}
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ a b : R
dvd : a ∣ b
⊢ torsionBy R M a ≤ torsionBy R M b
rw [← torsionBySet_span_singleton_eq, ← torsionBySet_singleton_eq]
case st
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ a b : R
dvd : a ∣ b
⊢ {b} ⊆ ↑(span R {a})
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ a b : R
dvd : a ∣ b
⊢ torsionBySet R M ↑(span R {a}) ≤ torsionBySet R M {b}
apply torsionBySet_le_torsionBySet_of_subset
case st
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ a c : R
dvd : a ∣ c
⊢ c ∈ ↑(span R {a})
case st
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ a b : R
dvd : a ∣ b
⊢ {b} ⊆ ↑(span R {a})
rintro c (rfl : c = b)
no goals
case st
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
a✝ a c : R
dvd : a ∣ c
⊢ c ∈ ↑(span R {a})
exact Ideal.mem_span_singleton.mpr dvd