[STATEMENT]
lemma is_regular_mult_sheaf_spec:
  assumes "is_regular s U" and "is_regular s' U" and "U \<subseteq> Spec"
  shows "is_regular (mult_sheaf_spec U s s') U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_regular (mult_sheaf_spec U s s') U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_regular (mult_sheaf_spec U s s') U
[PROOF STEP]
have "mult_sheaf_spec U s s' \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>" if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U s s' \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mult_sheaf_spec U s s' \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret pi: pr_ideal R \<pp> "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using \<open>U \<subseteq> Spec\<close>[unfolded spectrum_def] \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
U \<subseteq> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}
\<pp> \<in> U

goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mult_sheaf_spec U s s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
have "s \<pp> \<in> pi.carrier_local_ring_at"
      "s' \<pp> \<in> pi.carrier_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<pp> \<in> pi.carrier_local_ring_at &&& s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using \<open>is_regular s U\<close> \<open>is_regular s' U\<close>
[PROOF STATE]
proof (prove)
using this:
is_regular s U
is_regular s' U

goal (1 subgoal):
 1. s \<pp> \<in> pi.carrier_local_ring_at &&& s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
unfolding is_regular_def
[PROOF STATE]
proof (prove)
using this:
\<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)
\<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 \<pp> \<in> pi.carrier_local_ring_at &&& s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<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)
\<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)
\<pp> \<in> U

goal (1 subgoal):
 1. s \<pp> \<in> pi.carrier_local_ring_at &&& s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using assms(3) frac_in_carrier_local in_mono is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
\<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)
\<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)
\<pp> \<in> U
U \<subseteq> Spec
\<lbrakk>?\<pp> \<in> Spec; ?r \<in> R; ?s \<in> R; ?s \<notin> ?\<pp>\<rbrakk> \<Longrightarrow> quotient_ring.frac (R\<setminus>?\<pp>) R (+) (\<cdot>) \<zero> ?r ?s \<in> R \<^bsub>?\<pp> (+) (\<cdot>) \<zero>\<^esub>
?A \<subseteq> ?B \<Longrightarrow> ?x \<in> ?A \<longrightarrow> ?x \<in> ?B
is_locally_frac ?s ?V \<equiv> \<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>?V. f \<notin> \<qq> \<and> ?s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)

goal (1 subgoal):
 1. s \<pp> \<in> pi.carrier_local_ring_at &&& s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
s \<pp> \<in> pi.carrier_local_ring_at
s' \<pp> \<in> pi.carrier_local_ring_at

goal (1 subgoal):
 1. mult_sheaf_spec U s s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<pp> \<in> pi.carrier_local_ring_at
s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<pp> \<in> pi.carrier_local_ring_at
s' \<pp> \<in> pi.carrier_local_ring_at

goal (1 subgoal):
 1. mult_sheaf_spec U s s' \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
unfolding mult_sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
s \<pp> \<in> pi.carrier_local_ring_at
s' \<pp> \<in> pi.carrier_local_ring_at

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>) (s' \<pp>)) \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
s \<pp> \<in> pi.carrier_local_ring_at
s' \<pp> \<in> pi.carrier_local_ring_at
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>) (s' \<pp>)) \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
by (simp flip:pi.mult_local_ring_at_def)
[PROOF STATE]
proof (state)
this:
mult_sheaf_spec U s s' \<pp> \<in> pi.carrier_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> mult_sheaf_spec U s s' ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. is_regular (mult_sheaf_spec U s s') U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> mult_sheaf_spec U s s' ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. is_regular (mult_sheaf_spec U s s') U
[PROOF STEP]
have "(\<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (mult_sheaf_spec U s s') V)"
    if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (mult_sheaf_spec U s s') V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (mult_sheaf_spec U s s') V
[PROOF STEP]
obtain V1 r1 f1 where "V1 \<subseteq>U" "is_zariski_open V1" "\<pp> \<in> V1" "r1 \<in> R" "f1 \<in> R" and
        q_V1:"(\<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>V1 r1 f1. \<lbrakk>V1 \<subseteq> U; is_zariski_open V1; \<pp> \<in> V1; r1 \<in> R; f1 \<in> R; \<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>is_regular s U\<close>[unfolded is_regular_def] \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
\<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)
\<pp> \<in> U

goal (1 subgoal):
 1. (\<And>V1 r1 f1. \<lbrakk>V1 \<subseteq> U; is_zariski_open V1; \<pp> \<in> V1; r1 \<in> R; f1 \<in> R; \<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
\<pp> \<in> U

goal (1 subgoal):
 1. (\<And>V1 r1 f1. \<lbrakk>V1 \<subseteq> U; is_zariski_open V1; \<pp> \<in> V1; r1 \<in> R; f1 \<in> R; \<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V1 \<subseteq> U
is_zariski_open V1
\<pp> \<in> V1
r1 \<in> R
f1 \<in> R
\<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (mult_sheaf_spec U s s') V
[PROOF STEP]
obtain V2 r2 f2 where "V2 \<subseteq>U" "is_zariski_open V2" "\<pp> \<in> V2" "r2 \<in> R" "f2 \<in> R" and
        q_V2:"(\<forall>\<qq>. \<qq> \<in> V2 \<longrightarrow> f2 \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r2 f2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>V2 r2 f2. \<lbrakk>V2 \<subseteq> U; is_zariski_open V2; \<pp> \<in> V2; r2 \<in> R; f2 \<in> R; \<forall>\<qq>. \<qq> \<in> V2 \<longrightarrow> f2 \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r2 f2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>is_regular s' U\<close>[unfolded is_regular_def] \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
\<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)
\<pp> \<in> U

goal (1 subgoal):
 1. (\<And>V2 r2 f2. \<lbrakk>V2 \<subseteq> U; is_zariski_open V2; \<pp> \<in> V2; r2 \<in> R; f2 \<in> R; \<forall>\<qq>. \<qq> \<in> V2 \<longrightarrow> f2 \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r2 f2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
\<pp> \<in> U

goal (1 subgoal):
 1. (\<And>V2 r2 f2. \<lbrakk>V2 \<subseteq> U; is_zariski_open V2; \<pp> \<in> V2; r2 \<in> R; f2 \<in> R; \<forall>\<qq>. \<qq> \<in> V2 \<longrightarrow> f2 \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r2 f2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V2 \<subseteq> U
is_zariski_open V2
\<pp> \<in> V2
r2 \<in> R
f2 \<in> R
\<forall>\<qq>. \<qq> \<in> V2 \<longrightarrow> f2 \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r2 f2

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

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (mult_sheaf_spec U s s') V
[PROOF STEP]
define r3 where "r3 = r1 \<cdot> r2  "
[PROOF STATE]
proof (state)
this:
r3 = r1 \<cdot> r2

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (mult_sheaf_spec U s s') V
[PROOF STEP]
define f3 where "f3 = f1 \<cdot> f2"
[PROOF STATE]
proof (state)
this:
f3 = f1 \<cdot> f2

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (mult_sheaf_spec U s s') V
[PROOF STEP]
have "V3 \<subseteq>U" "\<pp> \<in> V3" "r3 \<in> R" "f3 \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V3 \<subseteq> U &&& \<pp> \<in> V3) &&& r3 \<in> R &&& f3 \<in> R
[PROOF STEP]
unfolding V3_def r3_def f3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V1 \<inter> V2 \<subseteq> U &&& \<pp> \<in> V1 \<inter> V2) &&& r1 \<cdot> r2 \<in> R &&& f1 \<cdot> f2 \<in> R
[PROOF STEP]
using \<open>V1 \<subseteq> U\<close> \<open>\<pp> \<in> V1\<close> \<open>\<pp> \<in> V2\<close> \<open>f1 \<in> R\<close> \<open>f2 \<in> R\<close> \<open>r1 \<in> R\<close> \<open>r2 \<in> R\<close>
[PROOF STATE]
proof (prove)
using this:
V1 \<subseteq> U
\<pp> \<in> V1
\<pp> \<in> V2
f1 \<in> R
f2 \<in> R
r1 \<in> R
r2 \<in> R

goal (1 subgoal):
 1. (V1 \<inter> V2 \<subseteq> U &&& \<pp> \<in> V1 \<inter> V2) &&& r1 \<cdot> r2 \<in> R &&& f1 \<cdot> f2 \<in> R
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (mult_sheaf_spec U s s') V
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (mult_sheaf_spec U s s') V
[PROOF STEP]
have "is_zariski_open V3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zariski_open V3
[PROOF STEP]
using topological_space.open_inter
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>topological_space ?S ?is_open; ?is_open ?U; ?is_open ?V\<rbrakk> \<Longrightarrow> ?is_open (?U \<inter> ?V)

goal (1 subgoal):
 1. is_zariski_open V3
[PROOF STEP]
by (simp add: V3_def \<open>is_zariski_open V1\<close> \<open>is_zariski_open V2\<close>)
[PROOF STATE]
proof (state)
this:
is_zariski_open V3

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

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (mult_sheaf_spec U s s') V
[PROOF STEP]
have "f3 \<notin> \<qq>"
        "mult_sheaf_spec U s s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3"
        if "\<qq> \<in> V3" for \<qq>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f3 \<notin> \<qq> &&& mult_sheaf_spec U s s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. mult_sheaf_spec U s s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
interpret q:quotient_ring "R\<setminus>\<qq>" R "(+)" "(\<cdot>)" \<zero>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using \<open>U \<subseteq> Spec\<close> \<open>V3 \<subseteq> U\<close> \<open>\<qq> \<in> V3\<close> quotient_ring_def local.comm_ring_axioms
          pr_ideal.submonoid_pr_ideal spectrum_def
[PROOF STATE]
proof (prove)
using this:
U \<subseteq> Spec
V3 \<subseteq> U
\<qq> \<in> V3
Comm_Ring.quotient_ring ?S ?R ?addition ?multiplication ?zero ?unit \<equiv> comm_ring ?R ?addition ?multiplication ?zero ?unit \<and> submonoid ?S ?R ?multiplication ?unit
comm_ring R (+) (\<cdot>) \<zero> \<one>
pr_ideal ?R ?I ?addition ?multiplication ?zero ?unit \<Longrightarrow> submonoid (?R\<setminus>?I) ?R ?multiplication ?unit
Spec \<equiv> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. mult_sheaf_spec U s s' \<qq> = q.frac r3 f3
[PROOF STEP]
have "f1 \<notin> \<qq>" "s \<qq> = q.frac r1 f1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1 \<notin> \<qq> &&& s \<qq> = q.frac r1 f1
[PROOF STEP]
using q_V1 \<open>\<qq> \<in> V3\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1
\<qq> \<in> V3

goal (1 subgoal):
 1. f1 \<notin> \<qq> &&& s \<qq> = q.frac r1 f1
[PROOF STEP]
unfolding V3_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1
\<qq> \<in> V1 \<inter> V2

goal (1 subgoal):
 1. f1 \<notin> \<qq> &&& s \<qq> = q.frac r1 f1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f1 \<notin> \<qq>
s \<qq> = q.frac r1 f1

goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. mult_sheaf_spec U s s' \<qq> = q.frac r3 f3
[PROOF STEP]
have "f2 \<notin> \<qq>" "s' \<qq> = q.frac r2 f2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f2 \<notin> \<qq> &&& s' \<qq> = q.frac r2 f2
[PROOF STEP]
using q_V2 \<open>\<qq> \<in> V3\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>\<qq>. \<qq> \<in> V2 \<longrightarrow> f2 \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r2 f2
\<qq> \<in> V3

goal (1 subgoal):
 1. f2 \<notin> \<qq> &&& s' \<qq> = q.frac r2 f2
[PROOF STEP]
unfolding V3_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<qq>. \<qq> \<in> V2 \<longrightarrow> f2 \<notin> \<qq> \<and> s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r2 f2
\<qq> \<in> V1 \<inter> V2

goal (1 subgoal):
 1. f2 \<notin> \<qq> &&& s' \<qq> = q.frac r2 f2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f2 \<notin> \<qq>
s' \<qq> = q.frac r2 f2

goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. mult_sheaf_spec U s s' \<qq> = q.frac r3 f3
[PROOF STEP]
have "q.mult_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 \<cdot> r2 ) (f1 \<cdot> f2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q.mult_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 \<cdot> r2) (f1 \<cdot> f2)
[PROOF STEP]
apply (rule q.mult_rel_frac)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (r1, f1) \<in> R \<times> (R\<setminus>\<qq>)
 2. (r2, f2) \<in> R \<times> (R\<setminus>\<qq>)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r1, f1) \<in> R \<times> (R\<setminus>\<qq>)
[PROOF STEP]
by (simp add: \<open>f1 \<in> R\<close> \<open>f1 \<notin> \<qq>\<close> \<open>r1 \<in> R\<close> \<open>r2 \<in> R\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r2, f2) \<in> R \<times> (R\<setminus>\<qq>)
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r2, f2) \<in> R \<times> (R\<setminus>\<qq>)
[PROOF STEP]
using \<open>f2 \<in> R\<close> \<open>f2 \<notin> \<qq>\<close> \<open>r2 \<in> R\<close>
[PROOF STATE]
proof (prove)
using this:
f2 \<in> R
f2 \<notin> \<qq>
r2 \<in> R

goal (1 subgoal):
 1. (r2, f2) \<in> R \<times> (R\<setminus>\<qq>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
q.mult_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 \<cdot> r2) (f1 \<cdot> f2)

goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. mult_sheaf_spec U s s' \<qq> = q.frac r3 f3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q.mult_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 \<cdot> r2) (f1 \<cdot> f2)
[PROOF STEP]
have "q.mult_rel (s \<qq>) (s' \<qq>) = q.frac r3 f3"
[PROOF STATE]
proof (prove)
using this:
q.mult_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 \<cdot> r2) (f1 \<cdot> f2)

goal (1 subgoal):
 1. q.mult_rel (s \<qq>) (s' \<qq>) = q.frac r3 f3
[PROOF STEP]
unfolding r3_def f3_def
[PROOF STATE]
proof (prove)
using this:
q.mult_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 \<cdot> r2) (f1 \<cdot> f2)

goal (1 subgoal):
 1. q.mult_rel (s \<qq>) (s' \<qq>) = q.frac (r1 \<cdot> r2) (f1 \<cdot> f2)
[PROOF STEP]
using \<open>s \<qq> = q.frac r1 f1\<close> \<open>s' \<qq> = q.frac r2 f2\<close>
[PROOF STATE]
proof (prove)
using this:
q.mult_rel (q.frac r1 f1) (q.frac r2 f2) = q.frac (r1 \<cdot> r2) (f1 \<cdot> f2)
s \<qq> = q.frac r1 f1
s' \<qq> = q.frac r2 f2

goal (1 subgoal):
 1. q.mult_rel (s \<qq>) (s' \<qq>) = q.frac (r1 \<cdot> r2) (f1 \<cdot> f2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q.mult_rel (s \<qq>) (s' \<qq>) = q.frac r3 f3

goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. mult_sheaf_spec U s s' \<qq> = q.frac r3 f3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q.mult_rel (s \<qq>) (s' \<qq>) = q.frac r3 f3
[PROOF STEP]
show "mult_sheaf_spec U s s' \<qq> = q.frac r3 f3"
[PROOF STATE]
proof (prove)
using this:
q.mult_rel (s \<qq>) (s' \<qq>) = q.frac r3 f3

goal (1 subgoal):
 1. mult_sheaf_spec U s s' \<qq> = q.frac r3 f3
[PROOF STEP]
unfolding mult_sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
q.mult_rel (s \<qq>) (s' \<qq>) = q.frac r3 f3

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>) (s' \<pp>)) \<qq> = q.frac r3 f3
[PROOF STEP]
using \<open>V3 \<subseteq> U\<close> \<open>\<qq> \<in> V3\<close>
[PROOF STATE]
proof (prove)
using this:
q.mult_rel (s \<qq>) (s' \<qq>) = q.frac r3 f3
V3 \<subseteq> U
\<qq> \<in> V3

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>) (s' \<pp>)) \<qq> = q.frac r3 f3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mult_sheaf_spec U s s' \<qq> = q.frac r3 f3

goal (1 subgoal):
 1. f3 \<notin> \<qq>
[PROOF STEP]
show "f3 \<notin> \<qq>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f3 \<notin> \<qq>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<qq> \<in> V3

goal (1 subgoal):
 1. f3 \<notin> \<qq>
[PROOF STEP]
unfolding V3_def f3_def
[PROOF STATE]
proof (prove)
using this:
\<qq> \<in> V1 \<inter> V2

goal (1 subgoal):
 1. f1 \<cdot> f2 \<notin> \<qq>
[PROOF STEP]
using \<open>f1 \<in> R\<close> \<open>f1 \<notin> \<qq>\<close> \<open>f2 \<in> R\<close> \<open>f2 \<notin> \<qq>\<close> q.sub_composition_closed
[PROOF STATE]
proof (prove)
using this:
\<qq> \<in> V1 \<inter> V2
f1 \<in> R
f1 \<notin> \<qq>
f2 \<in> R
f2 \<notin> \<qq>
\<lbrakk>?a \<in> R\<setminus>\<qq>; ?b \<in> R\<setminus>\<qq>\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<in> R\<setminus>\<qq>

goal (1 subgoal):
 1. f1 \<cdot> f2 \<notin> \<qq>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f3 \<notin> \<qq>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> mult_sheaf_spec U s s' ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (mult_sheaf_spec U s s') V
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> mult_sheaf_spec U s s' ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> mult_sheaf_spec U s s' ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (mult_sheaf_spec U s s') V
[PROOF STEP]
using is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> mult_sheaf_spec U s s' ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3
is_locally_frac ?s ?V \<equiv> \<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>?V. f \<notin> \<qq> \<and> ?s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)

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

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

goal (1 subgoal):
 1. is_regular (mult_sheaf_spec U s s') U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?\<pp>3 \<in> U \<Longrightarrow> mult_sheaf_spec U s s' ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> is_locally_frac (mult_sheaf_spec U s s') V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> mult_sheaf_spec U s s' ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> is_locally_frac (mult_sheaf_spec U s s') V

goal (1 subgoal):
 1. is_regular (mult_sheaf_spec U s s') U
[PROOF STEP]
unfolding is_regular_def is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> mult_sheaf_spec U s s' ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> mult_sheaf_spec U s s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f))

goal (1 subgoal):
 1. \<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> mult_sheaf_spec U s s' \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
is_regular (mult_sheaf_spec U s s') U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_sheaf_spec_in_sheaf_spec:
  assumes "s \<in> \<O> U" and "t \<in> \<O> U" and "U \<subseteq> Spec"
  shows "mult_sheaf_spec U s t \<in> \<O> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mult_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
have "mult_sheaf_spec U s t \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>"
      if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U s t \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mult_sheaf_spec U s t \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret qr: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]
apply (rule spectrum_imp_cxt_quotient_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pp> \<in> Spec
[PROOF STEP]
using that \<open>U \<subseteq> Spec\<close>
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
U \<subseteq> Spec

goal (1 subgoal):
 1. \<pp> \<in> Spec
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mult_sheaf_spec U s t \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret pi:pr_ideal R \<pp> "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using that \<open>U \<subseteq> Spec\<close>
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
U \<subseteq> Spec

goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by (auto intro:spectrum_imp_pr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mult_sheaf_spec U s t \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
have "qr.valid_frac (s \<pp>)" "qr.valid_frac (t \<pp>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qr.valid_frac (s \<pp>) &&& qr.valid_frac (t \<pp>)
[PROOF STEP]
using sec_has_right_codom[OF _ that] \<open>s \<in> \<O> U\<close> \<open>t \<in> \<O> U\<close>
[PROOF STATE]
proof (prove)
using this:
?s \<in> \<O> U \<Longrightarrow> ?s \<pp> \<in> pi.carrier_local_ring_at
s \<in> \<O> U
t \<in> \<O> U

goal (1 subgoal):
 1. qr.valid_frac (s \<pp>) &&& qr.valid_frac (t \<pp>)
[PROOF STEP]
by (auto simp:pi.carrier_local_ring_at_def)
[PROOF STATE]
proof (state)
this:
qr.valid_frac (s \<pp>)
qr.valid_frac (t \<pp>)

goal (1 subgoal):
 1. mult_sheaf_spec U s t \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qr.valid_frac (s \<pp>)
qr.valid_frac (t \<pp>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
qr.valid_frac (s \<pp>)
qr.valid_frac (t \<pp>)

goal (1 subgoal):
 1. mult_sheaf_spec U s t \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
qr.valid_frac (s \<pp>)
qr.valid_frac (t \<pp>)
\<pp> \<in> U

goal (1 subgoal):
 1. mult_sheaf_spec U s t \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
unfolding mult_sheaf_spec_def pi.carrier_local_ring_at_def
[PROOF STATE]
proof (prove)
using this:
qr.valid_frac (s \<pp>)
qr.valid_frac (t \<pp>)
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.mult_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>) (t \<pp>)) \<pp> \<in> qr.carrier_quotient_ring
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mult_sheaf_spec U s t \<pp> \<in> pi.carrier_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> mult_sheaf_spec U s t ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. mult_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> mult_sheaf_spec U s t ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. mult_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
have "is_regular (mult_sheaf_spec U s t) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_regular (mult_sheaf_spec U s t) U
[PROOF STEP]
using \<open>s \<in> \<O> U\<close> \<open>t \<in> \<O> U\<close> \<open>U \<subseteq> Spec\<close> is_regular_mult_sheaf_spec
[PROOF STATE]
proof (prove)
using this:
s \<in> \<O> U
t \<in> \<O> U
U \<subseteq> Spec
\<lbrakk>is_regular ?s ?U; is_regular ?s' ?U; ?U \<subseteq> Spec\<rbrakk> \<Longrightarrow> is_regular (mult_sheaf_spec ?U ?s ?s') ?U

goal (1 subgoal):
 1. is_regular (mult_sheaf_spec U s t) U
[PROOF STEP]
unfolding sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
s \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s U}
t \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s U}
U \<subseteq> Spec
\<lbrakk>is_regular ?s ?U; is_regular ?s' ?U; ?U \<subseteq> Spec\<rbrakk> \<Longrightarrow> is_regular (mult_sheaf_spec ?U ?s ?s') ?U

goal (1 subgoal):
 1. is_regular (mult_sheaf_spec U s t) U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_regular (mult_sheaf_spec U s t) U

goal (1 subgoal):
 1. mult_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_regular (mult_sheaf_spec U s t) U

goal (1 subgoal):
 1. mult_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
have "mult_sheaf_spec U s t \<in> extensional U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U s t \<in> extensional U
[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> (s \<pp>) (t \<pp>)) \<in> extensional U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mult_sheaf_spec U s t \<in> extensional U

goal (1 subgoal):
 1. mult_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?\<pp>3 \<in> U \<Longrightarrow> mult_sheaf_spec U s t ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (mult_sheaf_spec U s t) U
mult_sheaf_spec U s t \<in> extensional U
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> mult_sheaf_spec U s t ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (mult_sheaf_spec U s t) U
mult_sheaf_spec U s t \<in> extensional U

goal (1 subgoal):
 1. mult_sheaf_spec U s t \<in> \<O> U
[PROOF STEP]
unfolding sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> mult_sheaf_spec U s t ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (mult_sheaf_spec U s t) U
mult_sheaf_spec U s t \<in> extensional U

goal (1 subgoal):
 1. mult_sheaf_spec U s t \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s U}
[PROOF STEP]
by (simp add: PiE_iff)
[PROOF STATE]
proof (state)
this:
mult_sheaf_spec U s t \<in> \<O> U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_regular_uminus_sheaf_spec:
  assumes "is_regular s U" and "U \<subseteq> Spec"
  shows "is_regular (uminus_sheaf_spec U s) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_regular (uminus_sheaf_spec U s) U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_regular (uminus_sheaf_spec U s) U
[PROOF STEP]
have "uminus_sheaf_spec U s \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>" if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uminus_sheaf_spec U s \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. uminus_sheaf_spec U s \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret pi: pr_ideal R \<pp> "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using \<open>U \<subseteq> Spec\<close>[unfolded spectrum_def] \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
U \<subseteq> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}
\<pp> \<in> U

goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. uminus_sheaf_spec U s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
interpret qr:quotient_ring "(R\<setminus>\<pp>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by (simp add: quotient_ring_def local.comm_ring_axioms pi.submonoid_pr_ideal)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. uminus_sheaf_spec U s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
have "s \<pp> \<in> pi.carrier_local_ring_at"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using \<open>is_regular s U\<close>
[PROOF STATE]
proof (prove)
using this:
is_regular s U

goal (1 subgoal):
 1. s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
unfolding is_regular_def
[PROOF STATE]
proof (prove)
using this:
\<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 \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<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)
\<pp> \<in> U

goal (1 subgoal):
 1. s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using assms(2) frac_in_carrier_local in_mono is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
\<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)
\<pp> \<in> U
U \<subseteq> Spec
\<lbrakk>?\<pp> \<in> Spec; ?r \<in> R; ?s \<in> R; ?s \<notin> ?\<pp>\<rbrakk> \<Longrightarrow> quotient_ring.frac (R\<setminus>?\<pp>) R (+) (\<cdot>) \<zero> ?r ?s \<in> R \<^bsub>?\<pp> (+) (\<cdot>) \<zero>\<^esub>
?A \<subseteq> ?B \<Longrightarrow> ?x \<in> ?A \<longrightarrow> ?x \<in> ?B
is_locally_frac ?s ?V \<equiv> \<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>?V. f \<notin> \<qq> \<and> ?s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)

goal (1 subgoal):
 1. s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
s \<pp> \<in> pi.carrier_local_ring_at

goal (1 subgoal):
 1. uminus_sheaf_spec U s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
s \<pp> \<in> pi.carrier_local_ring_at

goal (1 subgoal):
 1. uminus_sheaf_spec U s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
unfolding uminus_sheaf_spec_def pi.carrier_local_ring_at_def
[PROOF STATE]
proof (prove)
using this:
s \<pp> \<in> qr.carrier_quotient_ring

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.uminus_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>)) \<pp> \<in> qr.carrier_quotient_ring
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
s \<pp> \<in> qr.carrier_quotient_ring
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.uminus_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>)) \<pp> \<in> qr.carrier_quotient_ring
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
uminus_sheaf_spec U s \<pp> \<in> pi.carrier_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> uminus_sheaf_spec U s ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. is_regular (uminus_sheaf_spec U s) U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> uminus_sheaf_spec U s ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. is_regular (uminus_sheaf_spec U s) U
[PROOF STEP]
have "(\<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (uminus_sheaf_spec U s) V)"
    if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (uminus_sheaf_spec U s) V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (uminus_sheaf_spec U s) V
[PROOF STEP]
obtain V1 r1 f1 where "V1 \<subseteq>U" "is_zariski_open V1" "\<pp> \<in> V1" "r1 \<in> R" "f1 \<in> R" and
        q_V1:"(\<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>V1 r1 f1. \<lbrakk>V1 \<subseteq> U; is_zariski_open V1; \<pp> \<in> V1; r1 \<in> R; f1 \<in> R; \<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>is_regular s U\<close>[unfolded is_regular_def] \<open>\<pp> \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
\<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)
\<pp> \<in> U

goal (1 subgoal):
 1. (\<And>V1 r1 f1. \<lbrakk>V1 \<subseteq> U; is_zariski_open V1; \<pp> \<in> V1; r1 \<in> R; f1 \<in> R; \<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
\<pp> \<in> U

goal (1 subgoal):
 1. (\<And>V1 r1 f1. \<lbrakk>V1 \<subseteq> U; is_zariski_open V1; \<pp> \<in> V1; r1 \<in> R; f1 \<in> R; \<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V1 \<subseteq> U
is_zariski_open V1
\<pp> \<in> V1
r1 \<in> R
f1 \<in> R
\<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1

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

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (uminus_sheaf_spec U s) V
[PROOF STEP]
define r3 where "r3 = additive.inverse r1"
[PROOF STATE]
proof (state)
this:
r3 = - r1

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (uminus_sheaf_spec U s) V
[PROOF STEP]
define f3 where "f3 = f1"
[PROOF STATE]
proof (state)
this:
f3 = f1

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (uminus_sheaf_spec U s) V
[PROOF STEP]
have "V3 \<subseteq>U" "\<pp> \<in> V3" "r3 \<in> R" "f3 \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V3 \<subseteq> U &&& \<pp> \<in> V3) &&& r3 \<in> R &&& f3 \<in> R
[PROOF STEP]
unfolding V3_def r3_def f3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V1 \<subseteq> U &&& \<pp> \<in> V1) &&& - r1 \<in> R &&& f1 \<in> R
[PROOF STEP]
using \<open>V1 \<subseteq> U\<close> \<open>\<pp> \<in> V1\<close> \<open>f1 \<in> R\<close>  \<open>r1 \<in> R\<close>
[PROOF STATE]
proof (prove)
using this:
V1 \<subseteq> U
\<pp> \<in> V1
f1 \<in> R
r1 \<in> R

goal (1 subgoal):
 1. (V1 \<subseteq> U &&& \<pp> \<in> V1) &&& - r1 \<in> R &&& f1 \<in> R
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (uminus_sheaf_spec U s) V
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (uminus_sheaf_spec U s) V
[PROOF STEP]
have "is_zariski_open V3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zariski_open V3
[PROOF STEP]
using topological_space.open_inter
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>topological_space ?S ?is_open; ?is_open ?U; ?is_open ?V\<rbrakk> \<Longrightarrow> ?is_open (?U \<inter> ?V)

goal (1 subgoal):
 1. is_zariski_open V3
[PROOF STEP]
by (simp add: V3_def \<open>is_zariski_open V1\<close>)
[PROOF STATE]
proof (state)
this:
is_zariski_open V3

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

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (uminus_sheaf_spec U s) V
[PROOF STEP]
have "f3 \<notin> \<qq>"
        "uminus_sheaf_spec U s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3"
        if "\<qq> \<in> V3" for \<qq>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f3 \<notin> \<qq> &&& uminus_sheaf_spec U s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. uminus_sheaf_spec U s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
interpret q:quotient_ring "R\<setminus>\<qq>" R "(+)" "(\<cdot>)" \<zero>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using \<open>U \<subseteq> Spec\<close> \<open>V3 \<subseteq> U\<close> \<open>\<qq> \<in> V3\<close> quotient_ring_def local.comm_ring_axioms
          pr_ideal.submonoid_pr_ideal spectrum_def
[PROOF STATE]
proof (prove)
using this:
U \<subseteq> Spec
V3 \<subseteq> U
\<qq> \<in> V3
Comm_Ring.quotient_ring ?S ?R ?addition ?multiplication ?zero ?unit \<equiv> comm_ring ?R ?addition ?multiplication ?zero ?unit \<and> submonoid ?S ?R ?multiplication ?unit
comm_ring R (+) (\<cdot>) \<zero> \<one>
pr_ideal ?R ?I ?addition ?multiplication ?zero ?unit \<Longrightarrow> submonoid (?R\<setminus>?I) ?R ?multiplication ?unit
Spec \<equiv> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. uminus_sheaf_spec U s \<qq> = q.frac r3 f3
[PROOF STEP]
have "f1 \<notin> \<qq>" "s \<qq> = q.frac r1 f1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f1 \<notin> \<qq> &&& s \<qq> = q.frac r1 f1
[PROOF STEP]
using q_V1 \<open>\<qq> \<in> V3\<close>
[PROOF STATE]
proof (prove)
using this:
\<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1
\<qq> \<in> V3

goal (1 subgoal):
 1. f1 \<notin> \<qq> &&& s \<qq> = q.frac r1 f1
[PROOF STEP]
unfolding V3_def
[PROOF STATE]
proof (prove)
using this:
\<forall>\<qq>. \<qq> \<in> V1 \<longrightarrow> f1 \<notin> \<qq> \<and> s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r1 f1
\<qq> \<in> V1

goal (1 subgoal):
 1. f1 \<notin> \<qq> &&& s \<qq> = q.frac r1 f1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f1 \<notin> \<qq>
s \<qq> = q.frac r1 f1

goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. uminus_sheaf_spec U s \<qq> = q.frac r3 f3
[PROOF STEP]
have "q.uminus_rel (q.frac r1 f1) = q.frac (additive.inverse r1) f1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q.uminus_rel (q.frac r1 f1) = q.frac (- r1) f1
[PROOF STEP]
apply (rule q.uminus_rel_frac)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r1, f1) \<in> R \<times> (R\<setminus>\<qq>)
[PROOF STEP]
by (simp add: \<open>f1 \<in> R\<close> \<open>f1 \<notin> \<qq>\<close> \<open>r1 \<in> R\<close>)
[PROOF STATE]
proof (state)
this:
q.uminus_rel (q.frac r1 f1) = q.frac (- r1) f1

goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. uminus_sheaf_spec U s \<qq> = q.frac r3 f3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q.uminus_rel (q.frac r1 f1) = q.frac (- r1) f1
[PROOF STEP]
have "q.uminus_rel (s \<qq>) = q.frac r3 f3"
[PROOF STATE]
proof (prove)
using this:
q.uminus_rel (q.frac r1 f1) = q.frac (- r1) f1

goal (1 subgoal):
 1. q.uminus_rel (s \<qq>) = q.frac r3 f3
[PROOF STEP]
unfolding r3_def f3_def
[PROOF STATE]
proof (prove)
using this:
q.uminus_rel (q.frac r1 f1) = q.frac (- r1) f1

goal (1 subgoal):
 1. q.uminus_rel (s \<qq>) = q.frac (- r1) f1
[PROOF STEP]
using \<open>s \<qq> = q.frac r1 f1\<close>
[PROOF STATE]
proof (prove)
using this:
q.uminus_rel (q.frac r1 f1) = q.frac (- r1) f1
s \<qq> = q.frac r1 f1

goal (1 subgoal):
 1. q.uminus_rel (s \<qq>) = q.frac (- r1) f1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q.uminus_rel (s \<qq>) = q.frac r3 f3

goal (2 subgoals):
 1. f3 \<notin> \<qq>
 2. uminus_sheaf_spec U s \<qq> = q.frac r3 f3
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
q.uminus_rel (s \<qq>) = q.frac r3 f3
[PROOF STEP]
show "uminus_sheaf_spec U s \<qq> = q.frac r3 f3"
[PROOF STATE]
proof (prove)
using this:
q.uminus_rel (s \<qq>) = q.frac r3 f3

goal (1 subgoal):
 1. uminus_sheaf_spec U s \<qq> = q.frac r3 f3
[PROOF STEP]
unfolding uminus_sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
q.uminus_rel (s \<qq>) = q.frac r3 f3

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.uminus_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>)) \<qq> = q.frac r3 f3
[PROOF STEP]
using \<open>V3 \<subseteq> U\<close> \<open>\<qq> \<in> V3\<close>
[PROOF STATE]
proof (prove)
using this:
q.uminus_rel (s \<qq>) = q.frac r3 f3
V3 \<subseteq> U
\<qq> \<in> V3

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.uminus_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>)) \<qq> = q.frac r3 f3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
uminus_sheaf_spec U s \<qq> = q.frac r3 f3

goal (1 subgoal):
 1. f3 \<notin> \<qq>
[PROOF STEP]
show "f3 \<notin> \<qq>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f3 \<notin> \<qq>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<qq> \<in> V3

goal (1 subgoal):
 1. f3 \<notin> \<qq>
[PROOF STEP]
unfolding V3_def f3_def
[PROOF STATE]
proof (prove)
using this:
\<qq> \<in> V1

goal (1 subgoal):
 1. f1 \<notin> \<qq>
[PROOF STEP]
using \<open>f1 \<in> R\<close> \<open>f1 \<notin> \<qq>\<close> q.sub_composition_closed
[PROOF STATE]
proof (prove)
using this:
\<qq> \<in> V1
f1 \<in> R
f1 \<notin> \<qq>
\<lbrakk>?a \<in> R\<setminus>\<qq>; ?b \<in> R\<setminus>\<qq>\<rbrakk> \<Longrightarrow> ?a \<cdot> ?b \<in> R\<setminus>\<qq>

goal (1 subgoal):
 1. f1 \<notin> \<qq>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f3 \<notin> \<qq>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> uminus_sheaf_spec U s ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (uminus_sheaf_spec U s) V
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> uminus_sheaf_spec U s ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> uminus_sheaf_spec U s ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (uminus_sheaf_spec U s) V
[PROOF STEP]
using is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> uminus_sheaf_spec U s ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3
is_locally_frac ?s ?V \<equiv> \<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>?V. f \<notin> \<qq> \<and> ?s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)

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

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

goal (1 subgoal):
 1. is_regular (uminus_sheaf_spec U s) U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?\<pp>3 \<in> U \<Longrightarrow> uminus_sheaf_spec U s ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> is_locally_frac (uminus_sheaf_spec U s) V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> uminus_sheaf_spec U s ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> is_locally_frac (uminus_sheaf_spec U s) V

goal (1 subgoal):
 1. is_regular (uminus_sheaf_spec U s) U
[PROOF STEP]
unfolding is_regular_def is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> uminus_sheaf_spec U s ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> uminus_sheaf_spec U s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f))

goal (1 subgoal):
 1. \<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> uminus_sheaf_spec U s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
is_regular (uminus_sheaf_spec U s) U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma uminus_sheaf_spec_in_sheaf_spec:
  assumes "s \<in> \<O> U" and "U \<subseteq> Spec"
  shows "uminus_sheaf_spec U s \<in> \<O> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uminus_sheaf_spec U s \<in> \<O> U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. uminus_sheaf_spec U s \<in> \<O> U
[PROOF STEP]
have "uminus_sheaf_spec U s \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>"
      if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uminus_sheaf_spec U s \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. uminus_sheaf_spec U s \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret qr: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]
apply (rule spectrum_imp_cxt_quotient_ring)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pp> \<in> Spec
[PROOF STEP]
using that \<open>U \<subseteq> Spec\<close>
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
U \<subseteq> Spec

goal (1 subgoal):
 1. \<pp> \<in> Spec
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. uminus_sheaf_spec U s \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret pi:pr_ideal R \<pp> "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using that \<open>U \<subseteq> Spec\<close>
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U
U \<subseteq> Spec

goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by (auto intro:spectrum_imp_pr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. uminus_sheaf_spec U s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
have "qr.valid_frac (s \<pp>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qr.valid_frac (s \<pp>)
[PROOF STEP]
using sec_has_right_codom[OF _ that] \<open>s \<in> \<O> U\<close>
[PROOF STATE]
proof (prove)
using this:
?s \<in> \<O> U \<Longrightarrow> ?s \<pp> \<in> pi.carrier_local_ring_at
s \<in> \<O> U

goal (1 subgoal):
 1. qr.valid_frac (s \<pp>)
[PROOF STEP]
by (auto simp:pi.carrier_local_ring_at_def)
[PROOF STATE]
proof (state)
this:
qr.valid_frac (s \<pp>)

goal (1 subgoal):
 1. uminus_sheaf_spec U s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qr.valid_frac (s \<pp>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
qr.valid_frac (s \<pp>)

goal (1 subgoal):
 1. uminus_sheaf_spec U s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
qr.valid_frac (s \<pp>)
\<pp> \<in> U

goal (1 subgoal):
 1. uminus_sheaf_spec U s \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
unfolding uminus_sheaf_spec_def pi.carrier_local_ring_at_def
[PROOF STATE]
proof (prove)
using this:
qr.valid_frac (s \<pp>)
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.uminus_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>)) \<pp> \<in> qr.carrier_quotient_ring
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
uminus_sheaf_spec U s \<pp> \<in> pi.carrier_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> uminus_sheaf_spec U s ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. uminus_sheaf_spec U s \<in> \<O> U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> uminus_sheaf_spec U s ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. uminus_sheaf_spec U s \<in> \<O> U
[PROOF STEP]
have "is_regular (uminus_sheaf_spec U s) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_regular (uminus_sheaf_spec U s) U
[PROOF STEP]
using \<open>s \<in> \<O> U\<close>  \<open>U \<subseteq> Spec\<close> is_regular_uminus_sheaf_spec
[PROOF STATE]
proof (prove)
using this:
s \<in> \<O> U
U \<subseteq> Spec
\<lbrakk>is_regular ?s ?U; ?U \<subseteq> Spec\<rbrakk> \<Longrightarrow> is_regular (uminus_sheaf_spec ?U ?s) ?U

goal (1 subgoal):
 1. is_regular (uminus_sheaf_spec U s) U
[PROOF STEP]
unfolding sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
s \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s U}
U \<subseteq> Spec
\<lbrakk>is_regular ?s ?U; ?U \<subseteq> Spec\<rbrakk> \<Longrightarrow> is_regular (uminus_sheaf_spec ?U ?s) ?U

goal (1 subgoal):
 1. is_regular (uminus_sheaf_spec U s) U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_regular (uminus_sheaf_spec U s) U

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

goal (1 subgoal):
 1. uminus_sheaf_spec U s \<in> \<O> U
[PROOF STEP]
have "uminus_sheaf_spec U s \<in> extensional U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uminus_sheaf_spec U s \<in> extensional U
[PROOF STEP]
unfolding uminus_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.uminus_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> (s \<pp>)) \<in> extensional U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
uminus_sheaf_spec U s \<in> extensional U

goal (1 subgoal):
 1. uminus_sheaf_spec U s \<in> \<O> U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?\<pp>3 \<in> U \<Longrightarrow> uminus_sheaf_spec U s ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (uminus_sheaf_spec U s) U
uminus_sheaf_spec U s \<in> extensional U
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> uminus_sheaf_spec U s ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (uminus_sheaf_spec U s) U
uminus_sheaf_spec U s \<in> extensional U

goal (1 subgoal):
 1. uminus_sheaf_spec U s \<in> \<O> U
[PROOF STEP]
unfolding sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> uminus_sheaf_spec U s ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (uminus_sheaf_spec U s) U
uminus_sheaf_spec U s \<in> extensional U

goal (1 subgoal):
 1. uminus_sheaf_spec U s \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s U}
[PROOF STEP]
by (simp add: PiE_iff)
[PROOF STATE]
proof (state)
this:
uminus_sheaf_spec U s \<in> \<O> U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_regular_zero_sheaf_spec:
  assumes "is_zariski_open U"
  shows "is_regular (zero_sheaf_spec U) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_regular (zero_sheaf_spec U) U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_regular (zero_sheaf_spec U) U
[PROOF STEP]
have "zero_sheaf_spec U \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>" if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_sheaf_spec U \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
unfolding zero_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
using assms comm_ring.frac_in_carrier_local local.comm_ring_axioms pr_ideal.not_1
          quotient_ring.zero_rel_def spectrum_imp_cxt_quotient_ring spectrum_imp_pr subsetD that
          zariski_top_space.open_imp_subset
[PROOF STATE]
proof (prove)
using this:
is_zariski_open U
\<lbrakk>comm_ring ?R ?addition ?multiplication ?zero ?unit; ?\<pp> \<in> comm_ring.spectrum ?R ?addition ?multiplication ?zero ?unit; ?r \<in> ?R; ?s \<in> ?R; ?s \<notin> ?\<pp>\<rbrakk> \<Longrightarrow> quotient_ring.frac (?R\<setminus>?\<pp>) ?R ?addition ?multiplication ?zero ?r ?s \<in> ?R \<^bsub>?\<pp> ?addition ?multiplication ?zero\<^esub>
comm_ring R (+) (\<cdot>) \<zero> \<one>
pr_ideal ?R ?I ?addition ?multiplication ?zero ?unit \<Longrightarrow> ?unit \<notin> ?I
Comm_Ring.quotient_ring ?S ?R ?addition ?multiplication ?zero ?unit \<Longrightarrow> quotient_ring.zero_rel ?S ?R ?addition ?multiplication ?zero ?unit = quotient_ring.frac ?S ?R ?addition ?multiplication ?zero ?zero ?unit
?\<pp> \<in> Spec \<Longrightarrow> Comm_Ring.quotient_ring (R\<setminus>?\<pp>) R (+) (\<cdot>) \<zero> \<one>
?\<pp> \<in> Spec \<Longrightarrow> pr_ideal R ?\<pp> (+) (\<cdot>) \<zero> \<one>
\<lbrakk>?A \<subseteq> ?B; ?c \<in> ?A\<rbrakk> \<Longrightarrow> ?c \<in> ?B
\<pp> \<in> U
is_zariski_open ?U \<Longrightarrow> ?U \<subseteq> Spec

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> zero_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. is_regular (zero_sheaf_spec U) U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> zero_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. is_regular (zero_sheaf_spec U) U
[PROOF STEP]
have "(\<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V)"
    if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V
[PROOF STEP]
define V3 where "V3 = U"
[PROOF STATE]
proof (state)
this:
V3 = U

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V
[PROOF STEP]
define r3 where "r3 = \<zero> "
[PROOF STATE]
proof (state)
this:
r3 = \<zero>

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V
[PROOF STEP]
define f3 where "f3 = \<one>"
[PROOF STATE]
proof (state)
this:
f3 = \<one>

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V
[PROOF STEP]
have "V3 \<subseteq>U" "\<pp> \<in> V3" "r3 \<in> R" "f3 \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V3 \<subseteq> U &&& \<pp> \<in> V3) &&& r3 \<in> R &&& f3 \<in> R
[PROOF STEP]
unfolding V3_def r3_def f3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (U \<subseteq> U &&& \<pp> \<in> U) &&& \<zero> \<in> R &&& \<one> \<in> R
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U

goal (1 subgoal):
 1. (U \<subseteq> U &&& \<pp> \<in> U) &&& \<zero> \<in> R &&& \<one> \<in> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V
[PROOF STEP]
have "is_zariski_open V3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zariski_open V3
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_zariski_open U

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

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_zariski_open V3

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V
[PROOF STEP]
have "f3 \<notin> \<qq>"
        "zero_sheaf_spec U \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3"
        if "\<qq> \<in> V3" for \<qq>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f3 \<notin> \<qq> &&& zero_sheaf_spec U \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f3 \<notin> \<qq>
[PROOF STEP]
using V3_def assms f3_def pr_ideal.submonoid_pr_ideal spectrum_def
          submonoid.sub_unit_closed that zariski_open_is_subset
[PROOF STATE]
proof (prove)
using this:
V3 = U
is_zariski_open U
f3 = \<one>
pr_ideal ?R ?I ?addition ?multiplication ?zero ?unit \<Longrightarrow> submonoid (?R\<setminus>?I) ?R ?multiplication ?unit
Spec \<equiv> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}
submonoid ?N ?M ?composition ?unit \<Longrightarrow> ?unit \<in> ?N
\<qq> \<in> V3
is_zariski_open ?U \<Longrightarrow> ?U \<subseteq> Spec

goal (1 subgoal):
 1. f3 \<notin> \<qq>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_sheaf_spec U \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_sheaf_spec U \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zero_sheaf_spec U \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
interpret q:quotient_ring "R\<setminus>\<qq>" R
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using V3_def assms quotient_ring_def local.comm_ring_axioms
            pr_ideal.submonoid_pr_ideal spectrum_def that zariski_open_is_subset
[PROOF STATE]
proof (prove)
using this:
V3 = U
is_zariski_open U
Comm_Ring.quotient_ring ?S ?R ?addition ?multiplication ?zero ?unit \<equiv> comm_ring ?R ?addition ?multiplication ?zero ?unit \<and> submonoid ?S ?R ?multiplication ?unit
comm_ring R (+) (\<cdot>) \<zero> \<one>
pr_ideal ?R ?I ?addition ?multiplication ?zero ?unit \<Longrightarrow> submonoid (?R\<setminus>?I) ?R ?multiplication ?unit
Spec \<equiv> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}
\<qq> \<in> V3
is_zariski_open ?U \<Longrightarrow> ?U \<subseteq> Spec

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zero_sheaf_spec U \<qq> = q.frac r3 f3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_sheaf_spec U \<qq> = q.frac r3 f3
[PROOF STEP]
unfolding zero_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<qq> = q.frac r3 f3
[PROOF STEP]
using V3_def f3_def q.zero_rel_def r3_def that
[PROOF STATE]
proof (prove)
using this:
V3 = U
f3 = \<one>
q.zero_rel = q.frac \<zero> \<one>
r3 = \<zero>
\<qq> \<in> V3

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<qq> = q.frac r3 f3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zero_sheaf_spec U \<qq> = q.frac r3 f3

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> zero_sheaf_spec U ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> zero_sheaf_spec U ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> zero_sheaf_spec U ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V
[PROOF STEP]
using is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> zero_sheaf_spec U ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3
is_locally_frac ?s ?V \<equiv> \<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>?V. f \<notin> \<qq> \<and> ?s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V

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

goal (1 subgoal):
 1. is_regular (zero_sheaf_spec U) U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?\<pp>3 \<in> U \<Longrightarrow> zero_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> zero_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> is_locally_frac (zero_sheaf_spec U) V

goal (1 subgoal):
 1. is_regular (zero_sheaf_spec U) U
[PROOF STEP]
unfolding is_regular_def is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> zero_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> zero_sheaf_spec U \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f))

goal (1 subgoal):
 1. \<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> zero_sheaf_spec U \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
is_regular (zero_sheaf_spec U) U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zero_sheaf_spec_in_sheaf_spec:
  assumes "is_zariski_open U"
  shows "zero_sheaf_spec U \<in> \<O> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_sheaf_spec U \<in> \<O> U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zero_sheaf_spec U \<in> \<O> U
[PROOF STEP]
have "zero_sheaf_spec U \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>"if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_sheaf_spec U \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zero_sheaf_spec U \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret qr: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]
by (meson assms comm_ring.zariski_open_is_subset local.comm_ring_axioms
          spectrum_imp_cxt_quotient_ring subsetD that)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zero_sheaf_spec U \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret pi:pr_ideal R \<pp> "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by (meson assms spectrum_imp_pr subsetD that zariski_open_is_subset)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. zero_sheaf_spec U \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_sheaf_spec U \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
unfolding zero_sheaf_spec_def pi.carrier_local_ring_at_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<pp> \<in> qr.carrier_quotient_ring
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<pp> \<in> qr.carrier_quotient_ring
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
zero_sheaf_spec U \<pp> \<in> pi.carrier_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> zero_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. zero_sheaf_spec U \<in> \<O> U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> zero_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. zero_sheaf_spec U \<in> \<O> U
[PROOF STEP]
have "is_regular (zero_sheaf_spec U) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_regular (zero_sheaf_spec U) U
[PROOF STEP]
using is_regular_zero_sheaf_spec assms
[PROOF STATE]
proof (prove)
using this:
is_zariski_open ?U \<Longrightarrow> is_regular (zero_sheaf_spec ?U) ?U
is_zariski_open U

goal (1 subgoal):
 1. is_regular (zero_sheaf_spec U) U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_regular (zero_sheaf_spec U) U

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

goal (1 subgoal):
 1. zero_sheaf_spec U \<in> \<O> U
[PROOF STEP]
have "zero_sheaf_spec U \<in> extensional U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_sheaf_spec U \<in> extensional U
[PROOF STEP]
by (simp add: zero_sheaf_spec_def)
[PROOF STATE]
proof (state)
this:
zero_sheaf_spec U \<in> extensional U

goal (1 subgoal):
 1. zero_sheaf_spec U \<in> \<O> U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?\<pp>3 \<in> U \<Longrightarrow> zero_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (zero_sheaf_spec U) U
zero_sheaf_spec U \<in> extensional U
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> zero_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (zero_sheaf_spec U) U
zero_sheaf_spec U \<in> extensional U

goal (1 subgoal):
 1. zero_sheaf_spec U \<in> \<O> U
[PROOF STEP]
unfolding sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> zero_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (zero_sheaf_spec U) U
zero_sheaf_spec U \<in> extensional U

goal (1 subgoal):
 1. zero_sheaf_spec U \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s U}
[PROOF STEP]
by (simp add: PiE_iff)
[PROOF STATE]
proof (state)
this:
zero_sheaf_spec U \<in> \<O> U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_regular_one_sheaf_spec:
  assumes "is_zariski_open U"
  shows "is_regular (one_sheaf_spec U) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_regular (one_sheaf_spec U) U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_regular (one_sheaf_spec U) U
[PROOF STEP]
have "one_sheaf_spec U \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>" if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_sheaf_spec U \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
unfolding one_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.one_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
by (smt assms closed_subsets_zero comm_ring.closed_subsets_def
        quotient_ring.carrier_quotient_ring_iff quotient_ring.valid_frac_one
        quotient_ring_def local.comm_ring_axioms mem_Collect_eq
        pr_ideal.carrier_local_ring_at_def pr_ideal.submonoid_pr_ideal
        restrict_apply subsetD that zariski_open_is_subset)
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> one_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. is_regular (one_sheaf_spec U) U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> one_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. is_regular (one_sheaf_spec U) U
[PROOF STEP]
have "(\<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (one_sheaf_spec U) V)"
    if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (one_sheaf_spec U) V
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (one_sheaf_spec U) V
[PROOF STEP]
define V3 where "V3 = U"
[PROOF STATE]
proof (state)
this:
V3 = U

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (one_sheaf_spec U) V
[PROOF STEP]
define r3 where "r3 = \<one>"
[PROOF STATE]
proof (state)
this:
r3 = \<one>

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (one_sheaf_spec U) V
[PROOF STEP]
define f3 where "f3 = \<one>"
[PROOF STATE]
proof (state)
this:
f3 = \<one>

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (one_sheaf_spec U) V
[PROOF STEP]
have "V3 \<subseteq>U" "\<pp> \<in> V3" "r3 \<in> R" "f3 \<in> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (V3 \<subseteq> U &&& \<pp> \<in> V3) &&& r3 \<in> R &&& f3 \<in> R
[PROOF STEP]
unfolding V3_def r3_def f3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (U \<subseteq> U &&& \<pp> \<in> U) &&& \<one> \<in> R &&& \<one> \<in> R
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U

goal (1 subgoal):
 1. (U \<subseteq> U &&& \<pp> \<in> U) &&& \<one> \<in> R &&& \<one> \<in> R
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (one_sheaf_spec U) V
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (one_sheaf_spec U) V
[PROOF STEP]
have "is_zariski_open V3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zariski_open V3
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_zariski_open U

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

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (one_sheaf_spec U) V
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_zariski_open V3

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (one_sheaf_spec U) V
[PROOF STEP]
have "f3 \<notin> \<qq>"
        "one_sheaf_spec U \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3"
        if "\<qq> \<in> V3" for \<qq>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f3 \<notin> \<qq> &&& one_sheaf_spec U \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f3 \<notin> \<qq>
[PROOF STEP]
using V3_def assms f3_def pr_ideal.submonoid_pr_ideal spectrum_def
          submonoid.sub_unit_closed that zariski_open_is_subset
[PROOF STATE]
proof (prove)
using this:
V3 = U
is_zariski_open U
f3 = \<one>
pr_ideal ?R ?I ?addition ?multiplication ?zero ?unit \<Longrightarrow> submonoid (?R\<setminus>?I) ?R ?multiplication ?unit
Spec \<equiv> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}
submonoid ?N ?M ?composition ?unit \<Longrightarrow> ?unit \<in> ?N
\<qq> \<in> V3
is_zariski_open ?U \<Longrightarrow> ?U \<subseteq> Spec

goal (1 subgoal):
 1. f3 \<notin> \<qq>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_sheaf_spec U \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_sheaf_spec U \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_sheaf_spec U \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
interpret q:quotient_ring "R\<setminus>\<qq>" R
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
using V3_def assms quotient_ring_def local.comm_ring_axioms
            pr_ideal.submonoid_pr_ideal spectrum_def that zariski_open_is_subset
[PROOF STATE]
proof (prove)
using this:
V3 = U
is_zariski_open U
Comm_Ring.quotient_ring ?S ?R ?addition ?multiplication ?zero ?unit \<equiv> comm_ring ?R ?addition ?multiplication ?zero ?unit \<and> submonoid ?S ?R ?multiplication ?unit
comm_ring R (+) (\<cdot>) \<zero> \<one>
pr_ideal ?R ?I ?addition ?multiplication ?zero ?unit \<Longrightarrow> submonoid (?R\<setminus>?I) ?R ?multiplication ?unit
Spec \<equiv> {I. pr_ideal R I (+) (\<cdot>) \<zero> \<one>}
\<qq> \<in> V3
is_zariski_open ?U \<Longrightarrow> ?U \<subseteq> Spec

goal (1 subgoal):
 1. Comm_Ring.quotient_ring (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_sheaf_spec U \<qq> = q.frac r3 f3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_sheaf_spec U \<qq> = q.frac r3 f3
[PROOF STEP]
unfolding one_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.one_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<qq> = q.frac r3 f3
[PROOF STEP]
using V3_def f3_def q.one_rel_def r3_def that
[PROOF STATE]
proof (prove)
using this:
V3 = U
f3 = \<one>
q.one_rel = q.frac \<one> \<one>
r3 = \<one>
\<qq> \<in> V3

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.one_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<qq> = q.frac r3 f3
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_sheaf_spec U \<qq> = q.frac r3 f3

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> one_sheaf_spec U ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (one_sheaf_spec U) V
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> one_sheaf_spec U ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> one_sheaf_spec U ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (one_sheaf_spec U) V
[PROOF STEP]
using is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
V3 \<subseteq> U
\<pp> \<in> V3
r3 \<in> R
f3 \<in> R
is_zariski_open V3
?\<qq>3 \<in> V3 \<Longrightarrow> f3 \<notin> ?\<qq>3
?\<qq>3 \<in> V3 \<Longrightarrow> one_sheaf_spec U ?\<qq>3 = quotient_ring.frac (R\<setminus>?\<qq>3) R (+) (\<cdot>) \<zero> r3 f3
is_locally_frac ?s ?V \<equiv> \<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>?V. f \<notin> \<qq> \<and> ?s \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)

goal (1 subgoal):
 1. \<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (one_sheaf_spec U) V
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>V\<subseteq>U. is_zariski_open V \<and> \<pp> \<in> V \<and> is_locally_frac (one_sheaf_spec U) V

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

goal (1 subgoal):
 1. is_regular (one_sheaf_spec U) U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?\<pp>3 \<in> U \<Longrightarrow> one_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> is_locally_frac (one_sheaf_spec U) V
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> one_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> is_locally_frac (one_sheaf_spec U) V

goal (1 subgoal):
 1. is_regular (one_sheaf_spec U) U
[PROOF STEP]
unfolding is_regular_def is_locally_frac_def
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> one_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
?\<pp>3 \<in> U \<Longrightarrow> \<exists>V\<subseteq>U. is_zariski_open V \<and> ?\<pp>3 \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> one_sheaf_spec U \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f))

goal (1 subgoal):
 1. \<forall>\<pp>. \<pp> \<in> U \<longrightarrow> (\<exists>V. is_zariski_open V \<and> V \<subseteq> U \<and> \<pp> \<in> V \<and> (\<exists>r f. r \<in> R \<and> f \<in> R \<and> (\<forall>\<qq>\<in>V. f \<notin> \<qq> \<and> one_sheaf_spec U \<qq> = quotient_ring.frac (R\<setminus>\<qq>) R (+) (\<cdot>) \<zero> r f)))
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
is_regular (one_sheaf_spec U) U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma one_sheaf_spec_in_sheaf_spec:
  assumes "is_zariski_open U"
  shows "one_sheaf_spec U \<in> \<O> U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_sheaf_spec U \<in> \<O> U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_sheaf_spec U \<in> \<O> U
[PROOF STEP]
have "one_sheaf_spec U \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>"if "\<pp> \<in> U" for \<pp>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_sheaf_spec U \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_sheaf_spec U \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret qr: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]
by (meson assms comm_ring.zariski_open_is_subset local.comm_ring_axioms
          spectrum_imp_cxt_quotient_ring subsetD that)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_sheaf_spec U \<pp> \<in> R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>
[PROOF STEP]
interpret pi:pr_ideal R \<pp> "(+)" "(\<cdot>)" \<zero> \<one>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pr_ideal R \<pp> (+) (\<cdot>) \<zero> \<one>
[PROOF STEP]
by (meson assms spectrum_imp_pr subsetD that zariski_open_is_subset)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. one_sheaf_spec U \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_sheaf_spec U \<pp> \<in> pi.carrier_local_ring_at
[PROOF STEP]
unfolding one_sheaf_spec_def pi.carrier_local_ring_at_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.one_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<pp> \<in> qr.carrier_quotient_ring
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
\<pp> \<in> U

goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.one_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<pp> \<in> qr.carrier_quotient_ring
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
one_sheaf_spec U \<pp> \<in> pi.carrier_local_ring_at

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> one_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. one_sheaf_spec U \<in> \<O> U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?\<pp>3 \<in> U \<Longrightarrow> one_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>

goal (1 subgoal):
 1. one_sheaf_spec U \<in> \<O> U
[PROOF STEP]
have "is_regular (one_sheaf_spec U) U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_regular (one_sheaf_spec U) U
[PROOF STEP]
using is_regular_one_sheaf_spec assms
[PROOF STATE]
proof (prove)
using this:
is_zariski_open ?U \<Longrightarrow> is_regular (one_sheaf_spec ?U) ?U
is_zariski_open U

goal (1 subgoal):
 1. is_regular (one_sheaf_spec U) U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
is_regular (one_sheaf_spec U) U

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

goal (1 subgoal):
 1. one_sheaf_spec U \<in> \<O> U
[PROOF STEP]
have "one_sheaf_spec U \<in> extensional U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_sheaf_spec U \<in> extensional U
[PROOF STEP]
by (simp add: one_sheaf_spec_def)
[PROOF STATE]
proof (state)
this:
one_sheaf_spec U \<in> extensional U

goal (1 subgoal):
 1. one_sheaf_spec U \<in> \<O> U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?\<pp>3 \<in> U \<Longrightarrow> one_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (one_sheaf_spec U) U
one_sheaf_spec U \<in> extensional U
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> one_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (one_sheaf_spec U) U
one_sheaf_spec U \<in> extensional U

goal (1 subgoal):
 1. one_sheaf_spec U \<in> \<O> U
[PROOF STEP]
unfolding sheaf_spec_def
[PROOF STATE]
proof (prove)
using this:
?\<pp>3 \<in> U \<Longrightarrow> one_sheaf_spec U ?\<pp>3 \<in> R \<^bsub>?\<pp>3 (+) (\<cdot>) \<zero>\<^esub>
is_regular (one_sheaf_spec U) U
one_sheaf_spec U \<in> extensional U

goal (1 subgoal):
 1. one_sheaf_spec U \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s U}
[PROOF STEP]
by (simp add: PiE_iff)
[PROOF STATE]
proof (state)
this:
one_sheaf_spec U \<in> \<O> U

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zero_sheaf_spec_extensional[simp]:
  "zero_sheaf_spec U \<in> extensional U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_sheaf_spec U \<in> extensional U
[PROOF STEP]
unfolding zero_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.zero_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<in> extensional U
[PROOF STEP]
by simp


[STATEMENT]
lemma one_sheaf_spec_extensional[simp]:
  "one_sheaf_spec U \<in> extensional U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. one_sheaf_spec U \<in> extensional U
[PROOF STEP]
unfolding one_sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<pp>\<in>U. quotient_ring.one_rel (R\<setminus>\<pp>) R (+) (\<cdot>) \<zero> \<one>) \<in> extensional U
[PROOF STEP]
by simp


[STATEMENT]
lemma add_sheaf_spec_extensional[simp]:
  "add_sheaf_spec U a b \<in> extensional U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. add_sheaf_spec U a b \<in> extensional U
[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> (a \<pp>) (b \<pp>)) \<in> extensional U
[PROOF STEP]
by simp


[STATEMENT]
lemma mult_sheaf_spec_extensional[simp]:
  "mult_sheaf_spec U a b \<in> extensional U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_sheaf_spec U a b \<in> extensional U
[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> (a \<pp>) (b \<pp>)) \<in> extensional U
[PROOF STEP]
by simp


[STATEMENT]
lemma sheaf_spec_extensional[simp]:
  "a \<in> \<O> U \<Longrightarrow> a \<in> extensional U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> \<O> U \<Longrightarrow> a \<in> extensional U
[PROOF STEP]
unfolding sheaf_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> {s \<in> \<Pi>\<^sub>E \<pp>\<in>U. R \<^bsub>\<pp> (+) (\<cdot>) \<zero>\<^esub>. is_regular s U} \<Longrightarrow> a \<in> extensional U
[PROOF STEP]
by (simp add: PiE_iff Set_Theory.map_def)