awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : V
rw :
  LinearIndependent.{u', u_3, u} (ι := ι) K (M := V)
        (comp (β := ι ⊕ PUnit.{u' + 1})
          ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
            (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
          Sum.inl) ∧
      Ne.{u + 1} (α := V)
          (comp (α := PUnit.{u' + 1}) (β := ι ⊕ PUnit.{u' + 1})
            ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
              (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
            Sum.inr default)
          0 ∧
        (Membership.mem (γ := Submodule K V)
            (span K
              (range (ι := ι)
                (comp (β := ι ⊕ PUnit.{u' + 1})
                  ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                    (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
                  Sum.inl)))
            (comp (α := PUnit.{u' + 1}) (β := ι ⊕ PUnit.{u' + 1})
              ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
              Sum.inr default) →
          Eq.{u + 1} (α := V)
            (comp (α := PUnit.{u' + 1}) (β := ι ⊕ PUnit.{u' + 1})
              ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
              Sum.inr default)
            0) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)
⊢ (LinearIndependent.{u', u_3, u} K (M := V) fun (o : Option ι) ↦ o.casesOn' x v) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
rw [← linearIndependent_equiv (Equiv.optionEquivSumPUnit.{u'} ι).symm, linearIndependent_sum,
    @range_unique _ PUnit, @linearIndependent_unique_iff PUnit, disjoint_span_singleton]

Premises used: Set.range_unique, linearIndependent_sum, Submodule.disjoint_span_singleton, linearIndependent_unique_iff
-- 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
x : V
dsimp :
  LinearIndependent.{u', u_3, u} (ι := ι) K (M := V)
        (comp (β := ι ⊕ PUnit.{u' + 1})
          ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
            (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
          Sum.inl) ∧
      ¬x = 0 ∧
        (Membership.mem (γ := Submodule K V)
            (span K
              (range (ι := ι)
                (comp (β := ι ⊕ PUnit.{u' + 1})
                  ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                    (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
                  Sum.inl)))
            x →
          x = 0) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)
⊢ LinearIndependent.{u', u_3, u} (ι := ι) K (M := V)
        (comp (β := ι ⊕ PUnit.{u' + 1})
          ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
            (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
          Sum.inl) ∧
      Ne.{u + 1} (α := V)
          (comp (α := PUnit.{u' + 1}) (β := ι ⊕ PUnit.{u' + 1})
            ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
              (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
            Sum.inr default)
          0 ∧
        (Membership.mem (γ := Submodule K V)
            (span K
              (range (ι := ι)
                (comp (β := ι ⊕ PUnit.{u' + 1})
                  ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                    (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
                  Sum.inl)))
            (comp (α := PUnit.{u' + 1}) (β := ι ⊕ PUnit.{u' + 1})
              ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
              Sum.inr default) →
          Eq.{u + 1} (α := V)
            (comp (α := PUnit.{u' + 1}) (β := ι ⊕ PUnit.{u' + 1})
              ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
              Sum.inr default)
            0) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
dsimp [(· ∘ ·)]

Premises used: Function.comp
-- 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
x : V
⊢ LinearIndependent.{u', u_3, u} (ι := ι) K (M := V)
        (comp (β := ι ⊕ PUnit.{u' + 1})
          ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
            (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
          Sum.inl) ∧
      ¬x = 0 ∧
        (Membership.mem (γ := Submodule K V)
            (span K
              (range (ι := ι)
                (comp (β := ι ⊕ PUnit.{u' + 1})
                  ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                    (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
                  Sum.inl)))
            x →
          x = 0) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
⟨fun h => ⟨h.1, fun hx => h.2.1 <| h.2.2 hx⟩, fun h => ⟨h.1, ?_, fun hx => (h.2 hx).elim⟩⟩

Premises used: False.elim, And.right, And.left, And.intro, Iff.intro
-- 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
x : V
refine : ∀ (h : LinearIndependent K v ∧ x ∉ span K (range v)), ¬x = 0
⊢ LinearIndependent.{u', u_3, u} (ι := ι) K (M := V)
        (comp (β := ι ⊕ PUnit.{u' + 1})
          ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
            (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
          Sum.inl) ∧
      ¬x = 0 ∧
        (Membership.mem (γ := Submodule K V)
            (span K
              (range (ι := ι)
                (comp (β := ι ⊕ PUnit.{u' + 1})
                  ((fun (o : Option ι) ↦ o.casesOn' x v) ∘
                    (⇑(Equiv.optionEquivSumPUnit ι).symm : (a : ι ⊕ PUnit.{u' + 1}) → Option ι))
                  Sum.inl)))
            x →
          x = 0) ↔
    LinearIndependent K v ∧ x ∉ span K (range v)

Tactic:
refine ⟨fun h => ⟨h.1, fun hx => h.2.1 <| h.2.2 hx⟩, fun h => ⟨h.1, ?_, fun hx => (h.2 hx).elim⟩⟩
-- 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
h : LinearIndependent K v ∧ 0 ∉ span K (range v)
⊢ False

Tactic:
h.2 (zero_mem _)

Premises used: And.right, ZeroMemClass.zero_mem
-- 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
h : LinearIndependent K v ∧ 0 ∉ span K (range v)
⊢ False

Tactic:
exact h.2 (zero_mem _)

Premises used: And.right, ZeroMemClass.zero_mem
-- 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
x : V
hv : LinearIndependent K v
hx : x ∉ span K (range v)
⊢ LinearIndependent.{u', u_3, u} K (M := V) fun (o : Option ι) ↦ o.casesOn' x v

Tactic:
linearIndependent_option'.2 ⟨hv, hx⟩

Premises used: Iff.mpr, And.intro, linearIndependent_option'
-- 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 : Option ι → V
⊢ LinearIndependent K v ↔ LinearIndependent K (v ∘ some) ∧ v none ∉ span K (range (v ∘ some))

Tactic:
simp only [← linearIndependent_option', Option.casesOn'_none_coe]

Premises used: Option.casesOn'_none_coe, linearIndependent_option'
-- 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} (ι := (↑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)

Tactic:
rw [LinearIndepOn, LinearIndepOn, ← linearIndependent_equiv
    ((Equiv.optionEquivSumPUnit _).trans (Equiv.Set.insert has).symm), linearIndependent_option]

Premises used: linearIndependent_option, Equiv.trans, Equiv.optionEquivSumPUnit, linearIndependent_equiv, Equiv.symm, Equiv.Set.insert, LinearIndepOn
-- 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
simp :
  (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)
⊢ 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)

Tactic:
simp only [comp_def]

Premises used: Function.comp_def
-- 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 : (↑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)
⊢ (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:
rw [range_comp']

Premises used: Set.range_comp'
-- 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
⊢ (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)

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
x : V
hxs : x ∉ s
⊢ LinearIndepOn K id s ∧ id x ∉ span K (id '' s) ↔ LinearIndepOn K id s ∧ x ∉ span K s

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
s : Set ι
a : ι
f : ι → V
pos :
  ∀ (has : a ∈ s),
    LinearIndepOn K f (insert a s) ↔
      LinearIndepOn K f s ∧ (Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) → a ∈ s)
neg :
  ∀ (has : a ∉ s),
    LinearIndepOn K f (insert a s) ↔
      LinearIndepOn K f s ∧ (Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) → a ∈ s)
⊢ LinearIndepOn K f (insert a s) ↔
    LinearIndepOn K f s ∧ (Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) → a ∈ s)

Tactic:
by_cases has : a ∈ s
-- 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
⊢ LinearIndepOn K f (insert a s) ↔
    LinearIndepOn K f s ∧ (Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) → a ∈ s)

Tactic:
simp [insert_eq_of_mem has, has]

Premises used: Set.insert_eq_of_mem
-- 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
⊢ LinearIndepOn K f (insert a s) ↔
    LinearIndepOn K f s ∧ (Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) → a ∈ s)

Tactic:
simp [linearIndepOn_insert has, has]

Premises used: linearIndepOn_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
a : V
s : Set V
⊢ LinearIndepOn K id (insert a s) ↔ LinearIndepOn K id s ∧ (Membership.mem (γ := Submodule K V) (span K s) a → a ∈ s)

Tactic:
simpa using linearIndepOn_insert_iff (a := a) (f := id)

Premises used: linearIndepOn_insert_iff
-- 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
h : LinearIndepOn K f s
pos :
  ∀ (has : a ∈ s), Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) ↔ LinearIndepOn K f (insert a s) → a ∈ s
neg :
  ∀ (has : a ∉ s), Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) ↔ LinearIndepOn K f (insert a s) → a ∈ s
⊢ Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) ↔ LinearIndepOn K f (insert a s) → a ∈ s

Tactic:
by_cases has : a ∈ s
-- 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
h : LinearIndepOn K f s
has : a ∈ s
⊢ Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) ↔ LinearIndepOn K f (insert a s) → a ∈ s

Tactic:
iff_of_true (subset_span <| mem_image_of_mem f has) fun _ ↦ has

Premises used: iff_of_true, Set.mem_image_of_mem, Submodule.subset_span
-- 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
h : LinearIndepOn K f s
has : a ∈ s
⊢ Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) ↔ LinearIndepOn K f (insert a s) → a ∈ s

Tactic:
exact iff_of_true (subset_span <| mem_image_of_mem f has) fun _ ↦ has

Premises used: iff_of_true, Set.mem_image_of_mem, Submodule.subset_span
-- 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
h : LinearIndepOn K f s
has : a ∉ s
⊢ Membership.mem (γ := Submodule K V) (span K (f '' s)) (f a) ↔ LinearIndepOn K f (insert a s) → a ∈ s

Tactic:
simp [linearIndepOn_insert_iff, h, has]

Premises used: linearIndepOn_insert_iff
-- 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
h : LinearIndepOn K f s
rw : ¬(LinearIndepOn K f (insert a s) → a ∈ s) ↔ LinearIndepOn K f (insert a s) ∧ a ∉ s
rw₁ rw₂ : LinearIndepOn K f (insert a s) ∧ a ∉ s ↔ LinearIndepOn K f (insert a s) ∧ a ∉ s
⊢ f a ∉ span K (f '' s) ↔ LinearIndepOn K f (insert a s) ∧ a ∉ s

Tactic:
rw [h.mem_span_iff, Classical.not_imp]

Premises used: LinearIndepOn.mem_span_iff, Classical.not_imp
-- 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
a : V
h : LinearIndepOn K id s
⊢ Membership.mem (γ := Submodule K V) (span K s) a ↔ LinearIndepOn K id (insert a s) → a ∈ s

Tactic:
simpa using h.mem_span_iff (a := a)

Premises used: LinearIndepOn.mem_span_iff
-- 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
a : V
h : LinearIndepOn K id s
rw : ¬(LinearIndepOn K id (insert a s) → a ∈ s) ↔ LinearIndepOn K id (insert a s) ∧ a ∉ s
rw₁ rw₂ : LinearIndepOn K id (insert a s) ∧ a ∉ s ↔ LinearIndepOn K id (insert a s) ∧ a ∉ s
⊢ a ∉ span K s ↔ LinearIndepOn K id (insert a s) ∧ a ∉ s

Tactic:
rw [h.mem_span_iff_id, Classical.not_imp]

Premises used: LinearIndepOn.mem_span_iff_id, Classical.not_imp
-- 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
x y : V
hx : x ≠ 0
hy : ∀ (a : K), a • x ≠ y
rw : LinearIndepOn (ι := V) K id {y, x}
⊢ LinearIndepOn (ι := V) K id {x, y}

Tactic:
rw [pair_comm]

Premises used: Set.pair_comm
-- 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
x y : V
hx : x ≠ 0
hy : ∀ (a : K), a • x ≠ y
⊢ y ∉ K ∙ x

Tactic:
simpa [mem_span_singleton]

Premises used: Submodule.mem_span_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
x y : V
hx : x ≠ 0
hy : ∀ (a : K), a • x ≠ y
⊢ LinearIndepOn (ι := V) K id {y, x}

Tactic:
exact .id_insert (.singleton hx) <| by simpa [mem_span_singleton]
-- 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
i j : ι
v : ι → V
hij : i ≠ j
hi : v i ≠ 0
rw : LinearIndepOn K v {j, i} ↔ ∀ (c : K), c • v i ≠ v j
⊢ LinearIndepOn K v {i, j} ↔ ∀ (c : K), c • v i ≠ v j

Tactic:
rw [pair_comm]

Premises used: Set.pair_comm
-- 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
i j : ι
v : ι → V
hij : i ≠ j
hi : v i ≠ 0
⊢ LinearIndepOn K v {j, i} ↔ LinearIndepOn K v {i} ∧ v j ∉ span K (v '' {i})

Tactic:
linearIndepOn_insert (s := { i }) (a := j) hij.symm

Premises used: Ne.symm, linearIndepOn_insert
-- 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
i j : ι
v : ι → V
hij : i ≠ j
hi : v i ≠ 0
h : (∀ (c : K), c • v i ≠ v j) ↔ LinearIndepOn K v {i} ∧ v j ∉ span K (v '' {i})
⊢ LinearIndepOn K v {j, i} ↔ ∀ (c : K), c • v i ≠ v j

Tactic:
convert! linearIndepOn_insert (s := { i }) (a := j) hij.symm

Premises used: Ne.symm, linearIndepOn_insert
-- 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
i j : ι
v : ι → V
hij : i ≠ j
hi : v i ≠ 0
⊢ (∀ (c : K), c • v i ≠ v j) ↔ LinearIndepOn K v {i} ∧ v j ∉ span K (v '' {i})

Tactic:
simp [hi, mem_span_singleton]

Premises used: Submodule.mem_span_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
x y : V
hx : x ≠ 0
⊢ Ne (α := Fin (Nat.succ 0).succ) 0 1

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
x y : V
hx : x ≠ 0
⊢ ![x, y] 0 ≠ 0

Tactic:
simpa