[STATEMENT]
lemma append_rows_mult_left_id:
  assumes A: "(A::'a::comm_semiring_1 mat) \<in> carrier_mat 1 n"
  and B: "B \<in> carrier_mat (m-1) n"
  and C: "C = four_block_mat (1\<^sub>m 1) (0\<^sub>m 1 (m - 1)) (0\<^sub>m (m - 1) 1) D"
  and D: "D \<in> carrier_mat (m-1) (m-1)"
shows "C * (A @\<^sub>r B) = A @\<^sub>r (D * B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
have "transpose_mat (C * (A @\<^sub>r B)) = (A @\<^sub>r B)\<^sup>T * C\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C * (A @\<^sub>r B))\<^sup>T = (A @\<^sub>r B)\<^sup>T * C\<^sup>T
[PROOF STEP]
by (metis (no_types, lifting) B C D Matrix.transpose_mult append_rows_def A carrier_matD
        carrier_mat_triv index_mat_four_block(2,3) index_zero_mat(2) one_carrier_mat)
[PROOF STATE]
proof (state)
this:
(C * (A @\<^sub>r B))\<^sup>T = (A @\<^sub>r B)\<^sup>T * C\<^sup>T

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(C * (A @\<^sub>r B))\<^sup>T = (A @\<^sub>r B)\<^sup>T * C\<^sup>T

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
have "... = (A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A @\<^sub>r B)\<^sup>T * C\<^sup>T = (A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T
[PROOF STEP]
using transpose_mat_append_rows[OF A B]
[PROOF STATE]
proof (prove)
using this:
(A @\<^sub>r B)\<^sup>T = A\<^sup>T @\<^sub>c B\<^sup>T

goal (1 subgoal):
 1. (A @\<^sub>r B)\<^sup>T * C\<^sup>T = (A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(A @\<^sub>r B)\<^sup>T * C\<^sup>T = (A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(A @\<^sub>r B)\<^sup>T * C\<^sup>T = (A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
have "... = A\<^sup>T @\<^sub>c (B\<^sup>T * D\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T = A\<^sup>T @\<^sub>c B\<^sup>T * D\<^sup>T
[PROOF STEP]
by (rule append_cols_mult_right_id, insert A B C D, auto)
[PROOF STATE]
proof (state)
this:
(A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T = A\<^sup>T @\<^sub>c B\<^sup>T * D\<^sup>T

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(A\<^sup>T @\<^sub>c B\<^sup>T) * C\<^sup>T = A\<^sup>T @\<^sub>c B\<^sup>T * D\<^sup>T

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
have "transpose_mat ... = A @\<^sub>r (D * B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A\<^sup>T @\<^sub>c B\<^sup>T * D\<^sup>T)\<^sup>T = A @\<^sub>r D * B
[PROOF STEP]
by (smt B D Matrix.transpose_mult Matrix.transpose_transpose append_cols_def append_rows_def A
        carrier_matD(2) carrier_mat_triv index_mult_mat(3) index_transpose_mat(3)
        transpose_four_block_mat zero_carrier_mat zero_transpose_mat)
[PROOF STATE]
proof (state)
this:
(A\<^sup>T @\<^sub>c B\<^sup>T * D\<^sup>T)\<^sup>T = A @\<^sub>r D * B

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(C * (A @\<^sub>r B))\<^sup>T\<^sup>T = A @\<^sub>r D * B
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(C * (A @\<^sub>r B))\<^sup>T\<^sup>T = A @\<^sub>r D * B

goal (1 subgoal):
 1. C * (A @\<^sub>r B) = A @\<^sub>r D * B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C * (A @\<^sub>r B) = A @\<^sub>r D * B

goal:
No subgoals!
[PROOF STEP]
qed