case nil
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.68668
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
M✝ : Matrix n n R
N✝ : Matrix p p R
M : Matrix n n R
N : Matrix p p R
⊢ fromBlocks M 0 0 N ⬝ List.prod (List.map (toMatrix ∘ sumInl p) []) =
    fromBlocks (M ⬝ List.prod (List.map toMatrix [])) 0 0 N

case cons
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.68668
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
M✝ : Matrix n n R
N✝ : Matrix p p R
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH :
  ∀ (M : Matrix n n R) (N : Matrix p p R),
    fromBlocks M 0 0 N ⬝ List.prod (List.map (toMatrix ∘ sumInl p) L) =
      fromBlocks (M ⬝ List.prod (List.map toMatrix L)) 0 0 N
M : Matrix n n R
N : Matrix p p R
⊢ fromBlocks M 0 0 N ⬝ List.prod (List.map (toMatrix ∘ sumInl p) (t :: L)) =
    fromBlocks (M ⬝ List.prod (List.map toMatrix (t :: L))) 0 0 N
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.68668
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
M : Matrix n n R
L : List (TransvectionStruct n R)
N : Matrix p p R
⊢ fromBlocks M 0 0 N ⬝ List.prod (List.map (toMatrix ∘ sumInl p) L) =
    fromBlocks (M ⬝ List.prod (List.map toMatrix L)) 0 0 N
induction' L with t L IH generalizing M N
no goals
case nil
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.68668
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
M✝ : Matrix n n R
N✝ : Matrix p p R
M : Matrix n n R
N : Matrix p p R
⊢ fromBlocks M 0 0 N ⬝ List.prod (List.map (toMatrix ∘ sumInl p) []) =
    fromBlocks (M ⬝ List.prod (List.map toMatrix [])) 0 0 N
simp
no goals
case cons
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.68668
inst✝⁵ : Field 𝕜
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : CommRing R
i j : n
inst✝¹ : Fintype n
inst✝ : Fintype p
M✝ : Matrix n n R
N✝ : Matrix p p R
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH :
  ∀ (M : Matrix n n R) (N : Matrix p p R),
    fromBlocks M 0 0 N ⬝ List.prod (List.map (toMatrix ∘ sumInl p) L) =
      fromBlocks (M ⬝ List.prod (List.map toMatrix L)) 0 0 N
M : Matrix n n R
N : Matrix p p R
⊢ fromBlocks M 0 0 N ⬝ List.prod (List.map (toMatrix ∘ sumInl p) (t :: L)) =
    fromBlocks (M ⬝ List.prod (List.map toMatrix (t :: L))) 0 0 N
simp [IH, toMatrix_sumInl, fromBlocks_multiply]