awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
rw : Set.range (ι := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M) ⊆ (↑(span R (Set.range v)) : Set M)
⊢ 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)

Tactic:
rw [hf_inj.injective_iff]

Premises used: Set.InjOn.injective_iff
-- 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)
rw :
  Set.range (ι := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M) ⊆
    (↑(range (Finsupp.linearCombination R v)) : Set M)
rw₁ rw₂ :
  Subset.{u_4} (α := Set M) (Set.range (ι := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M))
    (Set.range (ι := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M))
⊢ Set.range (ι := ι →₀ R) (⇑(Finsupp.linearCombination R v) : (a : ι →₀ R) → M) ⊆ (↑(span R (Set.range v)) : Set M)

Tactic:
rw [← Finsupp.range_linearCombination, LinearMap.coe_range]

Premises used: LinearMap.coe_range, Finsupp.range_linearCombination
-- 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'
hf_inj rwa rwa₁ rwa₂ rwa₃ : InjOn.{u_4, u_5} (β := M') (⇑f : (a : M) → M') (↑(span R (v '' s)) : Set M)
⊢ InjOn.{u_4, u_5} (β := M') (⇑f : (a : M) → M') (↑(span R (Set.range fun (i : (↑s : Type u')) ↦ v (↑i : ι))) : Set M)

Tactic:
rwa [← image_eq_range]

Premises used: Set.image_eq_range
-- 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 : Subsingleton R
⊢ LinearIndependent R v

Tactic:
linearIndependent_iffₛ.2 fun _l _l' _hl => Subsingleton.elim _ _

Premises used: Iff.mpr, linearIndependent_iffₛ, Subsingleton.elim
-- 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
inst_3 : Subsingleton R
⊢ LinearIndepOn R v s

Tactic:
linearIndependent_of_subsingleton

Premises used: linearIndependent_of_subsingleton, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι ≃ ι'
f : ι' → M
⊢ LinearIndependent.{u', u_2, u_4} (ι := ι) R (f ∘ (⇑e : (a : ι) → ι')) ↔ LinearIndependent R f

Tactic:
⟨fun h ↦ comp_id f ▸ e.self_comp_symm ▸ h.comp _ e.symm.injective,
    fun h ↦ h.comp _ e.injective⟩

Premises used: Function.comp_id, Eq.rec, Equiv.self_comp_symm, Iff.intro, Equiv.injective, Equiv.symm, DFunLike.coe, LinearIndependent.comp
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι ≃ ι'
f : ι' → M
g : ι → M
h : f ∘ (⇑e : (a : ι) → ι') = g
⊢ LinearIndependent R g ↔ LinearIndependent R f

Tactic:
h ▸ linearIndependent_equiv e

Premises used: Eq.rec, linearIndependent_equiv
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
e : ι ≃ ι'
f : ι' → M
s : Set ι
⊢ Eq (α := (↑s : Type u') → M)
    ((fun (x : (↑((⇑e : (a : ι) → ι') '' s) : Type u_1)) ↦ f (↑x : ι')) ∘
      (⇑(e.image s) : (a : (↑s : Type u')) → (↑((⇑e : (a : ι) → ι') '' s) : Type u_1)))
    fun (x : (↑s : Type u')) ↦ (f ∘ (⇑e : (a : ι) → ι')) (↑x : ι)

Tactic:
simp [funext_iff]

Premises used: funext_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
⊢ LinearIndepOn R v univ ↔ LinearIndependent R v

Tactic:
linearIndependent_equiv' (Equiv.Set.univ ι) rfl

Premises used: linearIndependent_equiv', rfl, LinearIndepOn, Equiv.Set.univ
-- 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 : LinearIndependent R v
s : Set ι
⊢ LinearIndepOn R v s

Tactic:
h.linearIndepOn_univ.mono s.subset_univ

Premises used: Set.subset_univ, LinearIndepOn.mono, LinearIndependent.linearIndepOn_univ
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_6
s : Set ι
f : ι → M
hf : InjOn f s
⊢ LinearIndepOn R f s ↔ LinearIndepOn R id (f '' s)

Tactic:
linearIndependent_equiv' (Equiv.Set.imageOfInjOn _ _ hf) rfl

Premises used: linearIndependent_equiv', Equiv.Set.imageOfInjOn, rfl, LinearIndepOn
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι' : Type u_1
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_6
f : ι → ι'
hf : Injective f
g : ι' → M
⊢ LinearIndepOn R g (range f) ↔ LinearIndependent R (g ∘ f)

Tactic:
Iff.symm <| linearIndependent_equiv' (Equiv.ofInjective f hf) rfl

Premises used: linearIndependent_equiv', Equiv.ofInjective, Iff.symm, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
R : Type u_2
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
ι : Type u_6
f : ι → M
hf : Injective f
⊢ LinearIndepOn R id (range f) ↔ LinearIndependent R f

Tactic:
linearIndepOn_range_iff hf id

Premises used: id, linearIndepOn_range_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
i : LinearIndependent R v
⊢ LinearIndepOn R id (range v)

Tactic:
simpa using i.comp _ (rangeSplitting_injective v)

Premises used: Set.rangeSplitting_injective, LinearIndependent.comp
-- 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
hv : LinearIndependent R v
t : Set M
ht : range v = t
⊢ LinearIndepOn R id t

Tactic:
ht ▸ hv.linearIndepOn_id

Premises used: Eq.rec, LinearIndependent.linearIndepOn_id
-- 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
⊢ (∀ (l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R),
      Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
          (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι)) →
        l₁ = l₂) ↔
    ∀ (f : ι →₀ R),
      (∀ x ∈ f.support, x ∈ s) →
        ∀ (g : ι →₀ R),
          (∀ x ∈ g.support, x ∈ s) →
            Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g

Tactic:
⟨fun h l₁ h₁ l₂ h₂ eq ↦ (Finsupp.subtypeDomain_eq_iff h₁ h₂).1 <| h _ _ <|
    (Finsupp.sum_subtypeDomain_index h₁).trans eq ▸ (Finsupp.sum_subtypeDomain_index h₂).symm,
    fun h l₁ l₂ eq ↦ ?_⟩

Premises used: Membership.mem, Eq.rec, Iff.intro, Iff.mp, Finsupp.sum_subtypeDomain_index, Finsupp.subtypeDomain_eq_iff, Finsupp.subtypeDomain, Eq.symm, Eq.trans
-- 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
refine :
  ∀
    (h :
      ∀ (f : ι →₀ R),
        (∀ x ∈ f.support, x ∈ s) →
          ∀ (g : ι →₀ R),
            (∀ x ∈ g.support, x ∈ s) →
              Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g)
    (l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R)
    (eq :
      Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
        (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))),
    l₁ = l₂
⊢ (∀ (l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R),
      Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
          (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι)) →
        l₁ = l₂) ↔
    ∀ (f : ι →₀ R),
      (∀ x ∈ f.support, x ∈ s) →
        ∀ (g : ι →₀ R),
          (∀ x ∈ g.support, x ∈ s) →
            Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g

Tactic:
refine ⟨fun h l₁ h₁ l₂ h₂ eq ↦ (Finsupp.subtypeDomain_eq_iff h₁ h₂).1 <| h _ _ <|
    (Finsupp.sum_subtypeDomain_index h₁).trans eq ▸ (Finsupp.sum_subtypeDomain_index h₂).symm,
    fun h l₁ l₂ eq ↦ ?_⟩
-- 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
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R),
        (∀ x ∈ g.support, x ∈ s) →
          Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R
eq :
  Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
    (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
⊢ l₁ = l₂

Tactic:
Finsupp.embDomain_injective (Embedding.subtype (· ∈ s)) <| h _ ?_ _ ?_ ?_

Premises used: Finsupp.embDomain_injective, Membership.mem, Function.Embedding.subtype
-- 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
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R),
        (∀ x ∈ g.support, x ∈ s) →
          Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R
eq :
  Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
    (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
refine_1 : ∀ x ∈ (Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₁).support, x ∈ s
refine_2 : ∀ x ∈ (Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₂).support, x ∈ s
refine_3 :
  Eq.{u_4 + 1} (α := M)
    ((Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₁).sum fun (i : ι) (a : R) ↦ a • v i)
    ((Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₂).sum fun (i : ι) (a : R) ↦ a • v i)
⊢ l₁ = l₂

Tactic:
refine Finsupp.embDomain_injective (Embedding.subtype (· ∈ s)) <| h _ ?_ _ ?_ ?_

Premises used: Finsupp.embDomain_injective, Membership.mem, Function.Embedding.subtype
-- 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
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R),
        (∀ x ∈ g.support, x ∈ s) →
          Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R
eq :
  Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
    (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
⊢ ∀ x ∈ (Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₁).support, x ∈ s

Tactic:
simpa using fun _ h _ ↦ h
-- 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
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R),
        (∀ x ∈ g.support, x ∈ s) →
          Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R
eq :
  Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
    (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
⊢ ∀ x ∈ (Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₂).support, x ∈ s

Tactic:
simpa using fun _ h _ ↦ h
-- 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
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R),
        (∀ x ∈ g.support, x ∈ s) →
          Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R
eq :
  Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
    (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
refine_3 :
  Eq.{u_4 + 1} (α := M)
    (Finsupp.sum (Finsupp.mapDomain (⇑(Embedding.subtype fun (x : ι) ↦ x ∈ s) : (a : { x : ι // x ∈ s }) → ι) l₁)
      fun (i : ι) (a : R) ↦ a • v i)
    (Finsupp.sum (Finsupp.mapDomain (⇑(Embedding.subtype fun (x : ι) ↦ x ∈ s) : (a : { x : ι // x ∈ s }) → ι) l₂)
      fun (i : ι) (a : R) ↦ a • v i)
⊢ Eq.{u_4 + 1} (α := M)
    ((Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₁).sum fun (i : ι) (a : R) ↦ a • v i)
    ((Finsupp.embDomain (Embedding.subtype fun (x : ι) ↦ x ∈ s) l₂).sum fun (i : ι) (a : R) ↦ a • v i)

Tactic:
simp_rw [Finsupp.embDomain_eq_mapDomain]

Premises used: Finsupp.embDomain_eq_mapDomain
-- 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
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R),
        (∀ x ∈ g.support, x ∈ s) →
          Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R
eq :
  Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
    (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
refine_3 : ∀ (b : ι), HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v b) = 0
refine_3₁ : ∀ (b : ι) (m₁ m₂ : R), (m₁ + m₂) • v b = m₁ • v b + m₂ • v b
refine_3₂ : ∀ (b : ι), HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v b) = 0
refine_3₃ : ∀ (b : ι) (m₁ m₂ : R), (m₁ + m₂) • v b = m₁ • v b + m₂ • v b
⊢ Eq.{u_4 + 1} (α := M)
    (Finsupp.sum (Finsupp.mapDomain (⇑(Embedding.subtype fun (x : ι) ↦ x ∈ s) : (a : { x : ι // x ∈ s }) → ι) l₁)
      fun (i : ι) (a : R) ↦ a • v i)
    (Finsupp.sum (Finsupp.mapDomain (⇑(Embedding.subtype fun (x : ι) ↦ x ∈ s) : (a : { x : ι // x ∈ s }) → ι) l₂)
      fun (i : ι) (a : R) ↦ a • v i)

Tactic:
rwa [Finsupp.sum_mapDomain_index, Finsupp.sum_mapDomain_index]

Premises used: Finsupp.sum_mapDomain_index
-- 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
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R),
        (∀ x ∈ g.support, x ∈ s) →
          Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R
eq :
  Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
    (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
b : ι
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) 0 (v b) = 0

Tactic:
simp only [zero_smul, add_smul]

Premises used: zero_smul, add_smul
-- 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
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R),
        (∀ x ∈ g.support, x ∈ s) →
          Eq.{u_4 + 1} (α := M) (f.sum fun (i : ι) (a : R) ↦ a • v i) (g.sum fun (i : ι) (a : R) ↦ a • v i) → f = g
l₁ l₂ : Finsupp.{u', u_2} (↑s : Type u') R
eq :
  Eq.{u_4 + 1} (α := M) (l₁.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
    (l₂.sum fun (i : (↑s : Type u')) (a : R) ↦ a • v (↑i : ι))
b : ι
m₁ m₂ : R
⊢ (m₁ + m₂) • v b = m₁ • v b + m₂ • v b

Tactic:
simp only [zero_smul, add_smul]

Premises used: zero_smul, add_smul
-- 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
⊢ ¬LinearIndepOn R v s ↔
    ∃ (f : ι →₀ R) (g : ι →₀ R),
      Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) f ∧
        Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) g ∧
          Eq.{u_4 + 1} (α := M) ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) f : M)
              ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) g : M) ∧
            f ≠ g

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
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ ¬LinearIndepOn R v s ↔
    ∃ (f : ι →₀ R) (g : ι →₀ R),
      Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) f ∧
        Membership.mem (γ := Submodule R (ι →₀ R)) (Finsupp.supported R R s) g ∧
          Eq.{u_4 + 1} (α := M) (∑ i ∈ f.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((f : (a : ι) → R) i : R) (v i))
              (∑ i ∈ g.support, HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((g : (a : ι) → R) i : R) (v i)) ∧
            f ≠ g

Tactic:
linearDepOn_iff'ₛ

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Finset.sum, linearDepOn_iff'ₛ
-- 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
⊢ LinearIndependent R (s.restrict (π := fun (a : ι) ↦ M) v) ↔ LinearIndepOn R v s

Tactic:
Iff.rfl

Premises used: Iff.rfl, Set.restrict, 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
hs : LinearIndepOn R v s
⊢ LinearIndependent R (s.restrict (π := fun (a : ι) ↦ M) v)

Tactic:
hs

Premises used: Set.restrict, 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
rw :
  LinearIndependent R (s.restrict (π := fun (a : ι) ↦ M) v) ↔
    Injective (α := ↥(Finsupp.supported R R s)) (β := ↥(span R (v '' s)))
      (⇑(Finsupp.linearCombinationOn ι M R v s) : (a : ↥(Finsupp.supported R R s)) → ↥(span R (v '' s)))
⊢ LinearIndepOn R v s ↔
    Injective (α := ↥(Finsupp.supported R R s)) (β := ↥(span R (v '' s)))
      (⇑(Finsupp.linearCombinationOn ι M R v s) : (a : ↥(Finsupp.supported R R s)) → ↥(span R (v '' s)))

Tactic:
rw [← linearIndependent_restrict_iff]

Premises used: linearIndependent_restrict_iff
-- 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
⊢ LinearIndependent R (s.restrict (π := fun (a : ι) ↦ M) v) ↔
    Injective (α := ↥(Finsupp.supported R R s)) (β := ↥(span R (v '' s)))
      (⇑(Finsupp.linearCombinationOn ι M R v s) : (a : ↥(Finsupp.supported R R s)) → ↥(span R (v '' s)))

Tactic:
simp [LinearIndependent, Finsupp.linearCombination_restrict]

Premises used: Finsupp.linearCombination_restrict, LinearIndependent
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
refine_1 :
  ∀ (c : ι →₀ R),
    Membership.mem (α := M) (γ := Submodule R M) (span R (range v))
      ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) c : M)
refine_2 :
  Surjective (α := ι →₀ R) (β := ↥(span R (range v)))
    (⇑(LinearMap.codRestrict (span R (range v)) (Finsupp.linearCombination R v) ⋯) : (a : ι →₀ R) → ↥(span R (range v)))
⊢ (ι →₀ R) ≃ₗ[R] ↥(span R (range v))

Tactic:
refine LinearEquiv.ofBijective (LinearMap.codRestrict (span R (range v))
    (Finsupp.linearCombination R v) ?_) ⟨hv.codRestrict _, ?_⟩

Premises used: Function.Injective.codRestrict, And.intro, Submodule.span, LinearMap.codRestrict, Set.range, Finsupp.linearCombination, LinearEquiv.ofBijective
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
refine_1 :
  ∀ (c : ι →₀ R),
    Membership.mem (α := M) (γ := Submodule R M) (LinearMap.range (Finsupp.linearCombination R v))
      ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) c : M)
⊢ ∀ (c : ι →₀ R),
    Membership.mem (α := M) (γ := Submodule R M) (span R (range v))
      ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) c : M)

Tactic:
simp_rw [← Finsupp.range_linearCombination]

Premises used: Finsupp.range_linearCombination
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
⊢ ∀ (c : ι →₀ R),
    Membership.mem (α := M) (γ := Submodule R M) (LinearMap.range (Finsupp.linearCombination R v))
      ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) c : M)

Tactic:
fun c ↦ ⟨c, rfl⟩

Premises used: Set.Mem, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.LinearAlgebra.LinearIndependent.Defs
Goal:
ι : Type u'
ι' : Type u_1
R : Type u_2
K : Type u_3
s : Set ι
M : Type u_4
M' : Type u_5
V : Type u
v : ι → M
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : Module R M'
hv : LinearIndependent R v
⊢ ∀ (c : ι →₀ R),
    Membership.mem (α := M) (γ := Submodule R M) (LinearMap.range (Finsupp.linearCombination R v))
      ((Finsupp.linearCombination R v : (a : ι →₀ R) → M) c : M)

Tactic:
exact fun c ↦ ⟨c, rfl⟩