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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
refine_2 :
  HAdd.hAdd (α := M)
      (∑ x ∈ s with g x ≤ f x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          g x • v x))
      (∑ i ∈ s with f i < g i, f i • v i) =
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i)
      (∑ x ∈ s with f x < g x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          f x • v x))
⊢ HAdd.hAdd (α := M)
      (∑ x ∈ s with g x ≤ f x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          g x • v x))
      (∑ i ∈ s with f i < g i, f i • v i) =
    ∑ i ∈ s with f i < g i,
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) i) (v i) +
      HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i) (∑ i ∈ s with f i < g i, f i • v i)

Tactic:
conv_rhs => rw [add_left_comm, ← Finset.sum_add_distrib]

Premises used: add_left_comm, Finset.sum_add_distrib
-- 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
h₁ :
  HAdd.hAdd (α := M)
      (∑ x ∈ s with g x ≤ f x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          g x • v x))
      (∑ i ∈ s with f i < g i, f i • v i) =
    ∑ i ∈ s, f i • v i
h₂ :
  HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i)
      (∑ x ∈ s with f x < g x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          f x • v x)) =
    ∑ i ∈ s, g i • v i
⊢ HAdd.hAdd (α := M)
      (∑ x ∈ s with g x ≤ f x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          g x • v x))
      (∑ i ∈ s with f i < g i, f i • v i) =
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i)
      (∑ x ∈ s with f x < g x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          f x • v x))

Tactic:
convert! 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
h₁ :
  HAdd.hAdd (α := M) (∑ x ∈ s with g x ≤ f x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + g x • v x))
      (∑ i ∈ s with f i < g i, f i • v i) =
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, f i • v i) (∑ i ∈ s with f i < g i, f i • v i)
⊢ HAdd.hAdd (α := M)
      (∑ x ∈ s with g x ≤ f x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          g x • v x))
      (∑ i ∈ s with f i < g i, f i • v i) =
    ∑ i ∈ s, f i • v i

Tactic:
simp_rw [← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i), not_le]

Premises used: not_le, LE.le, Finset.sum_filter_add_sum_filter_not
-- 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
h₁ :
  HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i)
      (∑ x ∈ s with f x < g x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + f x • v x)) =
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i) (∑ i ∈ s with f i < g i, g i • v i)
⊢ HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i)
      (∑ x ∈ s with f x < g x,
        (HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if g i ≤ f i then f i - g i else g i - f i) x) (v x) +
          f x • v x)) =
    ∑ i ∈ s, g i • v i

Tactic:
simp_rw [← Finset.sum_filter_add_sum_filter_not s (fun i => g i ≤ f i), not_le]

Premises used: not_le, LE.le, Finset.sum_filter_add_sum_filter_not
-- 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
h₁ :
  ∀ (i : ι) (hi : i ∈ {i ∈ s | g i ≤ f i}), (if g i ≤ f i then f i - g i else g i - f i) • v i + g i • v i = f i • v i
⊢ HAdd.hAdd (α := M) (∑ x ∈ s with g x ≤ f x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + g x • v x))
      (∑ i ∈ s with f i < g i, f i • v i) =
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, f i • v i) (∑ i ∈ s with f i < g i, f i • v i)

Tactic:
congr! 2 with 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
h₁ :
  ∀ (i : ι) (hi : i ∈ {x ∈ s | f x < g x}), (if g i ≤ f i then f i - g i else g i - f i) • v i + f i • v i = g i • v i
⊢ HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i)
      (∑ x ∈ s with f x < g x, ((if g x ≤ f x then f x - g x else g x - f x) • v x + f x • v x)) =
    HAdd.hAdd (α := M) (∑ i ∈ s with g i ≤ f i, g i • v i) (∑ i ∈ s with f i < g i, g i • v i)

Tactic:
congr! 2 with 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ {i ∈ s | g i ≤ f i}
⊢ i ∈ s ∧ g i ≤ f i

Tactic:
simp only [Finset.mem_filter] at hi

Premises used: Finset.mem_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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ {x ∈ s | f x < g x}
⊢ i ∈ s ∧ f i < g i

Tactic:
simp only [Finset.mem_filter] at hi

Premises used: Finset.mem_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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s ∧ g i ≤ f i
⊢ (if g i ≤ f i then f i - g i else g i - f i) • v i + g i • v i = f i • v i

Tactic:
simp [hi.2, ← add_smul, tsub_add_cancel_of_le hi.2]

Premises used: tsub_add_cancel_of_le, And.right, add_smul
-- 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s ∧ f i < g i
⊢ (if g i ≤ f i then f i - g i else g i - f i) • v i + f i • v i = g i • v i

Tactic:
simp [hi.2.not_ge, ← add_smul, tsub_add_cancel_of_le hi.2.le]

Premises used: tsub_add_cancel_of_le, LT.lt.le, And.right, add_smul, LT.lt.not_ge
-- 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
h :
  (∀ i ∈ {i ∈ s | g i ≤ f i}, (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ i ∈ {i ∈ s | f i < g i}, (if g i ≤ f i then f i - g i else g i - f i) = 0
⊢ (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0

Tactic:
simp only [Finset.mem_filter] at h

Premises used: Finset.mem_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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
pos : ∀ (hi' : g i ≤ f i), f i = g i
neg : ∀ (hi' : ¬g i ≤ f i), f i = g i
⊢ f i = g i

Tactic:
by_cases hi' : g i ≤ f 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : g i ≤ f i
pos : f i ≤ g i
⊢ f i = g i

Tactic:
apply hi'.antisymm'

Premises used: LE.le.antisymm'
-- 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : g i ≤ f i
⊢ f i ≤ g i

Tactic:
simpa [hi', tsub_eq_zero_iff_le] using h.1 i ⟨hi, hi'⟩

Premises used: tsub_eq_zero_iff_le, And.left, 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : ¬g i ≤ f i
neg : g i ≤ f i
⊢ f i = g i

Tactic:
apply (not_le.1 hi').le.antisymm

Premises used: not_le, LE.le.antisymm, LT.lt.le, 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
s : Finset ι
f g : ι → R
heq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
h :
  (∀ (i : ι), i ∈ s ∧ g i ≤ f i → (if g i ≤ f i then f i - g i else g i - f i) = 0) ∧
    ∀ (i : ι), i ∈ s ∧ f i < g i → (if g i ≤ f i then f i - g i else g i - f i) = 0
i : ι
hi : i ∈ s
hi' : ¬g i ≤ f i
⊢ g i ≤ f i

Tactic:
simpa [hi', tsub_eq_zero_iff_le] using h.2 i ⟨hi, not_le.1 hi'⟩

Premises used: not_le, tsub_eq_zero_iff_le, And.right, And.intro, 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
simp :
  (¬∀ (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) ↔
    ∃ (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
⊢ ¬LinearIndependent R v ↔
    ∃ (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, 0 < f i

Tactic:
simp only [linearIndependent_iffₒₛ, pos_iff_ne_zero]

Premises used: pos_iff_ne_zero, 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
push :
  (∃ (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 : 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
⊢ (¬∀ (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) ↔
    ∃ (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:
push +distrib Not

Premises used: Not
-- 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
⊢ (∃ (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 : 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:
⟨fun ⟨s, t, f, hst, heq, h⟩ => ?_,
    fun ⟨s, t, f, hst, heq, hi⟩ => ⟨s, t, f, hst, heq, .inl hi⟩⟩

Premises used: Disjoint, Membership.mem, Exists, Ne, _private.0.not_linearIndependent_iffₒₛ.match_3, _private.0.not_linearIndependent_iffₒₛ.match_2, And, And.intro, Iff.intro, Exists.intro, HSMul.hSMul, Or.inl, Or, OfNat.ofNat, Eq, 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
refine :
  (∃ (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))
      (h : (∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, 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
⊢ (∃ (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 : 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:
refine ⟨fun ⟨s, t, f, hst, heq, h⟩ => ?_,
    fun ⟨s, t, f, hst, heq, hi⟩ => ⟨s, t, f, hst, heq, .inl 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
h_1 :
  ∃ (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)
h : (∃ i ∈ s, f i ≠ 0) ∨ ∃ i ∈ t, f i ≠ 0
inl :
  ∀ (i : ι) (hi : i ∈ s) (hfi : 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
inr :
  ∀ (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
⊢ ∃ (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:
rcases h with ⟨i, hi, hfi⟩ | ⟨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
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 ∈ s
hfi : 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:
⟨s, t, f, hst, 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
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 ∈ s
hfi : 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 ⟨s, t, f, hst, 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
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:
⟨t, s, f, hst.symm, heq.symm, i, hi, hgi⟩

Premises used: Disjoint.symm, And.intro, Exists.intro, Eq.symm