R : Type u_2
M : Type u_1
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : { x // x ∈ R⁰ }
hax : a • x ∈ torsion R M
⊢ Quotient.mk'' x ∈ ⊥
R : Type u_2
M : Type u_1
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : { x // x ∈ R⁰ }
hax : a • Quotient.mk'' x = 0
⊢ Quotient.mk'' x ∈ ⊥
rw [Quotient.mk''_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero] at hax
R : Type u_2
M : Type u_1
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : { x // x ∈ R⁰ }
hax : a • x ∈ torsion R M
⊢ x ∈ torsion R M
R : Type u_2
M : Type u_1
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : { x // x ∈ R⁰ }
hax : a • x ∈ torsion R M
⊢ Quotient.mk'' x ∈ ⊥
rw [mem_bot, Quotient.mk''_eq_mk, Quotient.mk_eq_zero]
case intro
R : Type u_2
M : Type u_1
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a b : { x // x ∈ R⁰ }
h : b • a • x = 0
⊢ x ∈ torsion R M
R : Type u_2
M : Type u_1
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : { x // x ∈ R⁰ }
hax : a • x ∈ torsion R M
⊢ x ∈ torsion R M
cases' hax with b h
no goals
case intro
R : Type u_2
M : Type u_1
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a b : { x // x ∈ R⁰ }
h : b • a • x = 0
⊢ x ∈ torsion R M
exact ⟨b * a, (mul_smul _ _ _).trans h⟩