-- Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas
Goal:
K : Type u_3
V : Type u
inst : DivisionRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
s : Set V
t : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ (↑(span K (↑t : Set V)) : Set V)
have have₁ have₂ :
  ∀
    (this :
      ∀ (t s' : Finset V),
        (↑s' : Set V) ⊆ s →
          s ∩ (↑t : Set V) = ∅ →
            s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
              ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card),
    ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = t.card
have₃ :
  ∀
    (this :
      ∀ (t s' : Finset V),
        (↑s' : Set V) ⊆ s →
          s ∩ (↑t : Set V) = ∅ →
            s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
              ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card)
    (eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t),
    ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = t.card
have₄ have₅ :
  ∀
    (this :
      ∀ (t s' : Finset V),
        (↑s' : Set V) ⊆ s →
          s ∩ (↑t : Set V) = ∅ →
            s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V) →
              ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = (s' ∪ t).card)
    (eq : {x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s} = t) (u : Finset V)
    (h :
      (↑u : Set V) ⊆ s ∪ (↑({x ∈ t | x ∉ s}) : Set V) ∧
        s ⊆ (↑u : Set V) ∧ u.card = ({x ∈ t | x ∈ s} ∪ {x ∈ t | x ∉ s}).card),
    ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = t.card
⊢ ∃ (t' : Finset V), (↑t' : Set V) ⊆ s ∪ (↑t : Set V) ∧ s ⊆ (↑t' : Set V) ∧ t'.card = t.card

Tactic:
classical
  have :
    ∀ t : Finset V,
      ∀ s' : Finset V,
        ↑s' ⊆ s →
          s ∩ ↑t = ∅ →
            s ⊆ (span K ↑(s' ∪ t) : Submodule K V) →
              ∃ t' : Finset V, ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ t'.card = (s' ∪ t).card :=
    fun t =>
    Finset.induction_on t
      (fun s' hs' _ hss' =>
        have : s = ↑s' := eq_of_linearIndepOn_id_of_span_subtype hs hs' <| by simpa using hss'
        ⟨s', by simp [this]⟩)
      fun b₁ t hb₁t ih s' hs' hst hss' =>
      have hb₁s : b₁ ∉ s := fun h => by
        have : b₁ ∈ s ∩ ↑(insert b₁ t) := ⟨h, Finset.mem_insert_self _ _⟩
        rwa [hst] at this
      have hb₁s' : b₁ ∉ s' := fun h => hb₁s <| hs' h
      have hst : s ∩ ↑t = ∅ :=
        eq_empty_of_subset_empty <|
          -- Porting note: `-subset_inter_iff` required.
          Subset.trans
            (by simp [inter_subset_inter, -subset_inter_iff])
            (le_of_eq hst)
      Classical.by_cases (p := s ⊆ (span K ↑(s' ∪ t) : Submodule K V))
        (fun this =>
          let ⟨u, hust, hsu, Eq⟩ := ih _ hs' hst this
          have hb₁u : b₁ ∉ u := fun h => (hust h).elim hb₁s hb₁t
          ⟨insert b₁ u, by simp [insert_subset_insert hust], Subset.trans hsu (by simp), by
            simp [Eq, hb₁t, hb₁s', hb₁u]⟩)
        fun this =>
        let ⟨b₂, hb₂s, hb₂t⟩ := not_subset.mp this
        have hb₂t' : b₂ ∉ s' ∪ t := fun h => hb₂t <| subset_span h
        have : s ⊆ (span K ↑(insert b₂ s' ∪ t) : Submodule K V) := fun b₃ hb₃ => by
          have : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t) : Set V) := by
            simp only [insert_eq, union_subset_union, Subset.refl,
              subset_union_right, Finset.union_insert, Finset.coe_insert]
          have hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t) : Set V)) :=
            span_mono this (hss' hb₃)
          have : s ⊆ (span K (insert b₁ ↑(s' ∪ t)) : Submodule K V) := by
            simpa [insert_eq, -singleton_union, -union_singleton] using hss'
          have hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t)) :=
            mem_span_insert_exchange (this hb₂s) hb₂t
          rw [span_insert_eq_span hb₁] at hb₃; simpa using hb₃
        let ⟨u, hust, hsu, eq⟩ := ih _ (by simp [insert_subset_iff, hb₂s, hs']) hst this
        ⟨u, Subset.trans hust <| union_subset_union (Subset.refl _) (by simp [subset_insert]), hsu,
          by simp [eq, hb₂t', hb₁t, hb₁s']⟩
  have eq : ((t.filter fun x => x ∈ s) ∪ t.filter fun x => x ∉ s) = t := by
    ext1 x
    by_cases x ∈ s <;> simp [*]
  apply
    Exists.elim
      (this (t.filter fun x => x ∉ s) (t.filter fun x => x ∈ s) (by simp [Set.subset_def])
        (by simp +contextual [Set.ext_iff]) (by rwa [eq]))
  intro u h
  exact
    ⟨u, Subset.trans h.1 (by simp +contextual [subset_def, or_imp]),
      h.2.1, by simp only [h.2.2, eq]⟩