case h
ι : Type u_3
ι' : Type u_4
R : Type u_5
R₂ : Type ?u.578423
K : Type ?u.578426
M : Type u_2
M' : Type u_1
M'' : Type ?u.578435
V : Type u
V' : Type ?u.578440
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)).snd) j = ↑(↑b'.repr 0) j
ι : Type u_3
ι' : Type u_4
R : Type u_5
R₂ : Type ?u.578423
K : Type ?u.578426
M : Type u_2
M' : Type u_1
M'' : Type ?u.578435
V : Type u
V' : Type ?u.578440
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)).snd = ↑b'.repr 0
ext j
case h
ι : Type u_3
ι' : Type u_4
R : Type u_5
R₂ : Type ?u.578423
K : Type ?u.578426
M : Type u_2
M' : Type u_1
M'' : Type ?u.578435
V : Type u
V' : Type ?u.578440
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.inr j) = 0
case h
ι : Type u_3
ι' : Type u_4
R : Type u_5
R₂ : Type ?u.578423
K : Type ?u.578426
M : Type u_2
M' : Type u_1
M'' : Type ?u.578435
V : Type u
V' : Type ?u.578440
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)).snd) j = ↑(↑b'.repr 0) 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.snd_sumFinsuppLEquivProdFinsupp, LinearEquiv.map_zero,
  Finsupp.zero_apply]
no goals
case h
ι : Type u_3
ι' : Type u_4
R : Type u_5
R₂ : Type ?u.578423
K : Type ?u.578426
M : Type u_2
M' : Type u_1
M'' : Type ?u.578435
V : Type u
V' : Type ?u.578440
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.inr j) = 0
apply Finsupp.single_eq_of_ne Sum.inl_ne_inr