awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
rw :
  (∀ (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = 0) ↔
    ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
⊢ LinearIndepOn R v (↑s : Set ι) ↔
    ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0

Tactic:
rw [LinearIndepOn, Fintype.linearIndependent_iffₒₛ]

Premises used: Fintype.linearIndependent_iffₒₛ, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
⊢ (∀ (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = 0) ↔
    ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0

Tactic:
⟨fun h t ht f heq i hi => h { i | i.1 ∈ t } (f ∘ Subtype.val) ?_ ⟨i, hi⟩,
    fun h t f heq i => ?_⟩

Premises used: Finset.univ, Function.comp, Membership.mem, Subtype.mk, Iff.intro, Subtype.val, Finset.filter
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
refine_1 :
  ∀
    (h :
      ∀ (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R),
        Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)) →
          ∀ (i : (↑(↑s : Set ι) : Type u')), f i = 0)
    (t : Finset ι) (ht : t ⊆ s) (f : ι → R) (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i))
    (i : ι) (hi : i ∈ s),
    Eq.{u_4 + 1} (α := M)
      (∑ i : (↑(↑s : Set ι) : Type u') with (↑i : ι) ∈ t,
        (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑s : Set ι))) i • v (↑i : ι))
      (∑ i ∈ {i : (↑(↑s : Set ι) : Type u') | (↑i : ι) ∈ t}ᶜ,
        (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑s : Set ι))) i • v (↑i : ι))
refine_2 :
  ∀ (h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0)
    (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R)
    (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)))
    (i : (↑(↑s : Set ι) : Type u')), f i = 0
⊢ (∀ (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = 0) ↔
    ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0

Tactic:
refine ⟨fun h t ht f heq i hi => h { i | i.1 ∈ t } (f ∘ Subtype.val) ?_ ⟨i, hi⟩,
    fun h t f heq i => ?_⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h :
  ∀ (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = 0
t : Finset ι
ht : t ⊆ s
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)
i : ι
hi : i ∈ s
refine_1 :
  Eq.{u_4 + 1} (α := M) (∑ a : ↥s, if (↑a : ι) ∈ t then f (↑a : ι) • v (↑a : ι) else 0)
    (∑ a : ↥s, if (↑a : ι) ∉ t then f (↑a : ι) • v (↑a : ι) else 0)
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i : (↑(↑s : Set ι) : Type u') with (↑i : ι) ∈ t,
      (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑s : Set ι))) i • v (↑i : ι))
    (∑ i ∈ {i : (↑(↑s : Set ι) : Type u') | (↑i : ι) ∈ t}ᶜ,
      (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ (↑s : Set ι))) i • v (↑i : ι))

Tactic:
simp only [Finset.compl_filter, Finset.sum_filter, Function.comp_apply, Finset.coe_sort_coe]

Premises used: Finset.coe_sort_coe, Finset.compl_filter, Function.comp_apply, Finset.sum_filter
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h :
  ∀ (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = 0
t : Finset ι
ht : t ⊆ s
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)
i : ι
hi : i ∈ s
refine_1 : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, if i ∈ t then f i • v i else 0) (∑ i ∈ s, if i ∉ t then f i • v i else 0)
⊢ Eq.{u_4 + 1} (α := M) (∑ a : ↥s, if (↑a : ι) ∈ t then f (↑a : ι) • v (↑a : ι) else 0)
    (∑ a : ↥s, if (↑a : ι) ∉ t then f (↑a : ι) • v (↑a : ι) else 0)

Tactic:
rw [Finset.sum_coe_sort s fun i => if i ∈ t then f i • v i else 0,
      Finset.sum_coe_sort s fun i => if i ∉ t then f i • v i else 0]

Premises used: Membership.mem, HSMul.hSMul, OfNat.ofNat, Not, Finset.sum_coe_sort, ite
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h :
  ∀ (t : Finset (↑(↑s : Set ι) : Type u')) (f : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = 0
t : Finset ι
ht : t ⊆ s
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)
i : ι
hi : i ∈ s
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, if i ∈ t then f i • v i else 0) (∑ i ∈ s, if i ∉ t then f i • v i else 0)

Tactic:
simpa [Finset.inter_eq_right.2 ht, Finset.sum_ite, Finset.filter_notMem_eq_sdiff]

Premises used: Finset.filter_notMem_eq_sdiff, Iff.mpr, Finset.inter_eq_right, Finset.sum_ite
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
refine_2 :
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
    (∑ i ∈ s \ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
refine_2₁ :
  ∀
    (h :
      Eq.{u_2 + 1} (α := R)
        (if h : (↑i : ι) ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) (↑i : ι) h) else 0) 0),
    f i = 0
⊢ f i = 0

Tactic:
specialize h (t.map (Embedding.subtype _)) (Finset.map_subtype_subset _)
      (fun i => if h : i ∈ s then f ⟨i, h⟩ else 0) ?_ i i.2

Premises used: Finset.map_subtype_subset, Finset.map, Membership.mem, dite, Subtype.mk, Function.Embedding.subtype, OfNat.ofNat, Subtype.val, Subtype.property
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
enter : s
| Eq.{u_4 + 1} (α := M)
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
    (∑ i ∈ s \ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))

Tactic:
enter [2, 1, 1]
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
rw : Finset.map (Embedding.subtype (Membership.mem s)) Finset.univ
| s

Tactic:
rw [← s.subtype_map_of_mem (fun x hx => hx), Finset.subtype_eq_univ.2 (fun x hx => hx)]

Premises used: Iff.mpr, Finset.subtype_map_of_mem, Finset.subtype_eq_univ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
enter : Finset.map (α := { x : ι // x ∈ (↑s : Set ι) }) (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) Finset.univ
| Eq.{u_4 + 1} (α := M)
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
    (∑ i ∈ s \ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))

Tactic:
enter [2, 1, 1]
        rw [← s.subtype_map_of_mem (fun x hx => hx), Finset.subtype_eq_univ.2 (fun x hx => hx)]
        change Finset.map (Embedding.subtype (· ∈ (s : Set ι))) _

Premises used: Iff.mpr, Finset.subtype_map_of_mem, Finset.subtype_eq_univ, Finset.map, Membership.mem, SetLike.coe, Function.Embedding.subtype
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
refine_2 :
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
    (∑
      i ∈
        Finset.map (α := { x : ι // x ∈ (↑s : Set ι) }) (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) Finset.univ \
          Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
    (∑ i ∈ s \ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))

Tactic:
conv =>
        enter [2, 1, 1]
        rw [← s.subtype_map_of_mem (fun x hx => hx), Finset.subtype_eq_univ.2 (fun x hx => hx)]
        change Finset.map (Embedding.subtype (· ∈ (s : Set ι))) _

Premises used: Iff.mpr, Finset.subtype_map_of_mem, Finset.subtype_eq_univ, Finset.map, Membership.mem, SetLike.coe, Function.Embedding.subtype
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
refine_2 :
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) (Finset.univ \ t),
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
    (∑
      i ∈
        Finset.map (α := { x : ι // x ∈ (↑s : Set ι) }) (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) Finset.univ \
          Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))

Tactic:
rw [← Finset.map_sdiff]

Premises used: Finset.map_sdiff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h : ∀ t ⊆ s, ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) → ∀ i ∈ s, f i = 0
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) t,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))
    (∑ i ∈ Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ (↑s : Set ι)) (Finset.univ \ t),
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (i : ι) ↦ (if h : i ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i h) else 0 : R)) i)
        (v i))

Tactic:
simpa [Embedding.subtype, ← Finset.compl_eq_univ_sdiff]

Premises used: Finset.compl_eq_univ_sdiff, Function.Embedding.subtype
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
t : Finset (↑(↑s : Set ι) : Type u')
f : (↑(↑s : Set ι) : Type u') → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v (↑i : ι)) (∑ i ∈ tᶜ, f i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
h :
  Eq.{u_2 + 1} (α := R)
    (if h : (↑i : ι) ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) (↑i : ι) h) else 0) 0
⊢ f i = 0

Tactic:
simpa using h
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
simp :
  (∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
      Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0) ↔
    ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
⊢ ¬LinearIndepOn R v (↑s : Set ι) ↔
    ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, 0 < f i

Tactic:
simp only [linearIndepOn_finset_iffₒₛ, not_forall, pos_iff_ne_zero]

Premises used: linearIndepOn_finset_iffₒₛ, Classical.not_forall, pos_iff_ne_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
⊢ (∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
      Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0) ↔
    ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
⟨fun ⟨t, hst, f, heq, i, hi, hfi⟩ => ?_,
    fun ⟨t, hst, f, heq, i, hi, hfi⟩ => ⟨t, hst, f, heq, i, hst hi, hfi⟩⟩

Premises used: _private.0.not_linearIndepOn_finset_iffₒₛ.match_1, Membership.mem, Exists, HasSubset.Subset, Ne, _private.0.not_linearIndepOn_finset_iffₒₛ.match_2, SDiff.sdiff, And, Iff.intro, Exists.intro, HSMul.hSMul, OfNat.ofNat, Eq, Not, Finset.sum
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
refine :
  (∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
      Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0) →
    ∀ (t : Finset ι) (hst : t ⊆ s) (f : ι → R)
      (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)) (i : ι) (hi : i ∈ s) (hfi : ¬f i = 0),
      ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
⊢ (∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
      Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0) ↔
    ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
refine ⟨fun ⟨t, hst, f, heq, i, hi, hfi⟩ => ?_,
    fun ⟨t, hst, f, heq, i, hi, hfi⟩ => ⟨t, hst, f, heq, i, hst hi, hfi⟩⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h :
  ∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
    Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)
i : ι
hi : i ∈ s
hfi : ¬f i = 0
pos :
  ∀ (hi' : i ∈ t),
    ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
neg :
  ∀ (hi' : i ∉ t),
    ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
⊢ ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
by_cases hi' : i ∈ t
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h :
  ∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
    Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∈ t
⊢ ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
⟨t, hst, f, heq, i, hi', hfi⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : LinearOrder R
inst_4 : CanonicallyOrderedAdd R
inst_5 : AddRightReflectLE R
inst_6 : IsCancelAdd M
inst_7 : DecidableEq ι
s : Finset ι
h :
  ∃ (x : Finset ι) (_ : x ⊆ s) (x_1 : ι → R) (_ :
    Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ s \ x, x_1 i • v i)) (x : ι) (_ : x ∈ s), ¬x_1 x = 0
t : Finset ι
hst : t ⊆ s
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i)
i : ι
hi : i ∈ s
hfi : ¬f i = 0
hi' : i ∈ t
⊢ ∃ t ⊆ s, ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ s \ t, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
exact ⟨t, hst, f, heq, i, hi', hfi⟩