awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ id '' t ⊆ (↑(span K (id '' hs.extend (s := s) (t := t) hst)) : Set V)

Tactic:
hs.image_subset_span_image_extend hst

Premises used: LinearIndepOn.image_subset_span_image_extend
-- 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 t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
h : t = id '' t
h₁ : hs.extend (s := s) (t := t) hst = id '' hs.extend (s := s) (t := t) hst
⊢ t ⊆ (↑(span K (hs.extend (s := s) (t := t) hst)) : Set V)

Tactic:
convert! hs.image_subset_span_image_extend hst

Premises used: LinearIndepOn.image_subset_span_image_extend
-- 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 t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ t = id '' t

Tactic:
simp
-- 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 t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ hs.extend (s := s) (t := t) hst = id '' hs.extend (s := s) (t := t) hst

Tactic:
simp
-- 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
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
⊢ Eq (α := Submodule K V) (span K (v '' hs.extend (s := s) (t := t) hst)) (span K (v '' t))

Tactic:
le_antisymm (span_mono (image_mono (hs.extend_subset hst)))
    (span_le.2 (hs.image_subset_span_image_extend hst))

Premises used: Iff.mpr, LinearIndepOn.extend_subset, Set.image_mono, le_antisymm, LinearIndepOn.image_subset_span_image_extend, Submodule.span_mono, Submodule.span_le
-- 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 t : Set V
hs : LinearIndepOn K id s
hst : s ⊆ t
⊢ Eq (α := Submodule K V) (span K (hs.extend (s := s) (t := t) hst)) (span K t)

Tactic:
le_antisymm (span_mono (hs.extend_subset hst)) (span_le.2 (hs.subset_span_extend hst))

Premises used: Iff.mpr, LinearIndepOn.extend_subset, LinearIndepOn.subset_span_extend, le_antisymm, Submodule.span_mono, Submodule.span_le
-- 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
v : ι → V
s t : Set ι
hs : LinearIndepOn K v s
hst : s ⊆ t
⊢ LinearIndepOn K v (hs.extend (s := s) (t := t) hst)

Tactic:
let ⟨_hbt, _hsb, _htb, hli⟩ := Classical.choose_spec (exists_linearIndepOn_extension hs hst)
  hli

Premises used: LinearIndepOn.extend, exists_linearIndepOn_extension, Classical.choose_spec, _private.0.LinearIndepOn.extend_subset.match_1, LinearIndepOn
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t s' : Finset V
hs' : (↑s' : Set V) ⊆ s
h : s ∩ (↑∅ : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ ∅) : Set V)) : Set V)
⊢ s ⊆ (↑(span K (↑s' : Set V)) : Set V)

Tactic:
simpa using hss'
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t s' : Finset V
hs' : (↑s' : Set V) ⊆ s
h : s ∩ (↑∅ : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ ∅) : Set V)) : Set V)
this : s = (↑s' : Set V)
⊢ (↑s' : Set V) ⊆ s ∪ (↑∅ : Set V) ∧ s ⊆ (↑s' : Set V) ∧ s'.card = (s' ∪ ∅).card

Tactic:
simp [this]
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
h : b₁ ∈ s
⊢ b₁ ∈ s ∩ (↑(insert b₁ t) : Set V)

Tactic:
have : b₁ ∈ s ∩ ↑(insert b₁ t) := ⟨h, Finset.mem_insert_self _ _⟩
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
h : b₁ ∈ s
this : b₁ ∈ s ∩ (↑(insert b₁ t) : Set V)
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : Membership.mem (γ := Set V) ∅ b₁), False
⊢ False

Tactic:
rwa [hst] at this
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
⊢ s ∩ (↑t : Set V) ⊆ s ∩ (↑(insert b₁ t) : Set V)

Tactic:
simp [inter_subset_inter, -subset_inter_iff]

Premises used: Set.subset_inter_iff, Set.inter_subset_inter
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this : s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
u : Finset V
hust : (↑u : Set V) ⊆ s ∪ (↑t : Set V)
hsu : s ⊆ (↑u : Set V)
Eq : u.card = (s' ∪ t).card
hb₁u : b₁ ∉ u
⊢ (↑(insert b₁ u) : Set V) ⊆ s ∪ (↑(insert b₁ t) : Set V)

Tactic:
simp [insert_subset_insert hust]

Premises used: Set.insert_subset_insert
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this : s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
u : Finset V
hust : (↑u : Set V) ⊆ s ∪ (↑t : Set V)
hsu : s ⊆ (↑u : Set V)
Eq : u.card = (s' ∪ t).card
hb₁u : b₁ ∉ u
⊢ (↑u : Set V) ⊆ (↑(insert b₁ u) : Set V)

Tactic:
simp
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this : s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
u : Finset V
hust : (↑u : Set V) ⊆ s ∪ (↑t : Set V)
hsu : s ⊆ (↑u : Set V)
Eq : u.card = (s' ∪ t).card
hb₁u : b₁ ∉ u
⊢ (insert b₁ u).card = (s' ∪ insert b₁ t).card

Tactic:
simp [Eq, hb₁t, hb₁s', hb₁u]
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃ : b₃ ∈ s
⊢ (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))

Tactic:
simp only [insert_eq, union_subset_union, Subset.refl,
              subset_union_right, Finset.union_insert, Finset.coe_insert]

Premises used: Set.Subset.refl, Set.insert_eq, Set.union_subset_union, Set.subset_union_right, Finset.union_insert, Finset.coe_insert
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃ : b₃ ∈ s
⊢ (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))

Tactic:
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]
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this_1 : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃ : b₃ ∈ s
this : (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))
⊢ Membership.mem (γ := Submodule K V) (span K (insert b₁ (insert b₂ (↑(s' ∪ t) : Set V)))) b₃

Tactic:
have hb₃ : b₃ ∈ span K (insert b₁ (insert b₂ ↑(s' ∪ t) : Set V)) :=
            span_mono this (hss' hb₃)
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this_1 : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃_1 : b₃ ∈ s
this : (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))
hb₃ : Membership.mem (γ := Submodule K V) (span K (insert b₁ (insert b₂ (↑(s' ∪ t) : Set V)))) b₃
⊢ s ⊆ (↑(span K (insert b₁ (↑(s' ∪ t) : Set V))) : Set V)

Tactic:
simpa [insert_eq, -singleton_union, -union_singleton] using hss'

Premises used: Set.insert_eq, Set.singleton_union, Set.union_singleton
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this_1 : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃_1 : b₃ ∈ s
this : (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))
hb₃ : Membership.mem (γ := Submodule K V) (span K (insert b₁ (insert b₂ (↑(s' ∪ t) : Set V)))) b₃
⊢ s ⊆ (↑(span K (insert b₁ (↑(s' ∪ t) : Set V))) : Set V)

Tactic:
have : s ⊆ (span K (insert b₁ ↑(s' ∪ t)) : Submodule K V) := by
            simpa [insert_eq, -singleton_union, -union_singleton] using hss'
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this_1 : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃_1 : b₃ ∈ s
this_2 : (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))
hb₃ : Membership.mem (γ := Submodule K V) (span K (insert b₁ (insert b₂ (↑(s' ∪ t) : Set V)))) b₃
this : s ⊆ (↑(span K (insert b₁ (↑(s' ∪ t) : Set V))) : Set V)
⊢ Membership.mem (γ := Submodule K V) (span K (insert b₂ (↑(s' ∪ t) : Set V))) b₁

Tactic:
have hb₁ : b₁ ∈ span K (insert b₂ ↑(s' ∪ t)) :=
            mem_span_insert_exchange (this hb₂s) hb₂t
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this_1 : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃_1 : b₃ ∈ s
this_2 : (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))
hb₃ : Membership.mem (γ := Submodule K V) (span K (insert b₁ (insert b₂ (↑(s' ∪ t) : Set V)))) b₃
this : s ⊆ (↑(span K (insert b₁ (↑(s' ∪ t) : Set V))) : Set V)
hb₁ : Membership.mem (γ := Submodule K V) (span K (insert b₂ (↑(s' ∪ t) : Set V))) b₁
⊢ Membership.mem (γ := Submodule K V) (span K (insert b₂ (↑(s' ∪ t) : Set V))) b₃

Tactic:
rw [span_insert_eq_span hb₁] at hb₃

Premises used: Submodule.span_insert_eq_span
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this_1 : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃_1 : b₃ ∈ s
this_2 : (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))
hb₃ : Membership.mem (γ := Submodule K V) (span K (insert b₁ (insert b₂ (↑(s' ∪ t) : Set V)))) b₃
this : s ⊆ (↑(span K (insert b₁ (↑(s' ∪ t) : Set V))) : Set V)
hb₁ : Membership.mem (γ := Submodule K V) (span K (insert b₂ (↑(s' ∪ t) : Set V))) b₁
hb₄ : Membership.mem (γ := Submodule K V) (span K (insert b₂ (↑(s' ∪ t) : Set V))) b₃
⊢ s ⊆ (↑(span K (insert b₁ (↑(s' ∪ t) : Set V))) : Set V)

Tactic:
rw [span_insert_eq_span hb₁] at hb₃

Premises used: Submodule.span_insert_eq_span
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this_1 : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃_1 : b₃ ∈ s
this_2 : (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))
hb₃ : Membership.mem (γ := Submodule K V) (span K (insert b₁ (insert b₂ (↑(s' ∪ t) : Set V)))) b₃
this : s ⊆ (↑(span K (insert b₁ (↑(s' ∪ t) : Set V))) : Set V)
hb₁ : Membership.mem (γ := Submodule K V) (span K (insert b₂ (↑(s' ∪ t) : Set V))) b₁
hb₄ : Membership.mem (γ := Submodule K V) (span K (insert b₂ (↑(s' ∪ t) : Set V))) b₃
this₁ : s ⊆ (↑(span K (insert b₁ (↑(s' ∪ t) : Set V))) : Set V)
⊢ Membership.mem (γ := Submodule K V) (span K (insert b₂ (↑(s' ∪ t) : Set V))) b₁

Tactic:
rw [span_insert_eq_span hb₁] at hb₃

Premises used: Submodule.span_insert_eq_span
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this_1 : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
b₃ : V
hb₃_1 : b₃ ∈ s
this_2 : (↑(s' ∪ insert b₁ t) : Set V) ⊆ insert b₁ (insert b₂ (↑(s' ∪ t) : Set V))
hb₃ : Membership.mem (γ := Submodule K V) (span K (insert b₂ (↑(s' ∪ t) : Set V))) b₃
this : s ⊆ (↑(span K (insert b₁ (↑(s' ∪ t) : Set V))) : Set V)
hb₁ : Membership.mem (γ := Submodule K V) (span K (insert b₂ (↑(s' ∪ t) : Set V))) b₁
⊢ b₃ ∈ (↑(span K (↑(insert b₂ s' ∪ t) : Set V)) : Set V)

Tactic:
simpa using hb₃
-- 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_1 : Finset V
hs : LinearIndepOn K id s
hst_1 : s ⊆ (↑(span K (↑t_1 : Set V)) : Set V)
t_2 : Finset V
b₁ : V
t : Finset V
hb₁t : b₁ ∉ t
ih :
  ∀ (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
s' : Finset V
hs' : (↑s' : Set V) ⊆ s
hst_2 : s ∩ (↑(insert b₁ t) : Set V) = ∅
hss' : s ⊆ (↑(span K (↑(s' ∪ insert b₁ t) : Set V)) : Set V)
hb₁s : b₁ ∉ s
hb₁s' : b₁ ∉ s'
hst : s ∩ (↑t : Set V) = ∅
this_1 : ¬s ⊆ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
b₂ : V
hb₂s : b₂ ∈ s
hb₂t : b₂ ∉ (↑(span K (↑(s' ∪ t) : Set V)) : Set V)
hb₂t' : b₂ ∉ s' ∪ t
this : s ⊆ (↑(span K (↑(insert b₂ s' ∪ t) : Set V)) : Set V)
⊢ (↑(insert b₂ s') : Set V) ⊆ s

Tactic:
simp [insert_subset_iff, hb₂s, hs']

Premises used: Set.insert_subset_iff