-- Mathlib/Algebra/Module/Torsion.lean
theorem noZeroSMulDivisors_iff_torsion_eq_bot : NoZeroSMulDivisors R M ↔ torsion R M = ⊥

Proof state:
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 : ↥R⁰
hax : ↑a • x = 0
h0 : ↑a = 0
⊢ x ∈ ⊥

Tactic:
exfalso

Result:
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 : ↥R⁰
hax : ↑a • x = 0
h0 : ↑a = 0
⊢ False

Proof state:
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

Tactic:
by_cases ha : a = 0

Result:
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

Proof state:
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 : ↥R⁰
hax : a • x = 0
⊢ x ∈ ⊥

Tactic:
change (a : R) • x = 0 at hax

Result:
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 : ↥R⁰
hax : ↑a • x = 0
⊢ x ∈ ⊥

Proof state:
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 = ⊥

Tactic:
haveI : NoZeroSMulDivisors R M := h

Result:
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 = ⊥

Proof state:
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 ≤ ⊥

Tactic:
rintro x ⟨a, hax⟩

Result:
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 : ↥R⁰
hax : a • x = 0
⊢ x ∈ ⊥

Proof state:
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 = ⊥

Tactic:
constructor <;> intro h

Result:
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

Proof state:
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

Tactic:
exact ha

Result:
no goals

Proof state:
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

Tactic:
exact ⟨⟨a, mem_nonZeroDivisors_of_ne_zero ha⟩, hax⟩

Result:
no goals

Proof state:
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 : ↥R⁰
hax : ↑a • x = 0
h0 : ↑a = 0
⊢ False

Tactic:
exact nonZeroDivisors.coe_ne_zero a h0

Result:
no goals

Proof state:
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 = ⊥

Tactic:
rw [eq_bot_iff]

Result:
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 ≤ ⊥

Proof state:
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 : ↥R⁰
hax : ↑a • x = 0
h0 : x = 0
⊢ x ∈ ⊥

Tactic:
exact h0

Result:
no goals

Proof state:
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

Tactic:
right

Result:
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

Proof state:
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

Tactic:
rw [← mem_bot R, ← h]

Result:
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

Proof state:
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 : ↥R⁰
hax : ↑a • x = 0
⊢ x ∈ ⊥

Tactic:
rcases eq_zero_or_eq_zero_of_smul_eq_zero hax with h0 | h0

Result:
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 : ↥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 : ↥R⁰
hax : ↑a • x = 0
h0 : x = 0
⊢ x ∈ ⊥

Proof state:
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

Tactic:
left

Result:
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