case intro
l : Type u_4
m : Type u_3
n : Type u_1
o : Type u_2
m' : o → Type ?u.1174423
n' : o → Type ?u.1174428
R : Type ?u.1174431
S : Type ?u.1174434
α : Type v
β : Type w
γ : Type ?u.1174441
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
⊢ M ⬝ submatrix 1 (↑e₁) e₂ = submatrix M id (↑e₁.symm ∘ e₂)
l : Type u_4
m : Type u_3
n : Type u_1
o : Type u_2
m' : o → Type ?u.1174423
n' : o → Type ?u.1174428
R : Type ?u.1174431
S : Type ?u.1174434
α : Type v
β : Type w
γ : Type ?u.1174441
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
⊢ M ⬝ submatrix 1 (↑e₁) e₂ = submatrix M id (↑e₁.symm ∘ e₂)
cases nonempty_fintype o
case intro
l : Type u_4
m : Type u_3
n : Type u_1
o : Type u_2
m' : o → Type ?u.1174423
n' : o → Type ?u.1174428
R : Type ?u.1174431
S : Type ?u.1174434
α : Type v
β : Type w
γ : Type ?u.1174441
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
A : Matrix m o α := submatrix M id ↑e₁.symm
⊢ M ⬝ submatrix 1 (↑e₁) e₂ = submatrix M id (↑e₁.symm ∘ e₂)
case intro
l : Type u_4
m : Type u_3
n : Type u_1
o : Type u_2
m' : o → Type ?u.1174423
n' : o → Type ?u.1174428
R : Type ?u.1174431
S : Type ?u.1174434
α : Type v
β : Type w
γ : Type ?u.1174441
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
⊢ M ⬝ submatrix 1 (↑e₁) e₂ = submatrix M id (↑e₁.symm ∘ e₂)
let A := M.submatrix id e₁.symm
case intro
l : Type u_4
m : Type u_3
n : Type u_1
o : Type u_2
m' : o → Type ?u.1174423
n' : o → Type ?u.1174428
R : Type ?u.1174431
S : Type ?u.1174434
α : Type v
β : Type w
γ : Type ?u.1174441
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
A : Matrix m o α := submatrix M id ↑e₁.symm
this : M = submatrix A id ↑e₁
⊢ M ⬝ submatrix 1 (↑e₁) e₂ = submatrix M id (↑e₁.symm ∘ e₂)
case intro
l : Type u_4
m : Type u_3
n : Type u_1
o : Type u_2
m' : o → Type ?u.1174423
n' : o → Type ?u.1174428
R : Type ?u.1174431
S : Type ?u.1174434
α : Type v
β : Type w
γ : Type ?u.1174441
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
A : Matrix m o α := submatrix M id ↑e₁.symm
⊢ M ⬝ submatrix 1 (↑e₁) e₂ = submatrix M id (↑e₁.symm ∘ e₂)
have : M = A.submatrix id e₁ := by
  simp only [submatrix_submatrix, Function.comp.right_id, submatrix_id_id, Equiv.symm_comp_self]
case intro
l : Type u_4
m : Type u_3
n : Type u_1
o : Type u_2
m' : o → Type ?u.1174423
n' : o → Type ?u.1174428
R : Type ?u.1174431
S : Type ?u.1174434
α : Type v
β : Type w
γ : Type ?u.1174441
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
A : Matrix m o α := submatrix M id ↑e₁.symm
this : M = submatrix A id ↑e₁
⊢ submatrix (A ⬝ 1) id e₂ = submatrix (submatrix A id ↑e₁) id (↑e₁.symm ∘ e₂)
case intro
l : Type u_4
m : Type u_3
n : Type u_1
o : Type u_2
m' : o → Type ?u.1174423
n' : o → Type ?u.1174428
R : Type ?u.1174431
S : Type ?u.1174434
α : Type v
β : Type w
γ : Type ?u.1174441
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
A : Matrix m o α := submatrix M id ↑e₁.symm
this : M = submatrix A id ↑e₁
⊢ M ⬝ submatrix 1 (↑e₁) e₂ = submatrix M id (↑e₁.symm ∘ e₂)
rw [this, submatrix_mul_equiv]
no goals
case intro
l : Type u_4
m : Type u_3
n : Type u_1
o : Type u_2
m' : o → Type ?u.1174423
n' : o → Type ?u.1174428
R : Type ?u.1174431
S : Type ?u.1174434
α : Type v
β : Type w
γ : Type ?u.1174441
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
A : Matrix m o α := submatrix M id ↑e₁.symm
this : M = submatrix A id ↑e₁
⊢ submatrix (A ⬝ 1) id e₂ = submatrix (submatrix A id ↑e₁) id (↑e₁.symm ∘ e₂)
simp only [Matrix.mul_one, submatrix_submatrix, Function.comp.right_id, submatrix_id_id,
  Equiv.symm_comp_self]
no goals
l : Type u_4
m : Type u_3
n : Type u_1
o : Type u_2
m' : o → Type ?u.1174423
n' : o → Type ?u.1174428
R : Type ?u.1174431
S : Type ?u.1174434
α : Type v
β : Type w
γ : Type ?u.1174441
inst✝³ : Fintype n
inst✝² : Finite o
inst✝¹ : NonAssocSemiring α
inst✝ : DecidableEq o
e₁ : n ≃ o
e₂ : l → o
M : Matrix m n α
val✝ : Fintype o
A : Matrix m o α := submatrix M id ↑e₁.symm
⊢ M = submatrix A id ↑e₁
simp only [submatrix_submatrix, Function.comp.right_id, submatrix_id_id, Equiv.symm_comp_self]