Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff

Goal state before:
pp: case inl.inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i j : ↥s
⊢ A.submatrix (⇑e) (⇑e) (Sum.inl i) (Sum.inl j) =
    fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1 (Sum.inl i) (Sum.inl j)

pp: case inl.inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i : ↥s
j : { a // a ∉ s }
⊢ A.submatrix (⇑e) (⇑e) (Sum.inl i) (Sum.inr j) =
    fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1 (Sum.inl i) (Sum.inr j)

pp: case inr.inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i : { a // a ∉ s }
j : ↥s
⊢ A.submatrix (⇑e) (⇑e) (Sum.inr i) (Sum.inl j) =
    fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1 (Sum.inr i) (Sum.inl j)

pp: case inr.inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i j : { a // a ∉ s }
⊢ A.submatrix (⇑e) (⇑e) (Sum.inr i) (Sum.inr j) =
    fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1 (Sum.inr i) (Sum.inr j)

Tactic:
<;>

Goal state after:
case inl.inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i j : ↥s
⊢ A.submatrix (⇑e) (⇑e) (Sum.inl i) (Sum.inl j) =
    fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1 (Sum.inl i) (Sum.inl j)

case inl.inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i : ↥s
j : { a // a ∉ s }
⊢ A.submatrix (⇑e) (⇑e) (Sum.inl i) (Sum.inr j) =
    fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1 (Sum.inl i) (Sum.inr j)

case inr.inl
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i : { a // a ∉ s }
j : ↥s
⊢ A.submatrix (⇑e) (⇑e) (Sum.inr i) (Sum.inl j) =
    fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1 (Sum.inr i) (Sum.inl j)

case inr.inr
R : Type u
inst✝² : CommRing R
n : Type v
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : Matrix n n R
s : Finset n
e : ↥s ⊕ { a // a ∉ s } ≃ n := Equiv.sumCompl fun x ↦ x ∈ s
A : Matrix n n R := of (s.piecewise M 1)
i j : { a // a ∉ s }
⊢ A.submatrix (⇑e) (⇑e) (Sum.inr i) (Sum.inr j) =
    fromBlocks (M.submatrix Subtype.val Subtype.val) (M.submatrix Subtype.val Subtype.val) 0 1 (Sum.inr i) (Sum.inr j)