-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem mem_span_singleton {y : M} : (x ∈ R ∙ y) ↔ ∃ a : R, a • y = x :=
  ⟨fun h => by
    refine span_induction ?_ ?_ ?_ ?_ h
    · rintro y (rfl | ⟨⟨_⟩⟩)
      exact ⟨1, by simp⟩
    · exact ⟨0, by simp⟩
    · rintro _ _ - - ⟨a, rfl⟩ ⟨b, rfl⟩
      exact ⟨a + b, by simp [add_smul]⟩
    · rintro a _ - ⟨b, rfl⟩
      exact ⟨a * b, by simp [smul_smul]⟩, by
    rintro ⟨a, y, rfl⟩; exact smul_mem _ _ (subset_span <| by simp)⟩

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y : M
a : R
⊢ y ∈ {y}

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
⊢ (∃ a, a • y = x) → x ∈ span R {y}

Tactic:
rintro ⟨a, y, rfl⟩

Result:
case intro.refl
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y : M
a : R
⊢ a • y ∈ span R {y}

Proof state:
case refine_1.refl
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
⊢ ∃ a, a • y = y

Tactic:
exact ⟨1, by simp⟩

Result:
no goals

Proof state:
case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
⊢ ∃ a, a • y = 0

Tactic:
exact ⟨0, by simp⟩

Result:
no goals

Proof state:
case refine_4.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
a b : R
⊢ ∃ a_1, a_1 • y = a • b • y

Tactic:
exact ⟨a * b, by simp [smul_smul]⟩

Result:
no goals

Proof state:
case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
⊢ ∀ x ∈ {y}, ∃ a, a • y = x

Tactic:
rintro y (rfl | ⟨⟨_⟩⟩)

Result:
case refine_1.refl
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
⊢ ∃ a, a • y = y

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
a b : R
⊢ (a + b) • y = a • y + b • y

Tactic:
simp [add_smul]

Result:
no goals

Proof state:
case intro.refl
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
y : M
a : R
⊢ a • y ∈ span R {y}

Tactic:
exact smul_mem _ _ (subset_span <| by simp)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
⊢ ∃ a, a • y = x

Tactic:
refine span_induction ?_ ?_ ?_ ?_ h

Result:
case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
⊢ ∀ x ∈ {y}, ∃ a, a • y = x

case refine_2
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
⊢ ∃ a, a • y = 0

case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
⊢ ∀ (x y_1 : M), x ∈ span R {y} → y_1 ∈ span R {y} → (∃ a, a • y = x) → (∃ a, a • y = y_1) → ∃ a, a • y = x + y_1

case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
⊢ ∀ (a : R), ∀ x ∈ span R {y}, (∃ a, a • y = x) → ∃ a_2, a_2 • y = a • x

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
a b : R
⊢ (a * b) • y = a • b • y

Tactic:
simp [smul_smul]

Result:
no goals

Proof state:
case refine_3
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
⊢ ∀ (x y_1 : M), x ∈ span R {y} → y_1 ∈ span R {y} → (∃ a, a • y = x) → (∃ a, a • y = y_1) → ∃ a, a • y = x + y_1

Tactic:
rintro _ _ - - ⟨a, rfl⟩ ⟨b, rfl⟩

Result:
case refine_3.intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
a b : R
⊢ ∃ a_1, a_1 • y = a • y + b • y

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
⊢ 0 • y = 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_3.intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
a b : R
⊢ ∃ a_1, a_1 • y = a • y + b • y

Tactic:
exact ⟨a + b, by simp [add_smul]⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
⊢ 1 • y = y

Tactic:
simp

Result:
no goals

Proof state:
case refine_4
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
⊢ ∀ (a : R), ∀ x ∈ span R {y}, (∃ a, a • y = x) → ∃ a_2, a_2 • y = a • x

Tactic:
rintro a _ - ⟨b, rfl⟩

Result:
case refine_4.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x y : M
h : x ∈ span R {y}
a b : R
⊢ ∃ a_1, a_1 • y = a • b • y