-- Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
theorem linearIndependent_inl_union_inr' {v : ι → M} {v' : ι' → M'}
    (hv : LinearIndependent R v) (hv' : LinearIndependent R v') :
    LinearIndependent R (Sum.elim (inl R M M' ∘ v) (inr R M M' ∘ v'))

Proof state:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
this :
  linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) =
    (linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)
⊢ LinearIndependent R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v'))

Tactic:
rw [LinearIndependent, this]

Result:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
this :
  linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) =
    (linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)
⊢ Injective ⇑((linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R))

Proof state:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
this :
  linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) =
    (linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)
⊢ Injective ⇑((linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R))

Tactic:
simpa [LinearMap.coe_prodMap] using ⟨hv, hv'⟩

Result:
no goals

Proof state:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
⊢ LinearIndependent R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v'))

Tactic:
have : linearCombination R (Sum.elim (inl R M M' ∘ v) (inr R M M' ∘ v')) =
    .prodMap (linearCombination R v) (linearCombination R v') ∘ₗ
    (sumFinsuppLEquivProdFinsupp R).toLinearMap := by
  ext (_ | _) <;> simp [linearCombination_comapDomain]

Result:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
this :
  linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) =
    (linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)
⊢ LinearIndependent R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v'))

Proof state:
ι : Type u'
ι' : Type u_1
R : Type u_2
M : Type u_4
M' : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M
inst✝ : Module R M'
v : ι → M
v' : ι' → M'
hv : LinearIndependent R v
hv' : LinearIndependent R v'
⊢ linearCombination R (Sum.elim (⇑(inl R M M') ∘ v) (⇑(inr R M M') ∘ v')) =
    (linearCombination R v).prodMap (linearCombination R v') ∘ₗ ↑(sumFinsuppLEquivProdFinsupp R)

Tactic:
ext (_ | _) <;> simp [linearCombination_comapDomain]

Result:
no goals