case refine'_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : torsionOf R M m = ⊥
contra : m = 0
⊢ False

case refine'_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : m ≠ 0
r : R
hr : r ∈ torsionOf R M m
⊢ r = 0
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
⊢ torsionOf R M m = ⊥ ↔ m ≠ 0
refine' ⟨fun h contra => _, fun h => (Submodule.eq_bot_iff _).mpr fun r hr => _⟩
case refine'_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : ⊤ = ⊥
contra : m = 0
⊢ False
case refine'_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : torsionOf R M m = ⊥
contra : m = 0
⊢ False
rw [contra, torsionOf_zero] at h
no goals
case refine'_1
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : ⊤ = ⊥
contra : m = 0
⊢ False
exact bot_ne_top.symm h
case refine'_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : m ≠ 0
r : R
hr : r = 0 ∨ m = 0
⊢ r = 0
case refine'_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : m ≠ 0
r : R
hr : r ∈ torsionOf R M m
⊢ r = 0
rw [mem_torsionOf_iff, smul_eq_zero] at hr
no goals
case refine'_2
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
m : M
h : m ≠ 0
r : R
hr : r = 0 ∨ m = 0
⊢ r = 0
tauto