[STATEMENT]
lemma sum_reorder_triple: "(\<Sum> l \<in> A . (\<Sum> i \<in> B . (\<Sum> j \<in> C . g l i j))) = 
  (\<Sum> i \<in> B . (\<Sum> j \<in> C . (\<Sum> l \<in> A . g l i j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
have "(\<Sum> l \<in> A . (\<Sum> i \<in> B . (\<Sum> j \<in> C . g l i j))) = (\<Sum>i \<in> B . (\<Sum> l \<in> A  . (\<Sum> j \<in> C . g l i j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>l\<in>A. sum (g l i) C)
[PROOF STEP]
using sum.swap[of "(\<lambda> l i . (\<Sum> j \<in> C . g l i j))" "B" "A"]
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>A. \<Sum>ia\<in>B. sum (g i ia) C) = (\<Sum>j\<in>B. \<Sum>i\<in>A. sum (g i j) C)

goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>l\<in>A. sum (g l i) C)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>l\<in>A. sum (g l i) C)

goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>l\<in>A. sum (g l i) C)

goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
have "...  = (\<Sum>i \<in> B . (\<Sum> j \<in> C . (\<Sum>l \<in> A . g l i j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>B. \<Sum>l\<in>A. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
using sum.swap
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<in>?A. sum (?g i) ?B) = (\<Sum>j\<in>?B. \<Sum>i\<in>?A. ?g i j)

goal (1 subgoal):
 1. (\<Sum>i\<in>B. \<Sum>l\<in>A. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>B. \<Sum>l\<in>A. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)

goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)

goal (1 subgoal):
 1. (\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>l\<in>A. \<Sum>i\<in>B. sum (g l i) C) = (\<Sum>i\<in>B. \<Sum>j\<in>C. \<Sum>l\<in>A. g l i j)

goal:
No subgoals!
[PROOF STEP]
qed