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
H :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s
simp_rw simp_rw₁ :
  Eq.{u_4 + 1} (α := M) (∑ x ∈ s, (if x ∈ s then f x else 0) • v x) (∑ x ∈ s, (if x ∈ s then g x else 0) • v x)
simp_rw₂ :
  Eq.{u_4 + 1} (α := M) (∑ x ∈ s, if x ∈ s then f x • v x else HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v x))
    (∑ x ∈ s, if x ∈ s then g x • v x else HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v x))
simp_rw₃ : Eq.{u_4 + 1} (α := M) (∑ x ∈ s, if x ∈ s then f x • v x else 0) (∑ x ∈ s, if x ∈ s then g x • v x else 0)
simp_rw₄ : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (j : ι) ↦ if j ∈ s then f j else 0) i) (v i))
    (∑ i ∈ s, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((fun (j : ι) ↦ if j ∈ s then g j else 0) i) (v i))

Tactic:
simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]

Premises used: zero_smul, Finset.sum_extend_by_zero, ite_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
H :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s
h : f i = if i ∈ s then f i else 0
h₁ : g i = if i ∈ s then g i else 0
⊢ f i = g i

Tactic:
convert!
        H s (fun j ↦ if j ∈ s then f j else 0) (fun j ↦ if j ∈ s then g j else 0)
          (fun j hj ↦ (if_neg hj).trans (if_neg hj).symm)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]) i

Premises used: Membership.mem, OfNat.ofNat, Eq.symm, if_neg, Eq.trans, 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
H :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s
⊢ f i = if i ∈ s then f i else 0

Tactic:
(if_pos hi).symm

Premises used: if_pos, Eq.symm
-- 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
H :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s
⊢ f i = if i ∈ s then f i else 0

Tactic:
exact (if_pos hi).symm

Premises used: if_pos, Eq.symm
-- 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
H :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s
⊢ g i = if i ∈ s then g i else 0

Tactic:
(if_pos hi).symm

Premises used: if_pos, Eq.symm
-- 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
H :
  ∀ (s : Finset ι) (f g : ι → R),
    (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s
⊢ g i = if i ∈ s then g i else 0

Tactic:
exact (if_pos hi).symm

Premises used: if_pos, Eq.symm
-- 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
⊢ LinearIndependent R v ↔
    ∀ (s : Finset ι) (f g : ι → R),
      (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i

Tactic:
exact linearIndependent_iff'ₛ.trans
    ⟨fun H s f g eq hv i ↦ if his : i ∈ s then H s f g hv i his else eq i his,
      fun H s f g eq i hi ↦ by
      convert!
        H s (fun j ↦ if j ∈ s then f j else 0) (fun j ↦ if j ∈ s then g j else 0)
          (fun j hj ↦ (if_neg hj).trans (if_neg hj).symm)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]) i <;>
      exact (if_pos hi).symm⟩

Premises used: Iff.intro, Iff.trans, 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
⊢ LinearIndependent R v ↔
    ∀ (s : Finset ι) (f g : ι → R),
      (∀ i ∉ s, f i = g i) → Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i) → ∀ (i : ι), f i = g i

Tactic:
classical
  exact linearIndependent_iff'ₛ.trans
    ⟨fun H s f g eq hv i ↦ if his : i ∈ s then H s f g hv i his else eq i his,
      fun H s f g eq i hi ↦ by
      convert!
        H s (fun j ↦ if j ∈ s then f j else 0) (fun j ↦ if j ∈ s then g j else 0)
          (fun j hj ↦ (if_neg hj).trans (if_neg hj).symm)
          (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]) i <;>
      exact (if_pos hi).symm⟩

Premises used: Iff.intro, Iff.trans, 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
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 : Finset ι) (f : ι → R) (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
⊢ ¬LinearIndependent R v ↔
    ∃ (s : Finset ι) (f : ι → R) (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

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
⊢ (¬∀ (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 : Finset ι) (f : ι → R) (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

Tactic:
simp only [exists_prop, not_forall]

Premises used: exists_prop, Classical.not_forall
-- 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 : Fintype ι
simp_rw :
  Injective (α := ι → R) (β := M) (⇑(Fintype.linearCombination R v) : (a : ι → R) → M) ↔
    ∀ (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i) → ∀ (i : ι), f i = g i
simp_rw₁ :
  (∀ ⦃a₁ a₂ : ι → R⦄,
      Eq.{u_4 + 1} (α := M) ((Fintype.linearCombination R v : (a : ι → R) → M) a₁ : M)
          ((Fintype.linearCombination R v : (a : ι → R) → M) a₂ : M) →
        a₁ = a₂) ↔
    ∀ (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i) → ∀ (i : ι), f i = g i
simp_rw₂ :
  (∀ ⦃a₁ a₂ : ι → R⦄, Eq.{u_4 + 1} (α := M) (∑ i : ι, a₁ i • v i) (∑ i : ι, a₂ i • v i) → a₁ = a₂) ↔
    ∀ (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i) → ∀ (i : ι), f i = g i
⊢ LinearIndependent R v ↔
    ∀ (f g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i) → ∀ (i : ι), f i = g i

Tactic:
simp_rw [linearIndependent_iff_injective_fintypeLinearCombination,
    Injective, Fintype.linearCombination_apply, funext_iff]

Premises used: funext_iff, linearIndependent_iff_injective_fintypeLinearCombination, Function.Injective, Fintype.linearCombination_apply
-- 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 : Fintype ι
⊢ ¬LinearIndependent R v ↔
    ∃ (f : ι → R) (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, f i • v i) (∑ i : ι, g i • v i) ∧ ∃ (i : ι), f i ≠ g i

Tactic:
simpa using not_iff_not.2 Fintype.linearIndependent_iffₛ

Premises used: not_iff_not, Iff.mpr, Fintype.linearIndependent_iffₛ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset ι
simp_rw :
  (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
          (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) ↔
    ∀ (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
⊢ LinearIndepOn R v (↑s : Set ι) ↔
    ∀ (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

Tactic:
simp_rw [LinearIndepOn, Fintype.linearIndependent_iffₛ]

Premises used: Fintype.linearIndependent_iffₛ, LinearIndepOn
-- 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
s : Finset ι
mp :
  (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
          (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) →
    ∀ (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
mpr :
  (∀ (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) →
    ∀ (f g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
          (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i
⊢ (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
          (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) ↔
    ∀ (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

Tactic:
constructor
-- 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
s : Finset ι
hv :
  ∀ (f g : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
        (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i
f g : ι → R
hfg : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s
⊢ Eq.{u_4 + 1} (α := M) (∑ x ∈ s.attach, f (↑x : ι) • v (↑x : ι)) (∑ x ∈ s.attach, g (↑x : ι) • v (↑x : ι))

Tactic:
simp_rw [← s.sum_attach] at hfg

Premises used: Finset.sum_attach
-- 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
s : Finset ι
hv :
  ∀ (f g : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
        (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i
f g : ι → R
i : ι
hi : i ∈ s
hfg : Eq.{u_4 + 1} (α := M) (∑ x ∈ s.attach, f (↑x : ι) • v (↑x : ι)) (∑ x ∈ s.attach, g (↑x : ι) • v (↑x : ι))
⊢ f i = g i

Tactic:
hv (f ∘ Subtype.val) (g ∘ Subtype.val) hfg ⟨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
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset ι
hv :
  ∀ (f g : (↑(↑s : Set ι) : Type u') → R),
    Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
        (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
      ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i
f g : ι → R
i : ι
hi : i ∈ s
hfg : Eq.{u_4 + 1} (α := M) (∑ x ∈ s.attach, f (↑x : ι) • v (↑x : ι)) (∑ x ∈ s.attach, g (↑x : ι) • v (↑x : ι))
⊢ f i = g i

Tactic:
exact hv (f ∘ Subtype.val) (g ∘ Subtype.val) hfg ⟨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
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset ι
hv : ∀ (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
f g : (↑(↑s : Set ι) : Type u') → R
hfg :
  Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
    (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι))
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))
    (∑ i ∈ s,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R)
        ((fun (j : ι) ↦ (if hj : j ∈ s then g (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) j hj) else 0 : R)) i)
        (v i))

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
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset ι
hv : ∀ (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
f g : (↑(↑s : Set ι) : Type u') → R
hfg :
  Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
    (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι))
i : (↑(↑s : Set ι) : Type u')
⊢ f i = g i

Tactic:
simpa using hv (fun j ↦ if hj : j ∈ s then f ⟨j, hj⟩ else 0)
      (fun j ↦ if hj : j ∈ s then g ⟨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
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Finset ι
simp_rw :
  (LinearIndependent.{u', u_2, u_4} R (M := M) fun (x : (↑(↑s : Set ι) : Type u')) ↦ v (↑x : ι)) ↔
    ∀ (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
simp_rw₁ :
  (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
          (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) ↔
    ∀ (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
mp :
  (∀ (f g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
          (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i) →
    ∀ (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
mpr mpr₁ :
  (∀ (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) →
    ∀ (f g : (↑(↑s : Set ι) : Type u') → R),
      Eq.{u_4 + 1} (α := M) (∑ i : (↑(↑s : Set ι) : Type u'), f i • v (↑i : ι))
          (∑ i : (↑(↑s : Set ι) : Type u'), g i • v (↑i : ι)) →
        ∀ (i : (↑(↑s : Set ι) : Type u')), f i = g i
⊢ LinearIndepOn R v (↑s : Set ι) ↔
    ∀ (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

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

Premises used: Fintype.linearIndependent_iffₛ, Finset.sum_attach, LinearIndepOn
-- 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
s : Finset ι
⊢ ¬LinearIndepOn R v (↑s : Set ι) ↔
    ∃ (f : ι → R) (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

Tactic:
simpa using linearIndepOn_finset_iffₛ.not

Premises used: Iff.not, linearIndepOn_finset_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
H : ∀ (s : Finset ι), LinearIndependent (ι := ↥s) R (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s))
s : Finset ι
f g : ι → R
eq : Eq.{u_4 + 1} (α := M) (∑ i ∈ s, f i • v i) (∑ i ∈ s, g i • v i)
i : ι
hi : i ∈ s
⊢ Eq.{u_4 + 1} (α := M)
    (∑ i : ↥s, (f ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) i • (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) i)
    (∑ i : ↥s, (g ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) i • (v ∘ Subtype.val (p := fun (x : ι) ↦ x ∈ s)) i)

Tactic:
simpa only [← s.sum_coe_sort] using eq

Premises used: Finset.sum_coe_sort
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → LinearIndepOn R v (↑t : Set ι)
rw :
  ∀ (s_1 : Finset (↑s : Type u')),
    LinearIndependent.{u', u_2, u_4} (ι := ↥s_1) R (M := M)
      ((fun (x : (↑s : Type u')) ↦ v (↑x : ι)) ∘ Subtype.val (p := fun (x : (↑s : Type u')) ↦ x ∈ s_1))
⊢ LinearIndepOn R v s

Tactic:
rw [LinearIndepOn, linearIndependent_iff_finset_linearIndependent]

Premises used: linearIndependent_iff_finset_linearIndependent, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → LinearIndepOn R v (↑t : Set ι)
t : Finset (↑s : Type u')
⊢ (↑(Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ s) t) : Set ι) ⊆ s

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → LinearIndepOn R v (↑t : Set ι)
t : Finset (↑s : Type u')
x : ↥t
⊢ ∀ ⦃a₂ : ↥t⦄,
    Eq.{u' + 1} (α := (↑(↑(Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ s) t) : Set ι) : Type u'))
        ((fun (x : ↥t) ↦
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑(Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ s) t) : Set ι))
                (↑(↑x : (↑s : Type u')) : ι) ⋯ :
              { x : ι // x ∈ (↑(Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ s) t) : Set ι) }))
          x)
        ((fun (x : ↥t) ↦
            (Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑(Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ s) t) : Set ι))
                (↑(↑x : (↑s : Type u')) : ι) ⋯ :
              { x : ι // x ∈ (↑(Finset.map (Embedding.subtype fun (x : ι) ↦ x ∈ s) t) : Set ι) }))
          a₂) →
      x = a₂

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
hv : ∀ (t : Finset ι), (↑t : Set ι) ⊆ s → LinearIndepOn R v (↑t : Set ι)
⊢ ∀ (s_1 : Finset (↑s : Type u')),
    LinearIndependent.{u', u_2, u_4} (ι := ↥s_1) R (M := M)
      ((fun (x : (↑s : Type u')) ↦ v (↑x : ι)) ∘ Subtype.val (p := fun (x : (↑s : Type u')) ↦ x ∈ s_1))

Tactic:
exact fun t ↦ (hv (t.map <| .subtype _) (by simp)).comp (ι' := t)
      (fun x ↦ ⟨x, Finset.mem_map_of_mem (.subtype _) x.2⟩) fun x ↦ by aesop
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hfv : LinearIndependent.{u', u_2, u_5} R (M := M') ((⇑f : (a : M) → M') ∘ v)
⊢ Injective (α := ι →₀ R) (β := M')
    (Function.comp (β := M) (⇑f : (a : M) → M') (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M))

Tactic:
rw [LinearIndependent, Finsupp.linearCombination_linear_comp, LinearMap.coe_comp] at hfv

Premises used: Finsupp.linearCombination_linear_comp, LinearMap.coe_comp, LinearIndependent
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hfv :
  Injective (α := ι →₀ R) (β := M')
    (Function.comp (β := M) (⇑f : (a : M) → M') (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M))
⊢ LinearIndependent R v

Tactic:
hfv.of_comp

Premises used: LinearIndependent, Function.Injective.of_comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hfv :
  Injective (α := ι →₀ R) (β := M')
    (Function.comp (β := M) (⇑f : (a : M) → M') (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M))
⊢ LinearIndependent R v

Tactic:
exact hfv.of_comp

Premises used: Function.Injective.of_comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hfv : LinearIndepOn.{u', u_2, u_5} R (M := M') ((⇑f : (a : M) → M') ∘ v) s
⊢ LinearIndepOn R v s

Tactic:
LinearIndependent.of_comp f hfv

Premises used: LinearIndependent.of_comp, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
inst : Semiring R
s : Set ι'
v : ι → ι' → R
hv : LinearIndependent R (M := (j : (↑s : Type u_1)) → R) fun (i : ι) (j : (↑s : Type u_1)) ↦ v i (↑j : ι')
⊢ LinearIndependent R v

Tactic:
hv.of_comp ⟨⟨s.restrict, fun _ _ ↦ rfl⟩, fun _ _ ↦ rfl⟩

Premises used: LinearIndependent.of_comp, LinearMap.mk, AddHom.mk, Set.restrict, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
f : M →ₗ[R] M'
hf_inj : InjOn.{u_4, u_5} (β := M') (⇑f : (a : M) → M') (↑(span R (Set.range v)) : Set M)
simp_rw :
  Injective (α := ι →₀ R) (β := M')
      (Function.comp (β := M) (⇑f : (a : M) → M') (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M)) ↔
    Injective (α := ι →₀ R) (β := M) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M)
⊢ LinearIndependent.{u', u_2, u_5} R (M := M') ((⇑f : (a : M) → M') ∘ v) ↔ LinearIndependent R v

Tactic:
simp_rw [LinearIndependent, Finsupp.linearCombination_linear_comp, coe_comp]

Premises used: Finsupp.linearCombination_linear_comp, LinearMap.coe_comp, LinearIndependent