no goals
ι : Type u_1
ι' : Type u_2
R : Type u_5
R₂ : Type ?u.588552
K : Type ?u.588555
M : Type u_3
M' : Type u_4
M'' : Type ?u.588564
V : Type u
V' : Type ?u.588569
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b b₁ : Basis ι R M
i✝ : ι
c : R
x : M
b' : Basis ι' R M'
i : ι ⊕ ι'
⊢ ↑(Basis.prod b b') i = Sum.elim (↑(LinearMap.inl R M M') ∘ ↑b) (↑(LinearMap.inr R M M') ∘ ↑b') i
ext <;> cases i <;>
  simp only [prod_apply_inl_fst, Sum.elim_inl, LinearMap.inl_apply, prod_apply_inr_fst,
    Sum.elim_inr, LinearMap.inr_apply, prod_apply_inl_snd, prod_apply_inr_snd, Function.comp]