awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
⊢ Membership.mem (γ := Submodule R M) (span R (range v)) (∑ i : Fin m, g i.succ • v i)

Tactic:
exact sum_mem fun i _ => smul_mem _ _ (subset_span ⟨i, rfl⟩)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
⊢ g 0 = 0

Tactic:
have : g 0 = 0 := by
    refine x_ortho (g 0) (∑ i : Fin m, g i.succ • v i) ?_ total_eq
    exact sum_mem fun i _ => smul_mem _ _ (subset_span ⟨i, rfl⟩)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
this : g 0 = 0
⊢ Eq.{u_4 + 1} (α := M) (∑ x : Fin m, g x.succ • v x) 0

Tactic:
rw [this, zero_smul, zero_add] at total_eq

Premises used: zero_add, zero_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : g 0 • x + ∑ x : Fin m, g x.succ • v x = 0
this : g 0 = 0
total_eq₁ : Eq.{u_4 + 1} (α := M) (∑ x : Fin m, g x.succ • v x) 0
⊢ g 0 = 0

Tactic:
rw [this, zero_smul, zero_add] at total_eq

Premises used: zero_add, zero_smul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : Eq.{u_4 + 1} (α := M) (∑ x : Fin m, g x.succ • v x) 0
this : g 0 = 0
⊢ g j = 0

Tactic:
Fin.cases this (hli _ total_eq) j

Premises used: Fin.cases
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
x : M
v : Fin m → M
hli : ∀ (g : Fin m → R), Eq.{u_4 + 1} (α := M) (∑ i : Fin m, g i • v i) 0 → ∀ (i : Fin m), g i = 0
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
g : Fin (m + 1) → R
j : Fin (m + 1)
total_eq : Eq.{u_4 + 1} (α := M) (∑ x : Fin m, g x.succ • v x) 0
this : g 0 = 0
⊢ g j = 0

Tactic:
exact Fin.cases this (hli _ total_eq) j
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
v : Fin m → M
x : M
hli : LinearIndependent R v
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
rw :
  LinearIndependent.{0, u_2, u_4} (ι := Fin (m + 1)) R (M := M)
    (Function.comp (β := Fin (m + 1)) (Fin.cons (α := fun (x : Fin (m + 1)) ↦ M) x v)
      (⇑(finRotate (m + 1)) : (a : Fin (m + 1)) → Fin (m + 1)))
⊢ LinearIndependent.{0, u_2, u_4} (ι := Fin (m + 1)) R (M := M) (Fin.snoc (α := fun (a : Fin m.succ) ↦ M) v x)

Tactic:
rw [Fin.snoc_eq_cons_rotate v x, ← Function.comp_def]

Premises used: Fin.snoc_eq_cons_rotate, Function.comp_def
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
v : Fin m → M
x : M
hli : LinearIndependent R v
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
⊢ LinearIndependent.{0, u_2, u_4} (ι := Fin (m + 1)) R (M := M)
    (Function.comp (β := Fin (m + 1)) (Fin.cons (α := fun (x : Fin (m + 1)) ↦ M) x v)
      (⇑(finRotate (m + 1)) : (a : Fin (m + 1)) → Fin (m + 1)))

Tactic:
(linearIndependent_equiv _).mpr (.finCons' x v hli x_ortho)

Premises used: Iff.mpr, linearIndependent_equiv, LinearIndependent.finCons'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
m : ℕ
v : Fin m → M
x : M
hli : LinearIndependent R v
x_ortho : ∀ (c : R) (y : M), Membership.mem (γ := Submodule R M) (span R (range v)) y → c • x + y = 0 → c = 0
⊢ LinearIndependent.{0, u_2, u_4} (ι := Fin (m + 1)) R (M := M)
    (Function.comp (β := Fin (m + 1)) (Fin.cons (α := fun (x : Fin (m + 1)) ↦ M) x v)
      (⇑(finRotate (m + 1)) : (a : Fin (m + 1)) → Fin (m + 1)))

Tactic:
exact (linearIndependent_equiv _).mpr (.finCons' x v hli x_ortho)

Premises used: Iff.mpr, linearIndependent_equiv, LinearIndependent.finCons'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
rw :
  LinearIndependent R v ↔
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧
        Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
⊢ LinearIndependent R v ↔
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧
        Disjoint (α := Submodule R M) (span R (range (v ∘ Sum.inl))) (span R (range (v ∘ Sum.inr)))

Tactic:
rw [range_comp v, range_comp v]

Premises used: Set.range_comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
⊢ LinearIndependent R v ↔
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧
        Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
refine_1 :
  LinearIndependent R v →
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧
        Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
refine_2 :
  LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧
        Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr)) →
    LinearIndependent R v
⊢ LinearIndependent R v ↔
    LinearIndependent R (v ∘ Sum.inl) ∧
      LinearIndependent R (v ∘ Sum.inr) ∧
        Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
h : LinearIndependent R v
⊢ LinearIndependent R (v ∘ Sum.inl) ∧
    LinearIndependent R (v ∘ Sum.inr) ∧
      Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))

Tactic:
⟨h.comp _ Sum.inl_injective, h.comp _ Sum.inr_injective, ?_⟩

Premises used: Sum.inr_injective, Sum.inl_injective, And.intro, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
h : LinearIndependent R v
refine_1 : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
⊢ LinearIndependent R (v ∘ Sum.inl) ∧
    LinearIndependent R (v ∘ Sum.inr) ∧
      Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))

Tactic:
refine ⟨h.comp _ Sum.inl_injective, h.comp _ Sum.inr_injective, ?_⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
h : LinearIndependent R v
⊢ Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))

Tactic:
h.disjoint_span_image <| isCompl_range_inl_range_inr.disjoint

Premises used: LinearIndependent.disjoint_span_image, Set.isCompl_range_inl_range_inr, IsCompl.disjoint
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
h : LinearIndependent R v
⊢ Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))

Tactic:
exact h.disjoint_span_image <| isCompl_range_inl_range_inr.disjoint

Premises used: LinearIndependent.disjoint_span_image, Set.isCompl_range_inl_range_inr, IsCompl.disjoint
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
hl : LinearIndependent R (v ∘ Sum.inl)
hr : LinearIndependent R (v ∘ Sum.inr)
hlr : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
refine_2 :
  ∀ (hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0)
    (hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0)
    (hlr : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr)))
    (s : Finset (ι ⊕ ι')) (g : ι ⊕ ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0 → ∀ i ∈ s, g i = 0
⊢ LinearIndependent R v

Tactic:
rw [linearIndependent_iff'] at *

Premises used: linearIndependent_iff'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι ⊕ ι'
hi : i ∈ s
rw :
  Eq.{u_4 + 1} (α := M)
    (∑ x ∈ s with
      Membership.mem (γ := Set (ι ⊕ ι')) (range Sum.inl) x ∨ Membership.mem (γ := Set (ι ⊕ ι')) (range Sum.inr) x,
      g x • v x)
    0
rw₁ :
  Disjoint ({x ∈ s | Membership.mem (γ := Set (ι ⊕ ι')) (range Sum.inl) x})
    ({x ∈ s | Membership.mem (γ := Set (ι ⊕ ι')) (range Sum.inr) x})
⊢ HAdd.hAdd (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
      (∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i)) =
    0

Tactic:
rw [Finset.sum_preimage' (g := fun x => g x • v x),
      Finset.sum_preimage' (g := fun x => g x • v x), ← Finset.sum_union, ← Finset.filter_or]

Premises used: Finset.sum_preimage', Finset.sum_union, Finset.filter_or, HSMul.hSMul
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι ⊕ ι'
hi : i ∈ s
⊢ Eq.{u_4 + 1} (α := M)
    (∑ x ∈ s with
      Membership.mem (γ := Set (ι ⊕ ι')) (range Sum.inl) x ∨ Membership.mem (γ := Set (ι ⊕ ι')) (range Sum.inr) x,
      g x • v x)
    0

Tactic:
simpa only [← mem_union, range_inl_union_range_inr, mem_univ, Finset.filter_true]

Premises used: Set.mem_union, Set.range_inl_union_range_inr, Finset.filter_true, Set.mem_univ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι ⊕ ι'
hi : i ∈ s
⊢ Disjoint ({x ∈ s | Membership.mem (γ := Set (ι ⊕ ι')) (range Sum.inl) x})
    ({x ∈ s | Membership.mem (γ := Set (ι ⊕ ι')) (range Sum.inr) x})

Tactic:
Finset.disjoint_filter.2 fun x _ hx =>
        disjoint_left.1 isCompl_range_inl_range_inr.disjoint hx

Premises used: Iff.mpr, Set.disjoint_left, Finset.disjoint_filter, Set.isCompl_range_inl_range_inr, Iff.mp, IsCompl.disjoint
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι ⊕ ι'
hi : i ∈ s
⊢ Disjoint ({x ∈ s | Membership.mem (γ := Set (ι ⊕ ι')) (range Sum.inl) x})
    ({x ∈ s | Membership.mem (γ := Set (ι ⊕ ι')) (range Sum.inr) x})

Tactic:
exact Finset.disjoint_filter.2 fun x _ hx =>
        disjoint_left.1 isCompl_range_inl_range_inr.disjoint hx

Premises used: Iff.mpr, Set.disjoint_left, Finset.disjoint_filter, Set.isCompl_range_inl_range_inr, Iff.mp, IsCompl.disjoint
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι ⊕ ι'
hi : i ∈ s
⊢ HAdd.hAdd (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
      (∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i)) =
    0

Tactic:
have :
    ((∑ i ∈ s.preimage Sum.inl Sum.inl_injective.injOn, (fun x => g x • v x) (Sum.inl i)) +
        ∑ i ∈ s.preimage Sum.inr Sum.inr_injective.injOn, (fun x => g x • v x) (Sum.inr i)) =
      0 := by
    -- Porting note: `g` must be specified.
    rw [Finset.sum_preimage' (g := fun x => g x • v x),
      Finset.sum_preimage' (g := fun x => g x • v x), ← Finset.sum_union, ← Finset.filter_or]
    · simpa only [← mem_union, range_inl_union_range_inr, mem_univ, Finset.filter_true]
    · exact Finset.disjoint_filter.2 fun x _ hx =>
        disjoint_left.1 isCompl_range_inl_range_inr.disjoint hx
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι ⊕ ι'
hi : i ∈ s
this :
  HAdd.hAdd (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
      (∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i)) =
    0
⊢ Eq.{u_4 + 1} (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
    (-∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i))

Tactic:
rw [← eq_neg_iff_add_eq_zero] at this

Premises used: eq_neg_iff_add_eq_zero
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0
hlr : Disjoint (α := Submodule R M) (span R (v '' range Sum.inl)) (span R (v '' range Sum.inr))
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι ⊕ ι'
hi : i ∈ s
this :
  Eq.{u_4 + 1} (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
    (-∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i))
refine_2 :
  ∀
    (hlr :
      ∀ (x : M),
        Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inl)) x →
          ∀ (y : M), Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inr)) y → x = y → x = 0)
    (s : Finset (ι ⊕ ι')) (g : ι ⊕ ι' → R) (hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0) (i : ι ⊕ ι') (hi : i ∈ s)
    (this :
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
        (-∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i))),
    g i = 0
⊢ g i = 0

Tactic:
rw [disjoint_def'] at hlr

Premises used: Submodule.disjoint_def'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0
hlr :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inl)) x →
      ∀ (y : M), Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inr)) y → x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι ⊕ ι'
hi : i ∈ s
this :
  Eq.{u_4 + 1} (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
    (-∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i))
⊢ Eq.{u_4 + 1} (α := M) (∑ c ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl c)) 0

Tactic:
hlr _ (sum_mem fun i _ => ?_) _ (neg_mem <| sum_mem fun i _ => ?_) this

Premises used: sum_mem, NegMemClass.neg_mem
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0
hlr :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inl)) x →
      ∀ (y : M), Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inr)) y → x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i : ι ⊕ ι'
hi : i ∈ s
this :
  Eq.{u_4 + 1} (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
    (-∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i))
refine_1 :
  ∀ i ∈ s.preimage Sum.inl ⋯,
    Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inl)) ((fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
refine_2 :
  ∀ i ∈ s.preimage Sum.inr ⋯,
    Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inr)) ((fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i))
⊢ Eq.{u_4 + 1} (α := M) (∑ c ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl c)) 0

Tactic:
refine hlr _ (sum_mem fun i _ => ?_) _ (neg_mem <| sum_mem fun i _ => ?_) this

Premises used: sum_mem, NegMemClass.neg_mem
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0
hlr :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inl)) x →
      ∀ (y : M), Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inr)) y → x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i_1 : ι ⊕ ι'
hi : i_1 ∈ s
this :
  Eq.{u_4 + 1} (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
    (-∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i))
i : ι
h : i ∈ s.preimage Sum.inl ⋯
⊢ Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inl)) ((fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))

Tactic:
smul_mem _ _ (subset_span ⟨Sum.inl i, mem_range_self _, rfl⟩)

Premises used: Set.mem_range_self, Set.Mem, Sum.inl, And.intro, Exists.intro, Submodule.subset_span, rfl, Submodule.smul_mem
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Basic
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι ⊕ ι' → M
hl : ∀ (s : Finset ι) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inl) i) 0 → ∀ i ∈ s, g i = 0
hr : ∀ (s : Finset ι') (g : ι' → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • (v ∘ Sum.inr) i) 0 → ∀ i ∈ s, g i = 0
hlr :
  ∀ (x : M),
    Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inl)) x →
      ∀ (y : M), Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inr)) y → x = y → x = 0
s : Finset (ι ⊕ ι')
g : ι ⊕ ι' → R
hg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, g i • v i) 0
i_1 : ι ⊕ ι'
hi : i_1 ∈ s
this :
  Eq.{u_4 + 1} (α := M) (∑ i ∈ s.preimage Sum.inl ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))
    (-∑ i ∈ s.preimage Sum.inr ⋯, (fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inr i))
i : ι
h : i ∈ s.preimage Sum.inl ⋯
⊢ Membership.mem (γ := Submodule R M) (span R (v '' range Sum.inl)) ((fun (x : ι ⊕ ι') ↦ g x • v x) (Sum.inl i))

Tactic:
exact smul_mem _ _ (subset_span ⟨Sum.inl i, mem_range_self _, rfl⟩)