awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
s : Finset ι
mp :
  (∀ (g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) 0 →
        ∀ (i : (↑(↑s : Set ι) : Type u')), g i = 0) →
    ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
mpr :
  (∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0) →
    ∀ (g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) 0 →
        ∀ (i : (↑(↑s : Set ι) : Type u')), g i = 0
⊢ (∀ (g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) 0 →
        ∀ (i : (↑(↑s : Set ι) : Type u')), g i = 0) ↔
    ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
s : Finset ι
hv :
  ∀ (g : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) 0 →
      ∀ (i : (↑(↑s : Set ι) : Type u')), g i = 0
f : ι → R
hf : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0
i : ι
hi : i ∈ s
mp : ∀ (hf : Eq.{u_4 + 1} (α := M) (∑ x ∈ s.attach, f (↑x : ι) • v (↑x : ι)) 0) (i : ι) (hi : i ∈ s), f i = 0
⊢ f i = 0

Tactic:
rw [← s.sum_attach] at hf

Premises used: Finset.sum_attach
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
s : Finset ι
hv :
  ∀ (g : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) 0 →
      ∀ (i : (↑(↑s : Set ι) : Type u')), g i = 0
f : ι → R
hf : Eq.{u_4 + 1} (α := M) (∑ x ∈ s.attach, f (↑x : ι) • v (↑x : ι)) 0
i : ι
hi : i ∈ s
⊢ f i = 0

Tactic:
hv (f ∘ Subtype.val) hf ⟨i, hi⟩

Premises used: Function.comp, Subtype.mk, Subtype.val
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
s : Finset ι
hv :
  ∀ (g : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) 0 →
      ∀ (i : (↑(↑s : Set ι) : Type u')), g i = 0
f : ι → R
hf : Eq.{u_4 + 1} (α := M) (∑ x ∈ s.attach, f (↑x : ι) • v (↑x : ι)) 0
i : ι
hi : i ∈ s
⊢ f i = 0

Tactic:
exact hv (f ∘ Subtype.val) hf ⟨i, hi⟩

Premises used: Function.comp, Subtype.mk, Subtype.val
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
s : Finset ι
hv : ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
f : (↑(↑s : Set ι) : Type u') → R
hf₀ : Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι)) 0
i : (↑(↑s : Set ι) : Type u')
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ s,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (j : ι) ↦ (if hj : j ∈ s then f (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) j hj) else 0 : R)) i)
        (v i))
    0

Tactic:
simpa +contextual [← s.sum_attach]

Premises used: Finset.sum_attach
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
s : Finset ι
hv : ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
f : (↑(↑s : Set ι) : Type u') → R
hf₀ : Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι)) 0
i : (↑(↑s : Set ι) : Type u')
⊢ f i = 0

Tactic:
simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (by simpa +contextual [← s.sum_attach]) i

Premises used: Membership.mem, dite, Subtype.mk, OfNat.ofNat, Subtype.val
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
s : Finset ι
simp_rw :
  (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑(↑s : Set ι) : Type u')) ↦ v (↑x : ι)) ↔
    ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
simp_rw₁ :
  (∀ (g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) 0 →
        ∀ (i : (↑(↑s : Set ι) : Type u')), g i = 0) ↔
    ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
mp :
  (∀ (g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) 0 →
        ∀ (i : (↑(↑s : Set ι) : Type u')), g i = 0) →
    ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0
mpr mpr₁ :
  (∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0) →
    ∀ (g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) 0 →
        ∀ (i : (↑(↑s : Set ι) : Type u')), g i = 0
⊢ LinearIndepOn R v (↑s : Set ι) ↔ ∀ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 → ∀ i ∈ s, f i = 0

Tactic:
classical
  simp_rw [LinearIndepOn, Fintype.linearIndependent_iff]
  constructor
  · rintro hv f hf i hi
    rw [← s.sum_attach] at hf
    exact hv (f ∘ Subtype.val) hf ⟨i, hi⟩
  · rintro hv f hf₀ i
    simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (by simpa +contextual [← s.sum_attach]) i

Premises used: Finset.sum_attach, Fintype.linearIndependent_iff, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
s : Finset ι
⊢ ¬LinearIndepOn R v (↑s : Set ι) ↔ ∃ (f : ι → R), Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) 0 ∧ ∃ i ∈ s, f i ≠ 0

Tactic:
simpa using linearIndepOn_finset_iff.not

Premises used: linearIndepOn_finset_iff, Iff.not
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup M'
inst_3 : Module R M
inst_4 : Module R M'
v : ι → M
f : M →ₗ[R] M'
hf_inj : Disjoint (span R (Set.range v)) f.ker
⊢ LinearIndependent.{u', u_2, u_5} R (M := M') ((⇑f : (a : M) → M') ∘ v) ↔ LinearIndependent R v

Tactic:
f.linearIndependent_iff_of_injOn <| LinearMap.injOn_of_disjoint_ker le_rfl hf_inj

Premises used: le_rfl, LinearMap.linearIndependent_iff_of_injOn, LinearMap.injOn_of_disjoint_ker
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h :
  ∀ (l : ι →₀ R),
    Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) l →
      Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M) → l = 0
f : ι →₀ R
hf : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) f
g : ι →₀ R
hg : Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) g
eq :
  Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
    ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
rw :
  HSub.hSub (α := M) (β := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
      ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M) =
    0
rw₁ :
  HSub.hSub (α := M) (β := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M)
      ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M) =
    0
rw₂ rw₃ : Eq.{u_4 + 1} (α := M) 0 0
⊢ Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) (f - g) : M) (0 : M)

Tactic:
rw [map_sub, eq, sub_self]

Premises used: map_sub, sub_self
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ ¬LinearIndepOn R v s ↔
    ∃ (f : ι →₀ R),
      Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) f ∧
        Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M) (0 : M) ∧ f ≠ 0

Tactic:
simp [linearIndepOn_iff]

Premises used: linearIndepOn_iff
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ ¬LinearIndepOn R v s ↔
    ∃ (f : ι →₀ R),
      Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) f ∧
        Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
            0 ∧
          f ≠ 0

Tactic:
linearDepOn_iff'

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, linearDepOn_iff', Finset.sum
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
rw :
  (∀ (l : ι →₀ R),
      Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) l →
        Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M) → l = 0) ↔
    Disjoint (α := Submodule R (ι →₀ R)) (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R v))
rw₁ rw₂ :
  (∀ (l : ι →₀ R),
      Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) l →
        Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M) → l = 0) ↔
    ∀ (x : ι →₀ R),
      Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) x →
        Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) x : M) (0 : M) → x = 0
⊢ LinearIndepOn R v s ↔
    Disjoint (α := Submodule R (ι →₀ R)) (Finsupp.supported R R s) (LinearMap.ker (Finsupp.linearCombination R v))

Tactic:
rw [linearIndepOn_iff, LinearMap.disjoint_ker]

Premises used: linearIndepOn_iff, LinearMap.disjoint_ker
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ LinearIndepOn R v s ↔
    Eq (α := Submodule R ↥(Finsupp.supported R R s))
      (LinearMap.ker (M₂ := ↥(span R (v '' s))) (Finsupp.linearCombinationOn ι M R v s)) ⊥

Tactic:
linearIndepOn_iff_linearCombinationOnₛ.trans <|
    LinearMap.ker_eq_bot (M := Finsupp.supported R R s).symm

Premises used: LinearMap.ker_eq_bot, Iff.trans, Iff.symm, linearIndepOn_iff_linearCombinationOnₛ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
rw :
  (∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0) ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
⊢ LinearIndepOn R v s ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0

Tactic:
rw [LinearIndepOn, linearIndependent_iff']

Premises used: linearIndependent_iff', LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ (∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0) ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0

Tactic:
⟨fun h t g hts h0 i hit ↦ ?_, fun h t g h0 i hit ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
refine_1 :
  ∀
    (h :
      ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0)
    (t : Finset ι) (g : ι → R) (hts : (↑t : Set ι) ⊆ s) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0) (i : ι)
    (hit : i ∈ t), g i = 0
refine_2 :
  ∀
    (h :
      ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0)
    (t : Finset (↑s : Type u')) (g : (↑s : Type u') → R) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v (↑i : ι)) 0)
    (i : (↑s : Type u')) (hit : i ∈ t), g i = 0
⊢ (∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0) ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0

Tactic:
refine ⟨fun h t g hts h0 i hit ↦ ?_, fun h t g h0 i hit ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h :
  ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : (↑t : Set ι) ⊆ s
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0
i : ι
hit : i ∈ t
⊢ Membership.mem (γ := Finset (↑s : Type u')) (t.preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ⋯)
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i ⋯)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h :
  ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : (↑t : Set ι) ⊆ s
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0
i : ι
hit : i ∈ t
refine_1 :
  Eq.{u_4 + 1} (α := M)
    (∑ i ∈ t.preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ⋯,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : (↑s : Type u')) ↦ g (↑i : ι)) i) (v (↑i : ι)))
    0
⊢ g i = 0

Tactic:
refine h (t.preimage _ Subtype.val_injective.injOn) (fun i ↦ g i) ?_ ⟨i, hts hit⟩ (by simpa)

Premises used: Subtype.val_injective, Function.Injective.injOn, Subtype.mk, Finset.preimage, Subtype.val
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h :
  ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : (↑t : Set ι) ⊆ s
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0
i : ι
hit : i ∈ t
refine_1 : ∀ x ∈ t, x ∉ range (ι := { x : ι // x ∈ s }) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) → g x • v x = 0
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ t.preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) ⋯,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (i : (↑s : Type u')) ↦ g (↑i : ι)) i) (v (↑i : ι)))
    0

Tactic:
rwa [t.sum_preimage ((↑) : s → ι) Subtype.val_injective.injOn (fun i ↦ g i • v i)]

Premises used: Subtype.val_injective, Function.Injective.injOn, Finset.sum_preimage, HSMul.hSMul, Subtype.val
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h :
  ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : (↑t : Set ι) ⊆ s
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0
i : ι
hit : i ∈ t
refine_1 : ∀ x ∈ t, x ∉ s → g x • v x = 0
⊢ ∀ x ∈ t, x ∉ range (ι := { x : ι // x ∈ s }) (Subtype.val (p := fun (x : ι) ↦ x ∈ s)) → g x • v x = 0

Tactic:
simp only [Subtype.range_coe_subtype, setOf_mem_eq]

Premises used: Subtype.range_coe_subtype, Set.setOf_mem_eq
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h :
  ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : (↑t : Set ι) ⊆ s
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0
i : ι
hit : i ∈ t
⊢ ∀ x ∈ t, x ∉ s → g x • v x = 0

Tactic:
fun x hxt hxs ↦ (hxs (hts hxt)) |>.elim

Premises used: False.elim
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h :
  ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0
t : Finset ι
g : ι → R
hts : (↑t : Set ι) ⊆ s
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0
i : ι
hit : i ∈ t
⊢ ∀ x ∈ t, x ∉ s → g x • v x = 0

Tactic:
exact fun x hxt hxs ↦ (hxs (hts hxt)) |>.elim
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h : ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
t : Finset (↑s : Type u')
g : (↑s : Type u') → R
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v (↑i : ι)) 0
i : (↑s : Type u')
hit : i ∈ t
⊢ ∀ (i : ι) (hi : i ∈ s),
    Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi ∈ t → ∀ (h : i ∈ s), g (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) = 0

Tactic:
simpa [h0] using h (t.image (↑)) (fun i ↦ if hi : i ∈ s then g ⟨i, hi⟩ else 0)

Premises used: Membership.mem, dite, Subtype.mk, OfNat.ofNat, Finset.image
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h : ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
t : Finset (↑s : Type u')
g : (↑s : Type u') → R
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v (↑i : ι)) 0
i : (↑s : Type u')
hit : i ∈ t
⊢ ∀ (i : ι) (hi : i ∈ s),
    Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi ∈ t → ∀ (h : i ∈ s), g (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) = 0

Tactic:
replace h : ∀ i (hi : i ∈ s), ⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0 := by
    simpa [h0] using h (t.image (↑)) (fun i ↦ if hi : i ∈ s then g ⟨i, hi⟩ else 0)
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
t : Finset (↑s : Type u')
g : (↑s : Type u') → R
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v (↑i : ι)) 0
i : (↑s : Type u')
hit : i ∈ t
h :
  ∀ (i : ι) (hi : i ∈ s),
    Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi ∈ t → ∀ (h : i ∈ s), g (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) = 0
⊢ g i = 0

Tactic:
apply h _ _ hit
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
rw :
  (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑s : Type u')) ↦ v (↑x : ι)) ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
rw₁ rw₂ rw₃ :
  (∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0) ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
refine_1 :
  ∀
    (h :
      ∀ (s_1 : Finset (↑s : Type u')) (g : (↑s : Type u') → R),
        Eq.{u_4 + 1} (α := M) (∑ i ∈ s_1, g i • v (↑i : ι)) 0 → ∀ i ∈ s_1, g i = 0)
    (t : Finset ι) (g : ι → R) (hts : (↑t : Set ι) ⊆ s) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0) (i : ι)
    (hit : i ∈ t), g i = 0
refine_2 refine_2₁ :
  ∀
    (h :
      ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0)
    (t : Finset (↑s : Type u')) (g : (↑s : Type u') → R) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v (↑i : ι)) 0)
    (i : (↑s : Type u')) (hit : i ∈ t), g i = 0
refine_2₂ :
  ∀ (t : Finset (↑s : Type u')) (g : (↑s : Type u') → R) (h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v (↑i : ι)) 0)
    (i : (↑s : Type u')) (hit : i ∈ t)
    (h :
      ∀ (i : ι) (hi : i ∈ s),
        Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi ∈ t →
          ∀ (h : i ∈ s), g (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) = 0),
    g i = 0
⊢ LinearIndepOn R v s ↔
    ∀ (t : Finset ι) (g : ι → R), (↑t : Set ι) ⊆ s → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0

Tactic:
classical
  rw [LinearIndepOn, linearIndependent_iff']
  refine ⟨fun h t g hts h0 i hit ↦ ?_, fun h t g h0 i hit ↦ ?_⟩
  · refine h (t.preimage _ Subtype.val_injective.injOn) (fun i ↦ g i) ?_ ⟨i, hts hit⟩ (by simpa)
    rwa [t.sum_preimage ((↑) : s → ι) Subtype.val_injective.injOn (fun i ↦ g i • v i)]
    simp only [Subtype.range_coe_subtype, setOf_mem_eq]
    exact fun x hxt hxs ↦ (hxs (hts hxt)) |>.elim
  replace h : ∀ i (hi : i ∈ s), ⟨i, hi⟩ ∈ t → ∀ (h : i ∈ s), g ⟨i, h⟩ = 0 := by
    simpa [h0] using h (t.image (↑)) (fun i ↦ if hi : i ∈ s then g ⟨i, hi⟩ else 0)
  apply h _ _ hit

Premises used: linearIndependent_iff', Subtype.range_coe_subtype, Set.setOf_mem_eq, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
h :
  ∀ (t : Finset ι) (g : ι → R),
    (↑t : Set ι) ⊆ s → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0
t : Finset ι
g : ι → R
hts : (↑t : Set ι) ⊆ s
h0 : Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0
⊢ ∀ i ∈ t, g i = 0

Tactic:
simpa +contextual [h0] using h t (fun i ↦ if i ∈ t then g i else 0) hts

Premises used: Membership.mem, OfNat.ofNat, ite
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ LinearIndepOn R v s ↔
    ∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ s → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0

Tactic:
exact linearIndepOn_iff'.trans ⟨fun h t g hts htg h0 ↦ h _ _ hts h0, fun h t g hts h0 ↦
    by simpa +contextual [h0] using h t (fun i ↦ if i ∈ t then g i else 0) hts⟩

Premises used: Iff.intro, Iff.trans, linearIndepOn_iff'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
⊢ LinearIndepOn R v s ↔
    ∀ (t : Finset ι) (g : ι → R),
      (↑t : Set ι) ⊆ s → (∀ i ∉ t, g i = 0) → Eq.{u_4 + 1} (α := M) (∑ i ∈ t, g i • v i) 0 → ∀ i ∈ t, g i = 0

Tactic:
classical
  exact linearIndepOn_iff'.trans ⟨fun h t g hts htg h0 ↦ h _ _ hts h0, fun h t g hts h0 ↦
    by simpa +contextual [h0] using h t (fun i ↦ if i ∈ t then g i else 0) hts⟩

Premises used: Iff.intro, Iff.trans, linearIndepOn_iff'
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
H : ∀ (i : ι) (a : R), Membership.mem (γ := Submodule R M) (span R (v '' (univ \ {i}))) (a • v i) → a = 0
l : ι →₀ R
hl : Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) l : M) (0 : M)
h : ∀ (i : ι), Eq.{u_2 + 1} (α := R) ((l : (a : ι) → R) i : R) ((0 : (a : ι) → R) i : R)
⊢ l = 0

Tactic:
ext i