case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : NoZeroSMulDivisors R M
⊢ torsion R M = ⊥

case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
⊢ NoZeroSMulDivisors R M
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
⊢ NoZeroSMulDivisors R M ↔ torsion R M = ⊥
constructor <;> intro h
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
⊢ torsion R M = ⊥
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : NoZeroSMulDivisors R M
⊢ torsion R M = ⊥
haveI : NoZeroSMulDivisors R M := h
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
⊢ torsion R M ≤ ⊥
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
⊢ torsion R M = ⊥
rw [eq_bot_iff]
case mp.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : a • x = 0
⊢ x ∈ ⊥
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
⊢ torsion R M ≤ ⊥
rintro x ⟨a, hax⟩
case mp.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : ↑a • x = 0
⊢ x ∈ ⊥
case mp.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : a • x = 0
⊢ x ∈ ⊥
change (a : R) • x = 0 at hax
case mp.intro.inl
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : ↑a • x = 0
h0 : ↑a = 0
⊢ x ∈ ⊥

case mp.intro.inr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : ↑a • x = 0
h0 : x = 0
⊢ x ∈ ⊥
case mp.intro
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : ↑a • x = 0
⊢ x ∈ ⊥
cases' eq_zero_or_eq_zero_of_smul_eq_zero hax with h0 h0
case mp.intro.inl.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : ↑a • x = 0
h0 : ↑a = 0
⊢ False
case mp.intro.inl
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : ↑a • x = 0
h0 : ↑a = 0
⊢ x ∈ ⊥
exfalso
no goals
case mp.intro.inl.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : ↑a • x = 0
h0 : ↑a = 0
⊢ False
exact nonZeroDivisors.coe_ne_zero a h0
no goals
case mp.intro.inr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h this : NoZeroSMulDivisors R M
x : M
a : { x // x ∈ R⁰ }
hax : ↑a • x = 0
h0 : x = 0
⊢ x ∈ ⊥
exact h0
case pos
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : a = 0
⊢ a = 0 ∨ x = 0

case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : ¬a = 0
⊢ a = 0 ∨ x = 0
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
⊢ a = 0 ∨ x = 0
by_cases ha : a = 0
case pos.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : a = 0
⊢ a = 0
case pos
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : a = 0
⊢ a = 0 ∨ x = 0
left
no goals
case pos.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : a = 0
⊢ a = 0
exact ha
case neg.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : ¬a = 0
⊢ x = 0
case neg
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : ¬a = 0
⊢ a = 0 ∨ x = 0
right
case neg.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : ¬a = 0
⊢ x ∈ torsion R M
case neg.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : ¬a = 0
⊢ x = 0
rw [← mem_bot R, ← h]
no goals
case neg.h
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
h : torsion R M = ⊥
a : R
x : M
hax : a • x = 0
ha : ¬a = 0
⊢ x ∈ torsion R M
exact ⟨⟨a, mem_nonZeroDivisors_of_ne_zero ha⟩, hax⟩