[STATEMENT]
lemma sheaf_spec_on_open_is_comm_ring:
  assumes "is_zariski_open U"
  shows "comm_ring (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comm_ring (\<O> U) (add_sheaf_spec U) (mult_sheaf_spec U) (zero_sheaf_spec U) (one_sheaf_spec U)
[PROOF STEP]
proof unfold_locales
[PROOF STATE]
proof (state)
goal (15 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U a b \<in> \<O> U
 2. zero_sheaf_spec U \<in> \<O> U
 3. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U (add_sheaf_spec U a b) c = add_sheaf_spec U a (add_sheaf_spec U b c)
 4. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U (zero_sheaf_spec U) a = a
 5. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U a (zero_sheaf_spec U) = a
 6. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
 7. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U x y = add_sheaf_spec U y x
 8. \<And>a b. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a b \<in> \<O> U
 9. one_sheaf_spec U \<in> \<O> U
 10. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U a b) c = mult_sheaf_spec U a (mult_sheaf_spec U b c)
A total of 15 subgoals...
[PROOF STEP]
show add_\<O>:"add_sheaf_spec U a b \<in> \<O> U"
    and "mult_sheaf_spec U a b \<in> \<O> U"
    if "a \<in> \<O> U" "b \<in> \<O> U" for a b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U a b \<in> \<O> U &&& mult_sheaf_spec U a b \<in> \<O> U
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U a b \<in> \<O> U
[PROOF STEP]
by (simp add: add_sheaf_spec_in_sheaf_spec assms that(1,2) zariski_open_is_subset)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U a b \<in> \<O> U
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U a b \<in> \<O> U
[PROOF STEP]
by (simp add: assms mult_sheaf_spec_in_sheaf_spec that(1,2) zariski_open_is_subset)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a3 \<in> \<O> U; ?b3 \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U ?a3 ?b3 \<in> \<O> U
\<lbrakk>?a3 \<in> \<O> U; ?b3 \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U ?a3 ?b3 \<in> \<O> U

goal (13 subgoals):
 1. zero_sheaf_spec U \<in> \<O> U
 2. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U (add_sheaf_spec U a b) c = add_sheaf_spec U a (add_sheaf_spec U b c)
 3. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U (zero_sheaf_spec U) a = a
 4. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U a (zero_sheaf_spec U) = a
 5. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
 6. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U x y = add_sheaf_spec U y x
 7. one_sheaf_spec U \<in> \<O> U
 8. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U a b) c = mult_sheaf_spec U a (mult_sheaf_spec U b c)
 9. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) a = a
 10. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U a (one_sheaf_spec U) = a
A total of 13 subgoals...
[PROOF STEP]
show "zero_sheaf_spec U \<in> \<O> U" "one_sheaf_spec U \<in> \<O> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_sheaf_spec U \<in> \<O> U &&& one_sheaf_spec U \<in> \<O> U
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_sheaf_spec U \<in> \<O> U
[PROOF STEP]
by (simp add: assms zero_sheaf_spec_in_sheaf_spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_sheaf_spec U \<in> \<O> U
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_sheaf_spec U \<in> \<O> U
[PROOF STEP]
by (simp add: assms one_sheaf_spec_in_sheaf_spec)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
zero_sheaf_spec U \<in> \<O> U
one_sheaf_spec U \<in> \<O> U

goal (11 subgoals):
 1. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U (add_sheaf_spec U a b) c = add_sheaf_spec U a (add_sheaf_spec U b c)
 2. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U (zero_sheaf_spec U) a = a
 3. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U a (zero_sheaf_spec U) = a
 4. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
 5. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U x y = add_sheaf_spec U y x
 6. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U a b) c = mult_sheaf_spec U a (mult_sheaf_spec U b c)
 7. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) a = a
 8. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U a (one_sheaf_spec U) = a
 9. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c)
 10. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (add_sheaf_spec U b c) a = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)
A total of 11 subgoals...
[PROOF STEP]
have imp_qr:"quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>" if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by (meson assms comm_ring.spectrum_imp_cxt_quotient_ring in_mono local.comm_ring_axioms
          zariski_open_is_subset)
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>?\<pp>3) R (+) (\<cdot>) \<zero> \<one>

goal (11 subgoals):
 1. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U (add_sheaf_spec U a b) c = add_sheaf_spec U a (add_sheaf_spec U b c)
 2. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U (zero_sheaf_spec U) a = a
 3. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U a (zero_sheaf_spec U) = a
 4. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
 5. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U x y = add_sheaf_spec U y x
 6. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U a b) c = mult_sheaf_spec U a (mult_sheaf_spec U b c)
 7. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) a = a
 8. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U a (one_sheaf_spec U) = a
 9. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c)
 10. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (add_sheaf_spec U b c) a = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)
A total of 11 subgoals...
[PROOF STEP]
have qr_valid_frac:"quotient_ring.valid_frac (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>)"
      if "s \<in> \<O> U" "\<pp> \<in> U" for s \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quotient_ring.valid_frac (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>)
[PROOF STEP]
using assms comm_ring.zariski_open_is_subset quotient_ring.carrier_quotient_ring_iff
      imp_qr local.comm_ring_axioms pr_ideal.carrier_local_ring_at_def sec_has_right_codom
      spectrum_imp_pr that(1) that(2)
[PROOF STATE]
proof (prove)
using this:
is_zariski_open U
\<lbrakk>comm_ring ?R ?addition ?multiplication ?zero ?unit; comm_ring.is_zariski_open ?R ?addition ?multiplication ?zero ?unit ?U\<rbrakk> \<Longrightarrow> ?U \<subseteq> comm_ring.spectrum ?R ?addition ?multiplication ?zero ?unit
Comm_Ring.quotient_ring ?S ?R ?addition ?multiplication ?zero ?unit \<Longrightarrow> (?X \<in> ?S \<^sup>\<inverse> ?R \<^bsub>?addition ?multiplication ?zero\<^esub>) = quotient_ring.valid_frac ?S ?R ?addition ?multiplication ?zero ?X
?\<pp>3 \<in> U \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>?\<pp>3) R (+) (\<cdot>) \<zero> \<one>
comm_ring R (+) (\<cdot>) \<zero> \<one>
pr_ideal ?R ?I ?addition ?multiplication ?zero ?unit \<Longrightarrow> ?R \<^bsub>?I ?addition ?multiplication ?zero\<^esub> \<equiv> ?R\<setminus>?I \<^sup>\<inverse> ?R \<^bsub>?addition ?multiplication ?zero\<^esub>
\<lbrakk>?s \<in> \<O> ?U; ?\<pp> \<in> ?U\<rbrakk> \<Longrightarrow> ?s ?\<pp> \<in> R \<^bsub>?\<pp> (+) (\<cdot>) \<zero>\<^esub>
?\<pp> \<in> Spec \<Longrightarrow> pr_ideal R ?\<pp> (+) (\<cdot>) \<zero> \<one>
s \<in> \<O> U
\<pp> \<in> U

goal (1 subgoal):
 1. quotient_ring.valid_frac (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<lbrakk>?s3 \<in> \<O> U; ?\<pp>3 \<in> U\<rbrakk> \<Longrightarrow> quotient_ring.valid_frac (R\<setminus>?\<pp>3) R (+) (\<cdot>) \<zero> (?s3 ?\<pp>3)

goal (11 subgoals):
 1. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U (add_sheaf_spec U a b) c = add_sheaf_spec U a (add_sheaf_spec U b c)
 2. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U (zero_sheaf_spec U) a = a
 3. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U a (zero_sheaf_spec U) = a
 4. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
 5. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U x y = add_sheaf_spec U y x
 6. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U a b) c = mult_sheaf_spec U a (mult_sheaf_spec U b c)
 7. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) a = a
 8. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U a (one_sheaf_spec U) = a
 9. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c)
 10. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (add_sheaf_spec U b c) a = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)
A total of 11 subgoals...
[PROOF STEP]
show add_zero:"add_sheaf_spec U (zero_sheaf_spec U) a = a" if "a \<in> \<O> U" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U (zero_sheaf_spec U) a = a
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_sheaf_spec U (zero_sheaf_spec U) a = a
[PROOF STEP]
have "add_sheaf_spec U (zero_sheaf_spec U) a \<pp> = a \<pp>" if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U (zero_sheaf_spec U) a \<pp> = a \<pp>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_sheaf_spec U (zero_sheaf_spec U) a \<pp> = a \<pp>
[PROOF STEP]
interpret cq:quotient_ring "R\<setminus>\<pp>" R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using imp_qr that
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>?\<pp>3) R (+) (\<cdot>) \<zero> \<one>
\<pp> \<in> U

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. add_sheaf_spec U (zero_sheaf_spec U) a \<pp> = a \<pp>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U (zero_sheaf_spec U) a \<pp> = a \<pp>
[PROOF STEP]
unfolding add_sheaf_spec_def zero_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> ((\<lambda>\<pp>\<in>U. quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<pp>) (a \<pp>)) \<pp> = a \<pp>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> ((\<lambda>\<pp>\<in>U. quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<pp>) (a \<pp>)) \<pp> = a \<pp>
[PROOF STEP]
by (simp add: \<open>a \<in> \<O> U\<close> qr_valid_frac)
[PROOF STATE]
proof (state)
this:
add_sheaf_spec U (zero_sheaf_spec U) a \<pp> = a \<pp>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> add_sheaf_spec U (zero_sheaf_spec U) a ?\<pp>3 = a ?\<pp>3

goal (1 subgoal):
 1. add_sheaf_spec U (zero_sheaf_spec U) a = a
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?\<pp>3 \<in> U \<Longrightarrow> add_sheaf_spec U (zero_sheaf_spec U) a ?\<pp>3 = a ?\<pp>3
[PROOF STEP]
show "add_sheaf_spec U (zero_sheaf_spec U) a = a"
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> add_sheaf_spec U (zero_sheaf_spec U) a ?\<pp>3 = a ?\<pp>3

goal (1 subgoal):
 1. add_sheaf_spec U (zero_sheaf_spec U) a = a
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> add_sheaf_spec U (zero_sheaf_spec U) a ?\<pp>3 = a ?\<pp>3
a \<in> \<O> U

goal (1 subgoal):
 1. add_sheaf_spec U (zero_sheaf_spec U) a = a
[PROOF STEP]
by(auto intro: extensionalityI[where A=U])
[PROOF STATE]
proof (state)
this:
add_sheaf_spec U (zero_sheaf_spec U) a = a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?a3 \<in> \<O> U \<Longrightarrow> add_sheaf_spec U (zero_sheaf_spec U) ?a3 = ?a3

goal (10 subgoals):
 1. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U (add_sheaf_spec U a b) c = add_sheaf_spec U a (add_sheaf_spec U b c)
 2. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U a (zero_sheaf_spec U) = a
 3. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
 4. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U x y = add_sheaf_spec U y x
 5. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U a b) c = mult_sheaf_spec U a (mult_sheaf_spec U b c)
 6. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) a = a
 7. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U a (one_sheaf_spec U) = a
 8. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c)
 9. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (add_sheaf_spec U b c) a = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)
 10. \<And>a b. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a b = mult_sheaf_spec U b a
[PROOF STEP]
show add_assoc:"add_sheaf_spec U (add_sheaf_spec U a b) c
      = add_sheaf_spec U a (add_sheaf_spec U b c)"
    if "a \<in> \<O> U" and "b \<in> \<O> U" and "c \<in> \<O> U"
    for a b c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U (add_sheaf_spec U a b) c = add_sheaf_spec U a (add_sheaf_spec U b c)
[PROOF STEP]
proof (rule extensionalityI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. add_sheaf_spec U (add_sheaf_spec U a b) c \<in> extensional ?A
 2. add_sheaf_spec U a (add_sheaf_spec U b c) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> add_sheaf_spec U (add_sheaf_spec U a b) c x = add_sheaf_spec U a (add_sheaf_spec U b c) x
[PROOF STEP]
fix \<pp>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. add_sheaf_spec U (add_sheaf_spec U a b) c \<in> extensional ?A
 2. add_sheaf_spec U a (add_sheaf_spec U b c) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> add_sheaf_spec U (add_sheaf_spec U a b) c x = add_sheaf_spec U a (add_sheaf_spec U b c) x
[PROOF STEP]
assume "\<pp> \<in> U"
[PROOF STATE]
proof (state)
this:
\<pp> \<in> U

goal (3 subgoals):
 1. add_sheaf_spec U (add_sheaf_spec U a b) c \<in> extensional ?A
 2. add_sheaf_spec U a (add_sheaf_spec U b c) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> add_sheaf_spec U (add_sheaf_spec U a b) c x = add_sheaf_spec U a (add_sheaf_spec U b c) x
[PROOF STEP]
interpret cq:quotient_ring "R\<setminus>\<pp>" R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using \<open>\<pp> \<in> U\<close> imp_qr
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
?\<pp>3 \<in> U \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>?\<pp>3) R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. add_sheaf_spec U (add_sheaf_spec U a b) c \<in> extensional ?A
 2. add_sheaf_spec U a (add_sheaf_spec U b c) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> add_sheaf_spec U (add_sheaf_spec U a b) c x = add_sheaf_spec U a (add_sheaf_spec U b c) x
[PROOF STEP]
show "add_sheaf_spec U (add_sheaf_spec U a b) c \<pp> = add_sheaf_spec U a (add_sheaf_spec U b c) \<pp>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U (add_sheaf_spec U a b) c \<pp> = add_sheaf_spec U a (add_sheaf_spec U b c) \<pp>
[PROOF STEP]
unfolding add_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> ((\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (a \<pp>) (b \<pp>)) \<pp>) (c \<pp>)) \<pp> = (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (a \<pp>) ((\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (b \<pp>) (c \<pp>)) \<pp>)) \<pp>
[PROOF STEP]
using \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> ((\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (a \<pp>) (b \<pp>)) \<pp>) (c \<pp>)) \<pp> = (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (a \<pp>) ((\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (b \<pp>) (c \<pp>)) \<pp>)) \<pp>
[PROOF STEP]
by (simp add: cq.additive.associative qr_valid_frac that(1) that(2) that(3))
[PROOF STATE]
proof (state)
this:
add_sheaf_spec U (add_sheaf_spec U a b) c \<pp> = add_sheaf_spec U a (add_sheaf_spec U b c) \<pp>

goal (2 subgoals):
 1. add_sheaf_spec U (add_sheaf_spec U a b) c \<in> extensional U
 2. add_sheaf_spec U a (add_sheaf_spec U b c) \<in> extensional U
[PROOF STEP]
qed (auto simp add:add_sheaf_spec_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a3 \<in> \<O> U; ?b3 \<in> \<O> U; ?c3 \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U (add_sheaf_spec U ?a3 ?b3) ?c3 = add_sheaf_spec U ?a3 (add_sheaf_spec U ?b3 ?c3)

goal (9 subgoals):
 1. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U a (zero_sheaf_spec U) = a
 2. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
 3. \<And>x y. \<lbrakk>x \<in> \<O> U; y \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U x y = add_sheaf_spec U y x
 4. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U a b) c = mult_sheaf_spec U a (mult_sheaf_spec U b c)
 5. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) a = a
 6. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U a (one_sheaf_spec U) = a
 7. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c)
 8. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (add_sheaf_spec U b c) a = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)
 9. \<And>a b. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a b = mult_sheaf_spec U b a
[PROOF STEP]
show add_comm:"add_sheaf_spec U x y = add_sheaf_spec U y x"
    if "x \<in> \<O> U" and "y \<in> \<O> U" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U x y = add_sheaf_spec U y x
[PROOF STEP]
proof (rule extensionalityI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. add_sheaf_spec U x y \<in> extensional ?A
 2. add_sheaf_spec U y x \<in> extensional ?A
 3. \<And>xa. xa \<in> ?A \<Longrightarrow> add_sheaf_spec U x y xa = add_sheaf_spec U y x xa
[PROOF STEP]
fix \<pp>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. add_sheaf_spec U x y \<in> extensional ?A
 2. add_sheaf_spec U y x \<in> extensional ?A
 3. \<And>xa. xa \<in> ?A \<Longrightarrow> add_sheaf_spec U x y xa = add_sheaf_spec U y x xa
[PROOF STEP]
assume "\<pp> \<in> U"
[PROOF STATE]
proof (state)
this:
\<pp> \<in> U

goal (3 subgoals):
 1. add_sheaf_spec U x y \<in> extensional ?A
 2. add_sheaf_spec U y x \<in> extensional ?A
 3. \<And>xa. xa \<in> ?A \<Longrightarrow> add_sheaf_spec U x y xa = add_sheaf_spec U y x xa
[PROOF STEP]
interpret cq:quotient_ring "R\<setminus>\<pp>" R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using \<open>\<pp> \<in> U\<close> imp_qr
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
?\<pp>3 \<in> U \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>?\<pp>3) R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. add_sheaf_spec U x y \<in> extensional ?A
 2. add_sheaf_spec U y x \<in> extensional ?A
 3. \<And>xa. xa \<in> ?A \<Longrightarrow> add_sheaf_spec U x y xa = add_sheaf_spec U y x xa
[PROOF STEP]
show " add_sheaf_spec U x y \<pp> = add_sheaf_spec U y x \<pp>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U x y \<pp> = add_sheaf_spec U y x \<pp>
[PROOF STEP]
unfolding add_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (x \<pp>) (y \<pp>)) \<pp> = (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (y \<pp>) (x \<pp>)) \<pp>
[PROOF STEP]
using \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (x \<pp>) (y \<pp>)) \<pp> = (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (y \<pp>) (x \<pp>)) \<pp>
[PROOF STEP]
by (simp add: cq.additive.commutative qr_valid_frac that(1) that(2))
[PROOF STATE]
proof (state)
this:
add_sheaf_spec U x y \<pp> = add_sheaf_spec U y x \<pp>

goal (2 subgoals):
 1. add_sheaf_spec U x y \<in> extensional U
 2. add_sheaf_spec U y x \<in> extensional U
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x3 \<in> \<O> U; ?y3 \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U ?x3 ?y3 = add_sheaf_spec U ?y3 ?x3

goal (8 subgoals):
 1. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U a (zero_sheaf_spec U) = a
 2. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
 3. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U a b) c = mult_sheaf_spec U a (mult_sheaf_spec U b c)
 4. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) a = a
 5. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U a (one_sheaf_spec U) = a
 6. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c)
 7. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (add_sheaf_spec U b c) a = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)
 8. \<And>a b. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a b = mult_sheaf_spec U b a
[PROOF STEP]
show mult_comm:"mult_sheaf_spec U x y = mult_sheaf_spec U y x"
    if "x \<in> \<O> U" and "y \<in> \<O> U" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U x y = mult_sheaf_spec U y x
[PROOF STEP]
proof (rule extensionalityI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. mult_sheaf_spec U x y \<in> extensional ?A
 2. mult_sheaf_spec U y x \<in> extensional ?A
 3. \<And>xa. xa \<in> ?A \<Longrightarrow> mult_sheaf_spec U x y xa = mult_sheaf_spec U y x xa
[PROOF STEP]
fix \<pp>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. mult_sheaf_spec U x y \<in> extensional ?A
 2. mult_sheaf_spec U y x \<in> extensional ?A
 3. \<And>xa. xa \<in> ?A \<Longrightarrow> mult_sheaf_spec U x y xa = mult_sheaf_spec U y x xa
[PROOF STEP]
assume "\<pp> \<in> U"
[PROOF STATE]
proof (state)
this:
\<pp> \<in> U

goal (3 subgoals):
 1. mult_sheaf_spec U x y \<in> extensional ?A
 2. mult_sheaf_spec U y x \<in> extensional ?A
 3. \<And>xa. xa \<in> ?A \<Longrightarrow> mult_sheaf_spec U x y xa = mult_sheaf_spec U y x xa
[PROOF STEP]
interpret cq:quotient_ring "R\<setminus>\<pp>" R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using \<open>\<pp> \<in> U\<close> imp_qr
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
?\<pp>3 \<in> U \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>?\<pp>3) R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. mult_sheaf_spec U x y \<in> extensional ?A
 2. mult_sheaf_spec U y x \<in> extensional ?A
 3. \<And>xa. xa \<in> ?A \<Longrightarrow> mult_sheaf_spec U x y xa = mult_sheaf_spec U y x xa
[PROOF STEP]
show "mult_sheaf_spec U x y \<pp> = mult_sheaf_spec U y x \<pp>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U x y \<pp> = mult_sheaf_spec U y x \<pp>
[PROOF STEP]
unfolding mult_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (x \<pp>) (y \<pp>)) \<pp> = (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (y \<pp>) (x \<pp>)) \<pp>
[PROOF STEP]
using \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (x \<pp>) (y \<pp>)) \<pp> = (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (y \<pp>) (x \<pp>)) \<pp>
[PROOF STEP]
by (simp add: cq.comm_mult qr_valid_frac that(1) that(2))
[PROOF STATE]
proof (state)
this:
mult_sheaf_spec U x y \<pp> = mult_sheaf_spec U y x \<pp>

goal (2 subgoals):
 1. mult_sheaf_spec U x y \<in> extensional U
 2. mult_sheaf_spec U y x \<in> extensional U
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x3 \<in> \<O> U; ?y3 \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U ?x3 ?y3 = mult_sheaf_spec U ?y3 ?x3

goal (7 subgoals):
 1. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U a (zero_sheaf_spec U) = a
 2. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
 3. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U a b) c = mult_sheaf_spec U a (mult_sheaf_spec U b c)
 4. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) a = a
 5. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U a (one_sheaf_spec U) = a
 6. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c)
 7. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (add_sheaf_spec U b c) a = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)
[PROOF STEP]
show add_zero:"add_sheaf_spec U a (zero_sheaf_spec U) = a"
      if "a \<in> \<O> U" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U a (zero_sheaf_spec U) = a
[PROOF STEP]
using add_zero add_comm that
[PROOF STATE]
proof (prove)
using this:
?a3 \<in> \<O> U \<Longrightarrow> add_sheaf_spec U (zero_sheaf_spec U) ?a3 = ?a3
\<lbrakk>?x3 \<in> \<O> U; ?y3 \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U ?x3 ?y3 = add_sheaf_spec U ?y3 ?x3
a \<in> \<O> U

goal (1 subgoal):
 1. add_sheaf_spec U a (zero_sheaf_spec U) = a
[PROOF STEP]
by (simp add: \<open>zero_sheaf_spec U \<in> \<O> U\<close>)
[PROOF STATE]
proof (state)
this:
?a3 \<in> \<O> U \<Longrightarrow> add_sheaf_spec U ?a3 (zero_sheaf_spec U) = ?a3

goal (6 subgoals):
 1. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
 2. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U a b) c = mult_sheaf_spec U a (mult_sheaf_spec U b c)
 3. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) a = a
 4. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U a (one_sheaf_spec U) = a
 5. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c)
 6. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (add_sheaf_spec U b c) a = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)
[PROOF STEP]
show "mult_sheaf_spec U (mult_sheaf_spec U a b) c = mult_sheaf_spec U a (mult_sheaf_spec U b c)"
    if "a \<in> \<O> U" and "b \<in> \<O> U"
      and "c \<in> \<O> U"
    for a b c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U (mult_sheaf_spec U a b) c = mult_sheaf_spec U a (mult_sheaf_spec U b c)
[PROOF STEP]
proof (rule extensionalityI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. mult_sheaf_spec U (mult_sheaf_spec U a b) c \<in> extensional ?A
 2. mult_sheaf_spec U a (mult_sheaf_spec U b c) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U a b) c x = mult_sheaf_spec U a (mult_sheaf_spec U b c) x
[PROOF STEP]
fix \<pp>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. mult_sheaf_spec U (mult_sheaf_spec U a b) c \<in> extensional ?A
 2. mult_sheaf_spec U a (mult_sheaf_spec U b c) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U a b) c x = mult_sheaf_spec U a (mult_sheaf_spec U b c) x
[PROOF STEP]
assume "\<pp> \<in> U"
[PROOF STATE]
proof (state)
this:
\<pp> \<in> U

goal (3 subgoals):
 1. mult_sheaf_spec U (mult_sheaf_spec U a b) c \<in> extensional ?A
 2. mult_sheaf_spec U a (mult_sheaf_spec U b c) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U a b) c x = mult_sheaf_spec U a (mult_sheaf_spec U b c) x
[PROOF STEP]
interpret cq:quotient_ring "R\<setminus>\<pp>" R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using \<open>\<pp> \<in> U\<close> imp_qr
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
?\<pp>3 \<in> U \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>?\<pp>3) R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. mult_sheaf_spec U (mult_sheaf_spec U a b) c \<in> extensional ?A
 2. mult_sheaf_spec U a (mult_sheaf_spec U b c) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U a b) c x = mult_sheaf_spec U a (mult_sheaf_spec U b c) x
[PROOF STEP]
show "mult_sheaf_spec U (mult_sheaf_spec U a b) c \<pp>
                = mult_sheaf_spec U a (mult_sheaf_spec U b c) \<pp>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U (mult_sheaf_spec U a b) c \<pp> = mult_sheaf_spec U a (mult_sheaf_spec U b c) \<pp>
[PROOF STEP]
unfolding mult_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> ((\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (a \<pp>) (b \<pp>)) \<pp>) (c \<pp>)) \<pp> = (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (a \<pp>) ((\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (b \<pp>) (c \<pp>)) \<pp>)) \<pp>
[PROOF STEP]
using \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> ((\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (a \<pp>) (b \<pp>)) \<pp>) (c \<pp>)) \<pp> = (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (a \<pp>) ((\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (b \<pp>) (c \<pp>)) \<pp>)) \<pp>
[PROOF STEP]
by (simp add: cq.multiplicative.associative qr_valid_frac that(1) that(2) that(3))
[PROOF STATE]
proof (state)
this:
mult_sheaf_spec U (mult_sheaf_spec U a b) c \<pp> = mult_sheaf_spec U a (mult_sheaf_spec U b c) \<pp>

goal (2 subgoals):
 1. mult_sheaf_spec U (mult_sheaf_spec U a b) c \<in> extensional U
 2. mult_sheaf_spec U a (mult_sheaf_spec U b c) \<in> extensional U
[PROOF STEP]
qed (auto simp add:add_sheaf_spec_def)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a3 \<in> \<O> U; ?b3 \<in> \<O> U; ?c3 \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (mult_sheaf_spec U ?a3 ?b3) ?c3 = mult_sheaf_spec U ?a3 (mult_sheaf_spec U ?b3 ?c3)

goal (5 subgoals):
 1. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
 2. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) a = a
 3. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U a (one_sheaf_spec U) = a
 4. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c)
 5. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (add_sheaf_spec U b c) a = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)
[PROOF STEP]
show "mult_sheaf_spec U (one_sheaf_spec U) a = a"
    if "a \<in> \<O> U" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U (one_sheaf_spec U) a = a
[PROOF STEP]
proof (rule extensionalityI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. mult_sheaf_spec U (one_sheaf_spec U) a \<in> extensional ?A
 2. a \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) a x = a x
[PROOF STEP]
fix \<pp>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. mult_sheaf_spec U (one_sheaf_spec U) a \<in> extensional ?A
 2. a \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) a x = a x
[PROOF STEP]
assume "\<pp> \<in> U"
[PROOF STATE]
proof (state)
this:
\<pp> \<in> U

goal (3 subgoals):
 1. mult_sheaf_spec U (one_sheaf_spec U) a \<in> extensional ?A
 2. a \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) a x = a x
[PROOF STEP]
interpret cq:quotient_ring "R\<setminus>\<pp>" R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using \<open>\<pp> \<in> U\<close> imp_qr
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
?\<pp>3 \<in> U \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>?\<pp>3) R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. mult_sheaf_spec U (one_sheaf_spec U) a \<in> extensional ?A
 2. a \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) a x = a x
[PROOF STEP]
show "mult_sheaf_spec U (one_sheaf_spec U) a \<pp> = a \<pp>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U (one_sheaf_spec U) a \<pp> = a \<pp>
[PROOF STEP]
unfolding mult_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (one_sheaf_spec U \<pp>) (a \<pp>)) \<pp> = a \<pp>
[PROOF STEP]
using \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (one_sheaf_spec U \<pp>) (a \<pp>)) \<pp> = a \<pp>
[PROOF STEP]
by (simp add: one_sheaf_spec_def qr_valid_frac that)
[PROOF STATE]
proof (state)
this:
mult_sheaf_spec U (one_sheaf_spec U) a \<pp> = a \<pp>

goal (2 subgoals):
 1. mult_sheaf_spec U (one_sheaf_spec U) a \<in> extensional U
 2. a \<in> extensional U
[PROOF STEP]
qed (auto simp add: \<open>a \<in> \<O> U\<close>)
[PROOF STATE]
proof (state)
this:
?a3 \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) ?a3 = ?a3

goal (4 subgoals):
 1. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
 2. \<And>a. a \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U a (one_sheaf_spec U) = a
 3. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c)
 4. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (add_sheaf_spec U b c) a = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?a3 \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) ?a3 = ?a3
[PROOF STEP]
show "mult_sheaf_spec U a (one_sheaf_spec U) = a"
    if "a \<in> \<O> U" for a
[PROOF STATE]
proof (prove)
using this:
?a3 \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U (one_sheaf_spec U) ?a3 = ?a3

goal (1 subgoal):
 1. mult_sheaf_spec U a (one_sheaf_spec U) = a
[PROOF STEP]
by (simp add: \<open>one_sheaf_spec U \<in> \<O> U\<close> mult_comm that)
[PROOF STATE]
proof (state)
this:
?a3 \<in> \<O> U \<Longrightarrow> mult_sheaf_spec U ?a3 (one_sheaf_spec U) = ?a3

goal (3 subgoals):
 1. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
 2. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c)
 3. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (add_sheaf_spec U b c) a = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)
[PROOF STEP]
show "mult_sheaf_spec U a (add_sheaf_spec U b c)
          = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c)"
    if "a \<in> \<O> U" and "b \<in> \<O> U" and "c \<in> \<O> U" for a b c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U a (add_sheaf_spec U b c) = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c)
[PROOF STEP]
proof (rule extensionalityI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. mult_sheaf_spec U a (add_sheaf_spec U b c) \<in> extensional ?A
 2. add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) x = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c) x
[PROOF STEP]
fix \<pp>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. mult_sheaf_spec U a (add_sheaf_spec U b c) \<in> extensional ?A
 2. add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) x = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c) x
[PROOF STEP]
assume "\<pp> \<in> U"
[PROOF STATE]
proof (state)
this:
\<pp> \<in> U

goal (3 subgoals):
 1. mult_sheaf_spec U a (add_sheaf_spec U b c) \<in> extensional ?A
 2. add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) x = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c) x
[PROOF STEP]
interpret cq:quotient_ring "R\<setminus>\<pp>" R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using \<open>\<pp> \<in> U\<close> imp_qr
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
?\<pp>3 \<in> U \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>?\<pp>3) R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. mult_sheaf_spec U a (add_sheaf_spec U b c) \<in> extensional ?A
 2. add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c) \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> mult_sheaf_spec U a (add_sheaf_spec U b c) x = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c) x
[PROOF STEP]
show "mult_sheaf_spec U a (add_sheaf_spec U b c) \<pp> =
         add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c) \<pp>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U a (add_sheaf_spec U b c) \<pp> = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c) \<pp>
[PROOF STEP]
unfolding mult_sheaf_spec_def add_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (a \<pp>) ((\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (b \<pp>) (c \<pp>)) \<pp>)) \<pp> = (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> ((\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (a \<pp>) (b \<pp>)) \<pp>) ((\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (a \<pp>) (c \<pp>)) \<pp>)) \<pp>
[PROOF STEP]
by (simp add: cq.distributive(1) qr_valid_frac that(1) that(2) that(3))
[PROOF STATE]
proof (state)
this:
mult_sheaf_spec U a (add_sheaf_spec U b c) \<pp> = add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c) \<pp>

goal (2 subgoals):
 1. mult_sheaf_spec U a (add_sheaf_spec U b c) \<in> extensional U
 2. add_sheaf_spec U (mult_sheaf_spec U a b) (mult_sheaf_spec U a c) \<in> extensional U
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a3 \<in> \<O> U; ?b3 \<in> \<O> U; ?c3 \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U ?a3 (add_sheaf_spec U ?b3 ?c3) = add_sheaf_spec U (mult_sheaf_spec U ?a3 ?b3) (mult_sheaf_spec U ?a3 ?c3)

goal (2 subgoals):
 1. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
 2. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (add_sheaf_spec U b c) a = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?a3 \<in> \<O> U; ?b3 \<in> \<O> U; ?c3 \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U ?a3 (add_sheaf_spec U ?b3 ?c3) = add_sheaf_spec U (mult_sheaf_spec U ?a3 ?b3) (mult_sheaf_spec U ?a3 ?c3)
[PROOF STEP]
show "mult_sheaf_spec U (add_sheaf_spec U b c) a
                = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)"
    if "a \<in> \<O> U" and "b \<in> \<O> U" and "c \<in> \<O> U" for a b c
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a3 \<in> \<O> U; ?b3 \<in> \<O> U; ?c3 \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U ?a3 (add_sheaf_spec U ?b3 ?c3) = add_sheaf_spec U (mult_sheaf_spec U ?a3 ?b3) (mult_sheaf_spec U ?a3 ?c3)

goal (1 subgoal):
 1. mult_sheaf_spec U (add_sheaf_spec U b c) a = add_sheaf_spec U (mult_sheaf_spec U b a) (mult_sheaf_spec U c a)
[PROOF STEP]
by (simp add: add_\<O> mult_comm that(1) that(2) that(3))
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a3 \<in> \<O> U; ?b3 \<in> \<O> U; ?c3 \<in> \<O> U\<rbrakk> \<Longrightarrow> mult_sheaf_spec U (add_sheaf_spec U ?b3 ?c3) ?a3 = add_sheaf_spec U (mult_sheaf_spec U ?b3 ?a3) (mult_sheaf_spec U ?c3 ?a3)

goal (1 subgoal):
 1. \<And>u. u \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
[PROOF STEP]
show "monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u"
    if "u \<in> \<O> U" for u
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) u
[PROOF STEP]
proof (rule monoid.invertibleI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
 2. add_sheaf_spec U u ?v = zero_sheaf_spec U
 3. add_sheaf_spec U ?v u = zero_sheaf_spec U
 4. u \<in> \<O> U
 5. ?v \<in> \<O> U
[PROOF STEP]
show "Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U a b \<in> \<O> U
 2. zero_sheaf_spec U \<in> \<O> U
 3. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U (add_sheaf_spec U a b) c = add_sheaf_spec U a (add_sheaf_spec U b c)
 4. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U (zero_sheaf_spec U) a = a
 5. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U a (zero_sheaf_spec U) = a
[PROOF STEP]
using add_\<O> \<open>zero_sheaf_spec U \<in> \<O> U\<close> add_assoc \<open>zero_sheaf_spec U \<in> \<O> U\<close>
        add_comm add_zero  add_zero
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a3 \<in> \<O> U; ?b3 \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U ?a3 ?b3 \<in> \<O> U
zero_sheaf_spec U \<in> \<O> U
\<lbrakk>?a3 \<in> \<O> U; ?b3 \<in> \<O> U; ?c3 \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U (add_sheaf_spec U ?a3 ?b3) ?c3 = add_sheaf_spec U ?a3 (add_sheaf_spec U ?b3 ?c3)
zero_sheaf_spec U \<in> \<O> U
\<lbrakk>?x3 \<in> \<O> U; ?y3 \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U ?x3 ?y3 = add_sheaf_spec U ?y3 ?x3
?a3 \<in> \<O> U \<Longrightarrow> add_sheaf_spec U ?a3 (zero_sheaf_spec U) = ?a3
?a3 \<in> \<O> U \<Longrightarrow> add_sheaf_spec U ?a3 (zero_sheaf_spec U) = ?a3

goal (5 subgoals):
 1. \<And>a b. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U a b \<in> \<O> U
 2. zero_sheaf_spec U \<in> \<O> U
 3. \<And>a b c. \<lbrakk>a \<in> \<O> U; b \<in> \<O> U; c \<in> \<O> U\<rbrakk> \<Longrightarrow> add_sheaf_spec U (add_sheaf_spec U a b) c = add_sheaf_spec U a (add_sheaf_spec U b c)
 4. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U (zero_sheaf_spec U) a = a
 5. \<And>a. a \<in> \<O> U \<Longrightarrow> add_sheaf_spec U a (zero_sheaf_spec U) = a
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
Group_Theory.monoid (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U)

goal (4 subgoals):
 1. add_sheaf_spec U u ?v = zero_sheaf_spec U
 2. add_sheaf_spec U ?v u = zero_sheaf_spec U
 3. u \<in> \<O> U
 4. ?v \<in> \<O> U
[PROOF STEP]
show "add_sheaf_spec U u (uminus_sheaf_spec U u) = zero_sheaf_spec U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U u (uminus_sheaf_spec U u) = zero_sheaf_spec U
[PROOF STEP]
proof (rule extensionalityI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. add_sheaf_spec U u (uminus_sheaf_spec U u) \<in> extensional ?A
 2. zero_sheaf_spec U \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> add_sheaf_spec U u (uminus_sheaf_spec U u) x = zero_sheaf_spec U x
[PROOF STEP]
fix \<pp>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. add_sheaf_spec U u (uminus_sheaf_spec U u) \<in> extensional ?A
 2. zero_sheaf_spec U \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> add_sheaf_spec U u (uminus_sheaf_spec U u) x = zero_sheaf_spec U x
[PROOF STEP]
assume "\<pp> \<in> U"
[PROOF STATE]
proof (state)
this:
\<pp> \<in> U

goal (3 subgoals):
 1. add_sheaf_spec U u (uminus_sheaf_spec U u) \<in> extensional ?A
 2. zero_sheaf_spec U \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> add_sheaf_spec U u (uminus_sheaf_spec U u) x = zero_sheaf_spec U x
[PROOF STEP]
interpret cq:quotient_ring "R\<setminus>\<pp>" R "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using \<open>\<pp> \<in> U\<close> imp_qr
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
?\<pp>3 \<in> U \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>?\<pp>3) R (+) (\<cdot>) \<zero> \<one>

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. add_sheaf_spec U u (uminus_sheaf_spec U u) \<in> extensional ?A
 2. zero_sheaf_spec U \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> add_sheaf_spec U u (uminus_sheaf_spec U u) x = zero_sheaf_spec U x
[PROOF STEP]
have "cq.add_rel (u \<pp>) (cq.uminus_rel (u \<pp>)) = cq.zero_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cq.add_rel (u \<pp>) (cq.uminus_rel (u \<pp>)) = cq.zero_rel
[PROOF STEP]
by (simp add: \<open>\<pp> \<in> U\<close> cq.add_minus_zero_rel qr_valid_frac that)
[PROOF STATE]
proof (state)
this:
cq.add_rel (u \<pp>) (cq.uminus_rel (u \<pp>)) = cq.zero_rel

goal (3 subgoals):
 1. add_sheaf_spec U u (uminus_sheaf_spec U u) \<in> extensional ?A
 2. zero_sheaf_spec U \<in> extensional ?A
 3. \<And>x. x \<in> ?A \<Longrightarrow> add_sheaf_spec U u (uminus_sheaf_spec U u) x = zero_sheaf_spec U x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cq.add_rel (u \<pp>) (cq.uminus_rel (u \<pp>)) = cq.zero_rel
[PROOF STEP]
show "add_sheaf_spec U u (uminus_sheaf_spec U u) \<pp> = zero_sheaf_spec U \<pp>"
[PROOF STATE]
proof (prove)
using this:
cq.add_rel (u \<pp>) (cq.uminus_rel (u \<pp>)) = cq.zero_rel

goal (1 subgoal):
 1. add_sheaf_spec U u (uminus_sheaf_spec U u) \<pp> = zero_sheaf_spec U \<pp>
[PROOF STEP]
unfolding add_sheaf_spec_def uminus_sheaf_spec_def zero_sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
cq.add_rel (u \<pp>) (cq.uminus_rel (u \<pp>)) = cq.zero_rel

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (u \<pp>) ((\<lambda>\<pp>\<in>U. quotient_ring.uminus_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (u \<pp>)) \<pp>)) \<pp> = (\<lambda>\<pp>\<in>U. quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<pp>
[PROOF STEP]
using \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
cq.add_rel (u \<pp>) (cq.uminus_rel (u \<pp>)) = cq.zero_rel
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.add_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (u \<pp>) ((\<lambda>\<pp>\<in>U. quotient_ring.uminus_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (u \<pp>)) \<pp>)) \<pp> = (\<lambda>\<pp>\<in>U. quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<pp>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
add_sheaf_spec U u (uminus_sheaf_spec U u) \<pp> = zero_sheaf_spec U \<pp>

goal (2 subgoals):
 1. add_sheaf_spec U u (uminus_sheaf_spec U u) \<in> extensional U
 2. zero_sheaf_spec U \<in> extensional U
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
add_sheaf_spec U u (uminus_sheaf_spec U u) = zero_sheaf_spec U

goal (3 subgoals):
 1. add_sheaf_spec U (uminus_sheaf_spec U u) u = zero_sheaf_spec U
 2. u \<in> \<O> U
 3. uminus_sheaf_spec U u \<in> \<O> U
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
add_sheaf_spec U u (uminus_sheaf_spec U u) = zero_sheaf_spec U
[PROOF STEP]
show "add_sheaf_spec U (uminus_sheaf_spec U u) u = zero_sheaf_spec U"
[PROOF STATE]
proof (prove)
using this:
add_sheaf_spec U u (uminus_sheaf_spec U u) = zero_sheaf_spec U

goal (1 subgoal):
 1. add_sheaf_spec U (uminus_sheaf_spec U u) u = zero_sheaf_spec U
[PROOF STEP]
by (simp add: add_comm assms comm_ring.zariski_open_is_subset local.comm_ring_axioms
          that uminus_sheaf_spec_in_sheaf_spec)
[PROOF STATE]
proof (state)
this:
add_sheaf_spec U (uminus_sheaf_spec U u) u = zero_sheaf_spec U

goal (2 subgoals):
 1. u \<in> \<O> U
 2. uminus_sheaf_spec U u \<in> \<O> U
[PROOF STEP]
show "u \<in> \<O> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> \<O> U
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
u \<in> \<O> U

goal (1 subgoal):
 1. u \<in> \<O> U
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
u \<in> \<O> U

goal (1 subgoal):
 1. uminus_sheaf_spec U u \<in> \<O> U
[PROOF STEP]
show "uminus_sheaf_spec U u \<in> \<O> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uminus_sheaf_spec U u \<in> \<O> U
[PROOF STEP]
by (simp add: assms comm_ring.zariski_open_is_subset local.comm_ring_axioms
            that uminus_sheaf_spec_in_sheaf_spec)
[PROOF STATE]
proof (state)
this:
uminus_sheaf_spec U u \<in> \<O> U

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?u3 \<in> \<O> U \<Longrightarrow> monoid.invertible (\<O> U) (add_sheaf_spec U) (zero_sheaf_spec U) ?u3

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sheaf_morphisms_sheaf_spec:
  assumes "s \<in> \<O> U"
  shows "sheaf_spec_morphisms U U s = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms U U s = s
[PROOF STEP]
using assms sheaf_spec_def restrict_on_source sheaf_spec_morphisms_def
[PROOF STATE]
proof (prove)
using this:
s \<in> \<O> U
\<O> ?U \<equiv> {s \<in> \<Pi>\<^sub>E \<pp>\<in>?U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s ?U}
Set_Theory.map ?f ?S ?T \<Longrightarrow> restrict ?f ?S = ?f
sheaf_spec_morphisms ?U ?V \<equiv> \<lambda>s\<in>\<O> ?U. restrict s ?V

goal (1 subgoal):
 1. sheaf_spec_morphisms U U s = s
[PROOF STEP]
by auto


[STATEMENT]
lemma sheaf_spec_morphisms_are_maps:
  assumes (*this assumption seems redundant: "is_zariski_open U" and*)
    "is_zariski_open V" and "V \<subseteq> U"
  shows "Set_Theory.map (sheaf_spec_morphisms U V) (\<O> U) (\<O> V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Set_Theory.map (sheaf_spec_morphisms U V) (\<O> U) (\<O> V)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Set_Theory.map (sheaf_spec_morphisms U V) (\<O> U) (\<O> V)
[PROOF STEP]
have "sheaf_spec_morphisms U V \<in> extensional (\<O> U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms U V \<in> extensional (\<O> U)
[PROOF STEP]
unfolding sheaf_spec_morphisms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s\<in>\<O> U. restrict s V) \<in> extensional (\<O> U)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V \<in> extensional (\<O> U)

goal (1 subgoal):
 1. Set_Theory.map (sheaf_spec_morphisms U V) (\<O> U) (\<O> V)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V \<in> extensional (\<O> U)

goal (1 subgoal):
 1. Set_Theory.map (sheaf_spec_morphisms U V) (\<O> U) (\<O> V)
[PROOF STEP]
have "sheaf_spec_morphisms U V \<in> (\<O> U) \<rightarrow> (\<O> V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sheaf_spec_morphisms U V \<in> \<O> U \<rightarrow> \<O> V
[PROOF STEP]
unfolding sheaf_spec_morphisms_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>s\<in>\<O> U. restrict s V) \<in> \<O> U \<rightarrow> \<O> V
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> \<O> U \<Longrightarrow> restrict s V \<in> \<O> V
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>s. s \<in> \<O> U \<Longrightarrow> restrict s V \<in> \<O> V
[PROOF STEP]
assume "s \<in> \<O> U"
[PROOF STATE]
proof (state)
this:
s \<in> \<O> U

goal (1 subgoal):
 1. \<And>s. s \<in> \<O> U \<Longrightarrow> restrict s V \<in> \<O> V
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> \<O> U
[PROOF STEP]
have "s \<in> (\<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)"
        and p:"\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac s V)"
[PROOF STATE]
proof (prove)
using this:
s \<in> \<O> U

goal (1 subgoal):
 1. s \<in> (\<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>) &&& \<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac s V)
[PROOF STEP]
unfolding sheaf_spec_def is_regular_def
[PROOF STATE]
proof (prove)
using this:
s \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. \<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac s V)}

goal (1 subgoal):
 1. s \<in> (\<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>) &&& \<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac s V)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s \<in> (\<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)
\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac s V)

goal (1 subgoal):
 1. \<And>s. s \<in> \<O> U \<Longrightarrow> restrict s V \<in> \<O> V
[PROOF STEP]
have "restrict s V \<in> (\<Pi>\<^sub>E \<pp>\<in>V. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict s V \<in> (\<Pi>\<^sub>E \<pp>\<in>V. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)
[PROOF STEP]
using \<open>s \<in> (\<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)\<close>
[PROOF STATE]
proof (prove)
using this:
s \<in> (\<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)

goal (1 subgoal):
 1. restrict s V \<in> (\<Pi>\<^sub>E \<pp>\<in>V. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)
[PROOF STEP]
using \<open>V \<subseteq> U\<close>
[PROOF STATE]
proof (prove)
using this:
s \<in> (\<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)
V \<subseteq> U

goal (1 subgoal):
 1. restrict s V \<in> (\<Pi>\<^sub>E \<pp>\<in>V. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
restrict s V \<in> (\<Pi>\<^sub>E \<pp>\<in>V. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)

goal (1 subgoal):
 1. \<And>s. s \<in> \<O> U \<Longrightarrow> restrict s V \<in> \<O> V
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
restrict s V \<in> (\<Pi>\<^sub>E \<pp>\<in>V. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)

goal (1 subgoal):
 1. \<And>s. s \<in> \<O> U \<Longrightarrow> restrict s V \<in> \<O> V
[PROOF STEP]
have "(\<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> \<pp> \<in> Va \<and> is_locally_frac (restrict s V) Va)"
      if "\<pp> \<in> V" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> \<pp> \<in> Va \<and> is_locally_frac (restrict s V) Va
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> \<pp> \<in> Va \<and> is_locally_frac (restrict s V) Va
[PROOF STEP]
obtain U1 where "is_zariski_open U1" "U1 \<subseteq> U" "\<pp> \<in> U1" "is_locally_frac s U1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>U1. \<lbrakk>is_zariski_open U1; U1 \<subseteq> U; \<pp> \<in> U1; is_locally_frac s U1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using p[rule_format, of \<pp>] that \<open>V \<subseteq> U\<close> \<open>\<pp> \<in> V\<close>
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U \<Longrightarrow> \<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> is_locally_frac s V
\<lbrakk>is_zariski_open ?U1.3; ?U1.3 \<subseteq> U; \<pp> \<in> ?U1.3; is_locally_frac s ?U1.3\<rbrakk> \<Longrightarrow> thesis
V \<subseteq> U
\<pp> \<in> V

goal (1 subgoal):
 1. (\<And>U1. \<lbrakk>is_zariski_open U1; U1 \<subseteq> U; \<pp> \<in> U1; is_locally_frac s U1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_zariski_open U1
U1 \<subseteq> U
\<pp> \<in> U1
is_locally_frac s U1

goal (1 subgoal):
 1. \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> \<pp> \<in> Va \<and> is_locally_frac (restrict s V) Va
[PROOF STEP]
define V1 where "V1 = U1 \<inter> V"
[PROOF STATE]
proof (state)
this:
V1 = U1 \<inter> V

goal (1 subgoal):
 1. \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> \<pp> \<in> Va \<and> is_locally_frac (restrict s V) Va
[PROOF STEP]
have "is_zariski_open V1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zariski_open V1
[PROOF STEP]
using \<open>is_zariski_open V\<close> \<open>is_zariski_open U1\<close>
[PROOF STATE]
proof (prove)
using this:
is_zariski_open V
is_zariski_open U1

goal (1 subgoal):
 1. is_zariski_open V1
[PROOF STEP]
by (simp add: V1_def)
[PROOF STATE]
proof (state)
this:
is_zariski_open V1

goal (1 subgoal):
 1. \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> \<pp> \<in> Va \<and> is_locally_frac (restrict s V) Va
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_zariski_open V1

goal (1 subgoal):
 1. \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> \<pp> \<in> Va \<and> is_locally_frac (restrict s V) Va
[PROOF STEP]
have "is_locally_frac s V1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_locally_frac s V1
[PROOF STEP]
using is_locally_frac_subset[OF \<open>is_locally_frac s U1\<close>]
[PROOF STATE]
proof (prove)
using this:
?V \<subseteq> U1 \<Longrightarrow> is_locally_frac s ?V

goal (1 subgoal):
 1. is_locally_frac s V1
[PROOF STEP]
unfolding V1_def
[PROOF STATE]
proof (prove)
using this:
?V \<subseteq> U1 \<Longrightarrow> is_locally_frac s ?V

goal (1 subgoal):
 1. is_locally_frac s (U1 \<inter> V)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_locally_frac s V1

goal (1 subgoal):
 1. \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> \<pp> \<in> Va \<and> is_locally_frac (restrict s V) Va
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
is_locally_frac s V1
[PROOF STEP]
have "is_locally_frac (restrict s V) V1"
[PROOF STATE]
proof (prove)
using this:
is_locally_frac s V1

goal (1 subgoal):
 1. is_locally_frac (restrict s V) V1
[PROOF STEP]
unfolding restrict_def V1_def
[PROOF STATE]
proof (prove)
using this:
is_locally_frac s (U1 \<inter> V)

goal (1 subgoal):
 1. is_locally_frac (\<lambda>x. if x \<in> V then s x else undefined) (U1 \<inter> V)
[PROOF STEP]
using is_locally_frac_cong
[PROOF STATE]
proof (prove)
using this:
is_locally_frac s (U1 \<inter> V)
(\<And>x. x \<in> ?U \<Longrightarrow> ?f x = ?g x) \<Longrightarrow> is_locally_frac ?f ?U = is_locally_frac ?g ?U

goal (1 subgoal):
 1. is_locally_frac (\<lambda>x. if x \<in> V then s x else undefined) (U1 \<inter> V)
[PROOF STEP]
by (smt in_mono inf_le2)
[PROOF STATE]
proof (state)
this:
is_locally_frac (restrict s V) V1

goal (1 subgoal):
 1. \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> \<pp> \<in> Va \<and> is_locally_frac (restrict s V) Va
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_locally_frac (restrict s V) V1

goal (1 subgoal):
 1. \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> \<pp> \<in> Va \<and> is_locally_frac (restrict s V) Va
[PROOF STEP]
have "V1 \<subseteq> V" "\<pp> \<in> V1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V1 \<subseteq> V &&& \<pp> \<in> V1
[PROOF STEP]
unfolding V1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U1 \<inter> V \<subseteq> V &&& \<pp> \<in> U1 \<inter> V
[PROOF STEP]
using \<open>V \<subseteq> U\<close> \<open>\<pp> \<in> U1\<close> that
[PROOF STATE]
proof (prove)
using this:
V \<subseteq> U
\<pp> \<in> U1
\<pp> \<in> V

goal (1 subgoal):
 1. U1 \<inter> V \<subseteq> V &&& \<pp> \<in> U1 \<inter> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V1 \<subseteq> V
\<pp> \<in> V1

goal (1 subgoal):
 1. \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> \<pp> \<in> Va \<and> is_locally_frac (restrict s V) Va
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_zariski_open V1
is_locally_frac (restrict s V) V1
V1 \<subseteq> V
\<pp> \<in> V1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
is_zariski_open V1
is_locally_frac (restrict s V) V1
V1 \<subseteq> V
\<pp> \<in> V1

goal (1 subgoal):
 1. \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> \<pp> \<in> Va \<and> is_locally_frac (restrict s V) Va
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> \<pp> \<in> Va \<and> is_locally_frac (restrict s V) Va

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> V \<Longrightarrow> \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> ?\<pp>3 \<in> Va \<and> is_locally_frac (restrict s V) Va

goal (1 subgoal):
 1. \<And>s. s \<in> \<O> U \<Longrightarrow> restrict s V \<in> \<O> V
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
restrict s V \<in> (\<Pi>\<^sub>E \<pp>\<in>V. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)
?\<pp>3 \<in> V \<Longrightarrow> \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> ?\<pp>3 \<in> Va \<and> is_locally_frac (restrict s V) Va
[PROOF STEP]
show "restrict s V \<in> \<O> V"
[PROOF STATE]
proof (prove)
using this:
restrict s V \<in> (\<Pi>\<^sub>E \<pp>\<in>V. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)
?\<pp>3 \<in> V \<Longrightarrow> \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> ?\<pp>3 \<in> Va \<and> is_locally_frac (restrict s V) Va

goal (1 subgoal):
 1. restrict s V \<in> \<O> V
[PROOF STEP]
unfolding sheaf_spec_def is_regular_def
[PROOF STATE]
proof (prove)
using this:
restrict s V \<in> (\<Pi>\<^sub>E \<pp>\<in>V. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>)
?\<pp>3 \<in> V \<Longrightarrow> \<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> ?\<pp>3 \<in> Va \<and> is_locally_frac (restrict s V) Va

goal (1 subgoal):
 1. restrict s V \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>V. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. \<forall>\<pp>. \<pp> \<in> V \<longrightarrow> (\<exists>Va. is_zariski_open Va \<and> Va \<subseteq> V \<and> \<pp> \<in> Va \<and> is_locally_frac s Va)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
restrict s V \<in> \<O> V

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sheaf_spec_morphisms U V \<in> \<O> U \<rightarrow> \<O> V

goal (1 subgoal):
 1. Set_Theory.map (sheaf_spec_morphisms U V) (\<O> U) (\<O> V)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sheaf_spec_morphisms U V \<in> extensional (\<O> U)
sheaf_spec_morphisms U V \<in> \<O> U \<rightarrow> \<O> V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sheaf_spec_morphisms U V \<in> extensional (\<O> U)
sheaf_spec_morphisms U V \<in> \<O> U \<rightarrow> \<O> V

goal (1 subgoal):
 1. Set_Theory.map (sheaf_spec_morphisms U V) (\<O> U) (\<O> V)
[PROOF STEP]
by (simp add: extensional_funcset_def map.intro)
[PROOF STATE]
proof (state)
this:
Set_Theory.map (sheaf_spec_morphisms U V) (\<O> U) (\<O> V)

goal:
No subgoals!
[PROOF STEP]
qed