-- Mathlib/Algebra/Module/Torsion.lean
theorem torsionBy_eq_span_singleton {R : Type w} [CommRing R] (a b : R) (ha : a ∈ R⁰) :
    torsionBy R (R ⧸ R ∙ a * b) a = R ∙ mk (R ∙ a * b) b

Proof state:
case h
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}

Tactic:
rw [mem_torsionBy_iff, Submodule.mem_span_singleton]

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

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

Tactic:
obtain ⟨x, rfl⟩ := mk_surjective x

Result:
case h.intro
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

Proof state:
case h.intro.mp
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

Tactic:
obtain ⟨c, h⟩ := h

Result:
case h.intro.mp.intro
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

Proof state:
case h.intro.mpr.intro
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

Tactic:
rw [← h, smul_comm, ← mk_eq_mk, ← Quotient.mk_smul,
  (Quotient.mk_eq_zero _).mpr <| mem_span_singleton_self _, smul_zero]

Result:
no goals

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

Tactic:
ext x

Result:
case h
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}

Proof state:
case h.intro.mpr
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

Tactic:
obtain ⟨c, h⟩ := h

Result:
case h.intro.mpr.intro
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

Proof state:
case h.intro.mp.intro
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

Tactic:
use c

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

Proof state:
case h.intro.mp
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

Tactic:
rw [← mk_eq_mk, ← Quotient.mk_smul, Quotient.mk_eq_zero, Submodule.mem_span_singleton] at h

Result:
case h.intro.mp
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

Proof state:
case h.intro.mp.intro
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

Tactic:
rw [smul_eq_mul, smul_eq_mul, mul_comm, mul_assoc, mul_cancel_left_mem_nonZeroDivisors ha,
  mul_comm] at h

Result:
case h.intro.mp.intro
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

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

Tactic:
rw [← h, ← mk_eq_mk, ← Quotient.mk_smul, smul_eq_mul, mk_eq_mk]

Result:
no goals

Proof state:
case h.intro
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

Tactic:
constructor <;> intro h

Result:
case h.intro.mp
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 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