case h
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R ⧸ Submodule.span R {a * b}
⊢ x ∈ torsionBy R (R ⧸ Submodule.span R {a * b}) a ↔ x ∈ Submodule.span R {↑(mk (Submodule.span R {a * b})) b}
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
⊢ torsionBy R (R ⧸ Submodule.span R {a * b}) a = Submodule.span R {↑(mk (Submodule.span R {a * b})) b}
ext x
case h
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R ⧸ Submodule.span R {a * b}
⊢ a • x = 0 ↔ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = x
case h
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R ⧸ Submodule.span R {a * b}
⊢ x ∈ torsionBy R (R ⧸ Submodule.span R {a * b}) a ↔ x ∈ Submodule.span R {↑(mk (Submodule.span R {a * b})) b}
rw [mem_torsionBy_iff, Submodule.mem_span_singleton]
case h.intro
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
⊢ a • ↑(mk (Submodule.span R {a * b})) x = 0 ↔
    ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
case h
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R ⧸ Submodule.span R {a * b}
⊢ a • x = 0 ↔ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = x
obtain ⟨x, rfl⟩ := mk_surjective x
case h.intro.mp
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : a • ↑(mk (Submodule.span R {a * b})) x = 0
⊢ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x

case h.intro.mpr
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
⊢ a • ↑(mk (Submodule.span R {a * b})) x = 0
case h.intro
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
⊢ a • ↑(mk (Submodule.span R {a * b})) x = 0 ↔
    ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
constructor <;> intro h
case h.intro.mp
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : ∃ a_1, a_1 • (a * b) = a • x
⊢ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
case h.intro.mp
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : a • ↑(mk (Submodule.span R {a * b})) x = 0
⊢ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
rw [← mk_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero, Submodule.mem_span_singleton] at h
case h.intro.mp.intro
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c • (a * b) = a • x
⊢ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
case h.intro.mp
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : ∃ a_1, a_1 • (a * b) = a • x
⊢ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
obtain ⟨c, h⟩ := h
case h.intro.mp.intro
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c * b = x
⊢ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
case h.intro.mp.intro
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c • (a * b) = a • x
⊢ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
rw [smul_eq_mul, smul_eq_mul, mul_comm, mul_assoc, mul_cancel_left_mem_nonZeroDivisors ha,
  mul_comm] at h
case h.intro.mp.intro
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c * b = x
⊢ c • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
case h.intro.mp.intro
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c * b = x
⊢ ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
use c
no goals
case h.intro.mp.intro
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c * b = x
⊢ c • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
rw [← h, ← mk_eq_mk, ← Quotient.mk_smul, smul_eq_mul, mk_eq_mk]
case h.intro.mpr.intro
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
⊢ a • ↑(mk (Submodule.span R {a * b})) x = 0
case h.intro.mpr
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x : R
h : ∃ a_1, a_1 • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
⊢ a • ↑(mk (Submodule.span R {a * b})) x = 0
obtain ⟨c, h⟩ := h
no goals
case h.intro.mpr.intro
R✝ : Type ?u.707004
M : Type ?u.707007
R : Type w
inst✝ : CommRing R
a b : R
ha : a ∈ R⁰
x c : R
h : c • ↑(mk (Submodule.span R {a * b})) b = ↑(mk (Submodule.span R {a * b})) x
⊢ a • ↑(mk (Submodule.span R {a * b})) x = 0
rw [← h, smul_comm, ← mk_eq_mk, ← Quotient.mk_smul,
  (Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _, smul_zero]