ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
⊢ ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card t
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
⊢ ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card t
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_linearIndependent_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 <|
        Subset.trans
          (by simp [inter_subset_inter, Subset.refl, -inter_subset_left, -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)) := by
          exact 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, hb₂s, hs']) hst this
      ⟨u, Subset.trans hust <| union_subset_union (Subset.refl _) (by simp [subset_insert]), hsu,
        by simp [eq, Finset.card_insert_of_not_mem hb₂t', hb₁t, hb₁s']⟩
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
eq : Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t = t
⊢ ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card t
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
⊢ ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card t
have eq : ((t.filter fun x => x ∈ s) ∪ t.filter fun x => x ∉ s) = t := by
  ext1 x
  by_cases x ∈ s <;> simp [*]
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
eq : Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t = t
⊢ ∀ (a : Finset V),
    ↑a ⊆ s ∪ ↑(Finset.filter (fun x => ¬x ∈ s) t) ∧
        s ⊆ ↑a ∧ Finset.card a = Finset.card (Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t) →
      ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card t
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
eq : Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t = t
⊢ ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card t
apply
  Exists.elim
    (this (t.filter fun x => x ∉ s) (t.filter fun x => x ∈ s) (by simp [Set.subset_def])
      (by simp (config := { contextual := true }) [Set.ext_iff]) (by rwa [eq]))
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
eq : Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t = t
u : Finset V
h :
  ↑u ⊆ s ∪ ↑(Finset.filter (fun x => ¬x ∈ s) t) ∧
    s ⊆ ↑u ∧ Finset.card u = Finset.card (Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t)
⊢ ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card t
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
eq : Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t = t
⊢ ∀ (a : Finset V),
    ↑a ⊆ s ∪ ↑(Finset.filter (fun x => ¬x ∈ s) t) ∧
        s ⊆ ↑a ∧ Finset.card a = Finset.card (Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t) →
      ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card t
intro u h
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
eq : Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t = t
u : Finset V
h :
  ↑u ⊆ s ∪ ↑(Finset.filter (fun x => ¬x ∈ s) t) ∧
    s ⊆ ↑u ∧ Finset.card u = Finset.card (Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t)
⊢ ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card t
exact
  ⟨u, Subset.trans h.1 (by simp (config := { contextual := true }) [subset_def, and_imp, or_imp]),
    h.2.1, by simp only [h.2.2, eq]⟩
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝¹ : Set V
x y z : V
t✝ : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t✝)
t s' : Finset V
hs' : ↑s' ⊆ s
x✝ : s ∩ ↑∅ = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ ∅))
⊢ s ⊆ ↑(span K ↑s')
simpa using hss'
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝¹ : Set V
x y z : V
t✝ : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t✝)
t s' : Finset V
hs' : ↑s' ⊆ s
x✝ : s ∩ ↑∅ = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ ∅))
this : s = ↑s'
⊢ ↑s' ⊆ s ∪ ↑∅ ∧ s ⊆ ↑s' ∧ Finset.card s' = Finset.card (s' ∪ ∅)
simp [this]
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
h : b₁ ∈ s
this : b₁ ∈ s ∩ ↑(insert b₁ t)
⊢ False
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
h : b₁ ∈ s
⊢ False
have : b₁ ∈ s ∩ ↑(insert b₁ t) := ⟨h, Finset.mem_insert_self _ _⟩
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
h : b₁ ∈ s
this : b₁ ∈ s ∩ ↑(insert b₁ t)
⊢ False
rwa [hst] at this
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
⊢ s ∩ ↑t ⊆ s ∩ ↑(insert b₁ t)
simp [inter_subset_inter, Subset.refl, -inter_subset_left, -subset_inter_iff]
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this : s ⊆ ↑(span K ↑(s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
Eq : Finset.card u = Finset.card (s' ∪ t)
hb₁u : ¬b₁ ∈ u
⊢ ↑(insert b₁ u) ⊆ s ∪ ↑(insert b₁ t)
simp [insert_subset_insert hust]
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this : s ⊆ ↑(span K ↑(s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
Eq : Finset.card u = Finset.card (s' ∪ t)
hb₁u : ¬b₁ ∈ u
⊢ ↑u ⊆ ↑(insert b₁ u)
simp
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this : s ⊆ ↑(span K ↑(s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
Eq : Finset.card u = Finset.card (s' ∪ t)
hb₁u : ¬b₁ ∈ u
⊢ Finset.card (insert b₁ u) = Finset.card (s' ∪ insert b₁ t)
simp [Eq, hb₁t, hb₁s', hb₁u]
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
b₃ : V
hb₃ : b₃ ∈ s
this : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
b₃ : V
hb₃ : b₃ ∈ s
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))
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]
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t)))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
b₃ : V
hb₃ : b₃ ∈ s
this : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))
have hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t) : Set V)) :=
  span_mono this (hss' hb₃)
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝¹ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this✝ : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t)))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t)))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))
have : s ⊆ (span K (insert b₁ ↑(s' ∪ t)) : Submodule K V) := by
  simpa [insert_eq, -singleton_union, -union_singleton] using hss'
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝¹ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this✝ : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t)))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝¹ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this✝ : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t)))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))
have hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t)) := by
  exact mem_span_insert_exchange (this hb₂s) hb₂t
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝¹ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this✝ : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₂ ↑(s' ∪ t))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝¹ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this✝ : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t)))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))
rw [span_insert_eq_span hb₁] at hb₃
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝¹ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this✝ : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₂ ↑(s' ∪ t))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t))
⊢ b₃ ∈ ↑(span K ↑(insert b₂ s' ∪ t))
simpa using hb₃
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
b₃ : V
hb₃ : b₃ ∈ s
⊢ ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
simp only [insert_eq, union_subset_union, Subset.refl,
  subset_union_right, Finset.union_insert, Finset.coe_insert]
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t)))
⊢ s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
simpa [insert_eq, -singleton_union, -union_singleton] using hss'
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝¹ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
b₃ : V
hb₃✝ : b₃ ∈ s
this✝ : ↑(s' ∪ insert b₁ t) ⊆ insert b₁ (insert b₂ ↑(s' ∪ t))
hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t)))
this : s ⊆ ↑(span K (insert b₁ ↑(s' ∪ t)))
⊢ b₁ ∈ span K (insert b₂ ↑(s' ∪ t))
exact mem_span_insert_exchange (this hb₂s) hb₂t
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
this : s ⊆ ↑(span K ↑(insert b₂ s' ∪ t))
⊢ ↑(insert b₂ s') ⊆ s
simp [insert_subset, hb₂s, hs']
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
this : s ⊆ ↑(span K ↑(insert b₂ s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
eq : Finset.card u = Finset.card (insert b₂ s' ∪ t)
⊢ ↑t ⊆ ↑(insert b₁ t)
simp [subset_insert]
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝² : Set V
x y z : V
t✝¹ : Finset V
hs : LinearIndependent K fun x => ↑x
hst✝¹ : s ⊆ ↑(span K ↑t✝¹)
t✝ : Finset V
b₁ : V
t : Finset V
hb₁t : ¬b₁ ∈ t
ih :
  ∀ (s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
s' : Finset V
hs' : ↑s' ⊆ s
hst✝ : s ∩ ↑(insert b₁ t) = ∅
hss' : s ⊆ ↑(span K ↑(s' ∪ insert b₁ t))
hb₁s : ¬b₁ ∈ s
hb₁s' : ¬b₁ ∈ s'
hst : s ∩ ↑t = ∅
this✝ : ¬s ⊆ ↑(span K ↑(s' ∪ t))
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : ¬b₂ ∈ ↑(span K ↑(s' ∪ t))
hb₂t' : ¬b₂ ∈ s' ∪ t
this : s ⊆ ↑(span K ↑(insert b₂ s' ∪ t))
u : Finset V
hust : ↑u ⊆ s ∪ ↑t
hsu : s ⊆ ↑u
eq : Finset.card u = Finset.card (insert b₂ s' ∪ t)
⊢ Finset.card u = Finset.card (s' ∪ insert b₁ t)
simp [eq, Finset.card_insert_of_not_mem hb₂t', hb₁t, hb₁s']
case a
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x✝ y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
x : V
⊢ x ∈ Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t ↔ x ∈ t
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
⊢ Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t = t
ext1 x
no goals
case a
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x✝ y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
x : V
⊢ x ∈ Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t ↔ x ∈ t
by_cases x ∈ s <;> simp [*]
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
eq : Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t = t
⊢ ↑(Finset.filter (fun x => x ∈ s) t) ⊆ s
simp [Set.subset_def]
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
eq : Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t = t
⊢ s ∩ ↑(Finset.filter (fun x => ¬x ∈ s) t) = ∅
simp (config := { contextual := true }) [Set.ext_iff]
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
eq : Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t = t
⊢ s ⊆ ↑(span K ↑(Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t))
rwa [eq]
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
eq : Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t = t
u : Finset V
h :
  ↑u ⊆ s ∪ ↑(Finset.filter (fun x => ¬x ∈ s) t) ∧
    s ⊆ ↑u ∧ Finset.card u = Finset.card (Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t)
⊢ s ∪ ↑(Finset.filter (fun x => ¬x ∈ s) t) ⊆ s ∪ ↑t
simp (config := { contextual := true }) [subset_def, and_imp, or_imp]
no goals
ι : Type u'
ι' : Type ?u.1274584
R : Type ?u.1274587
K : Type u_1
M : Type ?u.1274593
M' : Type ?u.1274596
M'' : Type ?u.1274599
V : Type u
V' : Type ?u.1274604
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t✝ : Set V
x y z : V
t : Finset V
hs : LinearIndependent K fun x => ↑x
hst : s ⊆ ↑(span K ↑t)
this :
  ∀ (t s' : Finset V),
    ↑s' ⊆ s →
      s ∩ ↑t = ∅ → s ⊆ ↑(span K ↑(s' ∪ t)) → ∃ t', ↑t' ⊆ s ∪ ↑t ∧ s ⊆ ↑t' ∧ Finset.card t' = Finset.card (s' ∪ t)
eq : Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t = t
u : Finset V
h :
  ↑u ⊆ s ∪ ↑(Finset.filter (fun x => ¬x ∈ s) t) ∧
    s ⊆ ↑u ∧ Finset.card u = Finset.card (Finset.filter (fun x => x ∈ s) t ∪ Finset.filter (fun x => ¬x ∈ s) t)
⊢ Finset.card u = Finset.card t
simp only [h.2.2, eq]