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
h :
  ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
    Disjoint s t ∧
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ((∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, f i ≠ 0)
s t : Finset ι
f : ι → R
hst : Disjoint s t
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i)
i : ι
hi : i ∈ t
hgi : f i ≠ 0
⊢ ∃ (s : Finset ι) (t : Finset ι) (f : ι → R),
    Disjoint s t ∧ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) ∧ ∃ i ∈ s, f i ≠ 0

Tactic:
exact ⟨t, s, f, hst.symm, heq.symm, i, hi, hgi⟩
-- 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 ι
inst_8 : Fintype ι
rw :
  (∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0) ↔
    ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
⊢ LinearIndependent R v ↔
    ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0

Tactic:
rw [linearIndependent_iffₒₛ]

Premises used: Fintype.linearIndependent_iffₒₛ
-- 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 ι
inst_8 : Fintype ι
⊢ (∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0) ↔
    ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0

Tactic:
⟨fun h t f heq i => ?_, fun h t₁ t₂ f ht₁t₂ heq => ?_⟩

Premises used: Iff.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 ι
inst_8 : Fintype ι
refine_1 :
  ∀
    (h :
      ∀ (s t : Finset ι) (f : ι → R),
        Disjoint s t →
          Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0)
    (t : Finset ι) (f : ι → R) (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)) (i : ι), f i = 0
refine_2 :
  ∀
    (h :
      ∀ (t : Finset ι) (f : ι → R),
        Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0)
    (t₁ t₂ : Finset ι) (f : ι → R) (ht₁t₂ : Disjoint t₁ t₂)
    (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)), (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0
⊢ (∀ (s t : Finset ι) (f : ι → R),
      Disjoint s t →
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0) ↔
    ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0

Tactic:
refine ⟨fun h t f heq i => ?_, fun h t₁ t₂ f ht₁t₂ heq => ?_⟩
-- 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 ι
inst_8 : Fintype ι
h :
  ∀ (s t : Finset ι) (f : ι → R),
    Disjoint s t →
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ t, f i • v i) → (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
⊢ (∀ i ∈ t, f i = 0) ∧ ∀ i ∈ tᶜ, f i = 0

Tactic:
specialize h t tᶜ f disjoint_compl_right heq

Premises used: Compl.compl, disjoint_compl_right
-- 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 ι
inst_8 : Fintype ι
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
h : (∀ i ∈ t, f i = 0) ∧ ∀ i ∈ tᶜ, f i = 0
pos : ∀ (hi : i ∈ t), f i = 0
neg : ∀ (hi : i ∉ t), f i = 0
⊢ 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 ι
inst_8 : Fintype ι
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
h : (∀ i ∈ t, f i = 0) ∧ ∀ i ∈ tᶜ, f i = 0
hi : i ∈ t
⊢ f i = 0

Tactic:
h.1 i hi

Premises used: And.left
-- 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 ι
inst_8 : Fintype ι
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
h : (∀ i ∈ t, f i = 0) ∧ ∀ i ∈ tᶜ, f i = 0
hi : i ∈ t
⊢ f i = 0

Tactic:
exact h.1 i hi

Premises used: And.left
-- 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 ι
inst_8 : Fintype ι
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
h : (∀ i ∈ t, f i = 0) ∧ ∀ i ∈ tᶜ, f i = 0
hi : i ∉ t
⊢ f i = 0

Tactic:
h.2 i (Finset.mem_compl.2 hi)

Premises used: Iff.mpr, Finset.mem_compl, And.right
-- 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 ι
inst_8 : Fintype ι
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
h : (∀ i ∈ t, f i = 0) ∧ ∀ i ∈ tᶜ, f i = 0
hi : i ∉ t
⊢ f i = 0

Tactic:
exact h.2 i (Finset.mem_compl.2 hi)

Premises used: Iff.mpr, Finset.mem_compl, And.right
-- 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 ι
inst_8 : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
refine_2 :
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ t₁, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
    (∑ i ∈ t₁ᶜ, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
refine_2₁ : ∀ (h : ∀ (i : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0), (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0
⊢ (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0

Tactic:
specialize h t₁ (fun i => if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) ?_

Premises used: Membership.mem, Or, OfNat.ofNat, 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 ι
inst_8 : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
refine_2 :
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ t₁, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
    (∑ x ∈ t₂, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) x) (v x))
refine_2₁ :
  ∀ x ∈ t₁ᶜ,
    x ∉ t₂ → HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) x) (v x) = 0
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ t₁, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
    (∑ i ∈ t₁ᶜ, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))

Tactic:
rw [← Finset.sum_subset ht₁t₂.le_compl_left]

Premises used: Finset.sum_subset, Disjoint.le_compl_left
-- 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 ι
inst_8 : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)

Tactic:
heq
-- 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 ι
inst_8 : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
h₁ :
  ∀ (i : ι) (hi : i ∈ t₁),
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i) = f i • v i
h₂ :
  ∀ (i : ι) (hi : i ∈ t₂),
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i) = f i • v i
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ t₁, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i))
    (∑ x ∈ t₂, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) x) (v x))

Tactic:
convert! heq using 2 with i hi i hi
-- 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 ι
inst_8 : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
i : ι
hi : i ∈ t₁
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i) = f i • v i

Tactic:
simp [hi]
-- 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 ι
inst_8 : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
i : ι
hi : i ∈ t₂
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i) = f i • v i

Tactic:
simp [hi]
-- 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 ι
inst_8 : Fintype ι
h : ∀ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) → ∀ (i : ι), f i = 0
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
i : ι
hi : i ∈ t₁ᶜ
hi' : i ∉ t₂
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) i) (v i) = 0

Tactic:
simp [Finset.mem_compl.1 hi, hi']

Premises used: Finset.mem_compl, Iff.mp
-- 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 ι
inst_8 : Fintype ι
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
h : ∀ (i : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0
⊢ (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0

Tactic:
⟨fun i hi => ?_, fun i hi => ?_⟩

Premises used: And.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 ι
inst_8 : Fintype ι
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
h : ∀ (i : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0
refine_2 : ∀ (i : ι) (hi : i ∈ t₁), f i = 0
refine_2₁ : ∀ (i : ι) (hi : i ∈ t₂), f i = 0
⊢ (∀ i ∈ t₁, f i = 0) ∧ ∀ i ∈ t₂, f i = 0

Tactic:
refine ⟨fun i hi => ?_, fun i hi => ?_⟩
-- 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 ι
inst_8 : Fintype ι
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
h : ∀ (i : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0
i : ι
hi : i ∈ t₁
⊢ f i = 0

Tactic:
simpa [hi] using h 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 ι
inst_8 : Fintype ι
t₁ t₂ : Finset ι
f : ι → R
ht₁t₂ : Disjoint t₁ t₂
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t₁, f i • v i) (∑ i ∈ t₂, f i • v i)
h : ∀ (i : ι), (if i ∈ t₁ ∨ i ∈ t₂ then f i else 0) = 0
i : ι
hi : i ∈ t₂
⊢ f i = 0

Tactic:
simpa [hi] using h 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 ι
inst_8 : Fintype ι
simp :
  (∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
      ¬x_1 x = 0) ↔
    ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
⊢ ¬LinearIndependent R v ↔
    ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ i ∈ t, 0 < f i

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

Premises used: Fintype.linearIndependent_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 ι
inst_8 : Fintype ι
⊢ (∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
      ¬x_1 x = 0) ↔
    ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0

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

Premises used: Compl.compl, Membership.mem, Exists, _private.0.Fintype.not_linearIndependent_iffₒₛ.match_2, Ne, And, Iff.intro, Exists.intro, HSMul.hSMul, OfNat.ofNat, Eq, Not, Finset.sum, _private.0.Fintype.not_linearIndependent_iffₒₛ.match_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 ι
inst_8 : Fintype ι
refine :
  (∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
      ¬x_1 x = 0) →
    ∀ (t : Finset ι) (f : ι → R) (heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)) (i : ι)
      (hfi : ¬f i = 0),
      ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
⊢ (∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
      ¬x_1 x = 0) ↔
    ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
refine ⟨fun ⟨t, f, heq, i, hfi⟩ => ?_, fun ⟨t, f, heq, i, hi, hfi⟩ =>
    ⟨t, f, heq, i, 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 ι
inst_8 : Fintype ι
h :
  ∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
    ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
hfi : ¬f i = 0
pos :
  ∀ (hi' : i ∈ t),
    ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
neg :
  ∀ (hi' : i ∉ t),
    ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0
⊢ ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ 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 ι
inst_8 : Fintype ι
h :
  ∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
    ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
hfi : ¬f i = 0
hi' : i ∈ t
⊢ ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
⟨t, 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 ι
inst_8 : Fintype ι
h :
  ∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
    ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
hfi : ¬f i = 0
hi' : i ∈ t
⊢ ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
exact ⟨t, f, heq, i, 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 ι
inst_8 : Fintype ι
h :
  ∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
    ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
hfi : ¬f i = 0
hi' : i ∉ t
⊢ ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
⟨tᶜ, f, ?_, i, Finset.mem_compl.2 hi', hfi⟩

Premises used: Iff.mpr, Compl.compl, Finset.mem_compl, 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 ι
inst_8 : Fintype ι
h :
  ∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
    ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
hfi : ¬f i = 0
hi' : i ∉ t
neg : Eq.{u_4 + 1} (α := M) (∑ i ∈ tᶜ, f i • v i) (∑ i ∈ tᶜᶜ, f i • v i)
⊢ ∃ (t : Finset ι) (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i) ∧ ∃ i ∈ t, f i ≠ 0

Tactic:
refine ⟨tᶜ, f, ?_, i, Finset.mem_compl.2 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 ι
inst_8 : Fintype ι
h :
  ∃ (x : Finset ι) (x_1 : ι → R) (_ : Eq.{u_4 + 1} (α := M) (∑ i ∈ x, x_1 i • v i) (∑ i ∈ xᶜ, x_1 i • v i)) (x : ι),
    ¬x_1 x = 0
t : Finset ι
f : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, f i • v i) (∑ i ∈ tᶜ, f i • v i)
i : ι
hfi : ¬f i = 0
hi' : i ∉ t
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ tᶜ, f i • v i) (∑ i ∈ tᶜᶜ, f i • v i)

Tactic:
simp [heq]