-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem LinearIndependent.disjoint_span_image (hv : LinearIndependent R v) {s t : Set ι}
    (hs : Disjoint s t) : Disjoint (Submodule.span R <| v '' s) (Submodule.span R <| v '' t)

Proof state:
case intro.intro.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : l₁ ∈ Finsupp.supported R R s
l₂ : ι →₀ R
hl₂ : l₂ ∈ Finsupp.supported R R t
H : l₂ = l₁
⊢ (Finsupp.linearCombination R v) l₁ = 0

Tactic:
subst l₂

Result:
case intro.intro.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : l₁ ∈ Finsupp.supported R R s
hl₂ : l₁ ∈ Finsupp.supported R R t
⊢ (Finsupp.linearCombination R v) l₁ = 0

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
⊢ Disjoint (span R (v '' s)) (span R (v '' t))

Tactic:
simp only [disjoint_def, Finsupp.mem_span_image_iff_linearCombination]

Result:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
⊢ ∀ (x : M),
    (∃ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = x) →
      (∃ l ∈ Finsupp.supported R R t, (Finsupp.linearCombination R v) l = x) → x = 0

Proof state:
case intro.intro.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : l₁ ∈ Finsupp.supported R R s
hl₂ : l₁ ∈ Finsupp.supported R R t
⊢ (Finsupp.linearCombination R v) l₁ = 0

Tactic:
have : l₁ = 0 := Submodule.disjoint_def.mp (Finsupp.disjoint_supported_supported hs) _ hl₁ hl₂

Result:
case intro.intro.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : l₁ ∈ Finsupp.supported R R s
hl₂ : l₁ ∈ Finsupp.supported R R t
this : l₁ = 0
⊢ (Finsupp.linearCombination R v) l₁ = 0

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
⊢ ∀ (x : M),
    (∃ l ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) l = x) →
      (∃ l ∈ Finsupp.supported R R t, (Finsupp.linearCombination R v) l = x) → x = 0

Tactic:
rintro _ ⟨l₁, hl₁, rfl⟩ ⟨l₂, hl₂, H⟩

Result:
case intro.intro.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : l₁ ∈ Finsupp.supported R R s
l₂ : ι →₀ R
hl₂ : l₂ ∈ Finsupp.supported R R t
H : (Finsupp.linearCombination R v) l₂ = (Finsupp.linearCombination R v) l₁
⊢ (Finsupp.linearCombination R v) l₁ = 0

Proof state:
case intro.intro.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : l₁ ∈ Finsupp.supported R R s
hl₂ : l₁ ∈ Finsupp.supported R R t
this : l₁ = 0
⊢ (Finsupp.linearCombination R v) l₁ = 0

Tactic:
simp [this]

Result:
no goals

Proof state:
case intro.intro.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : l₁ ∈ Finsupp.supported R R s
l₂ : ι →₀ R
hl₂ : l₂ ∈ Finsupp.supported R R t
H : (Finsupp.linearCombination R v) l₂ = (Finsupp.linearCombination R v) l₁
⊢ (Finsupp.linearCombination R v) l₁ = 0

Tactic:
rw [hv.injective_linearCombination.eq_iff] at H

Result:
case intro.intro.intro.intro
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
hv : LinearIndependent R v
s t : Set ι
hs : Disjoint s t
l₁ : ι →₀ R
hl₁ : l₁ ∈ Finsupp.supported R R s
l₂ : ι →₀ R
hl₂ : l₂ ∈ Finsupp.supported R R t
H : l₂ = l₁
⊢ (Finsupp.linearCombination R v) l₁ = 0