-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem linearIndepOn_iffₛ : LinearIndepOn R v s ↔
      ∀ f ∈ Finsupp.supported R R s, ∀ g ∈ Finsupp.supported R R s,
        Finsupp.linearCombination R v f = Finsupp.linearCombination R v g → f = g

Proof state:
case refine_3
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ ((Finsupp.mapDomain (⇑(Embedding.subtype s)) l₁).sum fun i a => a • v i) =
    (Finsupp.mapDomain (⇑(Embedding.subtype s)) l₂).sum fun i a => a • v i

Tactic:
rwa [Finsupp.sum_mapDomain_index, Finsupp.sum_mapDomain_index] <;>
  intros <;> simp only [zero_smul, add_smul]

Result:
no goals

Proof state:
case refine_1
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ ∀ x ∈ (Finsupp.embDomain (Embedding.subtype s) l₁).support, x ∈ s

case refine_2
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ ∀ x ∈ (Finsupp.embDomain (Embedding.subtype s) l₂).support, x ∈ s

case refine_3
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ ((Finsupp.embDomain (Embedding.subtype s) l₁).sum fun i a => a • v i) =
    (Finsupp.embDomain (Embedding.subtype s) l₂).sum fun i a => a • v i

Tactic:
iterate 2 simpa using fun _ h _ ↦ h

Result:
case refine_3
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ ((Finsupp.embDomain (Embedding.subtype s) l₁).sum fun i a => a • v i) =
    (Finsupp.embDomain (Embedding.subtype s) l₂).sum fun i a => a • v i

Proof state:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ l₁ = l₂

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

Result:
case refine_1
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ ∀ x ∈ (Finsupp.embDomain (Embedding.subtype s) l₁).support, x ∈ s

case refine_2
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ ∀ x ∈ (Finsupp.embDomain (Embedding.subtype s) l₂).support, x ∈ s

case refine_3
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ ((Finsupp.embDomain (Embedding.subtype s) l₁).sum fun i a => a • v i) =
    (Finsupp.embDomain (Embedding.subtype s) l₂).sum fun i a => a • v i

Proof state:
case refine_3
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ ((Finsupp.embDomain (Embedding.subtype s) l₁).sum fun i a => a • v i) =
    (Finsupp.embDomain (Embedding.subtype s) l₂).sum fun i a => a • v i

Tactic:
simp_rw [Finsupp.embDomain_eq_mapDomain]

Result:
case refine_3
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ ((Finsupp.mapDomain (⇑(Embedding.subtype s)) l₁).sum fun i a => a • v i) =
    (Finsupp.mapDomain (⇑(Embedding.subtype s)) l₂).sum fun i a => a • v i

Proof state:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ (∀ (l₁ l₂ : ↑s →₀ R), ((l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i) → l₁ = l₂) ↔
    ∀ (f : ι →₀ R),
      (∀ x ∈ f.support, x ∈ s) →
        ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => 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 ↦ ?_⟩

Result:
ι : Type u'
R : Type u_2
s : Set ι
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h :
  ∀ (f : ι →₀ R),
    (∀ x ∈ f.support, x ∈ s) →
      ∀ (g : ι →₀ R), (∀ x ∈ g.support, x ∈ s) → ((f.sum fun i a => a • v i) = g.sum fun i a => a • v i) → f = g
l₁ l₂ : ↑s →₀ R
eq : (l₁.sum fun i a => a • v ↑i) = l₂.sum fun i a => a • v ↑i
⊢ l₁ = l₂