Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: case e_f.e_a.e_f.inl.inl
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
val✝¹ val✝ : { a // p a }
hy : σ (Sum.inl val✝¹) = Sum.inl val✝
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (Sum.inl val✝) (Sum.inl val✝¹) =
    fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
      (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (Sum.inl val✝) (Sum.inl val✝¹)

pp: case e_f.e_a.e_f.inl.inr
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
val✝¹ : { a // p a }
val✝ : { a // ¬p a }
hy : σ (Sum.inl val✝¹) = Sum.inr val✝
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (Sum.inr val✝) (Sum.inl val✝¹) =
    fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
      (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (Sum.inr val✝) (Sum.inl val✝¹)

pp: case e_f.e_a.e_f.inr.inl
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
val✝¹ : { a // ¬p a }
val✝ : { a // p a }
hy : σ (Sum.inr val✝¹) = Sum.inl val✝
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (Sum.inl val✝) (Sum.inr val✝¹) =
    fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
      (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (Sum.inl val✝) (Sum.inr val✝¹)

pp: case e_f.e_a.e_f.inr.inr
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
val✝¹ val✝ : { a // ¬p a }
hy : σ (Sum.inr val✝¹) = Sum.inr val✝
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (Sum.inr val✝) (Sum.inr val✝¹) =
    fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
      (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (Sum.inr val✝) (Sum.inr val✝¹)

Tactic:
<;>

Goal state after:
case e_f.e_a.e_f.inl.inl
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
val✝¹ val✝ : { a // p a }
hy : σ (Sum.inl val✝¹) = Sum.inl val✝
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (Sum.inl val✝) (Sum.inl val✝¹) =
    fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
      (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (Sum.inl val✝) (Sum.inl val✝¹)

case e_f.e_a.e_f.inl.inr
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
val✝¹ : { a // p a }
val✝ : { a // ¬p a }
hy : σ (Sum.inl val✝¹) = Sum.inr val✝
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (Sum.inr val✝) (Sum.inl val✝¹) =
    fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
      (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (Sum.inr val✝) (Sum.inl val✝¹)

case e_f.e_a.e_f.inr.inl
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
val✝¹ : { a // ¬p a }
val✝ : { a // p a }
hy : σ (Sum.inr val✝¹) = Sum.inl val✝
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (Sum.inl val✝) (Sum.inr val✝¹) =
    fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
      (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (Sum.inl val✝) (Sum.inr val✝¹)

case e_f.e_a.e_f.inr.inr
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
val✝¹ val✝ : { a // ¬p a }
hy : σ (Sum.inr val✝¹) = Sum.inr val✝
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (Sum.inr val✝) (Sum.inr val✝¹) =
    fromBlocks (M.toBlock p p) (M.toBlock p fun j ↦ ¬p j) (M.toBlock (fun j ↦ ¬p j) p)
      (M.toBlock (fun j ↦ ¬p j) fun j ↦ ¬p j) (Sum.inr val✝) (Sum.inr val✝¹)