Module: Mathlib.Data.Matrix.ColumnRowPartitioned

Goal state before:
pp: case inl.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₁
val✝ : n₁
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val✝¹) (Sum.inl val✝)

pp: case inl.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₁
val✝ : n₂
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val✝¹) (Sum.inr val✝)

pp: case inr.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₂
val✝ : n₁
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val✝¹) (Sum.inl val✝)

pp: case inr.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₂
val✝ : n₂
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case inl.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₁
val✝ : n₁
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val✝¹) (Sum.inl val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val✝¹) (Sum.inl val✝)

case inl.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₁
val✝ : n₂
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inl val✝¹) (Sum.inr val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inl val✝¹) (Sum.inr val✝)

case inr.inl
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₂
val✝ : n₁
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inr val✝¹) (Sum.inl val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val✝¹) (Sum.inl val✝)

case inr.inr
R : Type u_1
m₁ : Type u_3
m₂ : Type u_4
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A₁ : Matrix m₁ n R
A₂ : Matrix m₂ n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
val✝¹ : m₂
val✝ : n₂
⊢ (A₁.fromRows A₂ * B₁.fromCols B₂) (Sum.inr val✝¹) (Sum.inr val✝) =
    fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂) (Sum.inr val✝¹) (Sum.inr val✝)