-- Lean 4 proof step from Mathlib.LinearAlgebra.LinearIndependent.Lemmas (goal)
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)
⊢ LinearIndepOn K f (insert a s) ↔ LinearIndepOn K f s ∧ f a ∉ span K (f '' s)
have 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)
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