[STATEMENT]
lemma set_nn_integral_cong:
  assumes "M = M'" "A = B" "\<And>x. x \<in> space M \<inter> A \<Longrightarrow> f x = g x"
  shows   "set_nn_integral M A f = set_nn_integral M' B g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_nn_integral M A f = set_nn_integral M' B g
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
M = M'
A = B
?x \<in> space M \<inter> A \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. set_nn_integral M A f = set_nn_integral M' B g
[PROOF STEP]
unfolding assms(1,2)
[PROOF STATE]
proof (prove)
using this:
M' = M'
B = B
?x \<in> space M' \<inter> B \<Longrightarrow> f ?x = g ?x

goal (1 subgoal):
 1. set_nn_integral M' B f = set_nn_integral M' B g
[PROOF STEP]
by (intro nn_integral_cong) (auto simp: indicator_def)