case h
ι : Type u_3
ι' : Type u_4
R : Type u_5
R₂ : Type ?u.568294
K : Type ?u.568297
M : Type u_1
M' : Type u_2
M'' : Type ?u.568306
V : Type u
V' : Type ?u.568311
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 j : ι
⊢ ↑(↑b.repr (↑(Basis.prod b b') (Sum.inl i)).fst) j = ↑(↑b.repr (↑b i)) j
ι : Type u_3
ι' : Type u_4
R : Type u_5
R₂ : Type ?u.568294
K : Type ?u.568297
M : Type u_1
M' : Type u_2
M'' : Type ?u.568306
V : Type u
V' : Type ?u.568311
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 : ι
⊢ ↑b.repr (↑(Basis.prod b b') (Sum.inl i)).fst = ↑b.repr (↑b i)
ext j
case h
ι : Type u_3
ι' : Type u_4
R : Type u_5
R₂ : Type ?u.568294
K : Type ?u.568297
M : Type u_1
M' : Type u_2
M'' : Type ?u.568306
V : Type u
V' : Type ?u.568311
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 j : ι
⊢ ↑(Finsupp.single (Sum.inl i) 1) (Sum.inl j) = ↑(Finsupp.single i 1) j
case h
ι : Type u_3
ι' : Type u_4
R : Type u_5
R₂ : Type ?u.568294
K : Type ?u.568297
M : Type u_1
M' : Type u_2
M'' : Type ?u.568306
V : Type u
V' : Type ?u.568311
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 j : ι
⊢ ↑(↑b.repr (↑(Basis.prod b b') (Sum.inl i)).fst) j = ↑(↑b.repr (↑b i)) j
simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply, LinearEquiv.prod_symm,
  LinearEquiv.prod_apply, b.repr.apply_symm_apply, LinearEquiv.symm_symm, repr_self,
  Equiv.toFun_as_coe, Finsupp.fst_sumFinsuppLEquivProdFinsupp]
no goals
case h
ι : Type u_3
ι' : Type u_4
R : Type u_5
R₂ : Type ?u.568294
K : Type ?u.568297
M : Type u_1
M' : Type u_2
M'' : Type ?u.568306
V : Type u
V' : Type ?u.568311
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 j : ι
⊢ ↑(Finsupp.single (Sum.inl i) 1) (Sum.inl j) = ↑(Finsupp.single i 1) j
apply Finsupp.single_apply_left Sum.inl_injective