case inl
ι : Type u_1
ι' : Type ?u.851959
R : Type u_2
R₂ : Type ?u.851965
K : Type ?u.851968
M : Type u_3
M' : Type ?u.851974
M'' : Type ?u.851977
V : Type u
V' : Type ?u.851982
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x y : M
b : Basis ι R M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
inst✝ : DecidableEq ι
i j : ι
h : j = i
⊢ ↑(coord (Basis.mk hli hsp) i) (v j) = if j = i then 1 else 0

case inr
ι : Type u_1
ι' : Type ?u.851959
R : Type u_2
R₂ : Type ?u.851965
K : Type ?u.851968
M : Type u_3
M' : Type ?u.851974
M'' : Type ?u.851977
V : Type u
V' : Type ?u.851982
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x y : M
b : Basis ι R M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
inst✝ : DecidableEq ι
i j : ι
h : j ≠ i
⊢ ↑(coord (Basis.mk hli hsp) i) (v j) = if j = i then 1 else 0
ι : Type u_1
ι' : Type ?u.851959
R : Type u_2
R₂ : Type ?u.851965
K : Type ?u.851968
M : Type u_3
M' : Type ?u.851974
M'' : Type ?u.851977
V : Type u
V' : Type ?u.851982
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x y : M
b : Basis ι R M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
inst✝ : DecidableEq ι
i j : ι
⊢ ↑(coord (Basis.mk hli hsp) i) (v j) = if j = i then 1 else 0
cases' eq_or_ne j i with h h
no goals
case inl
ι : Type u_1
ι' : Type ?u.851959
R : Type u_2
R₂ : Type ?u.851965
K : Type ?u.851968
M : Type u_3
M' : Type ?u.851974
M'' : Type ?u.851977
V : Type u
V' : Type ?u.851982
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x y : M
b : Basis ι R M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
inst✝ : DecidableEq ι
i j : ι
h : j = i
⊢ ↑(coord (Basis.mk hli hsp) i) (v j) = if j = i then 1 else 0
simp only [h, if_true, eq_self_iff_true, mk_coord_apply_eq i]
no goals
case inr
ι : Type u_1
ι' : Type ?u.851959
R : Type u_2
R₂ : Type ?u.851965
K : Type ?u.851968
M : Type u_3
M' : Type ?u.851974
M'' : Type ?u.851977
V : Type u
V' : Type ?u.851982
v : ι → M
inst✝⁹ : Ring R
inst✝⁸ : CommRing R₂
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup M'
inst✝⁵ : AddCommGroup M''
inst✝⁴ : Module R M
inst✝³ : Module R₂ M
inst✝² : Module R M'
inst✝¹ : Module R M''
c d : R
x y : M
b : Basis ι R M
hli : LinearIndependent R v
hsp : ⊤ ≤ span R (Set.range v)
inst✝ : DecidableEq ι
i j : ι
h : j ≠ i
⊢ ↑(coord (Basis.mk hli hsp) i) (v j) = if j = i then 1 else 0
simp only [h, if_false, mk_coord_apply_ne h]