awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
κ : Type v
w : κ → M
i' : LinearIndependent R w
j : ι → κ
i : LinearIndependent R (w ∘ j)
p : i.Maximal
⊢ range (w ∘ j) = range w

Tactic:
specialize p (range w) i'.linearIndepOn_id (range_comp_subset_range _ _)

Premises used: Set.range_comp_subset_range, LinearIndependent.linearIndepOn_id, Set.range
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
κ : Type v
w : κ → M
i' : LinearIndependent R w
j : ι → κ
i : LinearIndependent R (w ∘ j)
p : range (w ∘ j) = range w
⊢ w '' range j = w '' univ

Tactic:
rw [range_comp, ← image_univ (f := w)] at p

Premises used: Set.range_comp, Set.image_univ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
κ : Type v
w : κ → M
i' : LinearIndependent R w
j : ι → κ
i : LinearIndependent R (w ∘ j)
p : w '' range j = w '' univ
⊢ Surjective j

Tactic:
range_eq_univ.mp (image_injective.mpr i'.injective p)

Premises used: Iff.mpr, Set.range_eq_univ, Set.image_injective, LinearIndependent.injective, Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
κ : Type v
w : κ → M
i' : LinearIndependent R w
j : ι → κ
i : LinearIndependent R (w ∘ j)
p : w '' range j = w '' univ
⊢ Surjective j

Tactic:
exact range_eq_univ.mp (image_injective.mpr i'.injective p)

Premises used: Iff.mpr, Set.range_eq_univ, Set.image_injective, LinearIndependent.injective, Iff.mp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j
w : Set M
i' : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range v ≤ w
h₁ :
  ∀ (x : ι),
    Function.comp (β := (↑w : Type v)) (Subtype.val (p := fun (x : M) ↦ x ∈ w))
        (fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) ⋯) x =
      v x
⊢ (Function.comp (β := (↑w : Type v)) (Subtype.val (p := fun (x : M) ↦ x ∈ w)) fun (i : ι) ↦
      Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) ⋯) =
    v

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j
w : Set M
i' : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range v ≤ w
x : ι
⊢ Function.comp (β := (↑w : Type v)) (Subtype.val (p := fun (x : M) ↦ x ∈ w))
      (fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) ⋯) x =
    v x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
i : LinearIndependent R v
p : ∀ (κ : Type v) (w : κ → M) (_i' : LinearIndependent R w) (j : ι → κ) (_h : w ∘ j = v), Surjective j
w : Set M
i' : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range v ≤ w
⊢ Surjective.{w + 1, v + 1} (β := (↑w : Type v)) fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) ⋯

Tactic:
specialize
      p w ((↑) : w → M) i' (fun i => ⟨v i, range_subset_iff.mp h i⟩)
        (by
          ext
          simp)

Premises used: Set.Elem, Subtype.mk, Iff.mp, Set.range_subset_iff, Subtype.val
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range v ≤ w
p : Surjective.{w + 1, v + 1} (β := (↑w : Type v)) fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) ⋯
⊢ Eq.{v + 1} (α := Set M)
    ((fun (s : Set { x : M // x ∈ w }) ↦ Subtype.val (p := fun (x : M) ↦ x ∈ w) '' s)
      (range fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) ⋯))
    ((fun (s : Set { x : M // x ∈ w }) ↦ Subtype.val (p := fun (x : M) ↦ x ∈ w) '' s) univ)

Tactic:
have q := congr_arg (fun s => ((↑) : w → M) '' s) p.range_eq
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range v ≤ w
p : Surjective.{w + 1, v + 1} (β := (↑w : Type v)) fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) ⋯
q :
  Eq.{v + 1} (α := Set M)
    (image (α := { x : M // x ∈ w }) (Subtype.val (p := fun (x : M) ↦ x ∈ w))
      (range fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) ⋯))
    (image (α := { x : M // x ∈ w }) (Subtype.val (p := fun (x : M) ↦ x ∈ w)) univ)
⊢ Eq.{v + 1} (α := Set M) ((fun (x : ι) ↦ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v x) ⋯) : M)) '' univ)
    (image (α := { x : M // x ∈ w }) (Subtype.val (p := fun (x : M) ↦ x ∈ w)) univ)

Tactic:
rw [← image_univ, image_image] at q

Premises used: Set.image_image, Set.image_univ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type w
R : Type u
inst : Semiring R
inst_1 : Nontrivial R
M : Type v
inst_2 : AddCommMonoid M
inst_3 : Module R M
v : ι → M
i : LinearIndependent R v
w : Set M
i' : LinearIndependent.{v, u, v} (ι := { x : M // x ∈ w }) R (Subtype.val (p := fun (x : M) ↦ x ∈ w))
h : range v ≤ w
p : Surjective.{w + 1, v + 1} (β := (↑w : Type v)) fun (i : ι) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v i) ⋯
q :
  Eq.{v + 1} (α := Set M) ((fun (x : ι) ↦ (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ w) (v x) ⋯) : M)) '' univ)
    (image (α := { x : M // x ∈ w }) (Subtype.val (p := fun (x : M) ↦ x ∈ w)) univ)
⊢ range v = w

Tactic:
simpa using q
-- 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 : Sub R := CanonicallyOrderedAdd.toSub
⊢ OrderedSub R

Tactic:
haveI : OrderedSub R := CanonicallyOrderedAdd.toOrderedSub
-- 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
rw :
  (∀ (s : Finset ι) (f g : ι → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i) ↔
    ∀ (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
⊢ LinearIndependent R v ↔
    ∀ (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

Tactic:
rw [linearIndependent_iff'ₛ]

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

Tactic:
⟨fun h s t f hst heq => ?_, fun h s f g 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
refine_1 :
  ∀
    (h :
      ∀ (s : Finset ι) (f g : ι → R),
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i)
    (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 ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
refine_2 :
  ∀
    (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 ∈ s, f i = g i
⊢ (∀ (s : Finset ι) (f g : ι → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i) ↔
    ∀ (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

Tactic:
refine ⟨fun h s t f hst heq => ?_, fun h s f g 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 : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
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)
refine_1 :
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ s ∪ t, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ s then f i else 0) i) (v i))
    (∑ i ∈ s ∪ t, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t then f i else 0) i) (v i))
refine_1₁ :
  ∀ (h : ∀ i ∈ s ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0), (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0
⊢ (∀ i ∈ s, f i = 0) ∧ ∀ i ∈ t, f i = 0

Tactic:
specialize h (s ∪ t) (fun i => if i ∈ s then f i else 0) (fun i => if i ∈ t then f i else 0) ?_

Premises used: Membership.mem, Union.union, 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
h : ∀ (s : Finset ι) (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ i ∈ s, f i = g i
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)
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ s ∪ t, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ s then f i else 0) i) (v i))
    (∑ i ∈ s ∪ t, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : ι) ↦ if i ∈ t then f i else 0) i) (v i))

Tactic:
simpa
-- 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 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 ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
⊢ (∀ i ∈ s, 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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 ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
refine_1 : ∀ (i : ι) (hi : i ∈ s), f i = 0
refine_1₁ : ∀ (i : ι) (hi : i ∈ t), f i = 0
⊢ (∀ i ∈ s, 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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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 ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
i : ι
hi : i ∈ s
⊢ f i = 0

Tactic:
simpa [hi, hst.notMem_of_mem_left_finset hi] using h i (Finset.mem_union_left _ hi)

Premises used: Disjoint.notMem_of_mem_left_finset, Finset.mem_union_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
this_1 : Sub R := CanonicallyOrderedAdd.toSub
this : OrderedSub R
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 ∪ t, (if i ∈ s then f i else 0) = if i ∈ t then f i else 0
i : ι
hi : i ∈ t
⊢ f i = 0

Tactic:
simpa [hi, hst.notMem_of_mem_right_finset hi] using (h i (Finset.mem_union_right _ hi)).symm

Premises used: Finset.mem_union_right, Eq.symm, Disjoint.notMem_of_mem_right_finset
-- 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 : Disjoint ({i ∈ s | g i ≤ f i}) ({i ∈ s | f i < g i})
refine_2₁ :
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ s with g i ≤ f 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))
    (∑ 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))
refine_2₂ :
  ∀
    (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 ∈ s, f i = g i
⊢ ∀ i ∈ s, f i = g i

Tactic:
specialize h { i ∈ s | g i ≤ f i } { i ∈ s | f i < g i }
      (fun i => if g i ≤ f i then f i - g i else g i - f i) ?_ ?_

Premises used: HSub.hSub, LE.le, LT.lt, Finset.filter, 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
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 : ∀ ⦃a : ι⦄, a ∈ s ∧ g a ≤ f a → ¬(a ∈ s ∧ f a < g a)
⊢ Disjoint ({i ∈ s | g i ≤ f i}) ({i ∈ s | f i < g i})

Tactic:
simp_rw [Finset.disjoint_left, Finset.mem_filter]

Premises used: Finset.mem_filter, Finset.disjoint_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
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)
⊢ ∀ ⦃a : ι⦄, a ∈ s ∧ g a ≤ f a → ¬(a ∈ s ∧ f a < g a)

Tactic:
fun i ⟨_, hi⟩ ⟨_, hi'⟩ => hi.not_gt hi'

Premises used: False, _private.0.linearIndependent_iffₒₛ.match_3, _private.0.linearIndependent_iffₒₛ.match_2, LE.le.not_gt, 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)
⊢ ∀ ⦃a : ι⦄, a ∈ s ∧ g a ≤ f a → ¬(a ∈ s ∧ f a < g a)

Tactic:
exact fun i ⟨_, hi⟩ ⟨_, hi'⟩ => hi.not_gt 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)
refine_2 :
  ∑ i ∈ s with g i ≤ f 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) =
    ∑ 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)
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ s with g i ≤ f 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))
    (∑ 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))

Tactic:
rw [← add_right_cancel_iff
        (a := ∑ i ∈ s with g i ≤ f i, g i • v i + ∑ i ∈ s with f i < g i, f i • v i)]

Premises used: add_right_cancel_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
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)
rw :
  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 g i ≤ f 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:
rw [← add_assoc, ← Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, add_assoc
-- 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) =
    ∑ 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)
⊢ ∑ i ∈ s with g i ≤ f 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) =
    ∑ 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_lhs => rw [← add_assoc, ← Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib, add_assoc
-- 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)
rw :
  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 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:
rw [add_left_comm, ← Finset.sum_add_distrib]

Premises used: add_left_comm, Finset.sum_add_distrib