case nil
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.60874
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
⊢ List.prod (List.map (toMatrix ∘ sumInl p) []) ⬝ fromBlocks M 0 0 N =
    fromBlocks (List.prod (List.map toMatrix []) ⬝ M) 0 0 N

case cons
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.60874
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 :
  List.prod (List.map (toMatrix ∘ sumInl p) L) ⬝ fromBlocks M 0 0 N =
    fromBlocks (List.prod (List.map toMatrix L) ⬝ M) 0 0 N
⊢ List.prod (List.map (toMatrix ∘ sumInl p) (t :: L)) ⬝ fromBlocks M 0 0 N =
    fromBlocks (List.prod (List.map toMatrix (t :: L)) ⬝ M) 0 0 N
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.60874
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
⊢ List.prod (List.map (toMatrix ∘ sumInl p) L) ⬝ fromBlocks M 0 0 N =
    fromBlocks (List.prod (List.map toMatrix L) ⬝ M) 0 0 N
induction' L with t L IH
no goals
case nil
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.60874
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
⊢ List.prod (List.map (toMatrix ∘ sumInl p) []) ⬝ fromBlocks M 0 0 N =
    fromBlocks (List.prod (List.map toMatrix []) ⬝ M) 0 0 N
simp
no goals
case cons
n : Type u_1
p : Type u_2
R : Type u₂
𝕜 : Type ?u.60874
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 :
  List.prod (List.map (toMatrix ∘ sumInl p) L) ⬝ fromBlocks M 0 0 N =
    fromBlocks (List.prod (List.map toMatrix L) ⬝ M) 0 0 N
⊢ List.prod (List.map (toMatrix ∘ sumInl p) (t :: L)) ⬝ fromBlocks M 0 0 N =
    fromBlocks (List.prod (List.map toMatrix (t :: L)) ⬝ M) 0 0 N
simp [Matrix.mul_assoc, IH, toMatrix_sumInl, fromBlocks_multiply]