case refine'_1
α : Type u_3
β : Type ?u.756
m : Type u_1
n : Type u_2
o : Type ?u.765
m' : α → Type ?u.770
n' : α → Type ?u.775
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : LT α
b : n → α
e : m ≃ n
h : BlockTriangular (↑(reindex e e) M) b
⊢ BlockTriangular M (b ∘ ↑e)

case refine'_2
α : Type u_3
β : Type ?u.756
m : Type u_1
n : Type u_2
o : Type ?u.765
m' : α → Type ?u.770
n' : α → Type ?u.775
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : LT α
b : n → α
e : m ≃ n
h : BlockTriangular M (b ∘ ↑e)
⊢ BlockTriangular (↑(reindex e e) M) b
α : Type u_3
β : Type ?u.756
m : Type u_1
n : Type u_2
o : Type ?u.765
m' : α → Type ?u.770
n' : α → Type ?u.775
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : LT α
b : n → α
e : m ≃ n
⊢ BlockTriangular (↑(reindex e e) M) b ↔ BlockTriangular M (b ∘ ↑e)
refine' ⟨fun h => _, fun h => _⟩
case h.e'_6
α : Type u_3
β : Type ?u.756
m : Type u_1
n : Type u_2
o : Type ?u.765
m' : α → Type ?u.770
n' : α → Type ?u.775
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : LT α
b : n → α
e : m ≃ n
h : BlockTriangular (↑(reindex e e) M) b
⊢ M = submatrix (↑(reindex e e) M) ↑e ↑e
case refine'_1
α : Type u_3
β : Type ?u.756
m : Type u_1
n : Type u_2
o : Type ?u.765
m' : α → Type ?u.770
n' : α → Type ?u.775
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : LT α
b : n → α
e : m ≃ n
h : BlockTriangular (↑(reindex e e) M) b
⊢ BlockTriangular M (b ∘ ↑e)
convert h.submatrix
no goals
case h.e'_6
α : Type u_3
β : Type ?u.756
m : Type u_1
n : Type u_2
o : Type ?u.765
m' : α → Type ?u.770
n' : α → Type ?u.775
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : LT α
b : n → α
e : m ≃ n
h : BlockTriangular (↑(reindex e e) M) b
⊢ M = submatrix (↑(reindex e e) M) ↑e ↑e
simp only [reindex_apply, submatrix_submatrix, submatrix_id_id, Equiv.symm_comp_self]
case h.e'_7
α : Type u_3
β : Type ?u.756
m : Type u_1
n : Type u_2
o : Type ?u.765
m' : α → Type ?u.770
n' : α → Type ?u.775
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : LT α
b : n → α
e : m ≃ n
h : BlockTriangular M (b ∘ ↑e)
⊢ b = (b ∘ ↑e) ∘ fun i => ↑e.symm i
case refine'_2
α : Type u_3
β : Type ?u.756
m : Type u_1
n : Type u_2
o : Type ?u.765
m' : α → Type ?u.770
n' : α → Type ?u.775
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : LT α
b : n → α
e : m ≃ n
h : BlockTriangular M (b ∘ ↑e)
⊢ BlockTriangular (↑(reindex e e) M) b
convert h.submatrix
no goals
case h.e'_7
α : Type u_3
β : Type ?u.756
m : Type u_1
n : Type u_2
o : Type ?u.765
m' : α → Type ?u.770
n' : α → Type ?u.775
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : LT α
b : n → α
e : m ≃ n
h : BlockTriangular M (b ∘ ↑e)
⊢ b = (b ∘ ↑e) ∘ fun i => ↑e.symm i
simp only [comp.assoc b e e.symm, Equiv.self_comp_symm, comp.right_id]