case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type ?u.1234961
n' : o → Type ?u.1234966
R : Type ?u.1234969
S : Type ?u.1234972
α : Type v
β : Type w
γ : Type ?u.1234979
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : l ≃ m
f : o ≃ n
i' : l
j : o
⊢ updateRow (submatrix A ↑e ↑f) i r i' j = submatrix (updateRow A (↑e i) fun j => r (↑f.symm j)) (↑e) (↑f) i' j
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type ?u.1234961
n' : o → Type ?u.1234966
R : Type ?u.1234969
S : Type ?u.1234972
α : Type v
β : Type w
γ : Type ?u.1234979
M : Matrix m n α
i✝ : m
j : n
b : n → α
c : m → α
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : l ≃ m
f : o ≃ n
⊢ updateRow (submatrix A ↑e ↑f) i r = submatrix (updateRow A (↑e i) fun j => r (↑f.symm j)) ↑e ↑f
ext (i' j)
no goals
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type ?u.1234961
n' : o → Type ?u.1234966
R : Type ?u.1234969
S : Type ?u.1234972
α : Type v
β : Type w
γ : Type ?u.1234979
M : Matrix m n α
i✝ : m
j✝ : n
b : n → α
c : m → α
inst✝¹ : DecidableEq l
inst✝ : DecidableEq m
A : Matrix m n α
i : l
r : o → α
e : l ≃ m
f : o ≃ n
i' : l
j : o
⊢ updateRow (submatrix A ↑e ↑f) i r i' j = submatrix (updateRow A (↑e i) fun j => r (↑f.symm j)) (↑e) (↑f) i' j
simp only [submatrix_apply, updateRow_apply, Equiv.apply_eq_iff_eq, Equiv.symm_apply_apply]