case a.h
ι : Type u_2
ι' : Type u_1
κ : Type ?u.150932
κ' : Type ?u.150935
R : Type u_3
M : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.151128
M₂ : Type ?u.151131
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
⊢ toMatrix e (update v j x) i' k = updateColumn (toMatrix e v) j (↑(↑e.repr x)) i' k
ι : Type u_2
ι' : Type u_1
κ : Type ?u.150932
κ' : Type ?u.150935
R : Type u_3
M : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.151128
M₂ : Type ?u.151131
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι'
x : M
⊢ toMatrix e (update v j x) = updateColumn (toMatrix e v) j ↑(↑e.repr x)
ext (i' k)
case a.h
ι : Type u_2
ι' : Type u_1
κ : Type ?u.150932
κ' : Type ?u.150935
R : Type u_3
M : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.151128
M₂ : Type ?u.151131
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
⊢ ↑(↑e.repr (update v j x k)) i' = if k = j then ↑(↑e.repr x) i' else ↑(↑e.repr (v k)) i'
case a.h
ι : Type u_2
ι' : Type u_1
κ : Type ?u.150932
κ' : Type ?u.150935
R : Type u_3
M : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.151128
M₂ : Type ?u.151131
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
⊢ toMatrix e (update v j x) i' k = updateColumn (toMatrix e v) j (↑(↑e.repr x)) i' k
rw [Basis.toMatrix, Matrix.updateColumn_apply, e.toMatrix_apply]
case a.h.inl
ι : Type u_2
ι' : Type u_1
κ : Type ?u.150932
κ' : Type ?u.150935
R : Type u_3
M : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.151128
M₂ : Type ?u.151131
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : k = j
⊢ ↑(↑e.repr (update v j x k)) i' = ↑(↑e.repr x) i'

case a.h.inr
ι : Type u_2
ι' : Type u_1
κ : Type ?u.150932
κ' : Type ?u.150935
R : Type u_3
M : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.151128
M₂ : Type ?u.151131
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : ¬k = j
⊢ ↑(↑e.repr (update v j x k)) i' = ↑(↑e.repr (v k)) i'
case a.h
ι : Type u_2
ι' : Type u_1
κ : Type ?u.150932
κ' : Type ?u.150935
R : Type u_3
M : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.151128
M₂ : Type ?u.151131
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
⊢ ↑(↑e.repr (update v j x k)) i' = if k = j then ↑(↑e.repr x) i' else ↑(↑e.repr (v k)) i'
split_ifs with h
no goals
case a.h.inl
ι : Type u_2
ι' : Type u_1
κ : Type ?u.150932
κ' : Type ?u.150935
R : Type u_3
M : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.151128
M₂ : Type ?u.151131
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : k = j
⊢ ↑(↑e.repr (update v j x k)) i' = ↑(↑e.repr x) i'
rw [h, update_same j x v]
no goals
case a.h.inr
ι : Type u_2
ι' : Type u_1
κ : Type ?u.150932
κ' : Type ?u.150935
R : Type u_3
M : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
R₂ : Type ?u.151128
M₂ : Type ?u.151131
inst✝³ : CommRing R₂
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
e : Basis ι R M
v : ι' → M
i : ι
j : ι'
inst✝ : DecidableEq ι'
x : M
i' : ι
k : ι'
h : ¬k = j
⊢ ↑(↑e.repr (update v j x k)) i' = ↑(↑e.repr (v k)) i'
rw [update_noteq h]