-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem span_singleton_eq_span_singleton {R M : Type*} [Ring R] [AddCommGroup M] [Module R M]
    [NoZeroSMulDivisors R M] {x y : M} : ((R ∙ x) = R ∙ y) ↔ ∃ z : Rˣ, z • x = y

Proof state:
case mp.intro.intro.intro.inr.refine_1
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ b * a = 1

Tactic:
apply smul_left_injective R hy

Result:
case mp.intro.intro.intro.inr.refine_1.a
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ (fun c => c • y) (b * a) = (fun c => c • y) 1

Proof state:
case mpr.intro
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
u : Rˣ
⊢ span R {x} = span R {u • x}

Tactic:
exact (span_singleton_group_smul_eq _ _ _).symm

Result:
no goals

Proof state:
case mp
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ ((∃ a, a • y = x) ∧ ∃ a, a • x = y) → ∃ z, z • x = y

Tactic:
rintro ⟨⟨a, rfl⟩, b, hb⟩

Result:
case mp.intro.intro.intro
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
y : M
a b : R
hb : b • a • y = y
⊢ ∃ z, z • a • y = y

Proof state:
case mp.intro.intro.intro.inr.refine_2
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
y : M
a b : R
hb : b • a • y = y
hy : b • a • y ≠ 0
⊢ a * b = 1

Tactic:
apply smul_left_injective R (smul_ne_zero_iff.1 hy).2

Result:
case mp.intro.intro.intro.inr.refine_2.a
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
y : M
a b : R
hb : b • a • y = y
hy : b • a • y ≠ 0
⊢ (fun c => c • a • y) (a * b) = (fun c => c • a • y) 1

Proof state:
case mp
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ span R {x} = span R {y} → ∃ z, z • x = y

Tactic:
simp only [le_antisymm_iff, span_singleton_le_iff_mem, mem_span_singleton]

Result:
case mp
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ ((∃ a, a • y = x) ∧ ∃ a, a • x = y) → ∃ z, z • x = y

Proof state:
case mpr
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ (∃ z, z • x = y) → span R {x} = span R {y}

Tactic:
rintro ⟨u, rfl⟩

Result:
case mpr.intro
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
u : Rˣ
⊢ span R {x} = span R {u • x}

Proof state:
case mp.intro.intro.intro.inr
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ ∃ z, z • a • y = y

Tactic:
refine ⟨⟨b, a, ?_, ?_⟩, hb⟩

Result:
case mp.intro.intro.intro.inr.refine_1
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ b * a = 1

case mp.intro.intro.intro.inr.refine_2
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ a * b = 1

Proof state:
case mp.intro.intro.intro
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
y : M
a b : R
hb : b • a • y = y
⊢ ∃ z, z • a • y = y

Tactic:
rcases eq_or_ne y 0 with rfl | hy

Result:
case mp.intro.intro.intro.inl
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
a b : R
hb : b • a • 0 = 0
⊢ ∃ z, z • a • 0 = 0

case mp.intro.intro.intro.inr
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ ∃ z, z • a • y = y

Proof state:
case mp.intro.intro.intro.inl
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
a b : R
hb : b • a • 0 = 0
⊢ ∃ z, z • a • 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case mp.intro.intro.intro.inr.refine_1.a
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ (fun c => c • y) (b * a) = (fun c => c • y) 1

Tactic:
simpa only [mul_smul, one_smul]

Result:
no goals

Proof state:
case mp.intro.intro.intro.inr.refine_2.a
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
y : M
a b : R
hb : b • a • y = y
hy : b • a • y ≠ 0
⊢ (fun c => c • a • y) (a * b) = (fun c => c • a • y) 1

Tactic:
simp only [mul_smul, one_smul, hb]

Result:
no goals

Proof state:
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ span R {x} = span R {y} ↔ ∃ z, z • x = y

Tactic:
constructor

Result:
case mp
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ span R {x} = span R {y} → ∃ z, z • x = y

case mpr
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x y : M
⊢ (∃ z, z • x = y) → span R {x} = span R {y}

Proof state:
case mp.intro.intro.intro.inr.refine_2
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
y : M
a b : R
hb : b • a • y = y
hy : y ≠ 0
⊢ a * b = 1

Tactic:
rw [← hb] at hy

Result:
case mp.intro.intro.intro.inr.refine_2
R : Type u_9
M : Type u_10
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
y : M
a b : R
hb : b • a • y = y
hy : b • a • y ≠ 0
⊢ a * b = 1