-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndepOn_insert {s : Set ι} {a : ι} {f : ι → V} (has : a ∉ s) :
    LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ Submodule.span K (f '' s)

Proof state:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ (LinearIndependent K fun (x : ↑s) =>
        f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) (some x))) ∧
      f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) none) ∉
        span K (range fun x => f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) (some x))) ↔
    (LinearIndependent K fun (x : ↑s) => f ↑x) ∧ f a ∉ span K (f '' s)

Tactic:
rw [range_comp']

Result:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ (LinearIndependent K fun (x : ↑s) =>
        f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) (some x))) ∧
      f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) none) ∉
        span K (f '' range fun x => ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) (some x))) ↔
    (LinearIndependent K fun (x : ↑s) => f ↑x) ∧ f a ∉ span K (f '' s)

Proof state:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ (LinearIndependent K fun (x : ↑s) =>
        f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) (some x))) ∧
      f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) none) ∉
        span K (f '' range fun x => ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) (some x))) ↔
    (LinearIndependent K fun (x : ↑s) => f ↑x) ∧ f a ∉ span K (f '' s)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ LinearIndependent (ι := ↑s) K
        (((fun x => f ↑x) ∘ ⇑((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm)) ∘ some) ∧
      ((fun x => f ↑x) ∘ ⇑((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm)) none ∉
        span K
          (range (((fun x => f ↑x) ∘ ⇑((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm)) ∘ some)) ↔
    (LinearIndependent K fun (x : ↑s) => f ↑x) ∧ f a ∉ span K (f '' s)

Tactic:
simp only [comp_def]

Result:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ (LinearIndependent K fun (x : ↑s) =>
        f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) (some x))) ∧
      f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) none) ∉
        span K (range fun x => f ↑(((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm) (some x))) ↔
    (LinearIndependent K fun (x : ↑s) => f ↑x) ∧ f a ∉ span K (f '' s)

Proof state:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ span K (f '' s)

Tactic:
classical
rw [LinearIndepOn, LinearIndepOn, ← linearIndependent_equiv
  ((Equiv.optionEquivSumPUnit _).trans (Equiv.Set.insert has).symm), linearIndependent_option]
simp only [comp_def]
rw [range_comp']
simp

Result:
no goals

Proof state:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ span K (f '' s)

Tactic:
rw [LinearIndepOn, LinearIndepOn, ← linearIndependent_equiv
  ((Equiv.optionEquivSumPUnit _).trans (Equiv.Set.insert has).symm), linearIndependent_option]

Result:
ι : Type u'
K : Type u_3
V : Type u
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
⊢ LinearIndependent (ι := ↑s) K
        (((fun x => f ↑x) ∘ ⇑((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm)) ∘ some) ∧
      ((fun x => f ↑x) ∘ ⇑((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm)) none ∉
        span K
          (range (((fun x => f ↑x) ∘ ⇑((Equiv.optionEquivSumPUnit ↑s).trans (Equiv.Set.insert has).symm)) ∘ some)) ↔
    (LinearIndependent K fun (x : ↑s) => f ↑x) ∧ f a ∉ span K (f '' s)