-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem LinearIndependent.linearCombination_ne_of_not_mem_support [Nontrivial R]
    (hv : LinearIndependent R v) {x : ι} (f : ι →₀ R) (h : x ∉ f.support) :
    Finsupp.linearCombination R v f ≠ 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
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
p : (Finsupp.linearCombination R v) f ∉ map (Finsupp.linearCombination R v) (Finsupp.supported R R ↑f.support)
w : (Finsupp.linearCombination R v) f = v x
⊢ False

Tactic:
simp only [not_exists, not_and, mem_map] at p

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
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
w : (Finsupp.linearCombination R v) f = v x
p : ∀ x ∈ Finsupp.supported R R ↑f.support, ¬(Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) f
⊢ 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
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
w : (Finsupp.linearCombination R v) f = v x
p : ∀ x ∈ Finsupp.supported R R ↑f.support, ¬(Finsupp.linearCombination R v) x = (Finsupp.linearCombination R v) f
⊢ False

Tactic:
exact p f (f.mem_supported_support R) rfl

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
x : ι
f : ι →₀ R
h : x ∉ f.support
⊢ (Finsupp.linearCombination R v) f ≠ v x

Tactic:
replace h : x ∉ (f.support : Set ι) := h

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
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
⊢ (Finsupp.linearCombination R v) f ≠ 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
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
p : (Finsupp.linearCombination R v) f ∉ span R (v '' ↑f.support)
w : (Finsupp.linearCombination R v) f = v x
⊢ False

Tactic:
rw [Finsupp.span_image_eq_map_linearCombination] at p

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
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
p : (Finsupp.linearCombination R v) f ∉ map (Finsupp.linearCombination R v) (Finsupp.supported R R ↑f.support)
w : (Finsupp.linearCombination R v) f = v x
⊢ 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
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
p : v x ∉ span R (v '' ↑f.support)
w : (Finsupp.linearCombination R v) f = v x
⊢ False

Tactic:
rw [← w] at p

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
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
p : (Finsupp.linearCombination R v) f ∉ span R (v '' ↑f.support)
w : (Finsupp.linearCombination R v) f = v x
⊢ 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
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
p : v x ∉ span R (v '' ↑f.support)
⊢ (Finsupp.linearCombination R v) f ≠ v x

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
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
p : v x ∉ span R (v '' ↑f.support)
w : (Finsupp.linearCombination R v) f = v x
⊢ 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
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
⊢ (Finsupp.linearCombination R v) f ≠ v x

Tactic:
have p := hv.not_mem_span_image h

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
x : ι
f : ι →₀ R
h : x ∉ ↑f.support
p : v x ∉ span R (v '' ↑f.support)
⊢ (Finsupp.linearCombination R v) f ≠ v x