-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
ι : Type u'
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set ι
a : ι
f : ι → V
has : a ∉ s
rw :
  (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι)) ↔
    LinearIndepOn K f s ∧ f a ∉ span K (f '' s)
rw₁ :
  (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι)) ↔
    (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦ f (↑x : ι)) ∧ f a ∉ span K (f '' s)
rw₂ :
  LinearIndependent.{u', u_3, u} (ι := Option (↑s : Type u')) K (M := V)
      ((fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι)) ∘
        (⇑(Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm) :
          (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))) ↔
    (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦ f (↑x : ι)) ∧ f a ∉ span K (f '' s)
rw₃ rw₄ rw₅ :
  LinearIndependent.{u', u_3, u} (ι := (↑s : Type u')) K (M := V)
        (((fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι)) ∘
            (⇑(Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm) :
              (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))) ∘
          some) ∧
      comp (α := Option (↑s : Type u')) (fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι))
          (⇑(Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm) :
            (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))
          none ∉
        span K
          (range (ι := (↑s : Type u'))
            (((fun (x : (↑(insert a s) : Type u')) ↦ f (↑x : ι)) ∘
                (⇑(Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm) :
                  (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))) ∘
              some)) ↔
    (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦ f (↑x : ι)) ∧ f a ∉ span K (f '' s)
rw₆ :
  (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦
        f
          (↑((Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm :
                  (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))
                (some x)) :
            ι)) ∧
      f
          (↑((Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm :
                  (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))
                none) :
            ι) ∉
        span K
          (range fun (x : (↑s : Type u')) ↦
            f
              (↑((Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm :
                      (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))
                    (some x)) :
                ι)) ↔
    (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦ f (↑x : ι)) ∧ f a ∉ span K (f '' s)
rw₇ :
  (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦
        f
          (↑((Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm :
                  (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))
                (some x)) :
            ι)) ∧
      f
          (↑((Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm :
                  (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))
                none) :
            ι) ∉
        span K
          (f ''
            range fun (x : (↑s : Type u')) ↦
              (↑((Equiv.trans (Equiv.optionEquivSumPUnit (↑s : Type u')) (Equiv.Set.insert (s := s) has).symm :
                      (a_1 : Option (↑s : Type u')) → (↑(insert a s) : Type u'))
                    (some x)) :
                ι)) ↔
    (LinearIndependent.{u', u_3, u} K (M := V) fun (x : (↑s : Type u')) ↦ f (↑x : ι)) ∧ f a ∉ span K (f '' 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

Premises used: linearIndependent_option, Function.comp_def, Set.range_comp', LinearIndepOn