-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem LinearIndependent.not_mem_span_image [Nontrivial R] (hv : LinearIndependent R v) {s : Set ι}
    {x : ι} (h : x ∉ s) : v x ∉ Submodule.span R (v '' s)

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
⊢ v x ∈ span R {v x}

Tactic:
exact mem_span_singleton_self (v x)

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ Disjoint {x} s

Tactic:
simpa using h

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
⊢ v x ∈ span R (v '' {x})

Tactic:
rw [Set.image_singleton]

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
⊢ v x ∈ span R {v x}

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : v x ∈ span R (v '' {x})
⊢ v x ∉ span R (v '' s)

Tactic:
intro w

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ False

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
⊢ v x ∉ span R (v '' s)

Tactic:
have h' : v x ∈ Submodule.span R (v '' {x}) := by
  rw [Set.image_singleton]
  exact mem_span_singleton_self (v x)

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : v x ∈ span R (v '' {x})
⊢ v x ∉ span R (v '' s)

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ v x = 0

Tactic:
refine disjoint_def.1 (hv.disjoint_span_image ?_) (v x) h' w

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ Disjoint {x} s

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ False

Tactic:
apply LinearIndependent.ne_zero x hv

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
hv : LinearIndependent R v
s : Set ι
x : ι
h : x ∉ s
h' : v x ∈ span R (v '' {x})
w : v x ∈ span R (v '' s)
⊢ v x = 0